Cubical chains on a space with a right action of a topological monoid

Let G be a topological monoid acting continuously and strictly on a space Y from the right, written y · g = op g • y. The action Y × G → Y and the cross product of normalized cubical chains give a right action of the Pontryagin algebra on the chains of Y: c · a := act_* (c × a) : C^□_{p + q}(Y; R) for c ∈ C^□_p(Y; R) and a ∈ C^□_q(G; R). It is strictly associative and unital, and the boundary is a derivation for it with the Koszul sign. Hence ⨁ n, C^□_n(Y; R), with C^□_n in cohomological degree -n, is a differential graded right module over the DG algebra ⨁ n, C^□_n(G; R) of TauCeti.AlgebraicTopology.Singular.Cubical.MonoidAlgebra.DGAlgebra.

An equivariant continuous map Y → Y' induces a morphism of these DG right modules, functorially.

The module TauCeti.cubicalChainModule Y G R is a one-field wrapper around normalizedCubicalChainAlgebra Y R, linearly equivalent to it (TauCeti.cubicalChainModuleEquiv): for Y = G acting on itself by right multiplication, the algebra already acts on itself, and the wrapper keeps the two actions apart.

Main definitions

• TauCeti.actMap Y G: the action Y × G → Y, (y, g) ↦ op g • y.
• TauCeti.NormalizedCubicalChain.act Y G R p q: the action C^□_p(Y; R) ⊗ C^□_q(G; R) → C^□_{p + q}(Y; R).
• TauCeti.cubicalChainModule Y G R: the DG right module ⨁ n, C^□_n(Y; R).
• TauCeti.cubicalChainModuleDG Y G R: it, as an object of DGRightModuleCat.
• TauCeti.cubicalChainModuleMap R f hf: the morphism induced by an equivariant map.

Main results

• TauCeti.NormalizedCubicalChain.act_assoc, TauCeti.NormalizedCubicalChain.act_one: the action is strictly associative and unital.
• TauCeti.NormalizedCubicalChain.boundary_act: the Leibniz rule.
• TauCeti.cubicalChainModule_isDGRightModule: the chains form a DG right module.
• TauCeti.cubicalChainModuleMap_id, TauCeti.cubicalChainModuleMap_comp: functoriality.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter VII.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Progress in Mathematics 360, Birkhäuser, 2025, §7.1.

def TauCeti.actMap (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [TopologicalSpace G] [SMul Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] : C(Y × G, Y)

The right action of G on Y as a continuous map Y × G → Y, (y, g) ↦ op g • y.

@[simp]

theorem TauCeti.actMap_apply (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [TopologicalSpace G] [SMul Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] (x : Y × G) : (actMap Y G) x = MulOpposite.op x.2 • x.1

noncomputable def TauCeti.NormalizedCubicalChain.act (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [TopologicalSpace G] [SMul Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] (R : Type u_3) [CommRing R] (p q : ℕ) : NormalizedCubicalChain Y R p →ₗ[R] NormalizedCubicalChain G R q →ₗ[R] NormalizedCubicalChain Y R (p + q)

The action of chains on G on chains on Y: c · a = act_* (c × a).

theorem TauCeti.NormalizedCubicalChain.act_def {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [TopologicalSpace G] [SMul Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {p q : ℕ} (c : NormalizedCubicalChain Y R p) (a : NormalizedCubicalChain G R q) : ((act Y G R p q) c) a = (map R (actMap Y G) (p + q)) (((crossProduct Y G R p q) c) a)

The action is the push-forward of the cross product along the action map.

theorem TauCeti.NormalizedCubicalChain.boundary_act {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [TopologicalSpace G] [SMul Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {p q : ℕ} (c : NormalizedCubicalChain Y R (p + 1)) (a : NormalizedCubicalChain G R (q + 1)) : (boundary Y R (p + q + 1)) ((cast R ⋯) (((act Y G R (p + 1) (q + 1)) c) a)) = ((act Y G R p (q + 1)) ((boundary Y R p) c)) a + (-1) ^ (p + 1) • (cast R ⋯) (((act Y G R (p + 1) q) c) ((boundary G R q) a))

The Leibniz rule for the action: for c of degree p + 1 and a of degree q + 1, ∂ (c · a) = ∂ c · a + (-1) ^ (p + 1) • (c · ∂ a), in degree p + q + 1.

theorem TauCeti.NormalizedCubicalChain.boundary_act_zero_right {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [TopologicalSpace G] [SMul Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {p : ℕ} (c : NormalizedCubicalChain Y R (p + 1)) (a : NormalizedCubicalChain G R 0) : (boundary Y R p) (((act Y G R (p + 1) 0) c) a) = ((act Y G R p 0) ((boundary Y R p) c)) a

The Leibniz rule for the action of a 0-chain.

theorem TauCeti.NormalizedCubicalChain.boundary_act_zero_left {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [TopologicalSpace G] [SMul Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {q : ℕ} (c : NormalizedCubicalChain Y R 0) (a : NormalizedCubicalChain G R (q + 1)) : (boundary Y R q) ((cast R ⋯) (((act Y G R 0 (q + 1)) c) a)) = (cast R ⋯) (((act Y G R 0 q) c) ((boundary G R q) a))

The Leibniz rule for the action on a 0-chain.

theorem TauCeti.NormalizedCubicalChain.map_act {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [TopologicalSpace G] [SMul Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {Y' : Type u_4} [TopologicalSpace Y'] [SMul Gᵐᵒᵖ Y'] [ContinuousSMul Gᵐᵒᵖ Y'] (f : C(Y, Y')) (hf : ∀ (g : G) (y : Y), f (MulOpposite.op g • y) = MulOpposite.op g • f y) {p q : ℕ} (c : NormalizedCubicalChain Y R p) (a : NormalizedCubicalChain G R q) : (map R f (p + q)) (((act Y G R p q) c) a) = ((act Y' G R p q) ((map R f p) c)) a

Pushing forward along an equivariant map commutes with the action.

theorem TauCeti.NormalizedCubicalChain.act_assoc {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {p q r : ℕ} (c : NormalizedCubicalChain Y R p) (a : NormalizedCubicalChain G R q) (b : NormalizedCubicalChain G R r) : (cast R ⋯) (((act Y G R (p + q) r) (((act Y G R p q) c) a)) b) = ((act Y G R p (q + r)) c) (((mul G R q r) a) b)

Strict associativity of the action, after the reindexing (p + q) + r = p + (q + r): (c · a) · b = c · (a b).

theorem TauCeti.NormalizedCubicalChain.act_one {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {p : ℕ} (c : NormalizedCubicalChain Y R p) : (cast R ⋯) (((act Y G R p 0) c) (one G R)) = c

The unit acts trivially, after the reindexing p + 0 = p.

@[simp]

theorem TauCeti.NormalizedCubicalChain.act_one_eq_self {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {p : ℕ} (c : NormalizedCubicalChain Y R p) : ((act Y G R p 0) c) (one G R) = c

The unit law in simp normal form: since p + 0 reduces to p, no reindexing is needed.

structure TauCeti.cubicalChainModule (Y : Type u_1) [TopologicalSpace Y] (_G : Type u_2) (R : Type u_3) [CommRing R] : Type (max u_1 u_3)

The DG right module of cubical chains of a space Y with a right action of G: the direct sum ⨁ n, C^□_n(Y; R), acted on by the chains of G. It is a one-field wrapper around normalizedCubicalChainAlgebra Y R rather than that type itself: for Y = G acting on itself the algebra already acts on itself, and the wrapper keeps the two actions apart. The monoid G is a phantom parameter, recording which action is meant.

• ofSum :: (
• toSum : normalizedCubicalChainAlgebra Y R

  The underlying chain of the direct sum.

• )

@[instance_reducible]

noncomputable instance TauCeti.instAddCommGroupCubicalChainModule (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] (R : Type u_3) [CommRing R] : AddCommGroup (cubicalChainModule Y G R)

The additive group structure, transported from the direct sum.

@[instance_reducible]

noncomputable instance TauCeti.instModuleCubicalChainModule (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] (R : Type u_3) [CommRing R] : Module R (cubicalChainModule Y G R)

The R-module structure, transported from the direct sum.

def TauCeti.cubicalChainModuleEquiv (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] (R : Type u_3) [CommRing R] : cubicalChainModule Y G R ≃ₗ[R] normalizedCubicalChainAlgebra Y R

The module is linearly equivalent to the direct sum of the normalized cubical chains.

noncomputable def TauCeti.cubicalChainModuleLof (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] (R : Type u_3) [CommRing R] (n : ℕ) : NormalizedCubicalChain Y R n →ₗ[R] cubicalChainModule Y G R

The inclusion of the chains of dimension n into the module.

noncomputable def TauCeti.cubicalChainModuleGrading (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] (R : Type u_3) [CommRing R] (i : ℤ) : Submodule R (cubicalChainModule Y G R)

The grading of the module, with C^□_n in cohomological degree -n.

noncomputable def TauCeti.cubicalChainModuleDifferential (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] (R : Type u_3) [CommRing R] : cubicalChainModule Y G R →ₗ[R] cubicalChainModule Y G R

The differential of the module: the boundary.

noncomputable def TauCeti.cubicalChainModuleDesc {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {N : Type u_4} [AddCommMonoid N] [Module R N] (φ : (n : ℕ) → NormalizedCubicalChain Y R n →ₗ[R] N) : cubicalChainModule Y G R →ₗ[R] N

The linear map out of the module given by linear maps out of its homogeneous parts.

@[simp]

theorem TauCeti.cubicalChainModuleEquiv_lof {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {n : ℕ} (c : NormalizedCubicalChain Y R n) : (cubicalChainModuleEquiv Y G R) ((cubicalChainModuleLof Y G R n) c) = (cubicalChainLof Y R n) c

The equivalence with the direct sum sends a homogeneous chain to itself.

@[simp]

theorem TauCeti.cubicalChainModuleEquiv_symm_lof {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {n : ℕ} (c : NormalizedCubicalChain Y R n) : (cubicalChainModuleEquiv Y G R).symm ((cubicalChainLof Y R n) c) = (cubicalChainModuleLof Y G R n) c

The inverse of the equivalence with the direct sum sends a homogeneous chain to itself.

theorem TauCeti.cubicalChainModuleLof_cast {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {n m : ℕ} (h : n = m) (x : NormalizedCubicalChain Y R n) : (cubicalChainModuleLof Y G R m) ((NormalizedCubicalChain.cast R h) x) = (cubicalChainModuleLof Y G R n) x

Reindexing a chain does not change its image in the module.

theorem TauCeti.cubicalChainModule.induction_on {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {motive : cubicalChainModule Y G R → Prop} (m : cubicalChainModule Y G R) (lof : ∀ (n : ℕ) (c : NormalizedCubicalChain Y R n), motive ((cubicalChainModuleLof Y G R n) c)) (add : ∀ (m m' : cubicalChainModule Y G R), motive m → motive m' → motive (m + m')) : motive m

Induction on the module: a property holds for every element once it holds for the homogeneous chains and is closed under sums.

@[simp]

theorem TauCeti.cubicalChainModuleDesc_lof {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {N : Type u_4} [AddCommMonoid N] [Module R N] (φ : (n : ℕ) → NormalizedCubicalChain Y R n →ₗ[R] N) {n : ℕ} (c : NormalizedCubicalChain Y R n) : (cubicalChainModuleDesc φ) ((cubicalChainModuleLof Y G R n) c) = (φ n) c

The linear map given by homogeneous parts, on a homogeneous chain.

theorem TauCeti.cubicalChainModule_linearMap_ext {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {N : Type u_4} [AddCommMonoid N] [Module R N] {f g : cubicalChainModule Y G R →ₗ[R] N} (h : ∀ (n : ℕ) (c : NormalizedCubicalChain Y R n), f ((cubicalChainModuleLof Y G R n) c) = g ((cubicalChainModuleLof Y G R n) c)) : f = g

Two linear maps out of the module agree when they agree on homogeneous chains.

theorem TauCeti.mem_cubicalChainModuleGrading_iff {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {i : ℤ} {m : cubicalChainModule Y G R} : m ∈ cubicalChainModuleGrading Y G R i ↔ m = 0 ∨ ∃ (n : ℕ) (c : NormalizedCubicalChain Y R n), ↑n = -i ∧ (cubicalChainModuleLof Y G R n) c = m

Membership in a graded piece of the module: zero, or a chain of dimension -i.

theorem TauCeti.mem_cubicalChainModuleGrading {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {i : ℤ} {m : cubicalChainModule Y G R} : m ∈ cubicalChainModuleGrading Y G R i ↔ (cubicalChainModuleEquiv Y G R) m ∈ cubicalChainGrading Y R i

Membership in a graded piece of the module is membership of the underlying chain of the direct sum.

theorem TauCeti.cubicalChainModuleLof_mem {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] {n : ℕ} (c : NormalizedCubicalChain Y R n) : (cubicalChainModuleLof Y G R n) c ∈ cubicalChainModuleGrading Y G R (-↑n)

A chain of dimension n lies in cohomological degree -n.

noncomputable def TauCeti.cubicalChainModuleDecompose (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] (R : Type u_3) [CommRing R] : cubicalChainModule Y G R →ₗ[R] DirectSum ℤ fun (i : ℤ) => ↥(cubicalChainModuleGrading Y G R i)

The decomposition of the module along its grading.

@[instance_reducible]

noncomputable instance TauCeti.instDecompositionIntCubicalChainModuleSubmoduleCubicalChainModuleGrading {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] : DirectSum.Decomposition (cubicalChainModuleGrading Y G R)

The module is the internal direct sum of its graded pieces: an element decomposes into its homogeneous chains, the chains of dimension n lying in cohomological degree -n.

@[simp]

theorem TauCeti.cubicalChainModuleDifferential_lof_zero {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] (c : NormalizedCubicalChain Y R 0) : (cubicalChainModuleDifferential Y G R) ((cubicalChainModuleLof Y G R 0) c) = 0

The differential vanishes on 0-chains.

@[simp]

theorem TauCeti.cubicalChainModuleDifferential_lof_succ {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] (k : ℕ) (c : NormalizedCubicalChain Y R (k + 1)) : (cubicalChainModuleDifferential Y G R) ((cubicalChainModuleLof Y G R (k + 1)) c) = (cubicalChainModuleLof Y G R k) ((NormalizedCubicalChain.boundary Y R k) c)

The differential on (k + 1)-chains is the boundary.

theorem TauCeti.cubicalChainModuleEquiv_differential {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] (m : cubicalChainModule Y G R) : (cubicalChainModuleEquiv Y G R) ((cubicalChainModuleDifferential Y G R) m) = (cubicalChainDifferential Y R) ((cubicalChainModuleEquiv Y G R) m)

The differential of the module is the boundary, read through the equivalence with the direct sum.

theorem TauCeti.cubicalChainModuleEquiv_symm_differential {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] (a : normalizedCubicalChainAlgebra Y R) : (cubicalChainModuleEquiv Y G R).symm ((cubicalChainDifferential Y R) a) = (cubicalChainModuleDifferential Y G R) ((cubicalChainModuleEquiv Y G R).symm a)

The inverse of the equivalence with the direct sum intertwines the differentials.

theorem TauCeti.cubicalChainModuleDifferential_isHomogeneous (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] (R : Type u_3) [CommRing R] : LinearMap.IsHomogeneous (cubicalChainModuleDifferential Y G R) (cubicalChainModuleGrading Y G R) (cubicalChainModuleGrading Y G R) 1

The differential of the module raises the cohomological degree by one.

@[simp]

theorem TauCeti.cubicalChainModuleDifferential_cubicalChainModuleDifferential {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] (m : cubicalChainModule Y G R) : (cubicalChainModuleDifferential Y G R) ((cubicalChainModuleDifferential Y G R) m) = 0

The differential of the module squares to zero.

theorem TauCeti.negOnePow_neg_natCast_smul_cubicalChainModule {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] {R : Type u_3} [CommRing R] (n : ℕ) (m : cubicalChainModule Y G R) : (-↑n).negOnePow • m = (-1) ^ n • m

The sign (-1) ^ (-n) acts on the module as (-1) ^ n ∈ R.

noncomputable def TauCeti.cubicalChainActLof (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] (R : Type u_3) [CommRing R] (p q : ℕ) : NormalizedCubicalChain Y R p →ₗ[R] NormalizedCubicalChain G R q →ₗ[R] cubicalChainModule Y G R

The action of a homogeneous chain of G on a homogeneous chain of Y, landing in the module.

noncomputable def TauCeti.cubicalChainActBilin (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] (R : Type u_3) [CommRing R] : cubicalChainModule Y G R →ₗ[R] normalizedCubicalChainAlgebra G R →ₗ[R] cubicalChainModule Y G R

The action as a bilinear map M × A → M, (m, a) ↦ m · a.

@[simp]

theorem TauCeti.cubicalChainActBilin_lof_lof {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {p q : ℕ} (c : NormalizedCubicalChain Y R p) (a : NormalizedCubicalChain G R q) : ((cubicalChainActBilin Y G R) ((cubicalChainModuleLof Y G R p) c)) ((cubicalChainLof G R q) a) = (cubicalChainModuleLof Y G R (p + q)) (((NormalizedCubicalChain.act Y G R p q) c) a)

The action on homogeneous elements.

theorem TauCeti.cubicalChainActBilin_one {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] (m : cubicalChainModule Y G R) : ((cubicalChainActBilin Y G R) m) 1 = m

The unit acts trivially on the module.

theorem TauCeti.cubicalChainActBilin_mul {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] (m : cubicalChainModule Y G R) (a b : normalizedCubicalChainAlgebra G R) : ((cubicalChainActBilin Y G R) m) (a * b) = ((cubicalChainActBilin Y G R) (((cubicalChainActBilin Y G R) m) a)) b

The action is associative: m · (a b) = (m · a) · b.

noncomputable def TauCeti.cubicalChainActHom (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] (R : Type u_3) [CommRing R] : (normalizedCubicalChainAlgebra G R)ᵐᵒᵖ →+* Module.End R (cubicalChainModule Y G R)

The action of the chain algebra of G on the module, as a ring homomorphism from the opposite algebra to the endomorphisms.

@[instance_reducible]

noncomputable instance TauCeti.instModuleMulOppositeNormalizedCubicalChainAlgebraCubicalChainModule (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] (R : Type u_3) [CommRing R] : Module (normalizedCubicalChainAlgebra G R)ᵐᵒᵖ (cubicalChainModule Y G R)

The chains of Y form a right module over the chains of G.

theorem TauCeti.op_smul_cubicalChainModule {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] (a : normalizedCubicalChainAlgebra G R) (m : cubicalChainModule Y G R) : MulOpposite.op a • m = ((cubicalChainActBilin Y G R) m) a

The right action of a chain of G.

@[simp]

theorem TauCeti.op_lof_smul_cubicalChainModuleLof {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {p q : ℕ} (c : NormalizedCubicalChain Y R p) (a : NormalizedCubicalChain G R q) : MulOpposite.op ((cubicalChainLof G R q) a) • (cubicalChainModuleLof Y G R p) c = (cubicalChainModuleLof Y G R (p + q)) (((NormalizedCubicalChain.act Y G R p q) c) a)

The right action of a homogeneous chain of G on a homogeneous chain of Y.

instance TauCeti.instIsScalarTowerMulOppositeNormalizedCubicalChainAlgebraCubicalChainModule {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] : IsScalarTower R (normalizedCubicalChainAlgebra G R)ᵐᵒᵖ (cubicalChainModule Y G R)

The ground ring and the chains of G act compatibly: (r • a) acts as r times the action of a, since the action is bilinear.

instance TauCeti.instGradedSMulIntSubmoduleMulOppositeNormalizedCubicalChainAlgebraCubicalChainModulePieceOppositeOfDecompositionCubicalChainGradingCubicalChainModuleGrading {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] : SetLike.GradedSMul ((InternalGrading.ofDecomposition (cubicalChainGrading G R)).opposite.piece ℤ) (cubicalChainModuleGrading Y G R)

The action is graded: a chain of G of cohomological degree i sends the chains of Y of degree j to degree i + j, as the action adds dimensions.

theorem TauCeti.cubicalChainModuleDifferential_act {Y : Type u_1} {G : Type u_2} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_3} [CommRing R] {m q : ℕ} (c : NormalizedCubicalChain Y R m) (a : NormalizedCubicalChain G R q) : (cubicalChainModuleDifferential Y G R) (MulOpposite.op ((cubicalChainLof G R q) a) • (cubicalChainModuleLof Y G R m) c) = MulOpposite.op ((cubicalChainLof G R q) a) • (cubicalChainModuleDifferential Y G R) ((cubicalChainModuleLof Y G R m) c) + (-↑m).negOnePow • MulOpposite.op ((cubicalChainDifferential G R) ((cubicalChainLof G R q) a)) • (cubicalChainModuleLof Y G R m) c

The graded Leibniz rule for the action on homogeneous chains.

theorem TauCeti.cubicalChainModule_isDGRightModule (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] (R : Type u_3) [CommRing R] : IsDGRightModule ⋯ (cubicalChainModuleGrading Y G R) (cubicalChainModuleDifferential Y G R)

The cubical chains of a space with a right action of a topological monoid G form a differential graded right module over the DG algebra of cubical chains of G.

@[reducible, inline]

noncomputable abbrev TauCeti.cubicalChainModuleDG (Y : Type u_1) (G : Type u_2) [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] (R : Type u_3) [CommRing R] : DGRightModuleCat ⋯

The cubical chains of Y as an object of the category of DG right modules over the chains of G.

noncomputable def TauCeti.cubicalChainModuleLinearMap {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] (R : Type u_2) [CommRing R] (f : C(Y, Y')) : cubicalChainModule Y G R →ₗ[R] cubicalChainModule Y' G R

The R-linear map of modules induced by a continuous map: the push-forward of chains in each dimension, TauCeti.cubicalChainSumMap read through the equivalences with the direct sums.

@[simp]

theorem TauCeti.cubicalChainModuleEquiv_linearMap {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] {R : Type u_2} [CommRing R] (f : C(Y, Y')) (x : cubicalChainModule Y G R) : (cubicalChainModuleEquiv Y' G R) ((cubicalChainModuleLinearMap R f) x) = (cubicalChainSumMap R f) ((cubicalChainModuleEquiv Y G R) x)

The induced map is the push-forward of the direct sums, read through the equivalences.

@[simp]

theorem TauCeti.cubicalChainModuleLinearMap_lof {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] {R : Type u_2} [CommRing R] (f : C(Y, Y')) {n : ℕ} (c : NormalizedCubicalChain Y R n) : (cubicalChainModuleLinearMap R f) ((cubicalChainModuleLof Y G R n) c) = (cubicalChainModuleLof Y' G R n) ((NormalizedCubicalChain.map R f n) c)

The induced map on a homogeneous chain.

theorem TauCeti.cubicalChainModuleLinearMap_op_smul {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] [MulAction Gᵐᵒᵖ Y'] [ContinuousSMul Gᵐᵒᵖ Y'] {R : Type u_2} [CommRing R] (f : C(Y, Y')) (hf : ∀ (g : G) (y : Y), f (MulOpposite.op g • y) = MulOpposite.op g • f y) (a : normalizedCubicalChainAlgebra G R) (x : cubicalChainModule Y G R) : (cubicalChainModuleLinearMap R f) (MulOpposite.op a • x) = MulOpposite.op a • (cubicalChainModuleLinearMap R f) x

The induced map of an equivariant map commutes with the action.

theorem TauCeti.cubicalChainModuleDifferential_linearMap {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] {R : Type u_2} [CommRing R] (f : C(Y, Y')) (x : cubicalChainModule Y G R) : (cubicalChainModuleDifferential Y' G R) ((cubicalChainModuleLinearMap R f) x) = (cubicalChainModuleLinearMap R f) ((cubicalChainModuleDifferential Y G R) x)

The induced map commutes with the differentials.

theorem TauCeti.cubicalChainModuleLinearMap_mem {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] {R : Type u_2} [CommRing R] (f : C(Y, Y')) {i : ℤ} {x : cubicalChainModule Y G R} (hx : x ∈ cubicalChainModuleGrading Y G R i) : (cubicalChainModuleLinearMap R f) x ∈ cubicalChainModuleGrading Y' G R i

The induced map preserves the grading.

noncomputable def TauCeti.cubicalChainModuleMap {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] [MulAction Gᵐᵒᵖ Y'] [ContinuousSMul Gᵐᵒᵖ Y'] (R : Type u_2) [CommRing R] (f : C(Y, Y')) (hf : ∀ (g : G) (y : Y), f (MulOpposite.op g • y) = MulOpposite.op g • f y) : cubicalChainModuleDG Y G R ⟶ cubicalChainModuleDG Y' G R

The morphism of DG right modules induced by an equivariant continuous map f : Y → Y'.

theorem TauCeti.cubicalChainModuleMap_apply {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] [MulAction Gᵐᵒᵖ Y'] [ContinuousSMul Gᵐᵒᵖ Y'] {R : Type u_2} [CommRing R] (f : C(Y, Y')) (hf : ∀ (g : G) (y : Y), f (MulOpposite.op g • y) = MulOpposite.op g • f y) (x : cubicalChainModule Y G R) : (cubicalChainModuleMap R f hf) x = (cubicalChainModuleLinearMap R f) x

The induced morphism is the push-forward of chains.

@[simp]

theorem TauCeti.cubicalChainModuleMap_lof {Y Y' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] [MulAction Gᵐᵒᵖ Y'] [ContinuousSMul Gᵐᵒᵖ Y'] {R : Type u_2} [CommRing R] (f : C(Y, Y')) (hf : ∀ (g : G) (y : Y), f (MulOpposite.op g • y) = MulOpposite.op g • f y) {n : ℕ} (c : NormalizedCubicalChain Y R n) : (cubicalChainModuleMap R f hf) ((cubicalChainModuleLof Y G R n) c) = (cubicalChainModuleLof Y' G R n) ((NormalizedCubicalChain.map R f n) c)

The induced morphism on a homogeneous chain.

@[simp]

theorem TauCeti.cubicalChainModuleLinearMap_id {Y : Type u} {G : Type u_1} [TopologicalSpace Y] {R : Type u_2} [CommRing R] : cubicalChainModuleLinearMap R (ContinuousMap.id Y) = LinearMap.id

The identity map induces the identity.

theorem TauCeti.cubicalChainModuleLinearMap_comp {Y Y' Y'' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] [TopologicalSpace Y''] {R : Type u_2} [CommRing R] (f : C(Y, Y')) (g : C(Y', Y'')) : cubicalChainModuleLinearMap R (g.comp f) = cubicalChainModuleLinearMap R g ∘ₗ cubicalChainModuleLinearMap R f

A composite map induces the composite of the induced maps.

@[simp]

theorem TauCeti.cubicalChainModuleMap_id {Y : Type u} {G : Type u_1} [TopologicalSpace Y] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] {R : Type u_2} [CommRing R] : cubicalChainModuleMap R (ContinuousMap.id Y) ⋯ = CategoryTheory.CategoryStruct.id (cubicalChainModuleDG Y G R)

The identity map induces the identity morphism.

theorem TauCeti.cubicalChainModuleMap_comp {Y Y' Y'' : Type u} {G : Type u_1} [TopologicalSpace Y] [TopologicalSpace Y'] [TopologicalSpace Y''] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [MulAction Gᵐᵒᵖ Y] [ContinuousSMul Gᵐᵒᵖ Y] [MulAction Gᵐᵒᵖ Y'] [ContinuousSMul Gᵐᵒᵖ Y'] [MulAction Gᵐᵒᵖ Y''] [ContinuousSMul Gᵐᵒᵖ Y''] {R : Type u_2} [CommRing R] (f : C(Y, Y')) (g : C(Y', Y'')) (hf : ∀ (a : G) (y : Y), f (MulOpposite.op a • y) = MulOpposite.op a • f y) (hg : ∀ (a : G) (y : Y'), g (MulOpposite.op a • y) = MulOpposite.op a • g y) : cubicalChainModuleMap R (g.comp f) ⋯ = CategoryTheory.CategoryStruct.comp (cubicalChainModuleMap R f hf) (cubicalChainModuleMap R g hg)

A composite of equivariant maps induces the composite of the induced morphisms.