The models of the tensor product of normalized cubical chains

The functor N(X) ⊗ N(Y) on pairs of spaces, with N the normalized cubical chains, is free on the models (Iᵖ, I^q), one for each pair of degrees p + q = n, in degree n (TauCeti.AcyclicModels.MultiModelPresentation): a chain of the summand Nₚ(X) ⊗ N_q(Y) is a combination of the images of the generator [Iᵖ] ⊗ [I^q] under the pairs of maps (Iᵖ, I^q) ⟶ (X, Y), with the coefficients of the two factors (TauCeti.cubicalModelPresentation). The simplicial singular chains of the product are acyclic on these models, since a product of cubes is contractible. This is the input to the method of acyclic models for natural maps out of the tensor product.

Main definitions

• TauCeti.cubicalTensor k: the functor (X, Y) ↦ N(X; k) ⊗ N(Y; k) on pairs of spaces.
• TauCeti.cubicalTensorModelPresentation k: its presentation on the models (Iᵖ, I^q).
• TauCeti.singularChainsProduct k: the singular chains of the product, as a functor on pairs of spaces.
• TauCeti.isAcyclicOnMulti_singularChainsProduct: it is acyclic on any family of models with contractible products, in particular on these.

@[reducible, inline]

noncomputable abbrev TauCeti.cubicalTensor (k : Type u) [CommRing k] : CategoryTheory.Functor (TopCat × TopCat) (ChainComplex (ModuleCat k) ℕ)

The functor (X, Y) ↦ N(X; k) ⊗ N(Y; k), the tensor product of the normalized cubical chain complexes, on pairs of spaces.

@[reducible, inline]

abbrev TauCeti.BidegreeIndex (n : ℕ) : Type

The bidegrees (p, q) with p + q = n: the index of the models in degree n.

theorem TauCeti.BidegreeIndex.eq_mk_zero_zero (i : BidegreeIndex 0) : i = ⟨(0, 0), ⋯⟩

The only bidegree of total degree 0 is (0, 0).

@[reducible, inline]

abbrev TauCeti.cubicalBidegreeModel (n : ℕ) (i : BidegreeIndex n) : TopCat × TopCat

The model of bidegree (p, q): the pair of cubes (Iᵖ, I^q).

noncomputable def TauCeti.cubicalTensorSummandCoord {k : Type u} [CommRing k] (X Y : TopCat) (n p q : ℕ) (h : p + q = n) : TensorProduct k (NormalizedCubicalChain (↑X) k p) (NormalizedCubicalChain (↑Y) k q) →ₗ[k] (i : BidegreeIndex n) × (cubicalBidegreeModel n i ⟶ (X, Y)) →₀ k

The coefficients of the tensor product of a normalized cubical chain of X of degree p and of one of Y of degree q on the pairs of maps from the models: the product of the coefficients of the factors.

noncomputable def TauCeti.cubicalTensorCoord (k : Type u) [CommRing k] (X : TopCat × TopCat) (n : ℕ) : ↑(((cubicalTensor k).obj X).X n) →ₗ[k] (i : BidegreeIndex n) × (cubicalBidegreeModel n i ⟶ X) →₀ k

The coefficients of a chain of the tensor product in degree n, on the pairs of maps from the models.

noncomputable def TauCeti.cubicalTensorGen (k : Type u) [CommRing k] (n : ℕ) (i : BidegreeIndex n) : ↑(((cubicalTensor k).obj (cubicalBidegreeModel n i)).X n)

The generator in bidegree (p, q): the tensor product of the identity cubes of Iᵖ and I^q, in the summand of bidegree (p, q).

theorem TauCeti.cubicalTensorGen_def {k : Type u} [CommRing k] (n : ℕ) (i : BidegreeIndex n) : cubicalTensorGen k n i = (ModuleCat.Hom.hom (HomologicalComplex.ιTensorObj ((normalizedCubicalChainComplex k).obj (cubeModel (↑i).1)) ((normalizedCubicalChainComplex k).obj (cubeModel (↑i).2)) (↑i).1 (↑i).2 n ⋯)) (NormalizedCubicalChain.ofCube (↑(cubeModel (↑i).1)) k (upCube (↑i).1) ⊗ₜ[k] NormalizedCubicalChain.ofCube (↑(cubeModel (↑i).2)) k (upCube (↑i).2))

The generator is the image of the tensor product of the two identity cubes.

theorem TauCeti.cubicalTensorCoord_ι {k : Type u} [CommRing k] (X : TopCat × TopCat) (n p q : ℕ) (h : p + q = n) (z : TensorProduct k (NormalizedCubicalChain (↑X.1) k p) (NormalizedCubicalChain (↑X.2) k q)) : (cubicalTensorCoord k X n) ((ModuleCat.Hom.hom (HomologicalComplex.ιTensorObj ((normalizedCubicalChainComplex k).obj X.1) ((normalizedCubicalChainComplex k).obj X.2) p q n h)) z) = (cubicalTensorSummandCoord X.1 X.2 n p q h) z

The coefficients of a chain of a summand of the tensor product are those of the summand.

theorem TauCeti.cubicalTensor_map_ι {k : Type u} [CommRing k] {X Y : TopCat × TopCat} (f : X ⟶ Y) (n p q : ℕ) (h : p + q = n) (a : NormalizedCubicalChain (↑X.1) k p) (b : NormalizedCubicalChain (↑X.2) k q) : (CategoryTheory.ConcreteCategory.hom (((cubicalTensor k).map f).f n)) ((ModuleCat.Hom.hom (HomologicalComplex.ιTensorObj ((normalizedCubicalChainComplex k).obj X.1) ((normalizedCubicalChainComplex k).obj X.2) p q n h)) (a ⊗ₜ[k] b)) = (ModuleCat.Hom.hom (HomologicalComplex.ιTensorObj ((normalizedCubicalChainComplex k).obj Y.1) ((normalizedCubicalChainComplex k).obj Y.2) p q n h)) ((CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex k).map f.1).f p)) a ⊗ₜ[k] (CategoryTheory.ConcreteCategory.hom (((normalizedCubicalChainComplex k).map f.2).f q)) b)

The map induced on a pure tensor of a summand of the tensor product by a pair of maps is the tensor product of the images of the factors.

theorem TauCeti.cubicalTensorSummandCoord_tmul {k : Type u} [CommRing k] (X Y : TopCat) (n p q : ℕ) (h : p + q = n) (a : NormalizedCubicalChain (↑X) k p) (b : NormalizedCubicalChain (↑Y) k q) : (cubicalTensorSummandCoord X Y n p q h) (a ⊗ₜ[k] b) = Finsupp.mapDomain (fun (st : (cubeModel p ⟶ X) × (cubeModel q ⟶ Y)) => ⟨⟨(p, q), h⟩, (st.1, st.2)⟩) ((finsuppTensorFinsupp' k (cubeModel p ⟶ X) (cubeModel q ⟶ Y)) ((cubicalCoord k X p) a ⊗ₜ[k] (cubicalCoord k Y q) b))

The coefficients of a tensor of two chains are the tensor product of their coefficients.

theorem TauCeti.cubicalTensorSummandCoord_map {k : Type u} [CommRing k] {X X' Y Y' : TopCat} (f₁ : X ⟶ X') (f₂ : Y ⟶ Y') (n p q : ℕ) (h : p + q = n) (a : NormalizedCubicalChain (↑X) k p) (b : NormalizedCubicalChain (↑Y) k q) : (cubicalTensorSummandCoord X' Y' n p q h) ((NormalizedCubicalChain.map k (TopCat.Hom.hom f₁) p) a ⊗ₜ[k] (NormalizedCubicalChain.map k (TopCat.Hom.hom f₂) q) b) = Finsupp.mapDomain (fun (s : (i : BidegreeIndex n) × (cubicalBidegreeModel n i ⟶ (X, Y))) => ⟨s.fst, CategoryTheory.CategoryStruct.comp s.snd (f₁, f₂)⟩) ((cubicalTensorSummandCoord X Y n p q h) (a ⊗ₜ[k] b))

The coefficients of the tensor of the images of two chains under maps of spaces are those of the chains, pushed forward by the composition with the maps.

theorem TauCeti.cubicalTensorCoord_map {k : Type u} [CommRing k] {X Y : TopCat × TopCat} (f : X ⟶ Y) (n : ℕ) (x : ↑(((cubicalTensor k).obj X).X n)) : (cubicalTensorCoord k Y n) ((CategoryTheory.ConcreteCategory.hom (((cubicalTensor k).map f).f n)) x) = Finsupp.mapDomain (fun (s : (i : BidegreeIndex n) × (cubicalBidegreeModel n i ⟶ X)) => ⟨s.fst, CategoryTheory.CategoryStruct.comp s.snd f⟩) ((cubicalTensorCoord k X n) x)

The coefficients of the tensor product are natural.

theorem TauCeti.map_cubicalTensorGen {k : Type u} [CommRing k] (X : TopCat × TopCat) (n p q : ℕ) (h : p + q = n) (σ : cubeModel p ⟶ X.1) (τ : cubeModel q ⟶ X.2) : (CategoryTheory.ConcreteCategory.hom (((cubicalTensor k).map (σ, τ)).f n)) (cubicalTensorGen k n ⟨(p, q), h⟩) = (ModuleCat.Hom.hom (HomologicalComplex.ιTensorObj ((normalizedCubicalChainComplex k).obj X.1) ((normalizedCubicalChainComplex k).obj X.2) p q n h)) ((NormalizedCubicalChain.map k (TopCat.Hom.hom σ) p) (NormalizedCubicalChain.ofCube (↑(cubeModel p)) k (upCube p)) ⊗ₜ[k] (NormalizedCubicalChain.map k (TopCat.Hom.hom τ) q) (NormalizedCubicalChain.ofCube (↑(cubeModel q)) k (upCube q)))

The image of the generator of bidegree (p, q) under a pair of maps is the tensor product of the images of the identity cubes.

theorem TauCeti.sum_cubicalTensorCoord {k : Type u} [CommRing k] (X : TopCat × TopCat) (n : ℕ) (x : ↑(((cubicalTensor k).obj X).X n)) : (((cubicalTensorCoord k X n) x).sum fun (s : (i : BidegreeIndex n) × (cubicalBidegreeModel n i ⟶ X)) (a : k) => a • (CategoryTheory.ConcreteCategory.hom (((cubicalTensor k).map s.snd).f n)) (cubicalTensorGen k n s.fst)) = x

Every chain of the tensor product is the combination of the images of the generators with its coefficients.

noncomputable def TauCeti.cubicalTensorModelPresentation (k : Type u) [CommRing k] : AcyclicModels.MultiModelPresentation (cubicalTensor k) BidegreeIndex

The tensor product of the normalized cubical chains is free on the pairs of cubes: in degree n, on the models (Iᵖ, I^q) with p + q = n.

@[simp]

theorem TauCeti.cubicalTensorModelPresentation_model {k : Type u} [CommRing k] (n : ℕ) (i : BidegreeIndex n) : (cubicalTensorModelPresentation k).model n i = cubicalBidegreeModel n i

The models of cubicalTensorModelPresentation are the pairs of cubes.

@[simp]

theorem TauCeti.cubicalTensorModelPresentation_gen {k : Type u} [CommRing k] (n : ℕ) (i : BidegreeIndex n) : (cubicalTensorModelPresentation k).gen n i = cubicalTensorGen k n i

The generators of cubicalTensorModelPresentation are the tensor products of the identity cubes.

@[simp]

theorem TauCeti.cubicalTensorModelPresentation_coord {k : Type u} [CommRing k] (X : TopCat × TopCat) (n : ℕ) : (cubicalTensorModelPresentation k).coord X n = cubicalTensorCoord k X n

The coefficients of cubicalTensorModelPresentation are cubicalTensorCoord.

@[reducible, inline]

noncomputable abbrev TauCeti.singularChainsProduct (k : Type u) [Ring k] : CategoryTheory.Functor (TopCat × TopCat) (ChainComplex (ModuleCat k) ℕ)

The simplicial singular chains of the product of the two spaces, as a functor on pairs of spaces.

instance TauCeti.instContractibleSpaceCarrierObjProdTopCatTensorMkCubeModel (p q : ℕ) : ContractibleSpace ↑((CategoryTheory.MonoidalCategory.tensor TopCat).obj (cubeModel p, cubeModel q))

The product of two cubes is contractible.

theorem TauCeti.isAcyclicOnMulti_singularChainsProduct (k : Type u) [Ring k] {ι : ℕ → Type u_1} (M : (n : ℕ) → ι n → TopCat × TopCat) [∀ (n : ℕ) (i : ι n), ContractibleSpace ↑((CategoryTheory.MonoidalCategory.tensor TopCat).obj (M n i))] : AcyclicModels.IsAcyclicOnMulti (singularChainsProduct k) M fun (X : TopCat × TopCat) => singularAugment k (CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 X.2)

The simplicial singular chains of the product are acyclic on any family of models whose products are contractible.

theorem TauCeti.isAcyclicOnMulti_singularChainsProduct_cubicalTensorModelPresentation (k : Type u) [CommRing k] : AcyclicModels.IsAcyclicOnMulti (singularChainsProduct k) (cubicalTensorModelPresentation k).model fun (X : TopCat × TopCat) => singularAugment k (CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 X.2)

The simplicial singular chains of the product are acyclic on the models of the tensor product of the normalized cubical chains, since a product of cubes is contractible.