WidePullbacks

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

Statistics

Metric	Count
Definitions HasWidePullback, HasWidePullbacks, HasWidePushout, HasWidePushouts, base, π, WidePullbackCone, mk, base, ext, mk, reindex, reindexIsLimitEquiv, π, WidePullbackShape, inhabited, category, diagramIsoWideCospan, equivalenceOfEquiv, evalCasesBash, functorExt, instDecidableEqHom, decEq, mkCone, struct, uliftEquivalence, wideCospan, desc, head, ι, WidePushoutShape, inhabited, category, diagramIsoWideSpan, equivalenceOfEquiv, evalCasesBash', instDecidableEqHom, decEq, mkCocone, struct, uliftEquivalence, wideSpan, instInhabitedWidePullbackShape, instInhabitedWidePushoutShape, widePullback, widePullbackShapeOp, widePullbackShapeOpEquiv, widePullbackShapeOpMap, widePullbackShapeOpUnop, widePullbackShapeUnop, widePullbackShapeUnopOp, widePushout, widePushoutShapeOp, widePushoutShapeOpEquiv, widePushoutShapeOpMap, widePushoutShapeOpUnop, widePushoutShapeUnop, widePushoutShapeUnopOp	58
Theorems eq_lift_of_comp_eq, hom_eq_lift, hom_ext, hom_ext_iff, lift_base, lift_base_assoc, lift_π, lift_π_assoc, π_arrow, π_arrow_assoc, hom_ext, lift_base, lift_base_assoc, lift_π, lift_π_assoc, condition, condition_assoc, mk_base, mk_pt, mk_π, reindex_base, reindex_pt, reindex_π, equivalenceOfEquiv_functor_map_term, equivalenceOfEquiv_functor_obj_none, equivalenceOfEquiv_functor_obj_some, functorExt_hom_app, functorExt_inv_app, hom_id, mkCone_pt, mkCone_π_app, subsingleton_hom, wideCospan_map, wideCospan_obj, arrow_ι, arrow_ι_assoc, eq_desc_of_comp_eq, head_desc, head_desc_assoc, hom_eq_desc, hom_ext, hom_ext_iff, ι_desc, ι_desc_assoc, hom_id, mkCocone_pt, mkCocone_ι_app, subsingleton_hom, wideSpan_map, wideSpan_obj, hasWidePullbacks_shrink, hasWidePushouts_shrink, widePullbackShapeOpEquiv_counitIso, widePullbackShapeOpEquiv_functor, widePullbackShapeOpEquiv_inverse, widePullbackShapeOpEquiv_unitIso, widePullbackShapeOp_map, widePullbackShapeOp_obj, widePullbackShapeUnop_map, widePullbackShapeUnop_obj, widePushoutShapeOpEquiv_counitIso, widePushoutShapeOpEquiv_functor, widePushoutShapeOpEquiv_inverse, widePushoutShapeOpEquiv_unitIso, widePushoutShapeOp_map, widePushoutShapeOp_obj, widePushoutShapeUnop_map, widePushoutShapeUnop_obj	68
Total	126

CategoryTheory.Limits

Definitions

Name	Category	Theorems
HasWidePullback 📖	MathDef	3 math math: hasWidePullback_of_isTerminal, CategoryTheory.CechNerveTerminalFrom.hasWidePullback', CategoryTheory.CechNerveTerminalFrom.hasWidePullback
HasWidePullbacks 📖	MathDef	—
HasWidePushout 📖	MathDef	—
HasWidePushouts 📖	MathDef	—
WidePullbackCone 📖	CompOp	—
WidePullbackShape 📖	CompOp	82 math math: CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_pt, walkingSpanOpEquiv_inverse_map, widePushoutShapeUnop_obj, widePushoutShapeOpEquiv_functor, widePushoutShapeOpEquiv_inverse, widePullbackShapeUnop_map, WidePullbackCone.reindex_pt, WidePullbackShape.functorExt_hom_app, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, CategoryTheory.Subobject.wideCospan_map_term, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_inv_app_hom_left, CategoryTheory.Over.ConstructProducts.conesEquiv_unitIso, walkingCospanOpEquiv_counitIso_hom_app, widePullbackShapeOpEquiv_inverse, walkingCospanOpEquiv_counitIso_inv_app, walkingCospanOpEquiv_inverse_obj, walkingSpanOpEquiv_inverse_obj, WidePullbackCone.IsLimit.lift_base, walkingCospanOpEquiv_unitIso_inv_app, opSpan_hom_app, widePushoutShapeOp_map, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom, walkingSpanOpEquiv_counitIso_hom_app, WidePullbackShape.wideCospan_obj, WidePullbackShape.hom_id, WidePullbackShape.equivalenceOfEquiv_functor_map_term, CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan, hasLimitsOfShape_widePullbackShape, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_inv_app_hom, WidePullbackShape.equivalenceOfEquiv_functor_obj_some, widePushoutShapeOp_obj, WidePullbackCone.mk_pt, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_hom_app_hom_left, WidePullbackCone.IsLimit.lift_π_assoc, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi, CategoryTheory.Over.ConstructProducts.conesEquiv_counitIso, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc, WidePullbackCone.condition_assoc, walkingSpanOpEquiv_unitIso_inv_app, WidePullbackCone.IsLimit.lift_base_assoc, CategoryTheory.widePullbackShape_connected, widePullbackShapeOp_obj, WidePullbackCone.IsLimit.lift_π, widePushoutShapeOpEquiv_counitIso, walkingCospanOpEquiv_functor_map, CategoryTheory.WithTerminal.widePullbackShapeEquiv_inverse_obj, walkingCospanOpEquiv_functor_obj, walkingSpanOpEquiv_functor_map, widePullbackShapeUnop_obj, CategoryTheory.Over.ConstructProducts.conesEquiv_functor, widePullbackShapeOpEquiv_functor, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range, widePushoutShapeUnop_map, WidePullbackShape.functorExt_inv_app, HasFiniteWidePullbacks.out, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt, CategoryTheory.Subobject.leInfCone_π_app_none, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_hom_app_hom, walkingSpanOpEquiv_functor_obj, CategoryTheory.Over.ConstructProducts.conesEquivInverse_obj, walkingSpanOpEquiv_unitIso_hom_app, WidePullbackShape.wideCospan_map, CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_π_app, CategoryTheory.instIsConnectedWidePullbackShape, WidePullbackShape.equivalenceOfEquiv_functor_obj_none, walkingSpanOpEquiv_counitIso_inv_app, CategoryTheory.Over.ConstructProducts.conesEquiv_inverse, walkingCospanOpEquiv_unitIso_hom_app, opSpan_inv_app, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi, WidePullbackShape.subsingleton_hom, widePullbackShapeOpEquiv_counitIso, widePushoutShapeOpEquiv_unitIso, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app, widePullbackShapeOp_map, CategoryTheory.WithTerminal.widePullbackShapeEquiv_functor_obj, CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom, WidePullbackCone.condition, walkingCospanOpEquiv_inverse_map, widePullbackShapeOpEquiv_unitIso
WidePushoutShape 📖	CompOp	42 math math: walkingSpanOpEquiv_inverse_map, widePushoutShapeUnop_obj, widePushoutShapeOpEquiv_functor, widePushoutShapeOpEquiv_inverse, widePullbackShapeUnop_map, hasColimitsOfShape_widePushoutShape, walkingCospanOpEquiv_counitIso_hom_app, widePullbackShapeOpEquiv_inverse, walkingCospanOpEquiv_counitIso_inv_app, walkingCospanOpEquiv_inverse_obj, walkingSpanOpEquiv_inverse_obj, walkingCospanOpEquiv_unitIso_inv_app, CategoryTheory.instIsConnectedWidePushoutShape, widePushoutShapeOp_map, walkingSpanOpEquiv_counitIso_hom_app, opCospan_hom_app, WidePushoutShape.hom_id, widePushoutShapeOp_obj, walkingSpanOpEquiv_unitIso_inv_app, opCospan_inv_app, widePullbackShapeOp_obj, WidePushoutShape.wideSpan_map, widePushoutShapeOpEquiv_counitIso, walkingCospanOpEquiv_functor_map, walkingCospanOpEquiv_functor_obj, walkingSpanOpEquiv_functor_map, widePullbackShapeUnop_obj, widePullbackShapeOpEquiv_functor, widePushoutShapeUnop_map, WidePushoutShape.subsingleton_hom, walkingSpanOpEquiv_functor_obj, CategoryTheory.widePushoutShape_connected, WidePushoutShape.wideSpan_obj, walkingSpanOpEquiv_unitIso_hom_app, walkingSpanOpEquiv_counitIso_inv_app, walkingCospanOpEquiv_unitIso_hom_app, widePullbackShapeOpEquiv_counitIso, widePushoutShapeOpEquiv_unitIso, HasFiniteWidePushouts.out, widePullbackShapeOp_map, walkingCospanOpEquiv_inverse_map, widePullbackShapeOpEquiv_unitIso
instInhabitedWidePullbackShape 📖	CompOp	—
instInhabitedWidePushoutShape 📖	CompOp	—
widePullback 📖	CompOp	14 math math: WidePullback.lift_base_assoc, WidePullback.π_arrow, CategoryTheory.Arrow.cechNerve_obj, WidePullback.hom_ext_iff, WidePullback.lift_base, WidePullback.π_arrow_assoc, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0, WidePullback.hom_eq_lift, CategoryTheory.Arrow.cechNerve_map, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, WidePullback.lift_π_assoc, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_obj, WidePullback.lift_π
widePullbackShapeOp 📖	CompOp	8 math math: widePushoutShapeOpEquiv_inverse, walkingSpanOpEquiv_counitIso_hom_app, walkingSpanOpEquiv_unitIso_inv_app, widePullbackShapeOp_obj, walkingSpanOpEquiv_unitIso_hom_app, walkingSpanOpEquiv_counitIso_inv_app, widePushoutShapeOpEquiv_unitIso, widePullbackShapeOp_map
widePullbackShapeOpEquiv 📖	CompOp	4 math math: widePullbackShapeOpEquiv_inverse, widePullbackShapeOpEquiv_functor, widePullbackShapeOpEquiv_counitIso, widePullbackShapeOpEquiv_unitIso
widePullbackShapeOpMap 📖	CompOp	4 math math: walkingSpanOpEquiv_inverse_map, widePullbackShapeUnop_map, walkingCospanOpEquiv_functor_map, widePullbackShapeOp_map
widePullbackShapeOpUnop 📖	CompOp	1 math math: widePullbackShapeOpEquiv_unitIso
widePullbackShapeUnop 📖	CompOp	8 math math: widePullbackShapeUnop_map, walkingCospanOpEquiv_counitIso_hom_app, walkingCospanOpEquiv_counitIso_inv_app, walkingCospanOpEquiv_unitIso_inv_app, widePullbackShapeUnop_obj, widePullbackShapeOpEquiv_functor, walkingCospanOpEquiv_unitIso_hom_app, widePullbackShapeOpEquiv_unitIso
widePullbackShapeUnopOp 📖	CompOp	1 math math: widePushoutShapeOpEquiv_counitIso
widePushout 📖	CompOp	13 math math: WidePushout.arrow_ι, WidePushout.ι_desc_assoc, WidePushout.hom_eq_desc, WidePushout.head_desc_assoc, WidePushout.hom_ext_iff, Concrete.widePushout_exists_rep', Concrete.widePushout_exists_rep, WidePushout.head_desc, CategoryTheory.Arrow.cechConerve_map, CategoryTheory.Arrow.cechConerve_obj, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right, WidePushout.ι_desc, WidePushout.arrow_ι_assoc
widePushoutShapeOp 📖	CompOp	8 math math: walkingCospanOpEquiv_counitIso_hom_app, widePullbackShapeOpEquiv_inverse, walkingCospanOpEquiv_counitIso_inv_app, walkingCospanOpEquiv_unitIso_inv_app, widePushoutShapeOp_map, widePushoutShapeOp_obj, walkingCospanOpEquiv_unitIso_hom_app, widePullbackShapeOpEquiv_unitIso
widePushoutShapeOpEquiv 📖	CompOp	4 math math: widePushoutShapeOpEquiv_functor, widePushoutShapeOpEquiv_inverse, widePushoutShapeOpEquiv_counitIso, widePushoutShapeOpEquiv_unitIso
widePushoutShapeOpMap 📖	CompOp	4 math math: widePushoutShapeOp_map, walkingSpanOpEquiv_functor_map, widePushoutShapeUnop_map, walkingCospanOpEquiv_inverse_map
widePushoutShapeOpUnop 📖	CompOp	1 math math: widePushoutShapeOpEquiv_unitIso
widePushoutShapeUnop 📖	CompOp	8 math math: widePushoutShapeUnop_obj, widePushoutShapeOpEquiv_functor, walkingSpanOpEquiv_counitIso_hom_app, walkingSpanOpEquiv_unitIso_inv_app, widePushoutShapeUnop_map, walkingSpanOpEquiv_unitIso_hom_app, walkingSpanOpEquiv_counitIso_inv_app, widePushoutShapeOpEquiv_unitIso
widePushoutShapeUnopOp 📖	CompOp	1 math math: widePullbackShapeOpEquiv_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasWidePullbacks_shrink 📖	—	HasWidePullbacks	—	—	hasLimitsOfShape_of_equivalence
hasWidePushouts_shrink 📖	—	HasWidePushouts	—	—	hasColimitsOfShape_of_equivalence
widePullbackShapeOpEquiv_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Opposite WidePullbackShape WidePushoutShape CategoryTheory.Category.opposite WidePullbackShape.category WidePushoutShape.category widePullbackShapeOpEquiv widePushoutShapeUnopOp	—	—
widePullbackShapeOpEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Opposite WidePullbackShape WidePushoutShape CategoryTheory.Category.opposite WidePullbackShape.category WidePushoutShape.category widePullbackShapeOpEquiv widePullbackShapeUnop	—	—
widePullbackShapeOpEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Opposite WidePullbackShape WidePushoutShape CategoryTheory.Category.opposite WidePullbackShape.category WidePushoutShape.category widePullbackShapeOpEquiv widePushoutShapeOp	—	—
widePullbackShapeOpEquiv_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Opposite WidePullbackShape WidePushoutShape CategoryTheory.Category.opposite WidePullbackShape.category WidePushoutShape.category widePullbackShapeOpEquiv CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp widePullbackShapeUnop widePushoutShapeOp CategoryTheory.Functor.id widePullbackShapeOpUnop	—	—
widePullbackShapeOp_map 📖	mathematical	—	CategoryTheory.Functor.map WidePullbackShape WidePullbackShape.category Opposite WidePushoutShape CategoryTheory.Category.opposite WidePushoutShape.category widePullbackShapeOp widePullbackShapeOpMap	—	—
widePullbackShapeOp_obj 📖	mathematical	—	CategoryTheory.Functor.obj WidePullbackShape WidePullbackShape.category Opposite WidePushoutShape CategoryTheory.Category.opposite WidePushoutShape.category widePullbackShapeOp Opposite.op	—	—
widePullbackShapeUnop_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite WidePullbackShape CategoryTheory.Category.opposite WidePullbackShape.category WidePushoutShape WidePushoutShape.category widePullbackShapeUnop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct widePullbackShapeOpMap Opposite.unop	—	—
widePullbackShapeUnop_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite WidePullbackShape CategoryTheory.Category.opposite WidePullbackShape.category WidePushoutShape WidePushoutShape.category widePullbackShapeUnop Opposite.unop	—	—
widePushoutShapeOpEquiv_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Opposite WidePushoutShape WidePullbackShape CategoryTheory.Category.opposite WidePushoutShape.category WidePullbackShape.category widePushoutShapeOpEquiv widePullbackShapeUnopOp	—	—
widePushoutShapeOpEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Opposite WidePushoutShape WidePullbackShape CategoryTheory.Category.opposite WidePushoutShape.category WidePullbackShape.category widePushoutShapeOpEquiv widePushoutShapeUnop	—	—
widePushoutShapeOpEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Opposite WidePushoutShape WidePullbackShape CategoryTheory.Category.opposite WidePushoutShape.category WidePullbackShape.category widePushoutShapeOpEquiv widePullbackShapeOp	—	—
widePushoutShapeOpEquiv_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Opposite WidePushoutShape WidePullbackShape CategoryTheory.Category.opposite WidePushoutShape.category WidePullbackShape.category widePushoutShapeOpEquiv CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp widePushoutShapeUnop widePullbackShapeOp CategoryTheory.Functor.id widePushoutShapeOpUnop	—	—
widePushoutShapeOp_map 📖	mathematical	—	CategoryTheory.Functor.map WidePushoutShape WidePushoutShape.category Opposite WidePullbackShape CategoryTheory.Category.opposite WidePullbackShape.category widePushoutShapeOp widePushoutShapeOpMap	—	—
widePushoutShapeOp_obj 📖	mathematical	—	CategoryTheory.Functor.obj WidePushoutShape WidePushoutShape.category Opposite WidePullbackShape CategoryTheory.Category.opposite WidePullbackShape.category widePushoutShapeOp Opposite.op	—	—
widePushoutShapeUnop_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite WidePushoutShape CategoryTheory.Category.opposite WidePushoutShape.category WidePullbackShape WidePullbackShape.category widePushoutShapeUnop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct widePushoutShapeOpMap Opposite.unop	—	—
widePushoutShapeUnop_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite WidePushoutShape CategoryTheory.Category.opposite WidePushoutShape.category WidePullbackShape WidePullbackShape.category widePushoutShapeUnop Opposite.unop	—	—

CategoryTheory.Limits.WidePullback

Definitions

Name	Category	Theorems
base 📖	CompOp	14 math math: CategoryTheory.Arrow.augmentedCechNerve_hom_app, CategoryTheory.Arrow.mapCechNerve_app, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base, lift_base_assoc, π_arrow, hom_ext_iff, lift_base, π_arrow_assoc, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0, hom_eq_lift, CategoryTheory.Arrow.cechNerve_map, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_hom_app
π 📖	CompOp	17 math math: CategoryTheory.Arrow.mapCechNerve_app, π_arrow, hom_ext_iff, π_arrow_assoc, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0, hom_eq_lift, CategoryTheory.SimplicialObject.equivalenceRightToLeft_left, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ, CategoryTheory.Arrow.cechNerve_map, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, lift_π_assoc, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi, lift_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_lift_of_comp_eq 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback π base	lift	—	CategoryTheory.Limits.IsLimit.uniq
hom_eq_lift 📖	mathematical	—	lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback base π	—	CategoryTheory.Limits.limit.hom_ext CategoryTheory.Limits.limit.lift_π
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback π base	—	—	CategoryTheory.Limits.limit.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback π base	—	hom_ext
lift_base 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.widePullback lift base	—	CategoryTheory.Limits.limit.lift_π
lift_base_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.widePullback lift base	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_base
lift_π 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.widePullback lift π	—	CategoryTheory.Limits.limit.lift_π
lift_π_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.widePullback lift π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_π
π_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback π base	—	CategoryTheory.Limits.limit.w
π_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback π base	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_arrow

CategoryTheory.Limits.WidePullbackCone

Definitions

Name	Category	Theorems
base 📖	CompOp	6 math math: reindex_base, IsLimit.lift_base, condition_assoc, IsLimit.lift_base_assoc, mk_base, condition
ext 📖	CompOp	—
mk 📖	CompOp	—
reindex 📖	CompOp	3 math math: reindex_pt, reindex_base, reindex_π
reindexIsLimitEquiv 📖	CompOp	—
π 📖	CompOp	6 math math: IsLimit.lift_π_assoc, condition_assoc, reindex_π, mk_π, IsLimit.lift_π, condition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan π base	—	CategoryTheory.Category.id_comp CategoryTheory.NatTrans.naturality
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan π base	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
mk_base 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	base	—	—
mk_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan	—	—
mk_π 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	π	—	—
reindex_base 📖	mathematical	—	base DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	—
reindex_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	—
reindex_π 📖	mathematical	—	π DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	—

CategoryTheory.Limits.WidePullbackCone.IsLimit

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan CategoryTheory.Limits.WidePullbackCone.base CategoryTheory.Limits.WidePullbackCone.π	—	—	CategoryTheory.Limits.IsLimit.hom_ext
lift_base 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan lift CategoryTheory.Limits.WidePullbackCone.base	—	CategoryTheory.Limits.IsLimit.fac
lift_base_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan lift CategoryTheory.Limits.WidePullbackCone.base	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_base
lift_π 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan lift CategoryTheory.Limits.WidePullbackCone.π	—	CategoryTheory.Limits.IsLimit.fac
lift_π_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WidePullbackShape.wideCospan lift CategoryTheory.Limits.WidePullbackCone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_π

CategoryTheory.Limits.WidePullbackShape

Definitions

Name	Category	Theorems
category 📖	CompOp	427 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, TopCat.isInducing_pullback_to_prod, CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, CategoryTheory.StructuredArrow.projectSubobject_mk, CategoryTheory.Over.μ_pullback_left_snd', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right', TopCat.pullbackIsoProdSubtype_hom_fst, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl', CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback', CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_pt, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, CategoryTheory.Limits.diagramIsoCospan_inv_app, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd_assoc, CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr, CategoryTheory.Limits.widePushoutShapeUnop_obj, CategoryTheory.Limits.widePushoutShapeOpEquiv_functor, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right', CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, CategoryTheory.Limits.pullbackFstFstIso_hom, prodIsoPullback_inv_fst, CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_left, CategoryTheory.Abelian.epi_pullback_of_epi_f, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_φ, CategoryTheory.Limits.widePushoutShapeOpEquiv_inverse, CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve, CategoryTheory.Limits.Types.range_pullbackFst, CategoryTheory.Limits.cospanExt_app_one, CategoryTheory.Over.monObjMkPullbackSnd_mul, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst, TopCat.snd_isOpenEmbedding_of_left, CategoryTheory.Limits.widePullbackShapeUnop_map, CategoryTheory.Limits.PullbackCone.π_app_right, CategoryTheory.Limits.PushoutCocone.unop_π_app, CategoryTheory.Over.grpObjMkPullbackSnd_one, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left', CategoryTheory.Over.grpObjMkPullbackSnd_mul, CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_φ, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst, CategoryTheory.IsPullback.isLimit', CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc, CategoryTheory.Limits.WidePullbackCone.reindex_pt, functorExt_hom_app, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, CategoryTheory.Subobject.wideCospan_map_term, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion, CompHausLike.pullback.isLimit_lift, CategoryTheory.Limits.PullbackCone.unop_inl, CategoryTheory.Over.isCommMonObj_mk_pullbackSnd, TopCat.pullback_topology, CategoryTheory.Limits.PullbackCone.mk_π_app, AlgebraicGeometry.Scheme.Pullback.gluedLift_p1, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_inv_app_hom_left, CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst, prodIsoPullback_inv_fst_assoc, CategoryTheory.Limits.PullbackCone.op_pt, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd, CategoryTheory.Over.ConstructProducts.conesEquiv_unitIso, CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_right, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst, CategoryTheory.Limits.pullbackObjIso_inv_comp_fst_assoc, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fst, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst, CategoryTheory.Limits.pullbackConeOfLeftIso_snd, CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_hom_app, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst_assoc, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, CategoryTheory.Limits.PullbackCone.condition_assoc, CategoryTheory.Over.preservesTerminalIso_pullback, CategoryTheory.Limits.PullbackCone.unop_inr, CategoryTheory.Limits.spanOp_hom_app, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left, CategoryTheory.Limits.widePullbackShapeOpEquiv_inverse, TopCat.fst_iso_of_right_embedding_range_subset, CategoryTheory.Limits.PullbackCone.combine_π_app, CategoryTheory.Abelian.Pseudoelement.pseudo_pullback, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesPullbacks, CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst_assoc, CategoryTheory.Limits.pullback.comp_diagonal_assoc, TopCat.pullbackIsoProdSubtype_inv_fst_assoc, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom, CategoryTheory.Limits.PullbackCone.op_inr, prodIsoPullback_hom_fst_assoc, CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_inv_app, AlgebraicGeometry.IsOpenImmersion.instπWalkingCospanSchemeCospanOne, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, CategoryTheory.Limits.PullbackCone.op_ι_app, CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst, CategoryTheory.Limits.diagramIsoCospan_hom_app, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd, CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left, AlgebraicGeometry.Scheme.Pullback.gluedLift_p2, CategoryTheory.Limits.cospan_left, CategoryTheory.Limits.walkingCospanOpEquiv_inverse_obj, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, CategoryTheory.Limits.walkingSpanOpEquiv_inverse_obj, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base, CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map, CategoryTheory.Limits.cospanExt_app_right, TopCat.range_pullback_map, CategoryTheory.Subobject.pullback_obj, CategoryTheory.Limits.pullback_lift_diagonal_isPullback, CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_inv_app, CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, CategoryTheory.Limits.cospan_map_inr, CategoryTheory.Limits.cospanCompIso_inv_app_left, CategoryTheory.Over.starPullbackIsoStar_hom_app_left, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, CategoryTheory.Limits.Cone.ofPullbackCone_pt, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion, CategoryTheory.Limits.spanOp_inv_app, CategoryTheory.Limits.cospan_map_inl, CategoryTheory.Over.tensorHom_left_snd_assoc, CategoryTheory.Limits.PullbackCone.isIso_fst_of_mono_of_isLimit, CategoryTheory.Limits.Types.pullbackLimitCone_cone, CategoryTheory.Limits.Cone.ofPullbackCone_π, CategoryTheory.Limits.pullbackConeOfRightIso_π_app_right, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right, CategoryTheory.Limits.PullbackCone.snd_limit_cone, CategoryTheory.Limits.PullbackCone.mk_π_app_right, CategoryTheory.Limits.opSpan_hom_app, CategoryTheory.Limits.widePushoutShapeOp_map, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_snd', CategoryTheory.Limits.pullbackConeOfRightIso_fst, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_right, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom, CategoryTheory.Limits.pullbackConeOfRightIso_x, CategoryTheory.Limits.PullbackCone.mk_π_app_one, TopCat.Sheaf.interUnionPullbackConeLift_right, CategoryTheory.Limits.preservesPullback_symmetry, CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair, CategoryTheory.IsPullback.of_isLimit, TopCat.fst_isEmbedding_of_right, CategoryTheory.Limits.isPullback_map_snd_snd, CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_obj, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj, CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_hom_app, CategoryTheory.Abelian.epi_snd_of_isLimit, TopCat.isOpenEmbedding_of_pullback, CategoryTheory.Limits.opCospan_hom_app, wideCospan_obj, equivalenceOfEquiv_functor_map_term, CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_snd, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd, CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape, CategoryTheory.Limits.PullbackCone.π_app_left, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Square.isPullback_iff, TopCat.pullbackIsoProdSubtype_inv_snd_apply, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_inv_app_hom, equivalenceOfEquiv_functor_obj_some, CategoryTheory.Limits.widePushoutShapeOp_obj, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, CategoryTheory.Limits.WidePullbackCone.mk_pt, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_left, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_hom_app_hom_left, TopCat.pullbackIsoProdSubtype_inv_fst, CategoryTheory.Limits.cospanCompIso_inv_app_right, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_f_coe, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π_assoc, CategoryTheory.Limits.PullbackCone.eta_inv_hom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst_assoc, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi, CategoryTheory.Over.ConstructProducts.conesEquiv_counitIso, CategoryTheory.Limits.PushoutCocone.op_π_app, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc, CategoryTheory.Limits.WidePullbackCone.condition_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, CategoryTheory.Over.closedUnderLimitsOfShape_pullback, CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_inv_app, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base_assoc, CategoryTheory.Limits.opCospan_inv_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left, TopCat.pullbackIsoProdSubtype_hom_snd, CategoryTheory.Limits.cospanExt_inv_app_one, CategoryTheory.Limits.PullbackCone.unop_ι_app, CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd, CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_none, CategoryTheory.Over.μ_pullback_left_fst_fst', TopCat.snd_iso_of_left_embedding_range_subset, CategoryTheory.Limits.pullbackObjIso_hom_comp_fst, CategoryTheory.widePullbackShape_connected, CategoryTheory.Limits.cospanOp_hom_app, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Over.monObjMkPullbackSnd_one, TopCat.pullbackIsoProdSubtype_inv_snd, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc, CategoryTheory.Limits.PullbackCone.isoMk_inv_hom, CategoryTheory.Limits.widePullbackShapeOp_obj, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π, CategoryTheory.Limits.PreservesPullback.of_iso_comparison, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst, prodIsoPullback_hom_snd, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right, CategoryTheory.Regular.instHasCoequalizerFstSnd, CategoryTheory.Limits.cospan_right, CategoryTheory.Limits.cospanExt_app_left, TopCat.range_pullback_to_prod, TopCat.Sheaf.interUnionPullbackConeLift_left, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst, TopCat.pullback_fst_image_snd_preimage, CategoryTheory.Limits.widePushoutShapeOpEquiv_counitIso, CompHausLike.instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop, CategoryTheory.Limits.CompleteLattice.pullback_eq_inf, CategoryTheory.Abelian.epi_pullback_of_epi_g, prodIsoPullback_hom_snd_assoc, CategoryTheory.Limits.pullbackConeOfRightIso_π_app_left, CategoryTheory.Limits.pullbackConeOfLeftIso_x, CategoryTheory.Limits.walkingCospanOpEquiv_functor_map, CompHausLike.pullback.cone_π, TopCat.pullbackIsoProdSubtype_inv_fst_apply, CategoryTheory.Limits.pullbackObjIso_hom_comp_fst_assoc, CategoryTheory.WithTerminal.widePullbackShapeEquiv_inverse_obj, CategoryTheory.Over.tensorHom_left_fst, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd_assoc, CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso, CategoryTheory.Limits.pullback.comp_diagonal, CategoryTheory.Limits.cospanExt_hom_app_one, CategoryTheory.Limits.cospan_map_id, CategoryTheory.Limits.walkingCospanOpEquiv_functor_obj, CategoryTheory.Over.tensorHom_left_fst_assoc, prodIsoPullback_hom_fst, CategoryTheory.Limits.walkingSpanOpEquiv_functor_map, CategoryTheory.Limits.PullbackCone.eta_hom_hom, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr', AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, CategoryTheory.Over.η_pullback_left, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.cospanCompIso_inv_app_one, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, CategoryTheory.Limits.widePullbackShapeUnop_obj, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left, CategoryTheory.Limits.PullbackCone.ofCone_π, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1, CategoryTheory.Limits.pullbackObjIso_inv_comp_fst, CategoryTheory.Limits.PullbackCone.op_inl, CategoryTheory.Over.ConstructProducts.conesEquiv_functor, CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd, CategoryTheory.Limits.PullbackCone.flip_pt, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply, CategoryTheory.Limits.cospanCompIso_hom_app_left, CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst, TopCat.isEmbedding_pullback_to_prod, CategoryTheory.MonoOver.pullback_obj_left, TopCat.pullbackIsoProdSubtype_hom_apply, CategoryTheory.Limits.CoproductDisjoint.nonempty_isInitial_of_ne, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_f, CategoryTheory.Limits.pullback.diagonal_comp, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', CategoryTheory.Limits.pullbackObjIso_hom_comp_snd_assoc, CategoryTheory.Limits.widePullbackShapeOpEquiv_functor, CategoryTheory.MorphismProperty.diagonal_iff, CategoryTheory.Limits.Types.range_pullbackSnd, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range, CompHausLike.instHasLimitWalkingCospanCospan, TopCat.fst_isOpenEmbedding_of_right, CategoryTheory.Limits.cospanCompIso_hom_app_one, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst, prodIsoPullback_inv_snd, CategoryTheory.Limits.PullbackCone.combine_pt_map, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, CategoryTheory.NormalMonoCategory.pullback_of_mono, CategoryTheory.Limits.PullbackCone.unop_pt, TopCat.pullbackIsoProdSubtype_inv_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst_assoc, CategoryTheory.Limits.widePushoutShapeUnop_map, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight, CategoryTheory.Limits.PullbackCone.combine_pt_obj, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, CategoryTheory.Limits.PushoutCocone.op_pt, functorExt_inv_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left, CategoryTheory.Limits.HasFiniteWidePullbacks.out, CategoryTheory.Limits.FormalCoproduct.pullbackCone_condition, CategoryTheory.regularTopology.equalizerCondition_w, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_to_base_isOpenImmersion, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt, CategoryTheory.Limits.pullbackConeOfRightIso_π_app_none, TopCat.pullback_map_isOpenEmbedding, CategoryTheory.Over.μ_pullback_left_snd, CategoryTheory.Limits.Types.pullbackLimitCone_isLimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd_assoc, CategoryTheory.Limits.cospanExt_inv_app_left, CategoryTheory.Subobject.leInfCone_π_app_none, CategoryTheory.Limits.PullbackCone.condition_one, CategoryTheory.Functor.PreservesPairwisePullbacks.preservesLimit, CategoryTheory.Limits.pullbackObjIso_inv_comp_snd_assoc, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_hom_app_hom, TopCat.pullback_map_isEmbedding, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_fst, CategoryTheory.Over.starPullbackIsoStar_inv_app_left, CategoryTheory.Limits.cospanOp_inv_app, CategoryTheory.Limits.cospanCompIso_hom_app_right, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc, CategoryTheory.Limits.PullbackCone.isIso_snd_of_mono_of_isLimit, CategoryTheory.Limits.cospanCompIso_app_one, CategoryTheory.Limits.walkingSpanOpEquiv_functor_obj, CategoryTheory.Abelian.epi_fst_of_isLimit, CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong, CompHausLike.instPreservesLimitWalkingCospanCospanToCompHausLike, CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1, CategoryTheory.Over.ConstructProducts.conesEquivInverse_obj, CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst_assoc, CategoryTheory.Limits.cospanCompIso_app_left, CategoryTheory.Over.tensorHom_left_snd, CategoryTheory.Limits.PushoutCocone.unop_pt, CategoryTheory.Presieve.uncurry_pullbackArrows, prodIsoPullback_inv_snd_assoc, CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_hom_app, wideCospan_map, CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_π_app, CategoryTheory.Over.lift_left, CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd_assoc, CategoryTheory.instIsConnectedWidePullbackShape, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget, CategoryTheory.Limits.PullbackCone.isoMk_hom_hom, equivalenceOfEquiv_functor_obj_none, CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv, CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_inv_app, CategoryTheory.mono_iff_isIso_fst, CategoryTheory.Over.ConstructProducts.conesEquiv_inverse, AlgebraicGeometry.Scheme.Pullback.forget_comparison_surjective, CategoryTheory.Limits.PullbackCone.ofCone_pt, CategoryTheory.Limits.PullbackCone.mk_π_app_left, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_apply_coe, CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso, CategoryTheory.Over.isMonHom_pullbackFst_id_right, TopCat.Sheaf.interUnionPullbackCone_pt, CategoryTheory.Over.tensorObj_left, CategoryTheory.mono_iff_isIso_snd, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst_assoc, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd, CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_hom_app, CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono, TopCat.pullback_snd_range, CategoryTheory.Limits.opSpan_inv_app, CategoryTheory.IsPullback.of_isLimit_cone, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', TopCat.snd_isEmbedding_of_left, CategoryTheory.Limits.pullbackObjIso_inv_comp_snd, CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc, CategoryTheory.Limits.cospanExt_inv_app_right, CategoryTheory.Over.ε_pullback_left, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right, CategoryTheory.Limits.pullback_fst_map_snd_isPullback, AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective, CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, CategoryTheory.Limits.cospanExt_hom_app_right, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left', CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi, CategoryTheory.Limits.pullbackFstFstIso_inv, SSet.instFinitePullback, TopCat.pullback_fst_range, CategoryTheory.Limits.cospanExt_hom_app_left, CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_f, CategoryTheory.Limits.widePullbackShapeOpEquiv_counitIso, CategoryTheory.Limits.cospan_one, CategoryTheory.Limits.diagonal_pullback_fst, AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, TopCat.pullback_snd_image_fst_preimage, CategoryTheory.Limits.pullback_lift_map_isPullback, CategoryTheory.Limits.widePushoutShapeOpEquiv_unitIso, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instSndPullbackConeOfLeft, CategoryTheory.Limits.widePullbackShapeOp_map, CategoryTheory.WithTerminal.widePullbackShapeEquiv_functor_obj, CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom, CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_φ, CategoryTheory.Limits.WidePullbackCone.condition, CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map, CategoryTheory.Over.tensorObj_hom, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, CategoryTheory.Limits.FormalCoproduct.isPullback, CategoryTheory.Limits.cospanCompIso_app_right, CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_map_hom, CompHausLike.pullback.cone_pt, CategoryTheory.Limits.PullbackCone.fst_limit_cone, CategoryTheory.Limits.pullbackObjIso_hom_comp_snd, TopCat.isEmbedding_of_pullback, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, CategoryTheory.Limits.pullback_equalizer, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft, CategoryTheory.Limits.widePullbackShapeOpEquiv_unitIso, CategoryTheory.Regular.instMonoDesc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right
diagramIsoWideCospan 📖	CompOp	—
equivalenceOfEquiv 📖	CompOp	3 math math: equivalenceOfEquiv_functor_map_term, equivalenceOfEquiv_functor_obj_some, equivalenceOfEquiv_functor_obj_none
evalCasesBash 📖	CompOp	—
functorExt 📖	CompOp	2 math math: functorExt_hom_app, functorExt_inv_app
instDecidableEqHom 📖	CompOp	—
mkCone 📖	CompOp	2 math math: mkCone_π_app, mkCone_pt
struct 📖	CompOp	3 math math: hom_id, CategoryTheory.Limits.WalkingCospan.instSubsingletonHom, subsingleton_hom
uliftEquivalence 📖	CompOp	—
wideCospan 📖	CompOp	10 math math: CategoryTheory.Limits.WidePullbackCone.reindex_pt, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base, wideCospan_obj, CategoryTheory.Limits.WidePullbackCone.mk_pt, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π_assoc, CategoryTheory.Limits.WidePullbackCone.condition_assoc, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base_assoc, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π, wideCospan_map, CategoryTheory.Limits.WidePullbackCone.condition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalenceOfEquiv_functor_map_term 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Limits.WidePullbackShape category CategoryTheory.Equivalence.functor equivalenceOfEquiv Hom.term DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
equivalenceOfEquiv_functor_obj_none 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.WidePullbackShape category CategoryTheory.Equivalence.functor equivalenceOfEquiv	—	—
equivalenceOfEquiv_functor_obj_some 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.WidePullbackShape category CategoryTheory.Equivalence.functor equivalenceOfEquiv DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
functorExt_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WidePullbackShape category CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category functorExt CategoryTheory.Functor.obj CategoryTheory.Iso	—	—
functorExt_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WidePullbackShape category CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category functorExt CategoryTheory.Functor.obj CategoryTheory.Iso	—	—
hom_id 📖	mathematical	—	Hom.id CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WidePullbackShape struct	—	—
mkCone_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WidePullbackShape category CategoryTheory.Functor.map Hom.term	CategoryTheory.Limits.Cone.pt mkCone	—	—
mkCone_π_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WidePullbackShape category CategoryTheory.Functor.map Hom.term	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π mkCone Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	—
subsingleton_hom 📖	mathematical	—	Quiver.IsThin CategoryTheory.Limits.WidePullbackShape CategoryTheory.CategoryStruct.toQuiver struct	—	—
wideCospan_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Limits.WidePullbackShape category wideCospan CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
wideCospan_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.WidePullbackShape category wideCospan	—	—

CategoryTheory.Limits.WidePullbackShape.Hom

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—

CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

CategoryTheory.Limits.WidePushout

Definitions

Name	Category	Theorems
desc 📖	CompOp	9 math math: ι_desc_assoc, hom_eq_desc, head_desc_assoc, eq_desc_of_comp_eq, CategoryTheory.Arrow.mapCechConerve_app, CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app, head_desc, CategoryTheory.Arrow.cechConerve_map, ι_desc
head 📖	CompOp	10 math math: arrow_ι, hom_eq_desc, head_desc_assoc, hom_ext_iff, CategoryTheory.Arrow.mapCechConerve_app, CategoryTheory.Limits.Concrete.widePushout_exists_rep, head_desc, CategoryTheory.Arrow.cechConerve_map, CategoryTheory.Arrow.augmentedCechConerve_hom_app, arrow_ι_assoc
ι 📖	CompOp	11 math math: arrow_ι, ι_desc_assoc, hom_eq_desc, hom_ext_iff, CategoryTheory.Arrow.mapCechConerve_app, CategoryTheory.Limits.Concrete.widePushout_exists_rep', CategoryTheory.Limits.Concrete.widePushout_exists_rep, CategoryTheory.Arrow.cechConerve_map, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right, ι_desc, arrow_ι_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrow_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePushout ι head	—	CategoryTheory.Limits.colimit.w
arrow_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePushout ι head	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' arrow_ι
eq_desc_of_comp_eq 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePushout ι head	desc	—	CategoryTheory.Limits.IsColimit.uniq
head_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.widePushout head desc	—	CategoryTheory.Limits.colimit.ι_desc
head_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.widePushout head desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' head_desc
hom_eq_desc 📖	mathematical	—	desc CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePushout head ι	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.colimit.ι_desc
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePushout ι head	—	—	CategoryTheory.Limits.colimit.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePushout ι head	—	hom_ext
ι_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.widePushout ι desc	—	CategoryTheory.Limits.colimit.ι_desc
ι_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.widePushout ι desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_desc

CategoryTheory.Limits.WidePushoutShape

Definitions

Name	Category	Theorems
category 📖	CompOp	201 math math: CategoryTheory.Limits.spanCompIso_app_left, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_right, CategoryTheory.Limits.PushoutCocone.flip_pt, CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map, CategoryTheory.Limits.widePushoutShapeUnop_obj, CategoryTheory.Limits.widePushoutShapeOpEquiv_functor, CommRingCat.pushoutCocone_pt, CategoryTheory.Limits.spanCompIso_inv_app_zero, CategoryTheory.Limits.widePushoutShapeOpEquiv_inverse, CategoryTheory.Limits.PushoutCocone.mk_ι_app_zero, CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone, CategoryTheory.Limits.widePullbackShapeUnop_map, inl_coprodIsoPushout_hom, CategoryTheory.Limits.PushoutCocone.unop_π_app, CategoryTheory.Limits.inl_comp_pushoutObjIso_hom, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_obj, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, CategoryTheory.Limits.PushoutCocone.condition_assoc, CategoryTheory.Limits.span_map_id, CategoryTheory.Limits.PushoutCocone.op_snd, CategoryTheory.Limits.PushoutCocone.isoMk_inv_hom, CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape, CategoryTheory.Limits.PullbackCone.op_pt, CategoryTheory.Limits.span_right, CategoryTheory.Limits.inr_comp_pushoutObjIso_hom_assoc, CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi, CategoryTheory.IsPushout.isColimit', CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_map_hom, CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_hom_app, CommRingCat.Under.preservesFiniteLimits_of_flat, CategoryTheory.Limits.hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, CategoryTheory.Limits.spanCompIso_hom_app_zero, CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.Limits.spanOp_hom_app, CategoryTheory.Under.postAdjunctionRight_unit_app_right, CategoryTheory.Limits.widePullbackShapeOpEquiv_inverse, CategoryTheory.Limits.spanExt_hom_app_right, CategoryTheory.Limits.spanCompIso_inv_app_left, CategoryTheory.Limits.Types.instMonoPushoutInl, CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_inv_app, CategoryTheory.Limits.PullbackCone.op_ι_app, CategoryTheory.Limits.span_map_snd, CategoryTheory.Limits.walkingCospanOpEquiv_inverse_obj, CategoryTheory.Limits.walkingSpanOpEquiv_inverse_obj, CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_inv_app, CategoryTheory.Limits.spanCompIso_app_zero, CategoryTheory.Limits.PushoutCocone.ofCocone_ι, CategoryTheory.Limits.spanExt_hom_app_zero, CommRingCat.HomTopology.isEmbedding_pushout, CategoryTheory.instIsConnectedWidePushoutShape, CategoryTheory.Limits.spanOp_inv_app, CategoryTheory.Limits.PushoutCocone.eta_inv_hom, inr_coprodIsoPushout_hom_assoc, CategoryTheory.Limits.opSpan_hom_app, CategoryTheory.Limits.widePushoutShapeOp_map, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, CategoryTheory.Limits.spanCompIso_app_right, CategoryTheory.Limits.pushoutCoconeOfRightIso_x, CommRingCat.Under.instPreservesFiniteProductsUnderPushout, CategoryTheory.Limits.PushoutCocone.condition_zero, CategoryTheory.Limits.PushoutCocone.ι_app_left, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_left, CategoryTheory.Limits.PushoutCocone.ofCocone_pt, CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_hom_app, CategoryTheory.Limits.spanExt_app_one, CategoryTheory.Limits.opCospan_hom_app, CategoryTheory.Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit, CategoryTheory.SmallObject.ιFunctorObj_eq, CommRingCat.inr_injective_of_flat, CategoryTheory.Limits.spanCompIso_inv_app_right, CategoryTheory.Limits.PushoutCocone.mk_ι_app, CategoryTheory.Limits.PushoutCocone.ι_app_right, CategoryTheory.Abelian.mono_pushout_of_mono_g, CategoryTheory.Limits.spanExt_inv_app_zero, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, CategoryTheory.Limits.spanExt_app_left, CategoryTheory.Limits.widePushoutShapeOp_obj, CategoryTheory.BicartesianSq.isColimit', CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom, CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc_assoc, CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone, CategoryTheory.Limits.PushoutCocone.op_π_app, CategoryTheory.Limits.CompleteLattice.pushout_eq_sup, CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_inv_app, CategoryTheory.Limits.opCospan_inv_app, CategoryTheory.Limits.PullbackCone.unop_ι_app, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, CategoryTheory.Limits.cospanOp_hom_app, AlgebraicGeometry.instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, CategoryTheory.Limits.widePullbackShapeOp_obj, wideSpan_map, CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_left, CategoryTheory.Limits.spanCompIso_hom_app_right, CategoryTheory.Limits.widePushoutShapeOpEquiv_counitIso, AlgebraicGeometry.isPullback_Spec_map_pushout, CategoryTheory.Limits.walkingCospanOpEquiv_functor_map, CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit, AlgebraicGeometry.instIsOpenImmersionMapWalkingSpanSchemeSpan, CategoryTheory.Limits.walkingCospanOpEquiv_functor_obj, CategoryTheory.Limits.walkingSpanOpEquiv_functor_map, CategoryTheory.Limits.PushoutCocone.mk_pt, CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc_assoc, CommRingCat.inl_injective_of_flat, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_none, CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc, CategoryTheory.Limits.spanCompIso_hom_app_left, CategoryTheory.Limits.widePullbackShapeUnop_obj, CategoryTheory.SmallObject.πFunctorObj_eq, CategoryTheory.Limits.inl_comp_pushoutObjIso_inv, CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi, CategoryTheory.Limits.inr_comp_pushoutObjIso_inv, CategoryTheory.Limits.spanExt_hom_app_left, CommRingCat.tensorProdIsoPushout_app, CategoryTheory.Square.isPushout_iff, CategoryTheory.Limits.Cocone.ofPushoutCocone_ι, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, CategoryTheory.Limits.inl_comp_pushoutObjIso_inv_assoc, CategoryTheory.Limits.widePullbackShapeOpEquiv_functor, CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right, CategoryTheory.MorphismProperty.ind_underObj_pushout, inr_coprodIsoPushout_hom, CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, CategoryTheory.Abelian.mono_inl_of_isColimit, CategoryTheory.Limits.PullbackCone.unop_pt, CategoryTheory.Limits.span_map_fst, CategoryTheory.Limits.widePushoutShapeUnop_map, CategoryTheory.Limits.pushoutCoconeOfLeftIso_x, CategoryTheory.Limits.PushoutCocone.op_pt, CategoryTheory.Limits.PushoutCocone.mk_ι_app_right, CategoryTheory.Limits.span_left, CategoryTheory.Limits.inl_comp_pushoutObjIso_hom_assoc, AlgebraicGeometry.isPullback_SpecMap_pushout, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, inl_coprodIsoPushout_inv, AlgebraicGeometry.isIso_pushoutSection_iff, CategoryTheory.Limits.PreservesPushout.of_iso_comparison, CategoryTheory.Limits.PushoutCocone.isoMk_hom_hom, CategoryTheory.Limits.cospanOp_inv_app, CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_none, CategoryTheory.Limits.PushoutCocone.mk_ι_app_left, CategoryTheory.Limits.walkingSpanOpEquiv_functor_obj, CategoryTheory.widePushoutShape_connected, CategoryTheory.Abelian.mono_pushout_of_mono_f, CategoryTheory.Limits.Types.Pushout.cocone_ι_app, CategoryTheory.epi_iff_isIso_inl, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, inr_coprodIsoPushout_inv, wideSpan_obj, CategoryTheory.Limits.PushoutCocone.unop_pt, CategoryTheory.Limits.PushoutCocone.eta_hom_hom, CategoryTheory.Limits.spanExt_app_right, CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_hom_app, inl_coprodIsoPushout_hom_assoc, CategoryTheory.Under.postAdjunctionRight_counit_app_right, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso, CategoryTheory.Limits.inr_comp_pushoutObjIso_inv_assoc, CategoryTheory.Limits.Types.instMonoPushoutInr, CategoryTheory.Limits.inr_comp_pushoutObjIso_hom, CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization, CategoryTheory.Abelian.mono_inr_of_isColimit, CategoryTheory.Limits.diagramIsoSpan_inv_app, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, CategoryTheory.IsPushout.of_isColimit, CategoryTheory.Limits.span_zero, CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_inv_app, CategoryTheory.Limits.preservesPushout_symmetry, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, CategoryTheory.Limits.Cocone.ofPushoutCocone_pt, inl_coprodIsoPushout_inv_assoc, CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_hom_app, CategoryTheory.Limits.opSpan_inv_app, CategoryTheory.Limits.PushoutCocone.isIso_inr_of_epi_of_isColimit, CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_right, CategoryTheory.NormalEpiCategory.pushout_of_epi, inr_coprodIsoPushout_inv_assoc, CategoryTheory.Limits.PushoutCocone.unop_snd, CategoryTheory.epi_iff_isIso_inr, CategoryTheory.Limits.diagramIsoSpan_hom_app, CategoryTheory.Limits.widePullbackShapeOpEquiv_counitIso, CategoryTheory.CostructuredArrow.projectQuotient_mk, CategoryTheory.Limits.PushoutCocone.unop_fst, CategoryTheory.Limits.widePushoutShapeOpEquiv_unitIso, CategoryTheory.IsPushout.of_isColimit_cocone, CategoryTheory.Limits.HasFiniteWidePushouts.out, CategoryTheory.Limits.PushoutCocone.op_fst, CategoryTheory.Limits.Types.pushoutCocone_inr_injective_of_isColimit, CategoryTheory.Limits.spanExt_inv_app_right, CategoryTheory.Limits.widePullbackShapeOp_map, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, RingHom.IsStableUnderBaseChange.pushout_inl, CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map, CategoryTheory.Limits.spanExt_inv_app_left, CategoryTheory.Limits.Types.Pushout.cocone_pt, CategoryTheory.IsPushout.isVanKampen_iff, CategoryTheory.Limits.widePullbackShapeOpEquiv_unitIso, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right
diagramIsoWideSpan 📖	CompOp	—
equivalenceOfEquiv 📖	CompOp	—
evalCasesBash' 📖	CompOp	—
instDecidableEqHom 📖	CompOp	—
mkCocone 📖	CompOp	2 math math: mkCocone_pt, mkCocone_ι_app
struct 📖	CompOp	3 math math: hom_id, subsingleton_hom, CategoryTheory.Limits.WalkingSpan.instSubsingletonHom
uliftEquivalence 📖	CompOp	—
wideSpan 📖	CompOp	2 math math: wideSpan_map, wideSpan_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_id 📖	mathematical	—	Hom.id CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WidePushoutShape struct	—	—
mkCocone_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WidePushoutShape category CategoryTheory.Functor.map Hom.init	CategoryTheory.Limits.Cocone.pt mkCocone	—	—
mkCocone_ι_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WidePushoutShape category CategoryTheory.Functor.map Hom.init	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι mkCocone Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	—
subsingleton_hom 📖	mathematical	—	Quiver.IsThin CategoryTheory.Limits.WidePushoutShape CategoryTheory.CategoryStruct.toQuiver struct	—	—
wideSpan_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Limits.WidePushoutShape category wideSpan CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
wideSpan_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.WidePushoutShape category wideSpan	—	—

CategoryTheory.Limits.WidePushoutShape.Hom

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—

CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

---

← Back to Index