NCompGamma

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

Statistics

Metric	Count
Definitions Γ₂N₁, natTrans, Γ₂N₂, natTrans, Γ₂N₂ToKaroubiIso	5
Theorems PInfty_comp_map_mono_eq_zero, compatibility_Γ₂N₁_Γ₂N₂_natTrans, identity_N₂, identity_N₂_objectwise, instIsIsoFunctorKaroubiSimplicialObjectNatTrans, instIsIsoFunctorSimplicialObjectKaroubiNatTrans, Γ₀_obj_termwise_mapMono_comp_PInfty, Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, natTrans_app_f_app, Γ₂N₁_inv, natTrans_app_f_app, Γ₂N₂ToKaroubiIso_hom_app, Γ₂N₂ToKaroubiIso_inv_app, Γ₂N₂_inv	14
Total	19

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
Γ₂N₁ 📖	CompOp	2 math math: CategoryTheory.Idempotents.DoldKan.hε, Γ₂N₁_inv
Γ₂N₂ 📖	CompOp	2 math math: CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, Γ₂N₂_inv
Γ₂N₂ToKaroubiIso 📖	CompOp	4 math math: compatibility_Γ₂N₁_Γ₂N₂_natTrans, Γ₂N₂ToKaroubiIso_hom_app, Γ₂N₂ToKaroubiIso_inv_app, Γ₂N₂.natTrans_app_f_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
PInfty_comp_map_mono_eq_zero 📖	mathematical	Isδ₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op HomologicalComplex.Hom.f PInfty CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd SimplexCategory.len_lt_of_mono SimplexCategory.eq_δ_of_mono SimplexCategory.instMonoδ Isδ₀.iff HigherFacesVanish.comp_δ_eq_zero HigherFacesVanish.of_P SimplexCategory.eq_comp_δ_of_not_surjective SimplexCategory.epi_iff_surjective CategoryTheory.Category.assoc Fin.le_iff_val_le_val SimplexCategory.δ_comp_δ'' CategoryTheory.Functor.map_comp HigherFacesVanish.comp_δ_eq_zero_assoc CategoryTheory.Limits.zero_comp
compatibility_Γ₂N₁_Γ₂N₂_natTrans 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp 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.toKaroubi Γ₂N₁.natTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj N₂ CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Iso.app Γ₂N₂ToKaroubiIso Γ₂N₂.natTrans	—	AddRightCancelSemigroup.toIsRightCancelAdd Γ₂N₂.natTrans_app_f_app CategoryTheory.Functor.map_id CategoryTheory.Iso.app_inv CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_app_assoc
identity_N₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Idempotents.Karoubi CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi.instCategory 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.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp N₂ CategoryTheory.Functor.id Γ₂ CategoryTheory.NatTrans.hcomp CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv N₂Γ₂ CategoryTheory.Functor.associator Γ₂N₂.natTrans	—	CategoryTheory.NatTrans.ext' AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp identity_N₂_objectwise
identity_N₂_objectwise 📖	mathematical	—	CategoryTheory.CategoryStruct.comp 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.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject N₂ CategoryTheory.Functor.comp Γ₂ CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category N₂Γ₂ CategoryTheory.Functor.map Γ₂N₂.natTrans CategoryTheory.CategoryStruct.id	—	CategoryTheory.Idempotents.Karoubi.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext N₂Γ₂_inv_app_f_f CategoryTheory.Category.assoc PInfty_on_Γ₀_splitting_summand_eq_self_assoc Γ₂N₂.natTrans_app_f_app Γ₂N₂ToKaroubiIso_hom_app SimplicialObject.Splitting.ι_desc_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id PInfty_f_idem_assoc PInfty_f_naturality_assoc CategoryTheory.Idempotents.app_idem
instIsIsoFunctorKaroubiSimplicialObjectNatTrans 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Idempotents.Karoubi CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp 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.Functor.id Γ₂N₂.natTrans	—	AddRightCancelSemigroup.toIsRightCancelAdd identity_N₂_objectwise CategoryTheory.NatIso.inv_app_isIso CategoryTheory.hom_comp_eq_id CategoryTheory.IsIso.inv_isIso CategoryTheory.isIso_of_reflects_iso instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂ CategoryTheory.NatIso.isIso_of_isIso_app
instIsIsoFunctorSimplicialObjectKaroubiNatTrans 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp 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.toKaroubi Γ₂N₁.natTrans	—	AddRightCancelSemigroup.toIsRightCancelAdd compatibility_Γ₂N₁_Γ₂N₂_natTrans CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.NatIso.isIso_app_of_isIso instIsIsoFunctorKaroubiSimplicialObjectNatTrans CategoryTheory.NatIso.isIso_of_isIso_app
Γ₀_obj_termwise_mapMono_comp_PInfty 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj SimplexCategory.len Γ₀.Obj.Termwise.mapMono HomologicalComplex.Hom.f PInfty CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	AddRightCancelSemigroup.toIsRightCancelAdd SimplexCategory.eq_id_of_mono Γ₀.Obj.Termwise.mapMono.congr_simp Γ₀.Obj.Termwise.mapMono_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id Γ₀.Obj.Termwise.mapMono_δ₀' HomologicalComplex.Hom.comm AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq CategoryTheory.Preadditive.comp_sum Finset.sum_eq_single CategoryTheory.Preadditive.comp_zsmul CategoryTheory.SimplicialObject.δ.eq_1 PInfty_comp_map_mono_eq_zero SimplexCategory.instMonoδ Isδ₀.iff zsmul_zero instIsEmptyFalse pow_zero one_zsmul Isδ₀.eq_δ₀ Γ₀.Obj.Termwise.mapMono_eq_zero CategoryTheory.Limits.zero_comp
Γ₀_obj_termwise_mapMono_comp_PInfty_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj SimplexCategory.len Γ₀.Obj.Termwise.mapMono HomologicalComplex.Hom.f PInfty CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Γ₀_obj_termwise_mapMono_comp_PInfty
Γ₂N₁_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.category CategoryTheory.Idempotents.toKaroubi CategoryTheory.Functor.comp 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₁ Γ₂ Γ₂N₁ Γ₂N₁.natTrans	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₂N₂ToKaroubiIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.Idempotents.toKaroubi ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup N₂ Γ₂ N₁ CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category AddRightCancelSemigroup.toIsRightCancelAdd Γ₂N₂ToKaroubiIso CategoryTheory.Functor.map CategoryTheory.Functor.obj toKaroubiCompN₂IsoN₁	—	CategoryTheory.Category.id_comp
Γ₂N₂ToKaroubiIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup N₁ Γ₂ CategoryTheory.Idempotents.toKaroubi N₂ CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category AddRightCancelSemigroup.toIsRightCancelAdd Γ₂N₂ToKaroubiIso CategoryTheory.Functor.map CategoryTheory.Functor.obj toKaroubiCompN₂IsoN₁	—	CategoryTheory.Category.comp_id
Γ₂N₂_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Idempotents.Karoubi CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp 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₂ Γ₂ Γ₂N₂ Γ₂N₂.natTrans	—	AddRightCancelSemigroup.toIsRightCancelAdd

AlgebraicTopology.DoldKan.Γ₂N₁

Definitions

Name	Category	Theorems
natTrans 📖	CompOp	5 math math: AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, natTrans_app_f_app, AlgebraicTopology.DoldKan.Γ₂N₁_inv, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natTrans_app_f_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Idempotents.Karoubi.X CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂ CategoryTheory.Idempotents.toKaroubi CategoryTheory.Idempotents.Karoubi.Hom.f AddRightCancelSemigroup.toIsRightCancelAdd natTrans SimplicialObject.Splitting.desc AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.AlternatingFaceMapComplex.obj AlgebraicTopology.DoldKan.Γ₀.splitting 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 AlgebraicTopology.DoldKan.PInfty CategoryTheory.Functor.map Opposite.op Quiver.Hom.op SimplicialObject.Splitting.IndexSet.e	—	AddRightCancelSemigroup.toIsRightCancelAdd

AlgebraicTopology.DoldKan.Γ₂N₂

Definitions

Name	Category	Theorems
natTrans 📖	CompOp	6 math math: AlgebraicTopology.DoldKan.identity_N₂, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, AlgebraicTopology.DoldKan.identity_N₂_objectwise, AlgebraicTopology.DoldKan.Γ₂N₂_inv, natTrans_app_f_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natTrans_app_f_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Idempotents.Karoubi CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂ CategoryTheory.Functor.id natTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi.X CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi.decompId_i CategoryTheory.Idempotents.toKaroubi CategoryTheory.Functor CategoryTheory.Functor.category AlgebraicTopology.DoldKan.N₁ CategoryTheory.Iso.hom AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso AlgebraicTopology.DoldKan.Γ₂N₁.natTrans CategoryTheory.Idempotents.Karoubi.decompId_p	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app CategoryTheory.Idempotents.instIsIdempotentCompleteKaroubi

---

← Back to Index