FunctorN

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

Statistics

Metric	Count
Definitions N₁, N₂, toKaroubiCompN₂IsoN₁	3
Theorems N₁_map_f, N₁_obj_X, N₁_obj_p, N₂_map_f_f, N₂_obj_X_X, N₂_obj_X_d, N₂_obj_p_f, toKaroubiCompN₂IsoN₁_hom_app, toKaroubiCompN₂IsoN₁_inv_app	9
Total	12

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
N₁ 📖	CompOp	38 math math: N₁_map_f, N₂Γ₂ToKaroubiIso_inv_app, instIsIsoFunctorSimplicialObjectKaroubiNatTrans, N₁_obj_p, CategoryTheory.Idempotents.DoldKan.hε, compatibility_Γ₂N₁_Γ₂N₂_natTrans, N₁Γ₀_hom_app_f_f, Γ₂N₂ToKaroubiIso_hom_app, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, N₂Γ₂ToKaroubiIso_hom_app, compatibility_N₂_N₁_karoubi, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, N₂Γ₂_compatible_with_N₁Γ₀, whiskerLeft_toKaroubi_N₂Γ₂_hom, CategoryTheory.Idempotents.DoldKan.N_obj, toKaroubiCompN₂IsoN₁_hom_app, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, toKaroubiCompN₂IsoN₁_inv_app, N₁_obj_X, Γ₂N₂ToKaroubiIso_inv_app, instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, N₂_obj_p_f, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, N₁Γ₀_hom_app, Γ₂N₁.natTrans_app_f_app, N₁Γ₀_inv_app, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, Γ₂N₁_inv, CategoryTheory.Idempotents.DoldKan.hη, N₁Γ₀_inv_app_f_f, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, N₂_map_f_f, N₁Γ₀_app, CategoryTheory.Idempotents.DoldKan.N_map, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, Γ₂N₂.natTrans_app_f_app
N₂ 📖	CompOp	22 math math: N₂Γ₂ToKaroubiIso_inv_app, identity_N₂, instIsIsoFunctorKaroubiSimplicialObjectNatTrans, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, compatibility_Γ₂N₁_Γ₂N₂_natTrans, Γ₂N₂ToKaroubiIso_hom_app, N₂Γ₂_inv_app_f_f, N₂Γ₂ToKaroubiIso_hom_app, compatibility_N₂_N₁_karoubi, N₂Γ₂_compatible_with_N₁Γ₀, whiskerLeft_toKaroubi_N₂Γ₂_hom, toKaroubiCompN₂IsoN₁_hom_app, toKaroubiCompN₂IsoN₁_inv_app, Γ₂N₂ToKaroubiIso_inv_app, N₂_obj_p_f, N₂_obj_X_X, N₂_obj_X_d, instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, identity_N₂_objectwise, N₂_map_f_f, Γ₂N₂_inv, Γ₂N₂.natTrans_app_f_app
toKaroubiCompN₂IsoN₁ 📖	CompOp	4 math math: Γ₂N₂ToKaroubiIso_hom_app, toKaroubiCompN₂IsoN₁_hom_app, toKaroubiCompN₂IsoN₁_inv_app, Γ₂N₂ToKaroubiIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
N₁_map_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 AlgebraicTopology.AlternatingFaceMapComplex.obj PInfty PInfty_idem CategoryTheory.Functor.map CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.Karoubi.instCategory N₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.X AlgebraicTopology.AlternatingFaceMapComplex.map	—	PInfty_idem AddRightCancelSemigroup.toIsRightCancelAdd
N₁_obj_X 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.X ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.Karoubi.instCategory N₁ AlgebraicTopology.AlternatingFaceMapComplex.obj	—	AddRightCancelSemigroup.toIsRightCancelAdd
N₁_obj_p 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.p ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.Karoubi.instCategory N₁ PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd
N₂_map_f_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.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory N₁ CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi.p AddRightCancelSemigroup.toIsRightCancelAdd N₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op AlgebraicTopology.AlternatingFaceMapComplex.obj PInfty CategoryTheory.NatTrans.app	—	PInfty_idem AddRightCancelSemigroup.toIsRightCancelAdd
N₂_obj_X_X 📖	mathematical	—	HomologicalComplex.X 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.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi.instCategory N₂ Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op	—	AddRightCancelSemigroup.toIsRightCancelAdd
N₂_obj_X_d 📖	mathematical	—	HomologicalComplex.d 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.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi.instCategory N₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.CategoryStruct.comp CategoryTheory.eqToHom Finset.sum AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Finset.univ Fin.fintype SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid CategoryTheory.SimplicialObject.δ CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
N₂_obj_p_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.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory N₁ CategoryTheory.Idempotents.Karoubi.p AddRightCancelSemigroup.toIsRightCancelAdd N₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op AlgebraicTopology.AlternatingFaceMapComplex.obj PInfty CategoryTheory.NatTrans.app	—	PInfty_idem AddRightCancelSemigroup.toIsRightCancelAdd
toKaroubiCompN₂IsoN₁_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.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.Idempotents.toKaroubi N₂ N₁ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category toKaroubiCompN₂IsoN₁ PInfty CategoryTheory.Idempotents.Karoubi.X	—	AddRightCancelSemigroup.toIsRightCancelAdd
toKaroubiCompN₂IsoN₁_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.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory N₁ CategoryTheory.Functor.comp CategoryTheory.Idempotents.toKaroubi N₂ CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category toKaroubiCompN₂IsoN₁ PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index