Commit 2023-09-05 14:01 a88ee8c5

View on Github →

feat(CategoryTheory): morphisms of localizers (#6869) This PR introduces the categorical notion of morphisms of localizers.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

added theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'

added theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization

added def CategoryTheory.LocalizerMorphism.comp

added def CategoryTheory.LocalizerMorphism.id

added theorem CategoryTheory.LocalizerMorphism.inverts

added theorem CategoryTheory.LocalizerMorphism.nonempty_isEquivalence_iff

added structure CategoryTheory.LocalizerMorphism

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

Modified docs/references.bib