Documentation Verification Report

EquivalenceAdditive

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

Statistics

Metric	Count
Definitions `N`, `equivalence`, `Γ`	3
Theorems `equivalence_counitIso`, `equivalence_functor`, `equivalence_inverse`, `equivalence_unitIso`	4
Total	7

CategoryTheory.Preadditive.DoldKan

Definitions

Name	Category	Theorems
`N` 📖	CompOp	1 math math: `equivalence_functor`
`equivalence` 📖	CompOp	8 math math: `equivalence_unitIso`, `equivalence_functor`, `equivalence_counitIso`, `CategoryTheory.Idempotents.DoldKan.hε`, `CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f`, `equivalence_inverse`, `CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f`, `CategoryTheory.Idempotents.DoldKan.hη`
`Γ` 📖	CompOp	1 math math: `equivalence_inverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `CategoryTheory.Idempotents.Karoubi` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Idempotents.Karoubi.instCategory` `equivalence` `AlgebraicTopology.DoldKan.N₂Γ₂`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`equivalence_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.Idempotents.Karoubi` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Idempotents.Karoubi.instCategory` `equivalence` `N`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`equivalence_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CategoryTheory.Idempotents.Karoubi` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Idempotents.Karoubi.instCategory` `equivalence` `Γ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`equivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `CategoryTheory.Idempotents.Karoubi` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Idempotents.Karoubi.instCategory` `equivalence` `AlgebraicTopology.DoldKan.Γ₂N₂`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

---

← Back to Index