Cochain tensor-product infrastructure for the cup product #

Registers the additive and sign instances needed to tensor chain and cochain complexes over ModuleCat, and packages the singular cochain tensor square with its functoriality laws. This is the algebraic substrate consumed by the Alexander–Whitney and cup-product modules; the diagonal itself is constructed in those later modules rather than in this file.

1. Coefficient-category wiring (gap `U6`) #

The chain/cochain monoidal structure on HomologicalComplex C c requires the additivity of curriedTensor C both in its argument object and as a functor. Both follow from MonoidalPreadditive C but are not registered upstream.

source

instance SphereOddDegree.curriedTensorObj_additive {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) :

((CategoryTheory.MonoidalCategory.curriedTensor C).obj X).Additive

For a preadditive monoidal category with MonoidalPreadditive, tensoring on the left by a fixed object is an additive functor. This is the ((curriedTensor C).obj X).Additive side condition required by HomologicalComplex.monoidalCategory; it holds because (curriedTensor C).obj X is definitionally tensorLeft X.

source

instance SphereOddDegree.curriedTensor_additive {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] :

(CategoryTheory.MonoidalCategory.curriedTensor C).Additive

For a preadditive monoidal category with MonoidalPreadditive, the currying functor curriedTensor C : C ⥤ C ⥤ C is itself additive. This is the (curriedTensor C).Additive side condition required by HomologicalComplex.monoidalCategory; additivity in the first variable is MonoidalPreadditive.add_tensor componentwise.

2. Tensor signs for the cochain shape `ComplexShape.up ℕ` #

Mathlib registers TensorSigns for down ℕ and up ℤ, but not for up ℕ, the shape of the singular cochain complex. We supply it with the same (-1)^• convention as the chain case.

source

@[instance_reducible]

instance SphereOddDegree.tensorSignsUpNat :

(ComplexShape.up ℕ).TensorSigns

The ComplexShape.TensorSigns instance for the cochain shape ComplexShape.up ℕ, using the sign ε n = (-1)^n. This instance makes HomologicalComplex.monoidalCategory apply to CochainComplex (ModuleCat R) ℕ.

Equations

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

source

@[simp]

theorem SphereOddDegree.ε_up_nat (n : ℕ) :

(ComplexShape.up ℕ).ε n = (-1) ^ n

The Koszul sign of ComplexShape.up ℕ at index n is (-1)^n.

3. The singular cochain tensor square `C^•(X) ⊗ C^•(X)` #

With the wiring of §1–§2 in place, the tensor product of the singular cochain complex with itself is a genuine cochain complex, functorial in X. This is the domain of a cup product (a map C^•(X) ⊗ C^•(X) → C^•(X)), and its functorial pullback is the naturality substrate for f^*(a ⌣ b) = f^* a ⌣ f^* b.

source

noncomputable def SphereOddDegree.singularCochainTensorSquare (R : Type) [CommRing R] (M : ModuleCat R) (X : TopCat ᵒᵖ) :

CochainComplex (ModuleCat R) ℕ

The tensor square of the singular cochain complex with coefficients in M : ModuleCat R, i.e. C^•(X; M) ⊗ C^•(X; M) as a CochainComplex (ModuleCat R) ℕ. This is the cochain-level domain of a cup product ⌣ : C^•(X) ⊗ C^•(X) → C^•(X).

Equations

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

Instances For

source

noncomputable def SphereOddDegree.singularCochainTensorSquareMap (R : Type) [CommRing R] (M : ModuleCat R) {X Y : TopCat ᵒᵖ} (f : X ⟶ Y) :

singularCochainTensorSquare R M X ⟶ singularCochainTensorSquare R M Y

The functorial pullback on the cochain tensor square: a continuous map (packaged as f : X ⟶ Y in TopCatᵒᵖ) induces f^* ⊗ f^* on the tensor squares. This is MonoidalCategory.tensorHom applied to the cochain pullback (singularCochainComplexFunctor R M).map f with itself.

Equations

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

Instances For

source

@[simp]

theorem SphereOddDegree.singularCochainTensorSquareMap_id (R : Type) [CommRing R] (M : ModuleCat R) (X : TopCat ᵒᵖ) :

singularCochainTensorSquareMap R M (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (singularCochainTensorSquare R M X)

Functoriality: the cochain tensor-square pullback preserves identities.

source

theorem SphereOddDegree.singularCochainTensorSquareMap_comp (R : Type) [CommRing R] (M : ModuleCat R) {X Y Z : TopCat ᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) :

singularCochainTensorSquareMap R M (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (singularCochainTensorSquareMap R M f) (singularCochainTensorSquareMap R M g)

Functoriality: the cochain tensor-square pullback preserves composition.

4. `ZMod 2` specializations #

The downstream RPⁿ work uses ZMod 2 coefficients, where the Koszul sign is trivial (-1 = 1). These are thin abbreviations of the general definitions.

source

@[reducible, inline]

noncomputable abbrev SphereOddDegree.singularCochainTensorSquareZMod2 (X : TopCat ᵒᵖ) :

CochainComplex (ModuleCat (ZMod 2)) ℕ

The tensor square of the singular F₂-cochain complex, C^•(X; F₂) ⊗ C^•(X; F₂).

Equations