Compatibility

📁 Source: Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean

Statistics

Metric	Count
Definitions equivalence, equivalenceCounitIso, equivalenceUnitIso, equivalence₀, equivalence₁, equivalence₁CounitIso, equivalence₁UnitIso, equivalence₂, equivalence₂CounitIso, equivalence₂UnitIso, τ₀, τ₁, υ	13
Theorems equivalenceCounitIso_eq, equivalenceCounitIso_hom_app, equivalenceCounitIso_inv_app, equivalenceUnitIso_eq, equivalenceUnitIso_hom_app, equivalenceUnitIso_inv_app, equivalence_functor, equivalence_inverse, equivalence₀_functor, equivalence₀_inverse, equivalence₀_unitIso_hom_app, equivalence₁CounitIso_eq, equivalence₁CounitIso_hom_app, equivalence₁CounitIso_inv_app, equivalence₁UnitIso_eq, equivalence₁UnitIso_hom_app, equivalence₁UnitIso_inv_app, equivalence₁_functor, equivalence₁_inverse, equivalence₂CounitIso_eq, equivalence₂CounitIso_hom_app, equivalence₂CounitIso_inv_app, equivalence₂UnitIso_eq, equivalence₂UnitIso_hom_app, equivalence₂UnitIso_inv_app, equivalence₂_functor, equivalence₂_inverse, τ₀_hom_app, τ₁_hom_app, υ_hom_app, υ_inv_app	31
Total	44

AlgebraicTopology.DoldKan.Compatibility

Definitions

Name	Category	Theorems
equivalence 📖	CompOp	4 math math: equivalenceCounitIso_eq, equivalence_functor, equivalenceUnitIso_eq, equivalence_inverse
equivalenceCounitIso 📖	CompOp	3 math math: equivalenceCounitIso_eq, equivalenceCounitIso_inv_app, equivalenceCounitIso_hom_app
equivalenceUnitIso 📖	CompOp	3 math math: equivalenceUnitIso_inv_app, equivalenceUnitIso_eq, equivalenceUnitIso_hom_app
equivalence₀ 📖	CompOp	3 math math: equivalence₀_unitIso_hom_app, equivalence₀_inverse, equivalence₀_functor
equivalence₁ 📖	CompOp	4 math math: equivalence₁UnitIso_eq, equivalence₁_functor, equivalence₁CounitIso_eq, equivalence₁_inverse
equivalence₁CounitIso 📖	CompOp	3 math math: equivalence₁CounitIso_hom_app, equivalence₁CounitIso_inv_app, equivalence₁CounitIso_eq
equivalence₁UnitIso 📖	CompOp	3 math math: equivalence₁UnitIso_eq, equivalence₁UnitIso_hom_app, equivalence₁UnitIso_inv_app
equivalence₂ 📖	CompOp	4 math math: equivalence₂CounitIso_eq, equivalence₂UnitIso_eq, equivalence₂_functor, equivalence₂_inverse
equivalence₂CounitIso 📖	CompOp	3 math math: equivalence₂CounitIso_inv_app, equivalence₂CounitIso_hom_app, equivalence₂CounitIso_eq
equivalence₂UnitIso 📖	CompOp	3 math math: equivalence₂UnitIso_inv_app, equivalence₂UnitIso_eq, equivalence₂UnitIso_hom_app
τ₀ 📖	CompOp	2 math math: τ₀_hom_app, CategoryTheory.Idempotents.DoldKan.hη
τ₁ 📖	CompOp	2 math math: τ₁_hom_app, CategoryTheory.Idempotents.DoldKan.hη
υ 📖	CompOp	3 math math: CategoryTheory.Idempotents.DoldKan.hε, υ_hom_app, υ_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalenceCounitIso_eq 📖	mathematical	τ₀ τ₁	CategoryTheory.Equivalence.counitIso equivalence equivalenceCounitIso	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp equivalence₂CounitIso_eq equivalence₂CounitIso_hom_app CategoryTheory.Category.assoc equivalenceCounitIso_hom_app τ₁_hom_app CategoryTheory.Functor.map_comp_assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Equivalence.fun_inv_map CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Equivalence.functor_unit_comp CategoryTheory.Functor.map_id
equivalenceCounitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category equivalenceCounitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.id_comp
equivalenceCounitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category equivalenceCounitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id
equivalenceUnitIso_eq 📖	mathematical	υ	CategoryTheory.Equivalence.unitIso equivalence equivalenceUnitIso	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext equivalence₂UnitIso_eq equivalence₂UnitIso_hom_app CategoryTheory.Functor.map_comp_assoc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc equivalenceUnitIso_hom_app υ_hom_app
equivalenceUnitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category equivalenceUnitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Functor.map_id
equivalenceUnitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category equivalenceUnitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
equivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor equivalence CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse	—	—
equivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse equivalence	—	—
equivalence₀_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor equivalence₀ CategoryTheory.Functor.comp	—	—
equivalence₀_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse equivalence₀ CategoryTheory.Functor.comp	—	—
equivalence₀_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso equivalence₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
equivalence₁CounitIso_eq 📖	mathematical	—	CategoryTheory.Equivalence.counitIso equivalence₁ equivalence₁CounitIso	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' CategoryTheory.Functor.isoWhiskerRight_trans CategoryTheory.Iso.trans_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp equivalence₁CounitIso_hom_app
equivalence₁CounitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category equivalence₁CounitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Iso.inv CategoryTheory.Functor.map CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
equivalence₁CounitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category equivalence₁CounitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	CategoryTheory.Category.id_comp
equivalence₁UnitIso_eq 📖	mathematical	—	CategoryTheory.Equivalence.unitIso equivalence₁ equivalence₁UnitIso	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' equivalence₀_unitIso_hom_app CategoryTheory.Category.assoc equivalence₁UnitIso_hom_app
equivalence₁UnitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category equivalence₁UnitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
equivalence₁UnitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category equivalence₁UnitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.id_comp
equivalence₁_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor equivalence₁	—	—
equivalence₁_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse equivalence₁ CategoryTheory.Functor.comp	—	—
equivalence₂CounitIso_eq 📖	mathematical	—	CategoryTheory.Equivalence.counitIso equivalence₂ equivalence₂CounitIso	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' equivalence₁CounitIso_eq CategoryTheory.Functor.isoWhiskerRight_trans CategoryTheory.Iso.trans_assoc CategoryTheory.Functor.map_id equivalence₁CounitIso_hom_app CategoryTheory.Functor.map_comp CategoryTheory.Category.id_comp CategoryTheory.Category.assoc equivalence₂CounitIso_hom_app
equivalence₂CounitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category equivalence₂CounitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.comp_id equivalence₁CounitIso_hom_app CategoryTheory.Functor.map_comp CategoryTheory.Category.id_comp CategoryTheory.Category.assoc
equivalence₂CounitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category equivalence₂CounitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map CategoryTheory.Equivalence.counitIso	—	equivalence₁CounitIso_inv_app CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
equivalence₂UnitIso_eq 📖	mathematical	—	CategoryTheory.Equivalence.unitIso equivalence₂ equivalence₂UnitIso	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' CategoryTheory.Functor.isoWhiskerRight_trans CategoryTheory.Iso.trans_assoc equivalence₀_unitIso_hom_app CategoryTheory.Category.assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp equivalence₂UnitIso_hom_app
equivalence₂UnitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category equivalence₂UnitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso	—	equivalence₁UnitIso_hom_app CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Functor.map_id
equivalence₂UnitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category equivalence₂UnitIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Functor.map_id equivalence₁UnitIso_inv_app CategoryTheory.Category.id_comp
equivalence₂_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor equivalence₂ CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse	—	—
equivalence₂_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse equivalence₂ CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor	—	—
τ₀_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category τ₀ CategoryTheory.Functor.id CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.obj	—	CategoryTheory.Category.comp_id
τ₁_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category τ₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
υ_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Equivalence.functor CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category υ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
υ_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category υ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

---

← Back to Index