Commit 2023-03-07 06:55 9222c02d

View on Github →

feat: port CategoryTheory.Preserves.Shapes.Equalizers (#2687)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.PreservesCoequalizer.iso

added theorem CategoryTheory.Limits.PreservesCoequalizer.iso_hom

added def CategoryTheory.Limits.PreservesEqualizer.iso

added theorem CategoryTheory.Limits.PreservesEqualizer.iso_hom

added def CategoryTheory.Limits.PreservesEqualizer.ofIsoComparison

added def CategoryTheory.Limits.isColimitCoforkMapOfIsColimit

added def CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv

added def CategoryTheory.Limits.isColimitOfHasCoequalizerOfPreservesColimit

added def CategoryTheory.Limits.isColimitOfIsColimitCoforkMap

added def CategoryTheory.Limits.isLimitForkMapOfIsLimit

added def CategoryTheory.Limits.isLimitMapConeForkEquiv

added def CategoryTheory.Limits.isLimitOfHasEqualizerOfPreservesLimit

added def CategoryTheory.Limits.isLimitOfIsLimitForkMap

added theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv

added theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap

added theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc

added theorem CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc

added def CategoryTheory.Limits.ofIsoComparison