GammaCompN

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

Statistics

Metric	Count
Definitions N₁Γ₀, N₂Γ₂, N₂Γ₂ToKaroubiIso, Γ₀'CompNondegComplexFunctor, Γ₀NondegComplexIso	5
Theorems N₁Γ₀_app, N₁Γ₀_hom_app, N₁Γ₀_hom_app_f_f, N₁Γ₀_inv_app, N₁Γ₀_inv_app_f_f, N₂Γ₂ToKaroubiIso_hom_app, N₂Γ₂ToKaroubiIso_inv_app, N₂Γ₂_compatible_with_N₁Γ₀, N₂Γ₂_inv_app_f_f, whiskerLeft_toKaroubi_N₂Γ₂_hom, Γ₀NondegComplexIso_hom_f, Γ₀NondegComplexIso_inv_f	12
Total	17

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
N₁Γ₀ 📖	CompOp	10 math math: N₁Γ₀_hom_app_f_f, N₂Γ₂_compatible_with_N₁Γ₀, whiskerLeft_toKaroubi_N₂Γ₂_hom, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, N₁Γ₀_hom_app, N₁Γ₀_inv_app, CategoryTheory.Idempotents.DoldKan.hη, N₁Γ₀_inv_app_f_f, N₁Γ₀_app, CategoryTheory.Idempotents.DoldKan.η_hom_app_f
N₂Γ₂ 📖	CompOp	6 math math: identity_N₂, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, N₂Γ₂_inv_app_f_f, N₂Γ₂_compatible_with_N₁Γ₀, whiskerLeft_toKaroubi_N₂Γ₂_hom, identity_N₂_objectwise
N₂Γ₂ToKaroubiIso 📖	CompOp	4 math math: N₂Γ₂ToKaroubiIso_inv_app, N₂Γ₂ToKaroubiIso_hom_app, N₂Γ₂_compatible_with_N₁Γ₀, whiskerLeft_toKaroubi_N₂Γ₂_hom
Γ₀'CompNondegComplexFunctor 📖	CompOp	—
Γ₀NondegComplexIso 📖	CompOp	5 math math: Γ₀NondegComplexIso_inv_f, Γ₀NondegComplexIso_hom_f, N₁Γ₀_hom_app, N₁Γ₀_inv_app, N₁Γ₀_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
N₁Γ₀_app 📖	mathematical	—	CategoryTheory.Iso.app 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 CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₀ N₁ CategoryTheory.Idempotents.toKaroubi N₁Γ₀ CategoryTheory.Iso.trans CategoryTheory.Functor.obj Γ₀.obj SimplicialObject.Splitting.nondegComplex Γ₀.splitting CategoryTheory.Iso.symm SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ CategoryTheory.Functor.mapIso Γ₀NondegComplexIso	—	CategoryTheory.Iso.ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.Karoubi.hom_ext HomologicalComplex.hom_ext CategoryTheory.Iso.trans_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp SimplicialObject.Splitting.PInfty_comp_πSummand_id
N₁Γ₀_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app 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 CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₀ N₁ CategoryTheory.Idempotents.toKaroubi CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category N₁Γ₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Γ₀.obj SimplicialObject.Splitting.nondegComplex Γ₀.splitting CategoryTheory.Iso.inv SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ CategoryTheory.Functor.map Γ₀NondegComplexIso	—	AddRightCancelSemigroup.toIsRightCancelAdd N₁Γ₀_app
N₁Γ₀_hom_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₀ N₁ CategoryTheory.Idempotents.toKaroubi CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category N₁Γ₀ Γ₀.obj SimplicialObject.Splitting.nondegComplex Γ₀.splitting CategoryTheory.Iso.inv SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁	—	AddRightCancelSemigroup.toIsRightCancelAdd N₁Γ₀_hom_app CategoryTheory.Category.comp_id
N₁Γ₀_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app 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 CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.toKaroubi CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₀ N₁ CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category N₁Γ₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplicialObject.Splitting.nondegComplex Γ₀.obj Γ₀.splitting CategoryTheory.Functor.map Γ₀NondegComplexIso CategoryTheory.Iso.hom SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁	—	AddRightCancelSemigroup.toIsRightCancelAdd N₁Γ₀_app
N₁Γ₀_inv_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.toKaroubi CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₀ N₁ CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category N₁Γ₀ SimplicialObject.Splitting.nondegComplex Γ₀.obj Γ₀.splitting CategoryTheory.Iso.hom SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁	—	AddRightCancelSemigroup.toIsRightCancelAdd N₁Γ₀_inv_app CategoryTheory.Category.id_comp
N₂Γ₂ToKaroubiIso_hom_app 📖	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.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.Idempotents.toKaroubi CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₂ N₂ Γ₀ N₁ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category N₂Γ₂ToKaroubiIso PInfty CategoryTheory.Idempotents.Karoubi.X	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id CategoryTheory.Category.assoc PInfty_f_idem SimplicialObject.Splitting.hom_ext' SimplicialObject.Splitting.ι_desc_assoc CategoryTheory.Category.id_comp
N₂Γ₂ToKaroubiIso_inv_app 📖	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.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₀ N₁ CategoryTheory.Idempotents.toKaroubi Γ₂ N₂ CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category N₂Γ₂ToKaroubiIso PInfty	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id PInfty_f_idem_assoc SimplicialObject.Splitting.hom_ext' SimplicialObject.Splitting.ι_desc CategoryTheory.Category.id_comp
N₂Γ₂_compatible_with_N₁Γ₀ 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Idempotents.Karoubi 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.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₂ N₂ CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category N₂Γ₂ CategoryTheory.Functor.obj CategoryTheory.Idempotents.toKaroubi CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Γ₀ N₁ N₂Γ₂ToKaroubiIso N₁Γ₀	—	CategoryTheory.congr_app AddRightCancelSemigroup.toIsRightCancelAdd whiskerLeft_toKaroubi_N₂Γ₂_hom
N₂Γ₂_inv_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₂ N₂ CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category N₂Γ₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet Opposite.op SimplexCategory CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.summand SimplicialObject.Splitting.N Γ₀.obj Γ₀.splitting SimplicialObject.Splitting.cofan CategoryTheory.Idempotents.Karoubi.p SimplicialObject.Splitting.IndexSet.id	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app CategoryTheory.Idempotents.instIsIdempotentCompleteKaroubi N₂Γ₂ToKaroubiIso_inv_app N₁Γ₀_inv_app_f_f PInfty_on_Γ₀_splitting_summand_eq_self PInfty_on_Γ₀_splitting_summand_eq_self_assoc SimplicialObject.Splitting.ι_desc CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc
whiskerLeft_toKaroubi_N₂Γ₂_hom 📖	mathematical	—	CategoryTheory.Functor.whiskerLeft 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 CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.toKaroubi CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₂ N₂ CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category N₂Γ₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Γ₀ N₁ N₂Γ₂ToKaroubiIso N₁Γ₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi CategoryTheory.Idempotents.instIsIdempotentCompleteKaroubi CategoryTheory.Functor.map_preimage
Γ₀NondegComplexIso_hom_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne SimplicialObject.Splitting.nondegComplex Γ₀.obj Γ₀.splitting CategoryTheory.Iso.hom ChainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd Γ₀NondegComplexIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₀NondegComplexIso_inv_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne SimplicialObject.Splitting.nondegComplex Γ₀.obj Γ₀.splitting CategoryTheory.Iso.inv ChainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd Γ₀NondegComplexIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N	—	AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index