Commit 2025-11-17 00:03 9e5cdbff

View on Github →

chore(CategoryTheory/Limits/Types): split Shapes.lean (#31258) The file CategoryTheory.Limits.Types.Shapes is split in several files corresponding to different kinds of shapes of limits/colimits. (As that constructions are not self-dual, dual shapes appear in separate files, e.g. Pushouts and Pullbacks.)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Grp/Adjunctions.lean

Modified Mathlib/AlgebraicGeometry/GluingOneHypercover.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Galois/Basic.lean

Modified Mathlib/CategoryTheory/GlueData.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

Modified Mathlib/CategoryTheory/Limits/FintypeCat.lean

Modified Mathlib/CategoryTheory/Limits/Pi.lean

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

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

Created Mathlib/CategoryTheory/Limits/Types/Coequalizers.lean

added def CategoryTheory.Limits.Types.coequalizerColimit

added theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv

added theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom

added theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq

Created Mathlib/CategoryTheory/Limits/Types/Coproducts.lean

added theorem CategoryTheory.Limits.Types.binaryCofan_isColimit_iff

added def CategoryTheory.Limits.Types.binaryCoproductCocone

added def CategoryTheory.Limits.Types.binaryCoproductColimit

added def CategoryTheory.Limits.Types.binaryCoproductColimitCocone

added theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom

added theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv

added theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom

added theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv

added def CategoryTheory.Limits.Types.coproductColimitCocone

added theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv

added theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom

added def CategoryTheory.Limits.Types.initialColimitCocone

added theorem CategoryTheory.Limits.Types.initial_iff_empty

Created Mathlib/CategoryTheory/Limits/Types/Equalizers.lean

added theorem CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype

added theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι

added def CategoryTheory.Limits.Types.equalizerLimit

added theorem CategoryTheory.Limits.Types.type_equalizer_iff_unique

added theorem CategoryTheory.Limits.Types.unique_of_type_equalizer

Created Mathlib/CategoryTheory/Limits/Types/Multiequalizer.lean

added structure CategoryTheory.Limits.MulticospanIndex.sections

added def CategoryTheory.Limits.MulticospanIndex.sectionsEquiv

added theorem CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val

added theorem CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val

added theorem CategoryTheory.Limits.Multifork.isLimit_types_iff

added def CategoryTheory.Limits.Multifork.toSections

added theorem CategoryTheory.Limits.Multifork.toSections_fac

Created Mathlib/CategoryTheory/Limits/Types/Products.lean

added theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval

added theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π

added def CategoryTheory.Limits.Types.binaryProductCone

added theorem CategoryTheory.Limits.Types.binaryProductCone_fst

added theorem CategoryTheory.Limits.Types.binaryProductCone_snd

added def CategoryTheory.Limits.Types.binaryProductFunctor

added theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst

added theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd

added theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst

added theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd

added def CategoryTheory.Limits.Types.binaryProductLimit

added def CategoryTheory.Limits.Types.binaryProductLimitCone

added theorem CategoryTheory.Limits.Types.pi_lift_π_apply'

added theorem CategoryTheory.Limits.Types.pi_lift_π_apply

added theorem CategoryTheory.Limits.Types.pi_map_π_apply'

added theorem CategoryTheory.Limits.Types.pi_map_π_apply

added theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval

added theorem CategoryTheory.Limits.Types.productIso_inv_comp_π

added def CategoryTheory.Limits.Types.productLimitCone

added def CategoryTheory.Limits.Types.terminalLimitCone

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

added theorem CategoryTheory.Limits.Types.CategoryTheory.Limits.Types.range_fst_of_isPullback

added theorem CategoryTheory.Limits.Types.CategoryTheory.Limits.Types.range_pullbackFst

added theorem CategoryTheory.Limits.Types.CategoryTheory.Limits.Types.range_pullbackSnd

added theorem CategoryTheory.Limits.Types.CategoryTheory.Limits.Types.range_snd_of_isPullback

added theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.equivPullbackObj_apply_fst

added theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.equivPullbackObj_apply_snd

added theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst

added theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd

added theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.type_ext

added def CategoryTheory.Limits.Types.PullbackCone.toPullbackObj

added theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_hom_fst

added theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_hom_snd

added theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_inv_fst

added theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_inv_fst_apply

added theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_inv_snd

added theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_inv_snd_apply

added def CategoryTheory.Limits.Types.pullbackLimitCone

deleted theorem CategoryTheory.Limits.Types.range_fst_of_isPullback

deleted theorem CategoryTheory.Limits.Types.range_pullbackFst

deleted theorem CategoryTheory.Limits.Types.range_pullbackSnd

deleted theorem CategoryTheory.Limits.Types.range_snd_of_isPullback

Created Mathlib/CategoryTheory/Limits/Types/Pushouts.lean

added def CategoryTheory.Limits.Types.Pushout'

added theorem CategoryTheory.Limits.Types.Pushout.Rel'.symm

added inductive CategoryTheory.Limits.Types.Pushout.Rel'

added inductive CategoryTheory.Limits.Types.Pushout.Rel

added def CategoryTheory.Limits.Types.Pushout.cocone

added theorem CategoryTheory.Limits.Types.Pushout.condition

added def CategoryTheory.Limits.Types.Pushout.equivPushout'

added theorem CategoryTheory.Limits.Types.Pushout.equivalence_rel'

added def CategoryTheory.Limits.Types.Pushout.inl

added theorem CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff

added theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff

added theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff

added def CategoryTheory.Limits.Types.Pushout.inr

added theorem CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff

added def CategoryTheory.Limits.Types.Pushout.isColimitCocone

added theorem CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff

added def CategoryTheory.Limits.Types.Pushout

added theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit

added theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso

added theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso

added theorem CategoryTheory.Limits.Types.pushoutCocone_inr_injective_of_isColimit

added theorem CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit

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

deleted structure CategoryTheory.Limits.Types.MulticospanIndex.sections

deleted def CategoryTheory.Limits.Types.MulticospanIndex.sectionsEquiv

deleted theorem CategoryTheory.Limits.Types.Multifork.IsLimit.sectionsEquiv_apply_val

deleted theorem CategoryTheory.Limits.Types.Multifork.IsLimit.sectionsEquiv_symm_apply_val

deleted theorem CategoryTheory.Limits.Types.Multifork.isLimit_types_iff

deleted def CategoryTheory.Limits.Types.Multifork.toSections

deleted theorem CategoryTheory.Limits.Types.Multifork.toSections_fac

deleted theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.equivPullbackObj_apply_fst

deleted theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.equivPullbackObj_apply_snd

deleted theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst

deleted theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd

deleted theorem CategoryTheory.Limits.Types.PullbackCone.IsLimit.type_ext

deleted def CategoryTheory.Limits.Types.PullbackCone.toPullbackObj

deleted theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval

deleted theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π

deleted def CategoryTheory.Limits.Types.Types.Pushout'

deleted theorem CategoryTheory.Limits.Types.Types.Pushout.Rel'.symm

deleted inductive CategoryTheory.Limits.Types.Types.Pushout.Rel'

deleted inductive CategoryTheory.Limits.Types.Types.Pushout.Rel

deleted def CategoryTheory.Limits.Types.Types.Pushout.cocone

deleted theorem CategoryTheory.Limits.Types.Types.Pushout.condition

deleted def CategoryTheory.Limits.Types.Types.Pushout.equivPushout'

deleted theorem CategoryTheory.Limits.Types.Types.Pushout.equivalence_rel'

deleted def CategoryTheory.Limits.Types.Types.Pushout.inl

deleted theorem CategoryTheory.Limits.Types.Types.Pushout.inl_eq_inr_iff

deleted theorem CategoryTheory.Limits.Types.Types.Pushout.inl_rel'_inl_iff

deleted theorem CategoryTheory.Limits.Types.Types.Pushout.inl_rel'_inr_iff

deleted def CategoryTheory.Limits.Types.Types.Pushout.inr

deleted theorem CategoryTheory.Limits.Types.Types.Pushout.inr_rel'_inr_iff

deleted def CategoryTheory.Limits.Types.Types.Pushout.isColimitCocone

deleted theorem CategoryTheory.Limits.Types.Types.Pushout.quot_mk_eq_iff

deleted def CategoryTheory.Limits.Types.Types.Pushout

deleted theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_hom_fst

deleted theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_hom_snd

deleted theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_inv_fst

deleted theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_inv_fst_apply

deleted theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_inv_snd

deleted theorem CategoryTheory.Limits.Types.Types.pullbackIsoPullback_inv_snd_apply

deleted theorem CategoryTheory.Limits.Types.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit

deleted theorem CategoryTheory.Limits.Types.Types.pushoutCocone_inl_eq_inr_iff_of_iso

deleted theorem CategoryTheory.Limits.Types.Types.pushoutCocone_inl_eq_inr_imp_of_iso

deleted theorem CategoryTheory.Limits.Types.Types.pushoutCocone_inr_injective_of_isColimit

deleted theorem CategoryTheory.Limits.Types.Types.pushoutCocone_inr_mono_of_isColimit

deleted theorem CategoryTheory.Limits.Types.binaryCofan_isColimit_iff

deleted def CategoryTheory.Limits.Types.binaryCoproductCocone

deleted def CategoryTheory.Limits.Types.binaryCoproductColimit

deleted def CategoryTheory.Limits.Types.binaryCoproductColimitCocone

deleted theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom

deleted theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv

deleted theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom

deleted theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv

deleted def CategoryTheory.Limits.Types.binaryProductCone

deleted theorem CategoryTheory.Limits.Types.binaryProductCone_fst

deleted theorem CategoryTheory.Limits.Types.binaryProductCone_snd

deleted def CategoryTheory.Limits.Types.binaryProductFunctor

deleted theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst

deleted theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd

deleted theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst

deleted theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd

deleted def CategoryTheory.Limits.Types.binaryProductLimit

deleted def CategoryTheory.Limits.Types.binaryProductLimitCone

deleted def CategoryTheory.Limits.Types.coequalizerColimit

deleted theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv

deleted theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom

deleted theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq

deleted def CategoryTheory.Limits.Types.coproductColimitCocone

deleted theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv

deleted theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom

deleted theorem CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype

deleted theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι

deleted def CategoryTheory.Limits.Types.equalizerLimit

deleted def CategoryTheory.Limits.Types.initialColimitCocone

deleted theorem CategoryTheory.Limits.Types.initial_iff_empty

deleted theorem CategoryTheory.Limits.Types.pi_lift_π_apply'

deleted theorem CategoryTheory.Limits.Types.pi_lift_π_apply

deleted theorem CategoryTheory.Limits.Types.pi_map_π_apply'

deleted theorem CategoryTheory.Limits.Types.pi_map_π_apply

deleted theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval

deleted theorem CategoryTheory.Limits.Types.productIso_inv_comp_π

deleted def CategoryTheory.Limits.Types.productLimitCone

deleted def CategoryTheory.Limits.Types.pullbackLimitCone

deleted def CategoryTheory.Limits.Types.terminalLimitCone

deleted theorem CategoryTheory.Limits.Types.type_equalizer_iff_unique

deleted theorem CategoryTheory.Limits.Types.unique_of_type_equalizer

Modified Mathlib/CategoryTheory/Monoidal/Types/Basic.lean

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

Modified Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

Modified Mathlib/CategoryTheory/Types/Monomorphisms.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/Topology/Category/TopCat/Yoneda.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean