Adjunction

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

Statistics

Metric	Count
Definitions ε, η, localization	3
Theorems ε_app, η_app, isLocalization, isLocalization', localization_counit_app, localization_unit_app	6
Total	9

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
localization 📖	CompOp	2 math math: localization_unit_app, localization_counit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.Localization.inverts CategoryTheory.Functor.q_isLocalization instIsIsoMapAppUnitOfFaithfulOfFull CategoryTheory.NatIso.isIso_of_isIso_app counit_isIso_of_R_fully_faithful CategoryTheory.Functor.IsLocalization.of_equivalence_target
isLocalization' 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.Functor.IsLocalization.op_iff CategoryTheory.MorphismProperty.op_inverseImage CategoryTheory.MorphismProperty.op_isomorphisms isLocalization CategoryTheory.Functor.instFullOppositeOp CategoryTheory.Functor.instFaithfulOppositeOp
localization_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit localization CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CatCommSq.iso	—	Localization.η_app
localization_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit localization CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CatCommSq.iso	—	Localization.ε_app

CategoryTheory.Adjunction.Localization

Definitions

Name	Category	Theorems
ε 📖	CompOp	1 math math: ε_app
η 📖	CompOp	1 math math: η_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ε_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp ε CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Adjunction.unit CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CatCommSq.iso	—	CategoryTheory.Localization.liftNatTrans_app CategoryTheory.CatCommSq.hComp_iso_hom_app CategoryTheory.Category.id_comp
η_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id η CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CatCommSq.iso CategoryTheory.Adjunction.counit	—	CategoryTheory.Localization.liftNatTrans_app CategoryTheory.CatCommSq.hComp_iso_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.assoc

---

← Back to Index