Commit 2023-03-14 10:33 0d10d3e7

View on Github →

feat: port CategoryTheory.Limits.Shapes.CommSq (#2867)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/CommSq.lean

added theorem CategoryTheory.BicartesianSq.flip

added theorem CategoryTheory.BicartesianSq.of_has_biproduct₁

added theorem CategoryTheory.BicartesianSq.of_has_biproduct₂

added theorem CategoryTheory.BicartesianSq.of_isPullback_isPushout

added theorem CategoryTheory.BicartesianSq.of_is_biproduct₁

added theorem CategoryTheory.BicartesianSq.of_is_biproduct₂

added structure CategoryTheory.BicartesianSq

added def CategoryTheory.CommSq.cocone

added def CategoryTheory.CommSq.coconeOp

added def CategoryTheory.CommSq.coconeUnop

added theorem CategoryTheory.CommSq.cocone_inl

added theorem CategoryTheory.CommSq.cocone_inr

added def CategoryTheory.CommSq.cone

added def CategoryTheory.CommSq.coneOp

added def CategoryTheory.CommSq.coneUnop

added theorem CategoryTheory.CommSq.cone_fst

added theorem CategoryTheory.CommSq.cone_snd

added theorem CategoryTheory.Functor.map_isPullback

added theorem CategoryTheory.Functor.map_isPushout

added def CategoryTheory.IsPullback.cone

added theorem CategoryTheory.IsPullback.cone_fst

added theorem CategoryTheory.IsPullback.cone_snd

added theorem CategoryTheory.IsPullback.flip

added theorem CategoryTheory.IsPullback.flip_iff

added theorem CategoryTheory.IsPullback.inl_snd'

added theorem CategoryTheory.IsPullback.inl_snd

added theorem CategoryTheory.IsPullback.inr_fst'

added theorem CategoryTheory.IsPullback.inr_fst

added theorem CategoryTheory.IsPullback.isoPullback_hom_fst

added theorem CategoryTheory.IsPullback.isoPullback_hom_snd

added theorem CategoryTheory.IsPullback.isoPullback_inv_fst

added theorem CategoryTheory.IsPullback.isoPullback_inv_snd

added theorem CategoryTheory.IsPullback.map_iff

added theorem CategoryTheory.IsPullback.of_bot

added theorem CategoryTheory.IsPullback.of_hasBinaryBiproduct

added theorem CategoryTheory.IsPullback.of_hasBinaryProduct'

added theorem CategoryTheory.IsPullback.of_hasBinaryProduct

added theorem CategoryTheory.IsPullback.of_hasPullback

added theorem CategoryTheory.IsPullback.of_has_biproduct

added theorem CategoryTheory.IsPullback.of_horiz_isIso

added theorem CategoryTheory.IsPullback.of_isBilimit

added theorem CategoryTheory.IsPullback.of_isLimit'

added theorem CategoryTheory.IsPullback.of_isLimit

added theorem CategoryTheory.IsPullback.of_is_bilimit'

added theorem CategoryTheory.IsPullback.of_is_product'

added theorem CategoryTheory.IsPullback.of_is_product

added theorem CategoryTheory.IsPullback.of_iso_pullback

added theorem CategoryTheory.IsPullback.of_map

added theorem CategoryTheory.IsPullback.of_map_of_faithful

added theorem CategoryTheory.IsPullback.of_right

added theorem CategoryTheory.IsPullback.of_vert_isIso

added theorem CategoryTheory.IsPullback.op

added theorem CategoryTheory.IsPullback.paste_horiz

added theorem CategoryTheory.IsPullback.paste_horiz_iff

added theorem CategoryTheory.IsPullback.paste_vert

added theorem CategoryTheory.IsPullback.paste_vert_iff

added def CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr

added theorem CategoryTheory.IsPullback.unop

added theorem CategoryTheory.IsPullback.zero_bot

added theorem CategoryTheory.IsPullback.zero_left

added theorem CategoryTheory.IsPullback.zero_right

added theorem CategoryTheory.IsPullback.zero_top

added structure CategoryTheory.IsPullback

added def CategoryTheory.IsPushout.cocone

added theorem CategoryTheory.IsPushout.cocone_inl

added theorem CategoryTheory.IsPushout.cocone_inr

added theorem CategoryTheory.IsPushout.flip

added theorem CategoryTheory.IsPushout.flip_iff

added theorem CategoryTheory.IsPushout.inl_isoPushout_hom

added theorem CategoryTheory.IsPushout.inl_isoPushout_inv

added theorem CategoryTheory.IsPushout.inl_snd'

added theorem CategoryTheory.IsPushout.inl_snd

added theorem CategoryTheory.IsPushout.inr_fst'

added theorem CategoryTheory.IsPushout.inr_fst

added theorem CategoryTheory.IsPushout.inr_isoPushout_hom

added theorem CategoryTheory.IsPushout.inr_isoPushout_inv

added theorem CategoryTheory.IsPushout.map_iff

added theorem CategoryTheory.IsPushout.of_bot

added theorem CategoryTheory.IsPushout.of_hasBinaryBiproduct

added theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct'

added theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct

added theorem CategoryTheory.IsPushout.of_hasPushout

added theorem CategoryTheory.IsPushout.of_has_biproduct

added theorem CategoryTheory.IsPushout.of_horiz_isIso

added theorem CategoryTheory.IsPushout.of_isBilimit

added theorem CategoryTheory.IsPushout.of_isColimit'

added theorem CategoryTheory.IsPushout.of_isColimit

added theorem CategoryTheory.IsPushout.of_is_bilimit'

added theorem CategoryTheory.IsPushout.of_is_coproduct'

added theorem CategoryTheory.IsPushout.of_is_coproduct

added theorem CategoryTheory.IsPushout.of_iso_pushout

added theorem CategoryTheory.IsPushout.of_map

added theorem CategoryTheory.IsPushout.of_map_of_faithful

added theorem CategoryTheory.IsPushout.of_right

added theorem CategoryTheory.IsPushout.of_vert_isIso

added theorem CategoryTheory.IsPushout.op

added theorem CategoryTheory.IsPushout.paste_horiz

added theorem CategoryTheory.IsPushout.paste_horiz_iff

added theorem CategoryTheory.IsPushout.paste_vert

added theorem CategoryTheory.IsPushout.paste_vert_iff

added def CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd

added theorem CategoryTheory.IsPushout.unop

added theorem CategoryTheory.IsPushout.zero_bot

added theorem CategoryTheory.IsPushout.zero_left

added theorem CategoryTheory.IsPushout.zero_right

added theorem CategoryTheory.IsPushout.zero_top

added structure CategoryTheory.IsPushout