Quotient

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

Statistics

Metric	Count
Definitions HasQuotient, quotient	2
Theorems iff, iff_of_eqvGen, eq_inverseImage_quotientFunctor, quotient_iff	4
Total	6

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
HasQuotient 📖	CompData	2 math math: HomotopicalAlgebra.FibrantObject.instHasQuotientWeakEquivalencesHomRel, HomotopicalAlgebra.CofibrantObject.instHasQuotientWeakEquivalencesHomRel
quotient 📖	CompOp	2 math math: eq_inverseImage_quotientFunctor, quotient_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_inverseImage_quotientFunctor 📖	mathematical	—	inverseImage CategoryTheory.Quotient CategoryTheory.Quotient.category quotient CategoryTheory.Quotient.functor	—	ext quotient_iff
quotient_iff 📖	mathematical	—	quotient CategoryTheory.Functor.obj CategoryTheory.Quotient CategoryTheory.Quotient.category CategoryTheory.Quotient.functor CategoryTheory.Functor.map	—	HasQuotient.iff_of_eqvGen CategoryTheory.HomRel.compClosure_eq_self CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen CategoryTheory.Functor.homRel_iff

CategoryTheory.MorphismProperty.HasQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff 📖	—	—	—	—	—
iff_of_eqvGen 📖	—	Relation.EqvGen Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—	iff

---

← Back to Index