Composition

📁 Source: Mathlib/CategoryTheory/Localization/Composition.lean

Statistics

Metric	Count
Definitions comp	1
Theorems comp, of_comp	2
Total	3

CategoryTheory.Functor.IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.Functor.comp CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.map	CategoryTheory.Functor.IsLocalization	—	CategoryTheory.Functor.q_isLocalization CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence CategoryTheory.MorphismProperty.isoClosure_respectsIso CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.MorphismProperty.map_isoClosure CategoryTheory.MorphismProperty.le_isoClosure CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence le_refl CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.faithful_inverse CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso LE.le.trans CategoryTheory.MorphismProperty.monotone_map CategoryTheory.MorphismProperty.map_map le_of_eq CategoryTheory.MorphismProperty.map_eq_of_iso mk' of_equivalence_target
of_comp 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.map	CategoryTheory.Functor.IsLocalization	—	comp CategoryTheory.Functor.q_isLocalization CategoryTheory.Localization.inverts CategoryTheory.MorphismProperty.map_mem_map le_refl of_equivalence_target

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget

Definitions

Name	Category	Theorems
comp 📖	CompOp	—

---

← Back to Index