Documentation

TauCeti.AlgebraicTopology.Cellular.Augmentation

The augmented cellular chain complex of a contractible CW complex #

The augmentation of the cellular chain complex of a CW complex C with coefficients in R is the map TauCeti.cellularAugmentation C R from the cellular chains in degree 0 to R obtained by passing to cellular homology in degree 0, identifying it with the ordinary singular homology H₀(C; R) by the cellular–singular comparison TauCeti.cellularSingularHomologyIsoOfCWComplex, and applying Mathlib's augmentation TopCat.singularHomology₀ε of singular homology in degree 0. It vanishes on the boundaries of 1-cells, so it defines a chain map TauCeti.cellularChainComplexAugmentation C R from the cellular chain complex to R placed in degree 0, and it is natural under cellular maps (TauCeti.cellularChainGroupMap_comp_cellularAugmentation).

If C is contractible, its singular homology is that of a point, so the cellular–singular comparison shows that the cellular chain complex is exact in positive degrees (TauCeti.exactAt_cellularChainComplex_of_contractibleSpace), and the augmentation is a quasi-isomorphism (TauCeti.quasiIso_cellularChainComplexAugmentation): the augmented cellular chain complex of a contractible CW complex is a resolution of the coefficients. Applied to the universal cover of a K(G, 1) CW complex with the lifted CW structure, this is the exactness behind the cellular projective resolution of the trivial representation of G.

The coefficients lie in an abelian category with coproducts in which coproducts are exact. The cellular–singular comparison in degree 0 needs the inclusion of the 1-skeleton to induce an isomorphism on H₀, which is assumed as an instance hypothesis; it holds for every finite-dimensional complex, and for every complex when sequential colimits are exact in the coefficient category, as for modules over a ring.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.cellularAugmentation {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] :
cellularChainGroup C R 0 ⟶ R

The augmentation of the cellular chains of a CW complex C in degree 0: the projection onto cellular homology in degree 0, followed by the cellular–singular comparison with H₀(C; R) and the augmentation TopCat.singularHomology₀ε of singular homology.

Instances For
    source
    theorem TauCeti.singularHomologyπ_comp_cellularAugmentation {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] :
    CategoryTheory.CategoryStruct.comp ((skeletonPair C 0).singularHomologyπ R 0) (cellularAugmentation C R) = (↧↑(skeletonObj C 1)).singularHomology₀ε R

    On the zeroth singular homology of the 0-skeleton, mapped to the cellular chains by the quotient for the empty subspace, the augmentation is the augmentation of singular homology.

    source
    theorem TauCeti.singularHomologyπ_comp_cellularAugmentation_assoc {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] {Z : A} (h : R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp ((skeletonPair C 0).singularHomologyπ R 0) (CategoryTheory.CategoryStruct.comp (cellularAugmentation C R) h) = CategoryTheory.CategoryStruct.comp ((↧↑↑(Topology.RelCWComplex.skeletonLT C ↑1)).singularHomology₀ε R) h

    On the zeroth singular homology of the 0-skeleton, mapped to the cellular chains by the quotient for the empty subspace, the augmentation is the augmentation of singular homology.

    source
    @[simp]
    theorem TauCeti.ι_cellularChainGroupIso_inv_comp_cellularAugmentation {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] (j : Topology.RelCWComplex.cell C 0) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C 0) => R) j) (CategoryTheory.CategoryStruct.comp (cellularChainGroupIso C R 0).inv (cellularAugmentation C R)) = CategoryTheory.CategoryStruct.id R

    The augmentation takes the value 1 on each 0-cell: it sends the generator of a 0-cell, under the identification TauCeti.cellularChainGroupIso of the cellular chains with copies of R indexed by the cells, to the identity of R.

    source
    @[simp]
    theorem TauCeti.ι_cellularChainGroupIso_inv_comp_cellularAugmentation_assoc {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] (j : Topology.RelCWComplex.cell C 0) {Z : A} (h : R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C 0) => R) j) (CategoryTheory.CategoryStruct.comp (cellularChainGroupIso C R 0).inv (CategoryTheory.CategoryStruct.comp (cellularAugmentation C R) h)) = h

    The augmentation takes the value 1 on each 0-cell: it sends the generator of a 0-cell, under the identification TauCeti.cellularChainGroupIso of the cellular chains with copies of R indexed by the cells, to the identity of R.

    source
    @[simp]
    theorem TauCeti.cellularDifferential_comp_cellularAugmentation {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] :
    CategoryTheory.CategoryStruct.comp (cellularDifferential C R 0) (cellularAugmentation C R) = 0

    The augmentation vanishes on the boundaries of 1-cells.

    source
    @[simp]
    theorem TauCeti.cellularDifferential_comp_cellularAugmentation_assoc {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] {Z : A} (h : R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (cellularDifferential C R 0) (CategoryTheory.CategoryStruct.comp (cellularAugmentation C R) h) = CategoryTheory.CategoryStruct.comp 0 h

    The augmentation vanishes on the boundaries of 1-cells.

    source
    noncomputable def TauCeti.cellularChainComplexAugmentation {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] :
    cellularChainComplex C R ⟶ (ChainComplex.single₀ A).obj R

    The augmentation of the cellular chain complex: the chain map to the coefficients placed in degree 0 given in degree 0 by TauCeti.cellularAugmentation.

    Instances For
      source
      @[simp]
      theorem TauCeti.cellularChainComplexAugmentation_f_zero {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] :
      (cellularChainComplexAugmentation C R).f 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (cellularAugmentation C R)

      In degree 0 the augmentation of the cellular chain complex is TauCeti.cellularAugmentation.

      source
      theorem TauCeti.descOpcycles_cellularAugmentation {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] :
      HomologicalComplex.descOpcycles (cellularChainComplex C R) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (cellularAugmentation C R)) 1 descOpcycles_cellularAugmentation._proof_1 ⋯ = CategoryTheory.CategoryStruct.comp (cellularChainComplex C R).isoHomologyι₀.inv (CategoryTheory.CategoryStruct.comp (cellularSingularHomologyIsoOfCWComplex C R 0).hom ((↧↑C).singularHomology₀ε R))

      The map that the augmentation induces on cellular homology in degree 0, identified with the opcycles, is the cellular–singular comparison followed by the augmentation of singular homology.

      source
      theorem TauCeti.exactAt_cellularChainComplex_of_contractibleSpace {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [ContractibleSpace ↑C] (n : ℕ) [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C (n + 2)) R (n + 1))] :
      HomologicalComplex.ExactAt (cellularChainComplex C R) (n + 1)

      The cellular chain complex of a contractible CW complex is exact in positive degrees: its homology there is the positive-degree singular homology of a contractible space. The hypothesis on the inclusion of the (n + 2)-skeleton holds for every finite-dimensional complex, and for every complex when sequential colimits are exact in the coefficient category.

      source
      theorem TauCeti.quasiIso_cellularChainComplexAugmentation {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] [ContractibleSpace ↑C] [∀ (n : ℕ), CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C (n + 2)) R (n + 1))] :
      QuasiIso (cellularChainComplexAugmentation C R)

      The augmented cellular chain complex of a contractible CW complex is a resolution of the coefficients: the augmentation is a quasi-isomorphism. In degree 0 it induces the composite of the cellular–singular comparison with the augmentation H₀(C; R) ⟶ R, an isomorphism because C is path connected; in positive degrees both complexes are exact. The hypotheses on the inclusions of the skeleta hold for every finite-dimensional complex, and for every complex when sequential colimits are exact in the coefficient category.

      source
      @[simp]
      theorem TauCeti.cellularChainGroupMap_comp_cellularAugmentation {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] (C : Set X) [Topology.CWComplex C] (C' : Set Y) [Topology.CWComplex C'] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C' 1) R 0)] :
      CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R 0) (cellularAugmentation C' R) = cellularAugmentation C R

      The augmentation is natural under cellular maps.

      source
      @[simp]
      theorem TauCeti.cellularChainGroupMap_comp_cellularAugmentation_assoc {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] (C : Set X) [Topology.CWComplex C] (C' : Set Y) [Topology.CWComplex C'] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C 1) R 0)] [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C' 1) R 0)] {Z : A} (h : R ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R 0) (CategoryTheory.CategoryStruct.comp (cellularAugmentation C' R) h) = CategoryTheory.CategoryStruct.comp (cellularAugmentation C R) h

      The augmentation is natural under cellular maps.