Commit 2023-09-06 15:49 c672a3ff

View on Github →

feat: composition of localization functors (#6882)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Arrow.lean

Created Mathlib/CategoryTheory/Localization/Composition.lean

added theorem CategoryTheory.Functor.IsLocalization.comp

added theorem CategoryTheory.Functor.IsLocalization.of_comp

added def CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.comp

Modified Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

added theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence