Documentation

TauCeti.AlgebraicTopology.Singular.Cubical.LocalCoefficients.ChainComplex

The normalized cubical chain complex with local coefficients #

The normalized cubical chains with coefficients in a local system L, with their boundary, form a chain complex of modules L.normalizedTwistedCubicalChainComplex. Morphisms of local systems and continuous maps (from the complex of the pulled back system) induce chain maps. This packages TauCeti.AlgebraicTopology.Singular.Cubical.LocalCoefficients.Normalized in the form in which it is compared with the singular chains with local coefficients twistedChainComplex, as TauCeti.AlgebraicTopology.Singular.Cubical.ChainComplex does for constant coefficients.

The chain maps induced by continuous maps compare two complexes in one category of modules, so here the spaces live in a common universe; the underlying linear maps of TauCeti.LocalCoefficientSystem.NormalizedTwistedCubicalChain.map have no such restriction.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplex {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) :
ChainComplex (ModuleCat R) ℕ

The normalized cubical chain complex with coefficients in a local system L.

Instances For
    source
    @[simp]
    theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplex_X {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) :
    L.normalizedTwistedCubicalChainComplex.X n = ↧(L.NormalizedTwistedCubicalChain n)

    The terms of the normalized cubical chain complex are the normalized chains.

    source
    @[simp]
    theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplex_d_apply {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) (x : L.NormalizedTwistedCubicalChain (n + 1)) :
    (CategoryTheory.ConcreteCategory.hom (L.normalizedTwistedCubicalChainComplex.d (n + 1) n)) x = (NormalizedTwistedCubicalChain.boundary L n) x

    The differential of the normalized cubical chain complex is the boundary.

    source
    theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplex_d {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) :
    L.normalizedTwistedCubicalChainComplex.d (n + 1) n = ModuleCat.ofHom (NormalizedTwistedCubicalChain.boundary L n)

    The differential of the normalized cubical chain complex is the boundary, as a morphism of modules.

    source
    noncomputable def TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexCoefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) :
    L.normalizedTwistedCubicalChainComplex ⟶ K.normalizedTwistedCubicalChainComplex

    The chain map of normalized cubical chain complexes induced by a morphism of local systems.

    Instances For
      source
      @[simp]
      theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexCoefficientMap_f {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : ℕ) :
      (normalizedTwistedCubicalChainComplexCoefficientMap η).f n = ModuleCat.ofHom (NormalizedTwistedCubicalChain.coefficientMap η n)

      The components of the chain map induced by a morphism of local systems.

      source
      noncomputable def TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap {R : Type u} [Ring R] {X Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) :
      ((pullback f).obj L).normalizedTwistedCubicalChainComplex ⟶ L.normalizedTwistedCubicalChainComplex

      The chain map of normalized cubical chain complexes induced by a continuous map f, from the complex with coefficients in f⁎L to the complex with coefficients in L.

      Instances For
        source
        @[simp]
        theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap_f {R : Type u} [Ring R] {X Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) (n : ℕ) :
        (normalizedTwistedCubicalChainComplexMap f L).f n = ModuleCat.ofHom (NormalizedTwistedCubicalChain.map f L n)

        The components of the chain map induced by a continuous map.

        source
        @[simp]
        theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexCoefficientMap_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) :
        normalizedTwistedCubicalChainComplexCoefficientMap (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id L.normalizedTwistedCubicalChainComplex

        The identity of a local system induces the identity chain map.

        source
        theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexCoefficientMap_comp {R : Type u} [Ring R] {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) :
        normalizedTwistedCubicalChainComplexCoefficientMap (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (normalizedTwistedCubicalChainComplexCoefficientMap η) (normalizedTwistedCubicalChainComplexCoefficientMap θ)

        A composite of morphisms of local systems induces the composite chain map.

        source
        @[simp]
        theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) :
        normalizedTwistedCubicalChainComplexMap (ContinuousMap.id ↑X) L = normalizedTwistedCubicalChainComplexCoefficientMap ((pullbackIdIso X).hom.app L)

        The identity map induces on the normalized cubical chain complex the chain map coming from the identification of a system with its pullback along the identity.

        source
        theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap_comp {R : Type u} [Ring R] {X Y Z : TopCat} (f : C(↑X, ↑Y)) (g : C(↑Y, ↑Z)) (L : LocalCoefficientSystem R Z) :
        normalizedTwistedCubicalChainComplexMap (g.comp f) L = CategoryTheory.CategoryStruct.comp (normalizedTwistedCubicalChainComplexCoefficientMap ((pullbackCompIso f g).hom.app L)) (CategoryTheory.CategoryStruct.comp (normalizedTwistedCubicalChainComplexMap f ((pullback g).obj L)) (normalizedTwistedCubicalChainComplexMap g L))

        A composite of continuous maps induces on normalized cubical chain complexes the composite of the two induced chain maps, after the identification of the pullback along the composite with the iterated pullback.

        source
        theorem TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap_naturality {R : Type u} [Ring R] {X Y : TopCat} (f : C(↑X, ↑Y)) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) :
        CategoryTheory.CategoryStruct.comp (normalizedTwistedCubicalChainComplexMap f L) (normalizedTwistedCubicalChainComplexCoefficientMap η) = CategoryTheory.CategoryStruct.comp (normalizedTwistedCubicalChainComplexCoefficientMap ((pullback f).map η)) (normalizedTwistedCubicalChainComplexMap f K)

        The chain map induced by a continuous map is natural in the coefficient system.