Quotient

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

Statistics

Metric	Count
Definitions FactorsThroughLocalization, strictUniversalPropertyFixedTarget, strictUniversalPropertyFixedTarget'	3
Theorems isLocalizedEquivalence	1
Total	4

HomRel

Definitions

Name	Category	Theorems
FactorsThroughLocalization 📖	MathDef	4 math math: HomotopicalAlgebra.LeftHomotopyRel.factorsThroughLocalization, HomotopicalAlgebra.RightHomotopyRel.factorsThroughLocalization, HomotopicalAlgebra.CofibrantObject.factorsThroughLocalization, HomotopicalAlgebra.FibrantObject.factorsThroughLocalization

HomRel.FactorsThroughLocalization

Definitions

Name	Category	Theorems
strictUniversalPropertyFixedTarget 📖	CompOp	—
strictUniversalPropertyFixedTarget' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalizedEquivalence 📖	mathematical	HomRel.FactorsThroughLocalization CategoryTheory.MorphismProperty.inverseImage CategoryTheory.Quotient CategoryTheory.Quotient.category CategoryTheory.Quotient.functor	CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence CategoryTheory.LocalizerMorphism.ofEq	—	CategoryTheory.Functor.IsLocalization.mk' CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization CategoryTheory.Functor.q_isLocalization

---

← Back to Index