Equivalence

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

Statistics

Metric	Count
Definitions equivalence	1
Theorems of_equivalence_source, of_equivalences, equivalence_counitIso_app, isEquivalence	4
Total	5

CategoryTheory.Functor.IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_equivalence_source 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isoClosure CategoryTheory.Equivalence.functor CategoryTheory.MorphismProperty.IsInvertedBy	CategoryTheory.Functor.IsLocalization	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms CategoryTheory.Localization.inverts CategoryTheory.Functor.q_isLocalization CategoryTheory.Localization.isEquivalence
of_equivalences 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isoClosure CategoryTheory.Equivalence.functor CategoryTheory.MorphismProperty.IsInvertedBy	CategoryTheory.Functor.IsLocalization	—	of_equivalence_source of_equivalence_target

CategoryTheory.Localization

Definitions

Name	Category	Theorems
equivalence 📖	CompOp	1 math math: equivalence_counitIso_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalence_counitIso_app 📖	mathematical	—	CategoryTheory.Iso.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse equivalence CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.obj CategoryTheory.Iso.trans Lifting.iso Lifting.compRight	—	CategoryTheory.Iso.ext liftNatTrans_app CategoryTheory.Category.comp_id
isEquivalence 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence	—	CategoryTheory.Equivalence.isEquivalence_functor

---

← Back to Index