Commit 2024-07-20 06:46 92b41b18

View on Github →

feat(CategoryTheory/Limits): identification of the point of any limit pullback cone in Type (#14935) The pullback of two maps in Type was already described explicitly. We generalize the API to any limit pullback cone.

Estimated changes

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

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

deleted def CategoryTheory.Limits.Types.Pushout'

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

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

deleted inductive CategoryTheory.Limits.Types.Pushout.Rel

deleted def CategoryTheory.Limits.Types.Pushout.cocone

deleted theorem CategoryTheory.Limits.Types.Pushout.condition

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

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

deleted def CategoryTheory.Limits.Types.Pushout.inl

deleted theorem CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff

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

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

deleted def CategoryTheory.Limits.Types.Pushout.inr

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

deleted def CategoryTheory.Limits.Types.Pushout.isColimitCocone

deleted theorem CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff

deleted def CategoryTheory.Limits.Types.Pushout

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

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

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

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

added def CategoryTheory.Limits.Types.Types.Pushout.cocone

added theorem CategoryTheory.Limits.Types.Types.Pushout.condition

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

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

added def CategoryTheory.Limits.Types.Types.Pushout.inl

added theorem CategoryTheory.Limits.Types.Types.Pushout.inl_eq_inr_iff

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

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

added def CategoryTheory.Limits.Types.Types.Pushout.inr

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

added def CategoryTheory.Limits.Types.Types.Pushout.isColimitCocone

added theorem CategoryTheory.Limits.Types.Types.Pushout.quot_mk_eq_iff

added def CategoryTheory.Limits.Types.Types.Pushout

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 theorem CategoryTheory.Limits.Types.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit

added theorem CategoryTheory.Limits.Types.Types.pushoutCocone_inl_eq_inr_iff_of_iso

added theorem CategoryTheory.Limits.Types.Types.pushoutCocone_inl_eq_inr_imp_of_iso

deleted theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst

deleted theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd

deleted theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst

deleted theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply

deleted theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd

deleted theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply

deleted theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit

deleted theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso

deleted theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso