Commit 2023-03-07 14:52 b96f7770

View on Github →

feat: port CategoryTheory.Limits.Preserves.Shapes.Pullbacks (#2571)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

added def CategoryTheory.Limits.PreservesPullback.iso

added theorem CategoryTheory.Limits.PreservesPullback.iso_hom

added theorem CategoryTheory.Limits.PreservesPullback.iso_hom_fst

added theorem CategoryTheory.Limits.PreservesPullback.iso_hom_snd

added theorem CategoryTheory.Limits.PreservesPullback.iso_inv_fst

added theorem CategoryTheory.Limits.PreservesPullback.iso_inv_snd

added def CategoryTheory.Limits.PreservesPullback.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesPushout.inl_iso_hom

added theorem CategoryTheory.Limits.PreservesPushout.inl_iso_inv

added theorem CategoryTheory.Limits.PreservesPushout.inr_iso_hom

added theorem CategoryTheory.Limits.PreservesPushout.inr_iso_inv

added def CategoryTheory.Limits.PreservesPushout.iso

added theorem CategoryTheory.Limits.PreservesPushout.iso_hom

added def CategoryTheory.Limits.PreservesPushout.ofIsoComparison

added theorem CategoryTheory.Limits.hasPullback_of_preserves_pullback

added theorem CategoryTheory.Limits.hasPushout_of_preserves_pushout

added def CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv

added def CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit

added def CategoryTheory.Limits.isColimitOfIsColimitPushoutCoconeMap

added def CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit

added def CategoryTheory.Limits.isLimitMapConePullbackConeEquiv

added def CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit

added def CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap

added def CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit

added def CategoryTheory.Limits.preservesPullbackSymmetry

added def CategoryTheory.Limits.preservesPushoutSymmetry