Pullbacks

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.lean

Statistics

Metric	Count
Definitions coconeOp, coconeUnop, coneOp, coneUnop, isLimitEquivIsColimitOp, isLimitEquivIsColimitUnop, op, opUnopIso, unop, unopOpIso, isColimitEquivIsLimitOp, isColimitEquivIsLimitUnop, op, opUnopIso, unop, unopOpIso, cospanOp, opCospan, opSpan, pullbackIsoOpPushout, pullbackIsoUnopPushout, pushoutIsoOpPullback, pushoutIsoUnopPullback, spanOp	24
Theorems op_inl, op_inr, op_pt, op_ι_app, unop_inl, unop_inr, unop_pt, unop_ι_app, op_fst, op_pt, op_snd, op_π_app, unop_fst, unop_pt, unop_snd, unop_π_app, cospanOp_hom_app, cospanOp_inv_app, hasPullbacks_opposite, hasPushouts_opposite, opCospan_hom_app, opCospan_inv_app, opSpan_hom_app, opSpan_inv_app, pullbackIsoOpPushout_hom_inl, pullbackIsoOpPushout_hom_inl_assoc, pullbackIsoOpPushout_hom_inr, pullbackIsoOpPushout_hom_inr_assoc, pullbackIsoOpPushout_inv_fst, pullbackIsoOpPushout_inv_fst_assoc, pullbackIsoOpPushout_inv_snd, pullbackIsoOpPushout_inv_snd_assoc, pullbackIsoUnopPushout_hom_inl, pullbackIsoUnopPushout_hom_inl_assoc, pullbackIsoUnopPushout_hom_inr, pullbackIsoUnopPushout_hom_inr_assoc, pullbackIsoUnopPushout_inv_fst, pullbackIsoUnopPushout_inv_fst_assoc, pullbackIsoUnopPushout_inv_snd, pullbackIsoUnopPushout_inv_snd_assoc, pushoutIsoOpPullback_inl_hom, pushoutIsoOpPullback_inl_hom_assoc, pushoutIsoOpPullback_inr_hom, pushoutIsoOpPullback_inr_hom_assoc, pushoutIsoOpPullback_inv_fst, pushoutIsoOpPullback_inv_snd, pushoutIsoUnopPullback_inl_hom, pushoutIsoUnopPullback_inl_hom_assoc, pushoutIsoUnopPullback_inr_hom, pushoutIsoUnopPullback_inr_hom_assoc, pushoutIsoUnopPullback_inv_fst, pushoutIsoUnopPullback_inv_snd, spanOp_hom_app, spanOp_inv_app	54
Total	78

CategoryTheory.CommSq

Definitions

Name	Category	Theorems
coconeOp 📖	CompOp	—
coconeUnop 📖	CompOp	—
coneOp 📖	CompOp	—
coneUnop 📖	CompOp	—

CategoryTheory.Limits

Definitions

Name	Category	Theorems
cospanOp 📖	CompOp	2 math math: cospanOp_hom_app, cospanOp_inv_app
opCospan 📖	CompOp	3 math math: PushoutCocone.unop_π_app, opCospan_hom_app, opCospan_inv_app
opSpan 📖	CompOp	3 math math: opSpan_hom_app, PullbackCone.unop_ι_app, opSpan_inv_app
pullbackIsoOpPushout 📖	CompOp	8 math math: pullbackIsoOpPushout_hom_inr_assoc, pullbackIsoOpPushout_inv_fst_assoc, pullbackIsoOpPushout_inv_fst, pullbackIsoOpPushout_inv_snd, pullbackIsoOpPushout_hom_inl, pullbackIsoOpPushout_hom_inr, pullbackIsoOpPushout_inv_snd_assoc, pullbackIsoOpPushout_hom_inl_assoc
pullbackIsoUnopPushout 📖	CompOp	8 math math: pullbackIsoUnopPushout_inv_snd, pullbackIsoUnopPushout_hom_inr_assoc, pullbackIsoUnopPushout_hom_inl, pullbackIsoUnopPushout_inv_fst, pullbackIsoUnopPushout_hom_inl_assoc, pullbackIsoUnopPushout_inv_fst_assoc, pullbackIsoUnopPushout_inv_snd_assoc, pullbackIsoUnopPushout_hom_inr
pushoutIsoOpPullback 📖	CompOp	6 math math: pushoutIsoOpPullback_inr_hom_assoc, pushoutIsoOpPullback_inl_hom, pushoutIsoOpPullback_inv_fst, pushoutIsoOpPullback_inr_hom, pushoutIsoOpPullback_inl_hom_assoc, pushoutIsoOpPullback_inv_snd
pushoutIsoUnopPullback 📖	CompOp	6 math math: pushoutIsoUnopPullback_inr_hom, pushoutIsoUnopPullback_inl_hom_assoc, pushoutIsoUnopPullback_inr_hom_assoc, pushoutIsoUnopPullback_inv_snd, pushoutIsoUnopPullback_inv_fst, pushoutIsoUnopPullback_inl_hom
spanOp 📖	CompOp	2 math math: spanOp_hom_app, spanOp_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cospanOp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingCospan WidePullbackShape.category WalkingPair Opposite CategoryTheory.Category.opposite cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp WalkingSpan WidePushoutShape.category CategoryTheory.Equivalence.inverse walkingSpanOpEquiv CategoryTheory.Functor.op span CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category cospanOp CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
cospanOp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingCospan WidePullbackShape.category WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp WalkingSpan WidePushoutShape.category CategoryTheory.Equivalence.inverse walkingSpanOpEquiv CategoryTheory.Functor.op span cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category cospanOp CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
hasPullbacks_opposite 📖	mathematical	—	HasPullbacks Opposite CategoryTheory.Category.opposite	—	hasLimitsOfShape_op_of_hasColimitsOfShape hasColimitsOfShape_of_equivalence
hasPushouts_opposite 📖	mathematical	—	HasPushouts Opposite CategoryTheory.Category.opposite	—	hasColimitsOfShape_op_of_hasLimitsOfShape hasLimitsOfShape_of_equivalence
opCospan_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingCospan CategoryTheory.Category.opposite WidePullbackShape.category WalkingPair CategoryTheory.Functor.op cospan CategoryTheory.Functor.comp WalkingSpan WidePushoutShape.category CategoryTheory.Equivalence.functor walkingCospanOpEquiv span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opCospan CategoryTheory.Iso.inv CategoryTheory.Functor.obj Opposite.unop WidePushoutShape CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
opCospan_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingCospan CategoryTheory.Category.opposite WidePullbackShape.category WalkingPair CategoryTheory.Functor.comp WalkingSpan WidePushoutShape.category CategoryTheory.Equivalence.functor walkingCospanOpEquiv span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op cospan CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opCospan CategoryTheory.Iso.hom CategoryTheory.Functor.obj Opposite.unop WidePushoutShape CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
opSpan_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingSpan CategoryTheory.Category.opposite WidePushoutShape.category WalkingPair CategoryTheory.Functor.op span CategoryTheory.Functor.comp WalkingCospan WidePullbackShape.category CategoryTheory.Equivalence.functor walkingSpanOpEquiv cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opSpan CategoryTheory.Iso.inv CategoryTheory.Functor.obj Opposite.unop WidePullbackShape CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
opSpan_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingSpan CategoryTheory.Category.opposite WidePushoutShape.category WalkingPair CategoryTheory.Functor.comp WalkingCospan WidePullbackShape.category CategoryTheory.Equivalence.functor walkingSpanOpEquiv cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op span CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opSpan CategoryTheory.Iso.hom CategoryTheory.Functor.obj Opposite.unop WidePullbackShape CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
pullbackIsoOpPushout_hom_inl 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pullback Opposite CategoryTheory.Category.opposite pushout.inl Opposite.op CategoryTheory.Iso.hom pullbackIsoOpPushout pullback.fst	—	CategoryTheory.Iso.hom_inv_id_assoc
pullbackIsoOpPushout_hom_inl_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pushout.inl pullback Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Iso.hom pullbackIsoOpPushout pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOpPushout_hom_inl
pullbackIsoOpPushout_hom_inr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pullback Opposite CategoryTheory.Category.opposite pushout.inr Opposite.op CategoryTheory.Iso.hom pullbackIsoOpPushout pullback.snd	—	CategoryTheory.Iso.hom_inv_id_assoc
pullbackIsoOpPushout_hom_inr_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pushout.inr pullback Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Iso.hom pullbackIsoOpPushout pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOpPushout_hom_inr
pullbackIsoOpPushout_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pullback CategoryTheory.Category.opposite CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.fst Quiver.Hom.op pushout.inl	—	IsLimit.conePointUniqueUpToIso_inv_comp CategoryTheory.Category.comp_id
pullbackIsoOpPushout_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op pushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pullback CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.fst Quiver.Hom.op pushout.inl	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOpPushout_inv_fst
pullbackIsoOpPushout_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pullback CategoryTheory.Category.opposite CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.snd Quiver.Hom.op pushout.inr	—	IsLimit.conePointUniqueUpToIso_inv_comp CategoryTheory.Category.comp_id
pullbackIsoOpPushout_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op pushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pullback CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.snd Quiver.Hom.op pushout.inr	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOpPushout_inv_snd
pullbackIsoUnopPushout_hom_inl 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout CategoryTheory.Category.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pullback pushout.inl Opposite.unop CategoryTheory.Iso.hom pullbackIsoUnopPushout pullback.fst	—	CategoryTheory.Iso.hom_inv_id_assoc
pullbackIsoUnopPushout_hom_inl_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op pushout Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pushout.inl pullback Opposite.unop CategoryTheory.Iso.hom pullbackIsoUnopPushout pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoUnopPushout_hom_inl
pullbackIsoUnopPushout_hom_inr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout CategoryTheory.Category.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pullback pushout.inr Opposite.unop CategoryTheory.Iso.hom pullbackIsoUnopPushout pullback.snd	—	CategoryTheory.Iso.hom_inv_id_assoc
pullbackIsoUnopPushout_hom_inr_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op pushout Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pushout.inr pullback Opposite.unop CategoryTheory.Iso.hom pullbackIsoUnopPushout pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoUnopPushout_hom_inr
pullbackIsoUnopPushout_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pullback CategoryTheory.Iso.inv pullbackIsoUnopPushout pullback.fst Quiver.Hom.unop pushout.inl	—	IsLimit.conePointUniqueUpToIso_inv_comp PushoutCocone.unop_π_app CategoryTheory.Category.comp_id
pullbackIsoUnopPushout_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pullback CategoryTheory.Iso.inv pullbackIsoUnopPushout pullback.fst Quiver.Hom.unop pushout.inl	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoUnopPushout_inv_fst
pullbackIsoUnopPushout_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pullback CategoryTheory.Iso.inv pullbackIsoUnopPushout pullback.snd Quiver.Hom.unop pushout.inr	—	IsLimit.conePointUniqueUpToIso_inv_comp PushoutCocone.unop_π_app CategoryTheory.Category.comp_id
pullbackIsoUnopPushout_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pullback CategoryTheory.Iso.inv pullbackIsoUnopPushout pullback.snd Quiver.Hom.unop pushout.inr	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoUnopPushout_inv_snd
pushoutIsoOpPullback_inl_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite pushout Opposite.op pullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pushout.inl CategoryTheory.Iso.hom pushoutIsoOpPullback Quiver.Hom.op pullback.fst	—	IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Category.id_comp
pushoutIsoOpPullback_inl_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite pushout pushout.inl Opposite.op pullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom pushoutIsoOpPullback Quiver.Hom.op pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutIsoOpPullback_inl_hom
pushoutIsoOpPullback_inr_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite pushout Opposite.op pullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver pushout.inr CategoryTheory.Iso.hom pushoutIsoOpPullback Quiver.Hom.op pullback.snd	—	IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Category.id_comp
pushoutIsoOpPullback_inr_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite pushout pushout.inr Opposite.op pullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom pushoutIsoOpPullback Quiver.Hom.op pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutIsoOpPullback_inr_hom
pushoutIsoOpPullback_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op pullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv pushoutIsoOpPullback pullback.fst pushout.inl	—	CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
pushoutIsoOpPullback_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op pullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv pushoutIsoOpPullback pullback.snd pushout.inr	—	CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
pushoutIsoUnopPullback_inl_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout Opposite.unop pullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pushout.inl CategoryTheory.Iso.hom pushoutIsoUnopPullback Quiver.Hom.unop pullback.fst	—	IsColimit.comp_coconePointUniqueUpToIso_hom PullbackCone.unop_ι_app CategoryTheory.Category.id_comp
pushoutIsoUnopPullback_inl_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout pushout.inl Opposite.unop pullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom pushoutIsoUnopPullback Quiver.Hom.unop pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutIsoUnopPullback_inl_hom
pushoutIsoUnopPullback_inr_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout Opposite.unop pullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pushout.inr CategoryTheory.Iso.hom pushoutIsoUnopPullback Quiver.Hom.unop pullback.snd	—	IsColimit.comp_coconePointUniqueUpToIso_hom PullbackCone.unop_ι_app CategoryTheory.Category.id_comp
pushoutIsoUnopPullback_inr_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout pushout.inr Opposite.unop pullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom pushoutIsoUnopPullback Quiver.Hom.unop pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutIsoUnopPullback_inr_hom
pushoutIsoUnopPullback_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout Opposite.unop pullback CategoryTheory.Category.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv pushoutIsoUnopPullback pullback.fst pushout.inl	—	CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
pushoutIsoUnopPullback_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout Opposite.unop pullback CategoryTheory.Category.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv pushoutIsoUnopPullback pullback.snd pushout.inr	—	CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
spanOp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingSpan WidePushoutShape.category WalkingPair Opposite CategoryTheory.Category.opposite span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp WalkingCospan WidePullbackShape.category CategoryTheory.Equivalence.inverse walkingCospanOpEquiv CategoryTheory.Functor.op cospan CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category spanOp CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
spanOp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingSpan WidePushoutShape.category WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp WalkingCospan WidePullbackShape.category CategoryTheory.Equivalence.inverse walkingCospanOpEquiv CategoryTheory.Functor.op cospan span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category spanOp CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—

CategoryTheory.Limits.PullbackCone

Definitions

Name	Category	Theorems
isLimitEquivIsColimitOp 📖	CompOp	—
isLimitEquivIsColimitUnop 📖	CompOp	—
op 📖	CompOp	4 math math: op_pt, op_inr, op_ι_app, op_inl
opUnopIso 📖	CompOp	—
unop 📖	CompOp	4 math math: unop_inl, unop_inr, unop_ι_app, unop_pt
unopOpIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_inl 📖	mathematical	—	CategoryTheory.Limits.PushoutCocone.inl Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan fst	—	CategoryTheory.Category.id_comp
op_inr 📖	mathematical	—	CategoryTheory.Limits.PushoutCocone.inr Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan snd	—	CategoryTheory.Category.id_comp
op_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.cospan	—	—
op_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Equivalence.inverse CategoryTheory.Limits.walkingCospanOpEquiv CategoryTheory.Functor.op CategoryTheory.Limits.cospan CategoryTheory.Limits.Cocone.whisker CategoryTheory.Limits.Cone.op CategoryTheory.Limits.Cocone.ι op CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Cone.pt CategoryTheory.Iso.hom CategoryTheory.Iso CategoryTheory.Iso.refl CategoryTheory.Limits.Cone.π	—	—
unop_inl 📖	mathematical	—	CategoryTheory.Limits.PushoutCocone.inl Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.cospan fst	—	unop_ι_app CategoryTheory.Category.id_comp
unop_inr 📖	mathematical	—	CategoryTheory.Limits.PushoutCocone.inr Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.cospan snd	—	unop_ι_app CategoryTheory.Category.id_comp
unop_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.cospan	—	—
unop_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Limits.Cone CategoryTheory.Functor.comp CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Equivalence.functor CategoryTheory.Limits.walkingSpanOpEquiv CategoryTheory.Limits.cospan Opposite.op Quiver.Hom.op CategoryTheory.Limits.Cone.category CategoryTheory.Limits.Cones.postcompose CategoryTheory.Iso.hom CategoryTheory.Iso.symm CategoryTheory.Limits.opSpan CategoryTheory.Limits.Cone.whisker CategoryTheory.Limits.Cocone.ι unop CategoryTheory.CategoryStruct.comp CategoryTheory.Iso CategoryTheory.Iso.refl CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.opSpan_inv_app

CategoryTheory.Limits.PushoutCocone

Definitions

Name	Category	Theorems
isColimitEquivIsLimitOp 📖	CompOp	—
isColimitEquivIsLimitUnop 📖	CompOp	—
op 📖	CompOp	4 math math: op_snd, op_π_app, op_pt, op_fst
opUnopIso 📖	CompOp	—
unop 📖	CompOp	4 math math: unop_π_app, unop_pt, unop_snd, unop_fst
unopOpIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_fst 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.fst Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span inl	—	CategoryTheory.Category.comp_id
op_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	—	—
op_snd 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.snd Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span inr	—	CategoryTheory.Category.comp_id
op_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Equivalence.inverse CategoryTheory.Limits.walkingSpanOpEquiv CategoryTheory.Functor.op CategoryTheory.Limits.span CategoryTheory.Limits.Cone.whisker CategoryTheory.Limits.Cocone.op CategoryTheory.Limits.cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.π op CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
unop_fst 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.fst Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span inl	—	unop_π_app CategoryTheory.Category.comp_id
unop_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span	—	—
unop_snd 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.snd Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span inr	—	unop_π_app CategoryTheory.Category.comp_id
unop_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Opposite.unop CategoryTheory.Limits.Cocone.pt Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Limits.cospan Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone CategoryTheory.Functor.comp CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Equivalence.functor CategoryTheory.Limits.walkingCospanOpEquiv CategoryTheory.Limits.span Opposite.op Quiver.Hom.op CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocones.precompose CategoryTheory.Iso.hom CategoryTheory.Limits.opCospan CategoryTheory.Limits.Cocone.whisker CategoryTheory.Limits.Cone.π unop CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Limits.opCospan_hom_app

---

← Back to Index