Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.PushoutCocone.mk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {W : C} →
            (inl : Y ⟶ W) →
              (inr : Z ⟶ W) →
                CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr →
                  CategoryTheory.Limits.PushoutCocone f g

A pushout cocone on f and g is determined by morphisms inl : Y ⟶ W and inr : Z ⟶ W such that f ≫ inl = g ↠ inr.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Cited by
89 results in Mathlib
Foundations
Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.Category
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Limits.pushout.desc · cited by 46pushout.descCategoryTheory.Limits.PushoutCocone.mk_ι_app · cited by 30PushoutCocone.mk_ι_appCategoryTheory.Limits.hasPushout_symmetry · cited by 18Limits.hasPushout_symmetryCategoryTheory.IsPushout.inl_isoPushout_inv · cited by 10IsPushout.inl_isoPushout_…CategoryTheory.IsPushout.of_iso · cited by 10IsPushout.of_isoCommRingCat.pushoutCocone · cited by 9CommRingCat.pushoutCoconeCategoryTheory.Limits.PushoutCocone.IsColimit.mk · cited by 8IsColimit.mkCategoryTheory.Limits.pushout.inr_desc · cited by 8pushout.inr_descCategoryTheory.Limits.pushout.inl_desc · cited by 8pushout.inl_descCategoryTheory.Limits.pushoutCoconeEquivBinaryCofan · cited by 7Limits.pushoutCoconeEquiv…CategoryTheory.Limits.pushoutCoconeOfLeftIso · cited by 7Limits.pushoutCoconeOfLef…CategoryTheory.Limits.pushoutCoconeOfRightIso · cited by 7Limits.pushoutCoconeOfRig…CategoryTheory.Limits.pushoutIsPushout · cited by 7Limits.pushoutIsPushoutCategoryTheory.IsPushout.inr_isoPushout_inv · cited by 7IsPushout.inr_isoPushout_…CategoryTheory.Limits.PushoutCocone.IsColimit.desc · cited by 6IsColimit.descCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compCategoryTheory.Limits.WalkingPair · cited by 1319Limits.WalkingPairCategoryTheory.Limits.WalkingSpan · cited by 300Limits.WalkingSpanCategoryTheory.Limits.PushoutCocone · cited by 66Limits.PushoutCoconeCategoryTheory.Limits.WalkingPair.casesOn · cited by 59WalkingPair.casesOnPushoutCocone.mkCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by134

Results whose statement or proof uses this declaration.