EquivalencePseudoabelian

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

Statistics

Metric	Count
Definitions N, equivalence, isoN₁, isoΓ₀, Γ, ε, η	7
Theorems N_map, N_obj, N₂_map_isoΓ₀_hom_app_f, equivalence_counitIso, equivalence_functor, equivalence_inverse, equivalence_unitIso, hε, hη, isoN₁_hom_app_f, Γ_map_app, Γ_obj_map, Γ_obj_obj, η_hom_app_f, η_inv_app_f	15
Total	22

CategoryTheory.Idempotents.DoldKan

Definitions

Name	Category	Theorems
N 📖	CompOp	7 math math: N_obj, η_inv_app_f, equivalence_functor, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, N_map, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, η_hom_app_f
equivalence 📖	CompOp	4 math math: equivalence_counitIso, equivalence_inverse, equivalence_functor, equivalence_unitIso
isoN₁ 📖	CompOp	3 math math: hε, isoN₁_hom_app_f, hη
isoΓ₀ 📖	CompOp	2 math math: N₂_map_isoΓ₀_hom_app_f, hη
Γ 📖	CompOp	8 math math: N₂_map_isoΓ₀_hom_app_f, equivalence_inverse, η_inv_app_f, Γ_obj_map, Γ_obj_obj, Γ_map_app, hη, η_hom_app_f
ε 📖	CompOp	1 math math: equivalence_unitIso
η 📖	CompOp	3 math math: equivalence_counitIso, η_inv_app_f, η_hom_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
N_map 📖	mathematical	—	CategoryTheory.Functor.map 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 N CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Equivalence.inverse CategoryTheory.Idempotents.toKaroubiEquivalence CategoryTheory.Functor.obj AlgebraicTopology.DoldKan.N₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
N_obj 📖	mathematical	—	CategoryTheory.Functor.obj 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 N CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Equivalence.inverse CategoryTheory.Idempotents.toKaroubiEquivalence AlgebraicTopology.DoldKan.N₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
N₂_map_isoΓ₀_hom_app_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f 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.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi.instCategory AlgebraicTopology.DoldKan.N₂ CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Idempotents.toKaroubiEquivalence CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex CategoryTheory.Equivalence.inverse CategoryTheory.Preadditive.DoldKan.equivalence Γ CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category isoΓ₀ AlgebraicTopology.DoldKan.PInfty CategoryTheory.Idempotents.Karoubi.X	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject CategoryTheory.Category.comp_id AlgebraicTopology.DoldKan.PInfty_idem
equivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.SimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.instCategorySimplicialObject HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd equivalence η	—	AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_eq AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject hη
equivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.SimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 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
equivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.SimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.instCategorySimplicialObject HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd equivalence ε	—	AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_eq AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject hε
hε 📖	mathematical	—	AlgebraicTopology.DoldKan.Compatibility.υ CategoryTheory.SimplicialObject CategoryTheory.Idempotents.Karoubi 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 CategoryTheory.Idempotents.toKaroubiEquivalence CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject CategoryTheory.Preadditive.DoldKan.equivalence AlgebraicTopology.DoldKan.N₁ isoN₁ AlgebraicTopology.DoldKan.Γ₂N₁	—	CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Iso.ext CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id CategoryTheory.NatTrans.ext' CategoryTheory.NatTrans.comp_app AlgebraicTopology.DoldKan.Γ₂N₁_inv AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans AlgebraicTopology.DoldKan.Compatibility.υ_hom_app CategoryTheory.Preadditive.DoldKan.equivalence_unitIso CategoryTheory.Iso.app_inv CategoryTheory.Category.assoc CategoryTheory.NatTrans.comp_app_assoc AlgebraicTopology.DoldKan.Γ₂N₂_inv CategoryTheory.NatTrans.id_app CategoryTheory.Category.id_comp AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app CategoryTheory.Functor.map_comp CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Functor.map_id
hη 📖	mathematical	—	AlgebraicTopology.DoldKan.Compatibility.τ₀ 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 CategoryTheory.Idempotents.toKaroubiEquivalence CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex CategoryTheory.Preadditive.DoldKan.equivalence AlgebraicTopology.DoldKan.Compatibility.τ₁ CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject AlgebraicTopology.DoldKan.N₁ isoN₁ Γ isoΓ₀ AlgebraicTopology.DoldKan.N₁Γ₀	—	CategoryTheory.Iso.ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject CategoryTheory.NatTrans.ext' AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app AlgebraicTopology.DoldKan.Compatibility.τ₁_hom_app AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀ AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app N₂_map_isoΓ₀_hom_app_f AlgebraicTopology.DoldKan.PInfty_idem_assoc
isoN₁_hom_app_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f 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.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Idempotents.toKaroubiEquivalence CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject CategoryTheory.Preadditive.DoldKan.equivalence AlgebraicTopology.DoldKan.N₁ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category isoN₁ AlgebraicTopology.DoldKan.PInfty CategoryTheory.Idempotents.Karoubi.X	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject
Γ_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj SimplicialObject.Split SimplicialObject.instCategorySplit CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject SimplicialObject.Split.forget ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AlgebraicTopology.DoldKan.Γ₀' CategoryTheory.Functor.map AddRightCancelSemigroup.toIsRightCancelAdd Γ SimplicialObject.Splitting.desc AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi HomologicalComplex.X HomologicalComplex.Hom.f SimplicialObject.Splitting.IndexSet SimplicialObject.Splitting.summand SimplicialObject.Splitting.cofan	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj 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.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ AlgebraicTopology.DoldKan.Γ₀.Obj.map	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory 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.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂	—	AddRightCancelSemigroup.toIsRightCancelAdd
η_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory AlgebraicTopology.DoldKan.N₁ CategoryTheory.Equivalence.inverse CategoryTheory.Idempotents.toKaroubiEquivalence CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category N η CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Equivalence.functor CategoryTheory.Functor.map AlgebraicTopology.DoldKan.N₁Γ₀ CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.id_comp
η_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory AlgebraicTopology.DoldKan.N₁ CategoryTheory.Equivalence.inverse CategoryTheory.Idempotents.toKaroubiEquivalence CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category N η CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map AlgebraicTopology.DoldKan.N₁Γ₀	—	CategoryTheory.Category.comp_id

---

← Back to Index