Commit 2023-09-05 20:39 686671be

View on Github →

feat(CategoryTheory): misc lemmas about morphism properties (#6887)

Estimated changes

Modified Mathlib/CategoryTheory/Arrow.lean

added def CategoryTheory.Functor.mapArrowEquivalence

added def CategoryTheory.Functor.mapArrowFunctor

Modified Mathlib/CategoryTheory/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_subset_isomorphisms

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.isoClosure_iff

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.map_iff

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_subset

added theorem CategoryTheory.MorphismProperty.RespectsIso.isoClosure_eq

added theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse

added theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor

added theorem CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence

added theorem CategoryTheory.MorphismProperty.isoClosure_isoClosure

added theorem CategoryTheory.MorphismProperty.isoClosure_subset_iff

added def CategoryTheory.MorphismProperty.map

added theorem CategoryTheory.MorphismProperty.map_eq_of_iso

added theorem CategoryTheory.MorphismProperty.map_id

added theorem CategoryTheory.MorphismProperty.map_id_eq_isoClosure

added theorem CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence

added theorem CategoryTheory.MorphismProperty.map_inverseImage_subset

added theorem CategoryTheory.MorphismProperty.map_isoClosure

added theorem CategoryTheory.MorphismProperty.map_map

added theorem CategoryTheory.MorphismProperty.map_mem_map

added theorem CategoryTheory.MorphismProperty.map_respectsIso

added theorem CategoryTheory.MorphismProperty.map_subset_iff

added theorem CategoryTheory.MorphismProperty.monotone_isoClosure

added theorem CategoryTheory.MorphismProperty.monotone_map

added theorem CategoryTheory.MorphismProperty.subset_iff_le