Commit 2024-10-14 11:53 e1266368

View on Github →

feat(CategoryTheory/Limits): Add basic pullback lemmas (#17685) This PR adds some basic lemmas about pullbacks of a monos/epi by itself. This is used in #14208.

Estimated changes

Modified Mathlib/CategoryTheory/CommSq.lean

added theorem CategoryTheory.CommSq.eq_of_epi

added theorem CategoryTheory.CommSq.eq_of_mono

Modified Mathlib/CategoryTheory/Galois/Basic.lean

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

added theorem CategoryTheory.IsPullback.isIso_fst_of_mono

added theorem CategoryTheory.IsPullback.isIso_snd_iso_of_mono

added theorem CategoryTheory.IsPushout.isIso_inl_iso_of_epi

added theorem CategoryTheory.IsPushout.isIso_inr_iso_of_epi

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

added theorem CategoryTheory.Limits.PullbackCone.fst_eq_snd_of_mono_eq

added theorem CategoryTheory.Limits.PullbackCone.isIso_fst_of_mono_of_isLimit

added theorem CategoryTheory.Limits.PullbackCone.isIso_snd_of_mono_of_isLimit

added theorem CategoryTheory.Limits.PushoutCocone.inl_eq_inr_of_epi_eq

added theorem CategoryTheory.Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit

added theorem CategoryTheory.Limits.PushoutCocone.isIso_inr_of_epi_of_isColimit

modified theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq

modified theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq

modified theorem CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq

modified theorem CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq