Commit 2026-05-01 22:04 e361dab6

View on Github →

feat(CategoryTheory/MorphismProperty): some lemmas for MorphismProperty.strictMap (#38787) Add some API lemmas for MorphismProperty.strictMap and other ways to transport morphism properties across functors.

Estimated changes

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

added theorem CategoryTheory.MorphismProperty.gc_strictMap

added theorem CategoryTheory.MorphismProperty.inverseImage_bot

added theorem CategoryTheory.MorphismProperty.inverseImage_iInf

added theorem CategoryTheory.MorphismProperty.inverseImage_id

added theorem CategoryTheory.MorphismProperty.inverseImage_inf

added theorem CategoryTheory.MorphismProperty.inverseImage_inverseImage

added theorem CategoryTheory.MorphismProperty.inverseImage_sInf

added theorem CategoryTheory.MorphismProperty.inverseImage_strictMap_inverseImage

added theorem CategoryTheory.MorphismProperty.inverseImage_strictMap_top

added theorem CategoryTheory.MorphismProperty.inverseImage_top

added theorem CategoryTheory.MorphismProperty.isoClosure_strictMap_le

added theorem CategoryTheory.MorphismProperty.le_inverseImage_strictMap

added theorem CategoryTheory.MorphismProperty.map_eq_isoClosure

modified theorem CategoryTheory.MorphismProperty.map_le_iff

added theorem CategoryTheory.MorphismProperty.monotone_inverseImage

added theorem CategoryTheory.MorphismProperty.monotone_strictMap

added theorem CategoryTheory.MorphismProperty.strictMap_bot

added theorem CategoryTheory.MorphismProperty.strictMap_iSup

added theorem CategoryTheory.MorphismProperty.strictMap_id

added theorem CategoryTheory.MorphismProperty.strictMap_inverseImage_le

added theorem CategoryTheory.MorphismProperty.strictMap_inverseImage_strictMap

added theorem CategoryTheory.MorphismProperty.strictMap_le_iff_le_inverseImage

added theorem CategoryTheory.MorphismProperty.strictMap_sSup

added theorem CategoryTheory.MorphismProperty.strictMap_strictMap

added theorem CategoryTheory.MorphismProperty.strictMap_sup