Commit 2023-08-06 06:23 e966251d

View on Github →

feat: localization functors are preserved through equivalences (#6236)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Localization/Equivalence.lean

added theorem CategoryTheory.Functor.IsLocalization.of_equivalence_source

added theorem CategoryTheory.Functor.IsLocalization.of_equivalences

added theorem CategoryTheory.Localization.equivalence_counitIso_app

Modified Mathlib/CategoryTheory/MorphismProperty.lean

added def CategoryTheory.MorphismProperty.isoClosure

added theorem CategoryTheory.MorphismProperty.isoClosure_respectsIso

added theorem CategoryTheory.MorphismProperty.subset_isoClosure