Commit 2026-01-15 20:10 3de2350c

View on Github →

chore(CategoryTheory/Limits/Shapes/Pullback): Split CommSq (#33968) Split the file CategoryTheory/Limits/Shapes/Pullback/CommSq.lean in twain: move defs/thms about BicartesianSq, HasZeroObject and HasZeroMorphism to CategoryTheory/Limits/Shapes/Pullback/BicartesianSq.lean

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

Modified Mathlib/Algebra/Category/Ring/LinearAlgebra.lean

Modified Mathlib/Algebra/Homology/CommSq.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/FiniteProd.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/SubcomplexColimits.lean

Modified Mathlib/CategoryTheory/Abelian/CommSq.lean

Modified Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean

Modified Mathlib/CategoryTheory/CommSq.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/LiftingProperties/Limits.lean

Modified Mathlib/CategoryTheory/LiftingProperties/ParametrizedAdjunction.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

Modified Mathlib/CategoryTheory/Limits/EpiMono.lean

Modified Mathlib/CategoryTheory/Limits/FormalCoproducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/MultiequalizerPullback.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.lean

added def CategoryTheory.Limits.CommSq.coconeOp

added def CategoryTheory.Limits.CommSq.coconeUnop

added def CategoryTheory.Limits.CommSq.coneOp

added def CategoryTheory.Limits.CommSq.coneUnop

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

deleted theorem CategoryTheory.BicartesianSq.flip

deleted theorem CategoryTheory.BicartesianSq.of_has_biproduct₁

deleted theorem CategoryTheory.BicartesianSq.of_has_biproduct₂

deleted theorem CategoryTheory.BicartesianSq.of_isPullback_isPushout

deleted theorem CategoryTheory.BicartesianSq.of_is_biproduct₁

deleted theorem CategoryTheory.BicartesianSq.of_is_biproduct₂

deleted structure CategoryTheory.BicartesianSq

deleted def CategoryTheory.CommSq.cocone

deleted def CategoryTheory.CommSq.coconeOp

deleted def CategoryTheory.CommSq.coconeUnop

deleted theorem CategoryTheory.CommSq.cocone_inl

deleted theorem CategoryTheory.CommSq.cocone_inr

deleted def CategoryTheory.CommSq.cone

deleted def CategoryTheory.CommSq.coneOp

deleted def CategoryTheory.CommSq.coneUnop

deleted theorem CategoryTheory.CommSq.cone_fst

deleted theorem CategoryTheory.CommSq.cone_snd

deleted theorem CategoryTheory.Functor.map_isPullback

deleted theorem CategoryTheory.Functor.map_isPushout

deleted def CategoryTheory.IsPullback.cone

deleted theorem CategoryTheory.IsPullback.cone_fst

deleted theorem CategoryTheory.IsPullback.cone_snd

deleted theorem CategoryTheory.IsPullback.exists_lift

deleted theorem CategoryTheory.IsPullback.flip

deleted theorem CategoryTheory.IsPullback.flip_iff

deleted theorem CategoryTheory.IsPullback.hasPullback

deleted theorem CategoryTheory.IsPullback.hom_ext

deleted theorem CategoryTheory.IsPullback.id_horiz

deleted theorem CategoryTheory.IsPullback.id_vert

deleted theorem CategoryTheory.IsPullback.inl_snd'

deleted theorem CategoryTheory.IsPullback.inl_snd

deleted theorem CategoryTheory.IsPullback.inr_fst'

deleted theorem CategoryTheory.IsPullback.inr_fst

deleted theorem CategoryTheory.IsPullback.isIso_fst_of_isIso

deleted theorem CategoryTheory.IsPullback.isIso_fst_of_mono

deleted theorem CategoryTheory.IsPullback.isIso_snd_iso_of_mono

deleted theorem CategoryTheory.IsPullback.isIso_snd_of_isIso

deleted theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst

deleted theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd

deleted theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst

deleted theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd

deleted theorem CategoryTheory.IsPullback.isoPullback_hom_fst

deleted theorem CategoryTheory.IsPullback.isoPullback_hom_snd

deleted theorem CategoryTheory.IsPullback.isoPullback_inv_fst

deleted theorem CategoryTheory.IsPullback.isoPullback_inv_snd

deleted theorem CategoryTheory.IsPullback.lift_fst

deleted theorem CategoryTheory.IsPullback.lift_snd

deleted theorem CategoryTheory.IsPullback.map_iff

deleted theorem CategoryTheory.IsPullback.of_bot'

deleted theorem CategoryTheory.IsPullback.of_bot

deleted theorem CategoryTheory.IsPullback.of_hasBinaryBiproduct

deleted theorem CategoryTheory.IsPullback.of_hasBinaryProduct'

deleted theorem CategoryTheory.IsPullback.of_hasBinaryProduct

deleted theorem CategoryTheory.IsPullback.of_hasPullback

deleted theorem CategoryTheory.IsPullback.of_has_biproduct

deleted theorem CategoryTheory.IsPullback.of_horiz_isIso

deleted theorem CategoryTheory.IsPullback.of_horiz_isIso_mono

deleted theorem CategoryTheory.IsPullback.of_id_fst

deleted theorem CategoryTheory.IsPullback.of_id_snd

deleted theorem CategoryTheory.IsPullback.of_isBilimit

deleted theorem CategoryTheory.IsPullback.of_isLimit'

deleted theorem CategoryTheory.IsPullback.of_isLimit

deleted theorem CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal

deleted theorem CategoryTheory.IsPullback.of_isLimit_cone

deleted theorem CategoryTheory.IsPullback.of_is_bilimit'

deleted theorem CategoryTheory.IsPullback.of_is_product'

deleted theorem CategoryTheory.IsPullback.of_is_product

deleted theorem CategoryTheory.IsPullback.of_iso'

deleted theorem CategoryTheory.IsPullback.of_iso

deleted theorem CategoryTheory.IsPullback.of_iso_pullback

deleted theorem CategoryTheory.IsPullback.of_map

deleted theorem CategoryTheory.IsPullback.of_map_of_faithful

deleted theorem CategoryTheory.IsPullback.of_prod_fst_with_id

deleted theorem CategoryTheory.IsPullback.of_right'

deleted theorem CategoryTheory.IsPullback.of_right

deleted theorem CategoryTheory.IsPullback.of_vert_isIso

deleted theorem CategoryTheory.IsPullback.of_vert_isIso_mono

deleted theorem CategoryTheory.IsPullback.op

deleted theorem CategoryTheory.IsPullback.paste_horiz

deleted theorem CategoryTheory.IsPullback.paste_horiz_iff

deleted theorem CategoryTheory.IsPullback.paste_vert

deleted theorem CategoryTheory.IsPullback.paste_vert_iff

deleted def CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr

deleted theorem CategoryTheory.IsPullback.unop

deleted theorem CategoryTheory.IsPullback.zero_bot

deleted theorem CategoryTheory.IsPullback.zero_left

deleted theorem CategoryTheory.IsPullback.zero_right

deleted theorem CategoryTheory.IsPullback.zero_top

deleted structure CategoryTheory.IsPullback

deleted def CategoryTheory.IsPushout.cocone

deleted theorem CategoryTheory.IsPushout.cocone_inl

deleted theorem CategoryTheory.IsPushout.cocone_inr

deleted theorem CategoryTheory.IsPushout.exists_desc

deleted theorem CategoryTheory.IsPushout.flip

deleted theorem CategoryTheory.IsPushout.flip_iff

deleted theorem CategoryTheory.IsPushout.hasPushout

deleted theorem CategoryTheory.IsPushout.hom_ext

deleted theorem CategoryTheory.IsPushout.id_horiz

deleted theorem CategoryTheory.IsPushout.id_vert

deleted theorem CategoryTheory.IsPushout.inl_desc

deleted theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom

deleted theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv

deleted theorem CategoryTheory.IsPushout.inl_isoPushout_hom

deleted theorem CategoryTheory.IsPushout.inl_isoPushout_inv

deleted theorem CategoryTheory.IsPushout.inl_snd'

deleted theorem CategoryTheory.IsPushout.inl_snd

deleted theorem CategoryTheory.IsPushout.inr_desc

deleted theorem CategoryTheory.IsPushout.inr_fst'

deleted theorem CategoryTheory.IsPushout.inr_fst

deleted theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom

deleted theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv

deleted theorem CategoryTheory.IsPushout.inr_isoPushout_hom

deleted theorem CategoryTheory.IsPushout.inr_isoPushout_inv

deleted theorem CategoryTheory.IsPushout.isIso_inl_iso_of_epi

deleted theorem CategoryTheory.IsPushout.isIso_inl_of_isIso

deleted theorem CategoryTheory.IsPushout.isIso_inr_iso_of_epi

deleted theorem CategoryTheory.IsPushout.isIso_inr_of_isIso

deleted theorem CategoryTheory.IsPushout.map_iff

deleted theorem CategoryTheory.IsPushout.of_coprod_inl_with_id

deleted theorem CategoryTheory.IsPushout.of_hasBinaryBiproduct

deleted theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct'

deleted theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct

deleted theorem CategoryTheory.IsPushout.of_hasPushout

deleted theorem CategoryTheory.IsPushout.of_has_biproduct

deleted theorem CategoryTheory.IsPushout.of_horiz_isIso

deleted theorem CategoryTheory.IsPushout.of_horiz_isIso_epi

deleted theorem CategoryTheory.IsPushout.of_id_fst

deleted theorem CategoryTheory.IsPushout.of_id_snd

deleted theorem CategoryTheory.IsPushout.of_isBilimit

deleted theorem CategoryTheory.IsPushout.of_isColimit'

deleted theorem CategoryTheory.IsPushout.of_isColimit

deleted theorem CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial

deleted theorem CategoryTheory.IsPushout.of_isColimit_cocone

deleted theorem CategoryTheory.IsPushout.of_is_bilimit'

deleted theorem CategoryTheory.IsPushout.of_is_coproduct'

deleted theorem CategoryTheory.IsPushout.of_is_coproduct

deleted theorem CategoryTheory.IsPushout.of_iso'

deleted theorem CategoryTheory.IsPushout.of_iso

deleted theorem CategoryTheory.IsPushout.of_iso_pushout

deleted theorem CategoryTheory.IsPushout.of_left'

deleted theorem CategoryTheory.IsPushout.of_left

deleted theorem CategoryTheory.IsPushout.of_map

deleted theorem CategoryTheory.IsPushout.of_map_of_faithful

deleted theorem CategoryTheory.IsPushout.of_top'

deleted theorem CategoryTheory.IsPushout.of_top

deleted theorem CategoryTheory.IsPushout.of_vert_isIso

deleted theorem CategoryTheory.IsPushout.of_vert_isIso_epi

deleted theorem CategoryTheory.IsPushout.op

deleted theorem CategoryTheory.IsPushout.paste_horiz

deleted theorem CategoryTheory.IsPushout.paste_horiz_iff

deleted theorem CategoryTheory.IsPushout.paste_vert

deleted theorem CategoryTheory.IsPushout.paste_vert_iff

deleted def CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd

deleted theorem CategoryTheory.IsPushout.unop

deleted theorem CategoryTheory.IsPushout.zero_bot

deleted theorem CategoryTheory.IsPushout.zero_left

deleted theorem CategoryTheory.IsPushout.zero_right

deleted theorem CategoryTheory.IsPushout.zero_top

deleted structure CategoryTheory.IsPushout

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Connected.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equalizer.lean

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean

added theorem CategoryTheory.Functor.map_isPullback

added theorem CategoryTheory.Functor.map_isPushout

added theorem CategoryTheory.IsPullback.id_horiz

added theorem CategoryTheory.IsPullback.id_vert

added theorem CategoryTheory.IsPullback.isIso_fst_of_isIso

added theorem CategoryTheory.IsPullback.isIso_fst_of_mono

added theorem CategoryTheory.IsPullback.isIso_snd_iso_of_mono

added theorem CategoryTheory.IsPullback.isIso_snd_of_isIso

added theorem CategoryTheory.IsPullback.map_iff

added theorem CategoryTheory.IsPullback.of_bot'

added theorem CategoryTheory.IsPullback.of_bot

added theorem CategoryTheory.IsPullback.of_hasBinaryProduct'

added theorem CategoryTheory.IsPullback.of_horiz_isIso

added theorem CategoryTheory.IsPullback.of_horiz_isIso_mono

added theorem CategoryTheory.IsPullback.of_id_fst

added theorem CategoryTheory.IsPullback.of_id_snd

added theorem CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal

added theorem CategoryTheory.IsPullback.of_is_product'

added theorem CategoryTheory.IsPullback.of_is_product

added theorem CategoryTheory.IsPullback.of_iso'

added theorem CategoryTheory.IsPullback.of_iso

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_prod_fst_with_id

added theorem CategoryTheory.IsPullback.of_right'

added theorem CategoryTheory.IsPullback.of_right

added theorem CategoryTheory.IsPullback.of_vert_isIso

added theorem CategoryTheory.IsPullback.of_vert_isIso_mono

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 theorem CategoryTheory.IsPushout.id_horiz

added theorem CategoryTheory.IsPushout.id_vert

added theorem CategoryTheory.IsPushout.isIso_inl_iso_of_epi

added theorem CategoryTheory.IsPushout.isIso_inl_of_isIso

added theorem CategoryTheory.IsPushout.isIso_inr_iso_of_epi

added theorem CategoryTheory.IsPushout.isIso_inr_of_isIso

added theorem CategoryTheory.IsPushout.map_iff

added theorem CategoryTheory.IsPushout.of_coprod_inl_with_id

added theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct'

added theorem CategoryTheory.IsPushout.of_horiz_isIso

added theorem CategoryTheory.IsPushout.of_horiz_isIso_epi

added theorem CategoryTheory.IsPushout.of_id_fst

added theorem CategoryTheory.IsPushout.of_id_snd

added theorem CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial

added theorem CategoryTheory.IsPushout.of_is_coproduct'

added theorem CategoryTheory.IsPushout.of_is_coproduct

added theorem CategoryTheory.IsPushout.of_iso'

added theorem CategoryTheory.IsPushout.of_iso

added theorem CategoryTheory.IsPushout.of_iso_pushout

added theorem CategoryTheory.IsPushout.of_left'

added theorem CategoryTheory.IsPushout.of_left

added theorem CategoryTheory.IsPushout.of_map

added theorem CategoryTheory.IsPushout.of_map_of_faithful

added theorem CategoryTheory.IsPushout.of_top'

added theorem CategoryTheory.IsPushout.of_top

added theorem CategoryTheory.IsPushout.of_vert_isIso

added theorem CategoryTheory.IsPushout.of_vert_isIso_epi

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

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/BicartesianSq.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 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.of_hasBinaryBiproduct

added theorem CategoryTheory.IsPullback.of_hasBinaryProduct

added theorem CategoryTheory.IsPullback.of_has_biproduct

added theorem CategoryTheory.IsPullback.of_isBilimit

added theorem CategoryTheory.IsPullback.of_is_bilimit'

added def CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr

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 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.of_hasBinaryBiproduct

added theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct

added theorem CategoryTheory.IsPushout.of_has_biproduct

added theorem CategoryTheory.IsPushout.of_isBilimit

added theorem CategoryTheory.IsPushout.of_is_bilimit'

added def CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd

added theorem CategoryTheory.IsPushout.zero_bot

added theorem CategoryTheory.IsPushout.zero_left

added theorem CategoryTheory.IsPushout.zero_right

added theorem CategoryTheory.IsPushout.zero_top

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Defs.lean

added def CategoryTheory.IsPullback.cone

added theorem CategoryTheory.IsPullback.cone_fst

added theorem CategoryTheory.IsPullback.cone_snd

added theorem CategoryTheory.IsPullback.exists_lift

added theorem CategoryTheory.IsPullback.flip

added theorem CategoryTheory.IsPullback.flip_iff

added theorem CategoryTheory.IsPullback.hasPullback

added theorem CategoryTheory.IsPullback.hom_ext

added theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst

added theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd

added theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst

added theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd

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.lift_fst

added theorem CategoryTheory.IsPullback.lift_snd

added theorem CategoryTheory.IsPullback.of_hasPullback

added theorem CategoryTheory.IsPullback.of_isLimit'

added theorem CategoryTheory.IsPullback.of_isLimit

added theorem CategoryTheory.IsPullback.of_isLimit_cone

added theorem CategoryTheory.IsPullback.op

added theorem CategoryTheory.IsPullback.unop

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.exists_desc

added theorem CategoryTheory.IsPushout.flip

added theorem CategoryTheory.IsPushout.flip_iff

added theorem CategoryTheory.IsPushout.hasPushout

added theorem CategoryTheory.IsPushout.hom_ext

added theorem CategoryTheory.IsPushout.inl_desc

added theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom

added theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv

added theorem CategoryTheory.IsPushout.inl_isoPushout_hom

added theorem CategoryTheory.IsPushout.inl_isoPushout_inv

added theorem CategoryTheory.IsPushout.inr_desc

added theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom

added theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv

added theorem CategoryTheory.IsPushout.inr_isoPushout_hom

added theorem CategoryTheory.IsPushout.inr_isoPushout_inv

added theorem CategoryTheory.IsPushout.of_hasPushout

added theorem CategoryTheory.IsPushout.of_isColimit'

added theorem CategoryTheory.IsPushout.of_isColimit

added theorem CategoryTheory.IsPushout.of_isColimit_cocone

added theorem CategoryTheory.IsPushout.op

added theorem CategoryTheory.IsPushout.unop

added structure CategoryTheory.IsPushout

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean

added def CategoryTheory.Limits.CommSq.cocone

added theorem CategoryTheory.Limits.CommSq.cocone_inl

added theorem CategoryTheory.Limits.CommSq.cocone_inr

added def CategoryTheory.Limits.CommSq.cone

added theorem CategoryTheory.Limits.CommSq.cone_fst

added theorem CategoryTheory.Limits.CommSq.cone_snd

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

Modified Mathlib/CategoryTheory/Limits/Types/Multicoequalizer.lean

Modified Mathlib/CategoryTheory/Limits/Types/Pullbacks.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean

Modified Mathlib/CategoryTheory/Sites/Preserves.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/SmallObject/Construction.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

Modified Mathlib/CategoryTheory/Topos/Classifier.lean