Equivalence

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

Statistics

Metric	Count
Definitions N, comparisonN, equivalence, Γ	4
Theorems comparisonN_hom_app_f, comparisonN_inv_app_f, equivalence_functor, equivalence_inverse	4
Total	8

CategoryTheory.Abelian.DoldKan

Definitions

Name	Category	Theorems
N 📖	CompOp	3 math math: equivalence_functor, comparisonN_hom_app_f, comparisonN_inv_app_f
comparisonN 📖	CompOp	2 math math: comparisonN_hom_app_f, comparisonN_inv_app_f
equivalence 📖	CompOp	2 math math: equivalence_inverse, equivalence_functor
Γ 📖	CompOp	1 math math: equivalence_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comparisonN_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex HomologicalComplex.instCategory N CategoryTheory.Idempotents.DoldKan.N CategoryTheory.Idempotents.isIdempotentComplete_of_abelian CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits comparisonN CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Equivalence.inverse CategoryTheory.Idempotents.toKaroubiEquivalence CategoryTheory.Equivalence.functor AlgebraicTopology.DoldKan.N₁ CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map CategoryTheory.Idempotents.toKaroubi AlgebraicTopology.NormalizedMooreComplex.obj AlgebraicTopology.normalizedMooreComplex CategoryTheory.Iso.inv AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi	—	CategoryTheory.Idempotents.isIdempotentComplete_of_abelian CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
comparisonN_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex HomologicalComplex.instCategory CategoryTheory.Idempotents.DoldKan.N CategoryTheory.Idempotents.isIdempotentComplete_of_abelian N CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits comparisonN CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Equivalence.inverse CategoryTheory.Idempotents.toKaroubiEquivalence AlgebraicTopology.DoldKan.N₁ CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Idempotents.toKaroubi AlgebraicTopology.NormalizedMooreComplex.obj CategoryTheory.Functor.comp AlgebraicTopology.normalizedMooreComplex CategoryTheory.Iso.hom AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi CategoryTheory.Functor.id CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Idempotents.isIdempotentComplete_of_abelian CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
equivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.SimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.instCategorySimplicialObject HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd equivalence N	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.SimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.instCategorySimplicialObject HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd equivalence Γ	—	AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index