Vertex classes and the augmentation in degree zero

Vertex classes generate zeroth simplicial homology and commute with induced maps. In particular, the augmentation is natural. These facts let the augmentation kernels form a functor and let a chosen vertex split the augmentation.

The construction uses Mathlib's SSet.homology₀ε and SSet.homology₀Iso. The mathematical convention is that of Hatcher, Algebraic Topology, Section 2.1.

noncomputable def TauCeti.SSet.ιHomology₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X : SSet} (R : C) (x : X.obj (Opposite.op { len := 0 })) : R ⟶ X.homology R 0

The class in zeroth homology of a vertex, with coefficients in R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.SSet.ιHomology₀_homology₀Iso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X : SSet} (R : C) (x : X.obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) (X.homology₀Iso R).hom = CategoryTheory.Limits.Sigma.ι (fun (x : X.π₀) => R) (SSet.π₀.mk x)

A vertex class corresponds to the coproduct inclusion indexed by its connected component.

@[simp]

theorem TauCeti.SSet.ιHomology₀_homology₀Iso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X : SSet} (R : C) (x : X.obj (Opposite.op { len := 0 })) {Z : C} (h : (∐ fun (x : X.π₀) => R) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) (CategoryTheory.CategoryStruct.comp (X.homology₀Iso R).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : X.π₀) => R) (SSet.π₀.mk x)) h

A vertex class corresponds to the coproduct inclusion indexed by its connected component.

theorem TauCeti.SSet.homology₀_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X : SSet} (R : C) {T : C} {f g : X.homology R 0 ⟶ T} (h : ∀ (x : X.obj (Opposite.op { len := 0 })), CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) f = CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) g) : f = g

Vertex classes generate zeroth homology.

theorem TauCeti.SSet.homology₀_hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X : SSet} {R T : C} {f g : X.homology R 0 ⟶ T} : f = g ↔ ∀ (x : X.obj (Opposite.op { len := 0 })), CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) f = CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) g

@[simp]

theorem TauCeti.SSet.ιHomology₀_homologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X Y : SSet} (R : C) (f : X ⟶ Y) (x : X.obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) (SSet.homologyMap f R 0) = ιHomology₀ R ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x)

The homology map of a simplicial map sends a vertex class to the class of its image.

@[simp]

theorem TauCeti.SSet.ιHomology₀_homologyMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X Y : SSet} (R : C) (f : X ⟶ Y) (x : X.obj (Opposite.op { len := 0 })) {Z : C} (h : Y.homology R 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) (CategoryTheory.CategoryStruct.comp (SSet.homologyMap f R 0) h) = CategoryTheory.CategoryStruct.comp (ιHomology₀ R ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x)) h

The homology map of a simplicial map sends a vertex class to the class of its image.

@[simp]

theorem TauCeti.SSet.ιHomology₀_homology₀ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X : SSet} (R : C) (x : X.obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) (X.homology₀ε R) = CategoryTheory.CategoryStruct.id R

The augmentation sends each vertex class to the identity of the coefficient object.

@[simp]

theorem TauCeti.SSet.ιHomology₀_homology₀ε_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X : SSet} (R : C) (x : X.obj (Opposite.op { len := 0 })) {Z : C} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιHomology₀ R x) (CategoryTheory.CategoryStruct.comp (X.homology₀ε R) h) = h

The augmentation sends each vertex class to the identity of the coefficient object.

@[simp]

theorem TauCeti.SSet.homologyMap_homology₀ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X Y : SSet} (R : C) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap f R 0) (Y.homology₀ε R) = X.homology₀ε R

The augmentation of zeroth homology commutes with maps of simplicial sets.

@[simp]

theorem TauCeti.SSet.homologyMap_homology₀ε_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X Y : SSet} (R : C) (f : X ⟶ Y) {Z : C} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap f R 0) (CategoryTheory.CategoryStruct.comp (Y.homology₀ε R) h) = CategoryTheory.CategoryStruct.comp (X.homology₀ε R) h

The augmentation of zeroth homology commutes with maps of simplicial sets.