Documentation

TauCeti.AlgebraicTopology.Singular.Cubical.ChainComplex

The normalized cubical chain complex functor #

The normalized cubical chains of a topological space, with their boundary, form a chain complex of modules over the coefficient ring, and continuous maps induce chain maps. This packages the concrete normalized cubical chains of TauCeti.AlgebraicTopology.Singular.Cubical.Normalized as a functor TopCat ⥤ ChainComplex (ModuleCat R) ℕ, the form in which they are compared with the simplicial singular chain complex.

Main definitions #

Main results #

source
noncomputable def TauCeti.normalizedCubicalChainComplexObj (R : Type u) [Ring R] (X : TopCat) :
ChainComplex (ModuleCat R) ℕ

The normalized cubical chain complex of a topological space, with coefficients in R.

Instances For
    source
    noncomputable def TauCeti.normalizedCubicalChainComplex (R : Type u) [Ring R] :
    CategoryTheory.Functor TopCat (ChainComplex (ModuleCat R) ℕ)

    The normalized cubical chain complex functor, with coefficients in R.

    Instances For
      source
      @[simp]
      theorem TauCeti.normalizedCubicalChainComplex_obj_X {R : Type u} [Ring R] (X : TopCat) (n : ℕ) :
      ((normalizedCubicalChainComplex R).obj X).X n = ↧(NormalizedCubicalChain (↑X) R n)
      source
      @[simp]
      theorem TauCeti.normalizedCubicalChainComplex_obj_d_apply {R : Type u} [Ring R] (X : TopCat) (n : ℕ) (x : NormalizedCubicalChain (↑X) R (n + 1)) :
      (CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex R).obj X).d (n + 1) n)) x = (NormalizedCubicalChain.boundary (↑X) R n) x
      source
      noncomputable def TauCeti.normalizedCubicalChainComplexXEquiv {R : Type u} [Ring R] (X : TopCat) (n : ℕ) :
      ↑(((normalizedCubicalChainComplex R).obj X).X n) ≃ₗ[R] NormalizedCubicalChain (↑X) R n

      The concrete identification of a term of the normalized cubical chain complex with the corresponding module of normalized cubical chains.

      Instances For
        source
        @[simp]
        theorem TauCeti.normalizedCubicalChainComplexXEquiv_apply {R : Type u} [Ring R] (X : TopCat) (n : ℕ) (g : ↑(((normalizedCubicalChainComplex R).obj X).X n)) :
        (normalizedCubicalChainComplexXEquiv X n) g = g

        The concrete identification of a chain-complex term acts as the identity on elements.

        source
        @[simp]
        theorem TauCeti.normalizedCubicalChainComplexXEquiv_symm_apply {R : Type u} [Ring R] (X : TopCat) (n : ℕ) (g : NormalizedCubicalChain (↑X) R n) :
        (normalizedCubicalChainComplexXEquiv X n).symm g = g

        The inverse concrete identification acts as the identity on normalized cubical chains.

        source
        theorem TauCeti.normalizedCubicalChainComplexXEquiv_d_apply {R : Type u} [Ring R] (X : TopCat) (n : ℕ) (g : ↑(((normalizedCubicalChainComplex R).obj X).X (n + 1))) :
        (normalizedCubicalChainComplexXEquiv X n) ((CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex R).obj X).d (n + 1) n)) g) = (NormalizedCubicalChain.boundary (↑X) R n) ((normalizedCubicalChainComplexXEquiv X (n + 1)) g)

        Under the concrete identification, the chain-complex differential is the cubical boundary.

        source
        theorem TauCeti.normalizedCubicalChainComplex_map_f {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) :
        ((normalizedCubicalChainComplex R).map f).f n = ModuleCat.ofHom (NormalizedCubicalChain.map R (TopCat.Hom.hom f) n)

        In each degree, the map of normalized cubical chain complexes induced by a map of spaces is the push-forward of normalized cubical chains.

        source
        @[simp]
        theorem TauCeti.normalizedCubicalChainComplex_map_f_apply {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (x : NormalizedCubicalChain (↑X) R n) :
        (CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex R).map f).f n)) x = (NormalizedCubicalChain.map R (TopCat.Hom.hom f) n) x
        source
        theorem TauCeti.normalizedCubicalChainComplexXEquiv_map_f_apply {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (x : ↑(((normalizedCubicalChainComplex R).obj X).X n)) :
        (normalizedCubicalChainComplexXEquiv Y n) ((CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex R).map f).f n)) x) = (NormalizedCubicalChain.map R (TopCat.Hom.hom f) n) ((normalizedCubicalChainComplexXEquiv X n) x)

        Under the concrete term identifications, a map of cubical complexes is the push-forward of normalized chains.

        source
        instance TauCeti.instProjectiveCarrierXNatModuleCatObjTopCatChainComplexNormalizedCubicalChainComplex {R : Type u} [Ring R] (X : TopCat) (n : ℕ) :
        Module.Projective R ↑(((normalizedCubicalChainComplex R).obj X).X n)

        The terms of the normalized cubical chain complex are projective modules.

        source
        theorem TauCeti.NormalizedCubicalChain.exists_boundary_eq_of_isZero_homology {R : Type u} [Ring R] {X : TopCat} {n : ℕ} (h : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex R).obj X) (n + 1))) {c : NormalizedCubicalChain (↑X) R (n + 1)} (hc : (boundary (↑X) R n) c = 0) :
        ∃ (c' : NormalizedCubicalChain (↑X) R (n + 2)), (boundary (↑X) R (n + 1)) c' = c

        If the normalized cubical homology of X vanishes in dimension n + 1, every normalized cubical (n + 1)-cycle of X is a boundary.