The tensor product of two super modules

For a super-commutative ℂ-algebra S and two modules M, N over it (RS.SuperCommAlgebra.Mod) this file builds the tensor product M ⊗_S N as another S-module, together with the canonical balanced map into it and its universal property.

The underlying ℤ/2-graded ℂ-space is the graded tensor product of RS.SuperVect.tensorObj: the even part of M ⊗_ℂ N is (M₀ ⊗ N₀) × (M₁ ⊗ N₁) and the odd part is (M₀ ⊗ N₁) × (M₁ ⊗ N₀), where M₀ = M.even and M₁ = M.odd. Balancing over S is imposed by quotienting each degree by the span of the relators listed below.

The sign convention

A left module over a super-commutative algebra is a right module under m · a = (−1)^{|a||m|} a · m, and the balancing relation of the tensor product is (m · a) ⊗ n = m ⊗ (a · n). Written with left actions throughout, the relator at homogeneous a, m, n is

(a · m) ⊗ n − (−1)^{|a||m|} m ⊗ (a · n),

so the only sign is a −1 when both the scalar and the left argument are odd; the parity of n never enters. The eight relator families are relEvenXYZ in total degree |a| + |m| + |n| = 0 and relOddXYZ in total degree 1, four each, indexed by the parity pattern (|a|, |m|, |n|).

The S-action on the quotient is the action on the left factor, with no sign: a · (m ⊗ n) = (a · m) ⊗ n. It descends because a · ((b · m) ⊗ n − (−1)^{|b||m|} m ⊗ (b · n)) is (−1)^{|a||b|} times the relator of b at (a · m, n); this is the one place where the super-commutativity of S is used, and it is the reason the construction needs a commutative base.

Contents

• RS.SuperCommAlgebra.Mod.actEE_actEE_comm and its five companions: an even scalar commutes with every scalar, and two odd scalars anticommute, in their action on a module.
• RS.tensorLeftDiag, RS.tensorLeftSwap: the two shapes of a parity block acting on the left factor of a two-summand graded tensor product, degree-preserving and degree-reversing.
• RS.descendAct: descent of a bilinear action along a pair of quotients.
• RS.SuperCommAlgebra.Mod.balEven, balOdd: the balancing submodules, and preActEE, preActEO, preActOE, preActOO: the four action blocks before quotienting, with the ten module laws proved at that level.
• RS.SuperCommAlgebra.Mod.tensor: the tensor product as an S-module.
• RS.SuperCommAlgebra.Mod.tmulEE, tmulEO, tmulOE, tmulOO: the canonical map, with its eight balancing laws and its eight action laws.
• RS.SuperCommAlgebra.Mod.liftEven, liftOdd and liftEven_unique, liftOdd_unique: the universal property, packaged as exists_unique_liftEven and exists_unique_liftOdd.

Parity blocks acting on the left factor

noncomputable def RS.tensorLeftDiag (P : Type u_1) (Q : Type u_2) [AddCommGroup P] [Module ℂ P] [AddCommGroup Q] [Module ℂ Q] {A : Type u_3} {X₁ : Type u_4} {X₂ : Type u_5} {Y₁ : Type u_6} {Y₂ : Type u_7} [AddCommGroup A] [Module ℂ A] [AddCommGroup X₁] [Module ℂ X₁] [AddCommGroup X₂] [Module ℂ X₂] [AddCommGroup Y₁] [Module ℂ Y₁] [AddCommGroup Y₂] [Module ℂ Y₂] (f : A →ₗ[ℂ] X₁ →ₗ[ℂ] X₂) (g : A →ₗ[ℂ] Y₁ →ₗ[ℂ] Y₂) : A →ₗ[ℂ] TensorProduct ℂ X₁ P × TensorProduct ℂ Y₁ Q →ₗ[ℂ] TensorProduct ℂ X₂ P × TensorProduct ℂ Y₂ Q

A pair of parity blocks acting on the left factor of a two-summand graded tensor product, in the degree-preserving pattern: each summand stays where it is.

Equations

• RS.tensorLeftDiag P Q f g = { toFun := fun (a : A) => (LinearMap.rTensor P (f a)).prodMap (LinearMap.rTensor Q (g a)), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.tensorLeftDiag_apply (P : Type u_1) (Q : Type u_2) [AddCommGroup P] [Module ℂ P] [AddCommGroup Q] [Module ℂ Q] {A : Type u_3} {X₁ : Type u_4} {X₂ : Type u_5} {Y₁ : Type u_6} {Y₂ : Type u_7} [AddCommGroup A] [Module ℂ A] [AddCommGroup X₁] [Module ℂ X₁] [AddCommGroup X₂] [Module ℂ X₂] [AddCommGroup Y₁] [Module ℂ Y₁] [AddCommGroup Y₂] [Module ℂ Y₂] (f : A →ₗ[ℂ] X₁ →ₗ[ℂ] X₂) (g : A →ₗ[ℂ] Y₁ →ₗ[ℂ] Y₂) (a : A) (t : TensorProduct ℂ X₁ P × TensorProduct ℂ Y₁ Q) : ((tensorLeftDiag P Q f g) a) t = ((LinearMap.rTensor P (f a)) t.1, (LinearMap.rTensor Q (g a)) t.2)

The degree-preserving block pattern, evaluated.

noncomputable def RS.tensorLeftSwap (P : Type u_1) (Q : Type u_2) [AddCommGroup P] [Module ℂ P] [AddCommGroup Q] [Module ℂ Q] {A : Type u_3} {X₁ : Type u_4} {X₂ : Type u_5} {Y₁ : Type u_6} {Y₂ : Type u_7} [AddCommGroup A] [Module ℂ A] [AddCommGroup X₁] [Module ℂ X₁] [AddCommGroup X₂] [Module ℂ X₂] [AddCommGroup Y₁] [Module ℂ Y₁] [AddCommGroup Y₂] [Module ℂ Y₂] (f : A →ₗ[ℂ] X₁ →ₗ[ℂ] X₂) (g : A →ₗ[ℂ] Y₁ →ₗ[ℂ] Y₂) : A →ₗ[ℂ] TensorProduct ℂ X₁ P × TensorProduct ℂ Y₁ Q →ₗ[ℂ] TensorProduct ℂ Y₂ Q × TensorProduct ℂ X₂ P

A pair of parity blocks acting on the left factor of a two-summand graded tensor product, in the degree-reversing pattern: the two summands are interchanged.

Equations

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

@[simp]

theorem RS.tensorLeftSwap_apply (P : Type u_1) (Q : Type u_2) [AddCommGroup P] [Module ℂ P] [AddCommGroup Q] [Module ℂ Q] {A : Type u_3} {X₁ : Type u_4} {X₂ : Type u_5} {Y₁ : Type u_6} {Y₂ : Type u_7} [AddCommGroup A] [Module ℂ A] [AddCommGroup X₁] [Module ℂ X₁] [AddCommGroup X₂] [Module ℂ X₂] [AddCommGroup Y₁] [Module ℂ Y₁] [AddCommGroup Y₂] [Module ℂ Y₂] (f : A →ₗ[ℂ] X₁ →ₗ[ℂ] X₂) (g : A →ₗ[ℂ] Y₁ →ₗ[ℂ] Y₂) (a : A) (t : TensorProduct ℂ X₁ P × TensorProduct ℂ Y₁ Q) : ((tensorLeftSwap P Q f g) a) t = ((LinearMap.rTensor Q (g a)) t.2, (LinearMap.rTensor P (f a)) t.1)

The degree-reversing block pattern, evaluated.

Descent of an action along a quotient

noncomputable def RS.descendAct {A : Type u_1} {T : Type u_2} {T' : Type u_3} [AddCommGroup A] [Module ℂ A] [AddCommGroup T] [Module ℂ T] [AddCommGroup T'] [Module ℂ T'] (R : Submodule ℂ T) (R' : Submodule ℂ T') (f : A →ₗ[ℂ] T →ₗ[ℂ] T') (h : ∀ (a : A), ∀ t ∈ R, (f a) t ∈ R') : A →ₗ[ℂ] T ⧸ R →ₗ[ℂ] T' ⧸ R'

Descend a bilinear action along a pair of quotients: a bilinear action of A carrying a submodule R of its source into a submodule R' of its target induces an action on the quotients.

Equations

• RS.descendAct R R' f h = (R.liftQ (f.compr₂ R'.mkQ).flip ⋯).flip

@[simp]

theorem RS.descendAct_apply {A : Type u_1} {T : Type u_2} {T' : Type u_3} [AddCommGroup A] [Module ℂ A] [AddCommGroup T] [Module ℂ T] [AddCommGroup T'] [Module ℂ T'] (R : Submodule ℂ T) (R' : Submodule ℂ T') (f : A →ₗ[ℂ] T →ₗ[ℂ] T') (h : ∀ (a : A), ∀ t ∈ R, (f a) t ∈ R') (a : A) (t : T) : ((descendAct R R' f h) a) (Submodule.Quotient.mk t) = Submodule.Quotient.mk ((f a) t)

The descended action, evaluated on a class.

Commutation of the action blocks

theorem RS.SuperCommAlgebra.Mod.actEE_actEE_comm {S : SuperCommAlgebra} (M : S.Mod) (a b : S.even) (m : M.even) : (M.actEE a) ((M.actEE b) m) = (M.actEE b) ((M.actEE a) m)

Two even scalars commute on the even component.

theorem RS.SuperCommAlgebra.Mod.actEO_actEO_comm {S : SuperCommAlgebra} (M : S.Mod) (a b : S.even) (m : M.odd) : (M.actEO a) ((M.actEO b) m) = (M.actEO b) ((M.actEO a) m)

Two even scalars commute on the odd component.

theorem RS.SuperCommAlgebra.Mod.actEO_actOE {S : SuperCommAlgebra} (M : S.Mod) (a : S.even) (c : S.odd) (m : M.even) : (M.actEO a) ((M.actOE c) m) = (M.actOE c) ((M.actEE a) m)

An even scalar commutes with an odd one, on the even component.

theorem RS.SuperCommAlgebra.Mod.actEE_actOO {S : SuperCommAlgebra} (M : S.Mod) (a : S.even) (c : S.odd) (m : M.odd) : (M.actEE a) ((M.actOO c) m) = (M.actOO c) ((M.actEO a) m)

An even scalar commutes with an odd one, on the odd component.

theorem RS.SuperCommAlgebra.Mod.actOO_actOE_neg {S : SuperCommAlgebra} (M : S.Mod) (c d : S.odd) (m : M.even) : (M.actOO c) ((M.actOE d) m) = -(M.actOO d) ((M.actOE c) m)

Two odd scalars anticommute, on the even component.

theorem RS.SuperCommAlgebra.Mod.actOE_actOO_neg {S : SuperCommAlgebra} (M : S.Mod) (c d : S.odd) (m : M.odd) : (M.actOE c) ((M.actOO d) m) = -(M.actOE d) ((M.actOO c) m)

Two odd scalars anticommute, on the odd component.

The graded tensor product over ℂ

@[reducible, inline]

abbrev RS.SuperCommAlgebra.Mod.tenEven {S : SuperCommAlgebra} (M N : S.Mod) : Type (max w w')

The even component of the graded ℂ-tensor product of the underlying super spaces.

Equations

• M.tenEven N = (TensorProduct ℂ M.even N.even × TensorProduct ℂ M.odd N.odd)

@[reducible, inline]

abbrev RS.SuperCommAlgebra.Mod.tenOdd {S : SuperCommAlgebra} (M N : S.Mod) : Type (max w w')

The odd component of the graded ℂ-tensor product of the underlying super spaces.

Equations

• M.tenOdd N = (TensorProduct ℂ M.even N.odd × TensorProduct ℂ M.odd N.even)

The balancing relators

def RS.SuperCommAlgebra.Mod.relEvenEEE {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.even) (n : N.even) : M.tenEven N

The even-degree relator at parity pattern even-even-even.

Equations

• M.relEvenEEE N b m n = ((M.actEE b) m ⊗ₜ[ℂ] n - m ⊗ₜ[ℂ] (N.actEE b) n, 0)

def RS.SuperCommAlgebra.Mod.relEvenEOO {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.odd) (n : N.odd) : M.tenEven N

The even-degree relator at parity pattern even-odd-odd.

Equations

• M.relEvenEOO N b m n = (0, (M.actEO b) m ⊗ₜ[ℂ] n - m ⊗ₜ[ℂ] (N.actEO b) n)

def RS.SuperCommAlgebra.Mod.relEvenOEO {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.odd) : M.tenEven N

The even-degree relator at parity pattern odd-even-odd. The scalar is odd and the left argument even, so the Koszul sign is +1.

Equations

• M.relEvenOEO N c m n = (-m ⊗ₜ[ℂ] (N.actOO c) n, (M.actOE c) m ⊗ₜ[ℂ] n)

def RS.SuperCommAlgebra.Mod.relEvenOOE {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.even) : M.tenEven N

The even-degree relator at parity pattern odd-odd-even. Both the scalar and the left argument are odd, so the Koszul sign is −1 and the two terms are added.

Equations

• M.relEvenOOE N c m n = ((M.actOO c) m ⊗ₜ[ℂ] n, m ⊗ₜ[ℂ] (N.actOE c) n)

def RS.SuperCommAlgebra.Mod.relOddEEO {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.even) (n : N.odd) : M.tenOdd N

The odd-degree relator at parity pattern even-even-odd.

Equations

• M.relOddEEO N b m n = ((M.actEE b) m ⊗ₜ[ℂ] n - m ⊗ₜ[ℂ] (N.actEO b) n, 0)

def RS.SuperCommAlgebra.Mod.relOddEOE {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.odd) (n : N.even) : M.tenOdd N

The odd-degree relator at parity pattern even-odd-even.

Equations

• M.relOddEOE N b m n = (0, (M.actEO b) m ⊗ₜ[ℂ] n - m ⊗ₜ[ℂ] (N.actEE b) n)

def RS.SuperCommAlgebra.Mod.relOddOEE {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.even) : M.tenOdd N

The odd-degree relator at parity pattern odd-even-even. The Koszul sign is +1.

Equations

• M.relOddOEE N c m n = (-m ⊗ₜ[ℂ] (N.actOE c) n, (M.actOE c) m ⊗ₜ[ℂ] n)

def RS.SuperCommAlgebra.Mod.relOddOOO {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.odd) : M.tenOdd N

The odd-degree relator at parity pattern odd-odd-odd. The Koszul sign is −1.

Equations

• M.relOddOOO N c m n = ((M.actOO c) m ⊗ₜ[ℂ] n, m ⊗ₜ[ℂ] (N.actOO c) n)

def RS.SuperCommAlgebra.Mod.balEven {S : SuperCommAlgebra} (M N : S.Mod) : Submodule ℂ (M.tenEven N)

The balancing submodule in even degree: the span of the four even-degree relator families.

Equations

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

def RS.SuperCommAlgebra.Mod.balOdd {S : SuperCommAlgebra} (M N : S.Mod) : Submodule ℂ (M.tenOdd N)

The balancing submodule in odd degree: the span of the four odd-degree relator families.

Equations

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

theorem RS.SuperCommAlgebra.Mod.relEvenEEE_mem {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.even) (n : N.even) : M.relEvenEEE N b m n ∈ M.balEven N

The even-even-even relators are balanced.

theorem RS.SuperCommAlgebra.Mod.relEvenEOO_mem {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.odd) (n : N.odd) : M.relEvenEOO N b m n ∈ M.balEven N

The even-odd-odd relators are balanced.

theorem RS.SuperCommAlgebra.Mod.relEvenOEO_mem {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.odd) : M.relEvenOEO N c m n ∈ M.balEven N

The odd-even-odd relators are balanced.

theorem RS.SuperCommAlgebra.Mod.relEvenOOE_mem {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.even) : M.relEvenOOE N c m n ∈ M.balEven N

The odd-odd-even relators are balanced.

theorem RS.SuperCommAlgebra.Mod.relOddEEO_mem {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.even) (n : N.odd) : M.relOddEEO N b m n ∈ M.balOdd N

The even-even-odd relators are balanced.

theorem RS.SuperCommAlgebra.Mod.relOddEOE_mem {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.odd) (n : N.even) : M.relOddEOE N b m n ∈ M.balOdd N

The even-odd-even relators are balanced.

theorem RS.SuperCommAlgebra.Mod.relOddOEE_mem {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.even) : M.relOddOEE N c m n ∈ M.balOdd N

The odd-even-even relators are balanced.

theorem RS.SuperCommAlgebra.Mod.relOddOOO_mem {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.odd) : M.relOddOOO N c m n ∈ M.balOdd N

The odd-odd-odd relators are balanced.

theorem RS.SuperCommAlgebra.Mod.relEvenOEO_neg_mem {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.odd) : (m ⊗ₜ[ℂ] (N.actOO c) n, -(M.actOE c) m ⊗ₜ[ℂ] n) ∈ M.balEven N

The negated odd-even-odd relators, in expanded form.

theorem RS.SuperCommAlgebra.Mod.relEvenOOE_neg_mem {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.even) : (-(M.actOO c) m ⊗ₜ[ℂ] n, -m ⊗ₜ[ℂ] (N.actOE c) n) ∈ M.balEven N

The negated odd-odd-even relators, in expanded form.

theorem RS.SuperCommAlgebra.Mod.relOddOEE_neg_mem {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.even) : (m ⊗ₜ[ℂ] (N.actOE c) n, -(M.actOE c) m ⊗ₜ[ℂ] n) ∈ M.balOdd N

The negated odd-even-even relators, in expanded form.

theorem RS.SuperCommAlgebra.Mod.relOddOOO_neg_mem {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.odd) : (-(M.actOO c) m ⊗ₜ[ℂ] n, -m ⊗ₜ[ℂ] (N.actOO c) n) ∈ M.balOdd N

The negated odd-odd-odd relators, in expanded form.

The four action blocks before quotienting

noncomputable def RS.SuperCommAlgebra.Mod.preActEE {S : SuperCommAlgebra} (M N : S.Mod) : S.even →ₗ[ℂ] M.tenEven N →ₗ[ℂ] M.tenEven N

An even scalar acting on the left factor of the even part.

Equations

• M.preActEE N = RS.tensorLeftDiag N.even N.odd M.actEE M.actEO

noncomputable def RS.SuperCommAlgebra.Mod.preActEO {S : SuperCommAlgebra} (M N : S.Mod) : S.even →ₗ[ℂ] M.tenOdd N →ₗ[ℂ] M.tenOdd N

An even scalar acting on the left factor of the odd part.

Equations

• M.preActEO N = RS.tensorLeftDiag N.odd N.even M.actEE M.actEO

noncomputable def RS.SuperCommAlgebra.Mod.preActOE {S : SuperCommAlgebra} (M N : S.Mod) : S.odd →ₗ[ℂ] M.tenEven N →ₗ[ℂ] M.tenOdd N

An odd scalar acting on the left factor of the even part.

Equations

• M.preActOE N = RS.tensorLeftSwap N.even N.odd M.actOE M.actOO

noncomputable def RS.SuperCommAlgebra.Mod.preActOO {S : SuperCommAlgebra} (M N : S.Mod) : S.odd →ₗ[ℂ] M.tenOdd N →ₗ[ℂ] M.tenEven N

An odd scalar acting on the left factor of the odd part.

Equations

• M.preActOO N = RS.tensorLeftSwap N.odd N.even M.actOE M.actOO

@[simp]

theorem RS.SuperCommAlgebra.Mod.preActEE_apply {S : SuperCommAlgebra} (M N : S.Mod) (a : S.even) (t : M.tenEven N) : ((M.preActEE N) a) t = ((LinearMap.rTensor N.even (M.actEE a)) t.1, (LinearMap.rTensor N.odd (M.actEO a)) t.2)

The even-even block, evaluated.

@[simp]

theorem RS.SuperCommAlgebra.Mod.preActEO_apply {S : SuperCommAlgebra} (M N : S.Mod) (a : S.even) (t : M.tenOdd N) : ((M.preActEO N) a) t = ((LinearMap.rTensor N.odd (M.actEE a)) t.1, (LinearMap.rTensor N.even (M.actEO a)) t.2)

The even-odd block, evaluated.

@[simp]

theorem RS.SuperCommAlgebra.Mod.preActOE_apply {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (t : M.tenEven N) : ((M.preActOE N) c) t = ((LinearMap.rTensor N.odd (M.actOO c)) t.2, (LinearMap.rTensor N.even (M.actOE c)) t.1)

The odd-even block, evaluated.

@[simp]

theorem RS.SuperCommAlgebra.Mod.preActOO_apply {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (t : M.tenOdd N) : ((M.preActOO N) c) t = ((LinearMap.rTensor N.even (M.actOO c)) t.2, (LinearMap.rTensor N.odd (M.actOE c)) t.1)

The odd-odd block, evaluated.

The module laws before quotienting

theorem RS.SuperCommAlgebra.Mod.preActEE_one {S : SuperCommAlgebra} (M N : S.Mod) (t : M.tenEven N) : ((M.preActEE N) S.one) t = t

The unit acts as the identity on the even part.

theorem RS.SuperCommAlgebra.Mod.preActEO_one {S : SuperCommAlgebra} (M N : S.Mod) (t : M.tenOdd N) : ((M.preActEO N) S.one) t = t

The unit acts as the identity on the odd part.

theorem RS.SuperCommAlgebra.Mod.preActEE_mulEE {S : SuperCommAlgebra} (M N : S.Mod) (x y : S.even) (t : M.tenEven N) : ((M.preActEE N) ((S.mulEE x) y)) t = ((M.preActEE N) x) (((M.preActEE N) y) t)

Associativity at parity pattern even-even-even.

theorem RS.SuperCommAlgebra.Mod.preActEO_mulEE {S : SuperCommAlgebra} (M N : S.Mod) (x y : S.even) (t : M.tenOdd N) : ((M.preActEO N) ((S.mulEE x) y)) t = ((M.preActEO N) x) (((M.preActEO N) y) t)

Associativity at parity pattern even-even-odd.

theorem RS.SuperCommAlgebra.Mod.preActOE_mulEO {S : SuperCommAlgebra} (M N : S.Mod) (x : S.even) (u : S.odd) (t : M.tenEven N) : ((M.preActOE N) ((S.mulEO x) u)) t = ((M.preActEO N) x) (((M.preActOE N) u) t)

Associativity at parity pattern even-odd-even.

theorem RS.SuperCommAlgebra.Mod.preActOO_mulEO {S : SuperCommAlgebra} (M N : S.Mod) (x : S.even) (u : S.odd) (t : M.tenOdd N) : ((M.preActOO N) ((S.mulEO x) u)) t = ((M.preActEE N) x) (((M.preActOO N) u) t)

Associativity at parity pattern even-odd-odd.

theorem RS.SuperCommAlgebra.Mod.preActOE_mulOE {S : SuperCommAlgebra} (M N : S.Mod) (u : S.odd) (x : S.even) (t : M.tenEven N) : ((M.preActOE N) ((S.mulOE u) x)) t = ((M.preActOE N) u) (((M.preActEE N) x) t)

Associativity at parity pattern odd-even-even.

theorem RS.SuperCommAlgebra.Mod.preActOO_mulOE {S : SuperCommAlgebra} (M N : S.Mod) (u : S.odd) (x : S.even) (t : M.tenOdd N) : ((M.preActOO N) ((S.mulOE u) x)) t = ((M.preActOO N) u) (((M.preActEO N) x) t)

Associativity at parity pattern odd-even-odd.

theorem RS.SuperCommAlgebra.Mod.preActEE_mulOO {S : SuperCommAlgebra} (M N : S.Mod) (u v : S.odd) (t : M.tenEven N) : ((M.preActEE N) ((S.mulOO u) v)) t = ((M.preActOO N) u) (((M.preActOE N) v) t)

Associativity at parity pattern odd-odd-even.

theorem RS.SuperCommAlgebra.Mod.preActEO_mulOO {S : SuperCommAlgebra} (M N : S.Mod) (u v : S.odd) (t : M.tenOdd N) : ((M.preActEO N) ((S.mulOO u) v)) t = ((M.preActOE N) u) (((M.preActOO N) v) t)

Associativity at parity pattern odd-odd-odd.

The blocks preserve balancing

theorem RS.SuperCommAlgebra.Mod.preActEE_mem_balEven {S : SuperCommAlgebra} (M N : S.Mod) (a : S.even) (t : M.tenEven N) (ht : t ∈ M.balEven N) : ((M.preActEE N) a) t ∈ M.balEven N

An even scalar carries the even balancing submodule into itself.

theorem RS.SuperCommAlgebra.Mod.preActEO_mem_balOdd {S : SuperCommAlgebra} (M N : S.Mod) (a : S.even) (t : M.tenOdd N) (ht : t ∈ M.balOdd N) : ((M.preActEO N) a) t ∈ M.balOdd N

An even scalar carries the odd balancing submodule into itself.

theorem RS.SuperCommAlgebra.Mod.preActOE_mem_balOdd {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (t : M.tenEven N) (ht : t ∈ M.balEven N) : ((M.preActOE N) c) t ∈ M.balOdd N

An odd scalar carries the even balancing submodule into the odd one.

theorem RS.SuperCommAlgebra.Mod.preActOO_mem_balEven {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (t : M.tenOdd N) (ht : t ∈ M.balOdd N) : ((M.preActOO N) c) t ∈ M.balEven N

An odd scalar carries the odd balancing submodule into the even one.

The tensor product

noncomputable def RS.SuperCommAlgebra.Mod.tensor {S : SuperCommAlgebra} (M N : S.Mod) : S.Mod

The tensor product of two super modules over a super-commutative ℂ-algebra: the graded ℂ-tensor product of the underlying super spaces, quotiented in each degree by the balancing relators, with the S-action induced from the action on the left factor.

Equations

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

The canonical balanced map

noncomputable def RS.SuperCommAlgebra.Mod.tmulEE {S : SuperCommAlgebra} (M N : S.Mod) : M.even →ₗ[ℂ] N.even →ₗ[ℂ] (M.tensor N).even

The canonical map, even times even.

Equations

• M.tmulEE N = (TensorProduct.mk ℂ M.even N.even).compr₂ ((M.balEven N).mkQ ∘ₗ LinearMap.inl ℂ (TensorProduct ℂ M.even N.even) (TensorProduct ℂ M.odd N.odd))

noncomputable def RS.SuperCommAlgebra.Mod.tmulOO {S : SuperCommAlgebra} (M N : S.Mod) : M.odd →ₗ[ℂ] N.odd →ₗ[ℂ] (M.tensor N).even

The canonical map, odd times odd.

Equations

• M.tmulOO N = (TensorProduct.mk ℂ M.odd N.odd).compr₂ ((M.balEven N).mkQ ∘ₗ LinearMap.inr ℂ (TensorProduct ℂ M.even N.even) (TensorProduct ℂ M.odd N.odd))

noncomputable def RS.SuperCommAlgebra.Mod.tmulEO {S : SuperCommAlgebra} (M N : S.Mod) : M.even →ₗ[ℂ] N.odd →ₗ[ℂ] (M.tensor N).odd

The canonical map, even times odd.

Equations

• M.tmulEO N = (TensorProduct.mk ℂ M.even N.odd).compr₂ ((M.balOdd N).mkQ ∘ₗ LinearMap.inl ℂ (TensorProduct ℂ M.even N.odd) (TensorProduct ℂ M.odd N.even))

noncomputable def RS.SuperCommAlgebra.Mod.tmulOE {S : SuperCommAlgebra} (M N : S.Mod) : M.odd →ₗ[ℂ] N.even →ₗ[ℂ] (M.tensor N).odd

The canonical map, odd times even.

Equations

• M.tmulOE N = (TensorProduct.mk ℂ M.odd N.even).compr₂ ((M.balOdd N).mkQ ∘ₗ LinearMap.inr ℂ (TensorProduct ℂ M.even N.odd) (TensorProduct ℂ M.odd N.even))

theorem RS.SuperCommAlgebra.Mod.tmulEE_apply {S : SuperCommAlgebra} (M N : S.Mod) (m : M.even) (n : N.even) : ((M.tmulEE N) m) n = Submodule.Quotient.mk (m ⊗ₜ[ℂ] n, 0)

The even-even canonical map, evaluated. Not a simp lemma: the quotient class is the implementation, and tmulEE is the interface the computation rules downstream are stated in.

theorem RS.SuperCommAlgebra.Mod.tmulOO_apply {S : SuperCommAlgebra} (M N : S.Mod) (m : M.odd) (n : N.odd) : ((M.tmulOO N) m) n = Submodule.Quotient.mk (0, m ⊗ₜ[ℂ] n)

The odd-odd canonical map, evaluated. Not a simp lemma, for the reason given at tmulEE_apply.

theorem RS.SuperCommAlgebra.Mod.tmulEO_apply {S : SuperCommAlgebra} (M N : S.Mod) (m : M.even) (n : N.odd) : ((M.tmulEO N) m) n = Submodule.Quotient.mk (m ⊗ₜ[ℂ] n, 0)

The even-odd canonical map, evaluated. Not a simp lemma, for the reason given at tmulEE_apply.

theorem RS.SuperCommAlgebra.Mod.tmulOE_apply {S : SuperCommAlgebra} (M N : S.Mod) (m : M.odd) (n : N.even) : ((M.tmulOE N) m) n = Submodule.Quotient.mk (0, m ⊗ₜ[ℂ] n)

The odd-even canonical map, evaluated. Not a simp lemma, for the reason given at tmulEE_apply.

Balancing

theorem RS.SuperCommAlgebra.Mod.tmulEE_balanced_eee {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.even) (n : N.even) : ((M.tmulEE N) ((M.actEE b) m)) n = ((M.tmulEE N) m) ((N.actEE b) n)

Balancing at parity pattern even-even-even.

theorem RS.SuperCommAlgebra.Mod.tmulOO_balanced_eoo {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.odd) (n : N.odd) : ((M.tmulOO N) ((M.actEO b) m)) n = ((M.tmulOO N) m) ((N.actEO b) n)

Balancing at parity pattern even-odd-odd.

theorem RS.SuperCommAlgebra.Mod.tmulOO_balanced_oeo {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.odd) : ((M.tmulOO N) ((M.actOE c) m)) n = ((M.tmulEE N) m) ((N.actOO c) n)

Balancing at parity pattern odd-even-odd.

theorem RS.SuperCommAlgebra.Mod.tmulEE_balanced_ooe {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.even) : ((M.tmulEE N) ((M.actOO c) m)) n = -((M.tmulOO N) m) ((N.actOE c) n)

Balancing at parity pattern odd-odd-even: both arguments are odd, so the Koszul sign appears.

theorem RS.SuperCommAlgebra.Mod.tmulEO_balanced_eeo {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.even) (n : N.odd) : ((M.tmulEO N) ((M.actEE b) m)) n = ((M.tmulEO N) m) ((N.actEO b) n)

Balancing at parity pattern even-even-odd.

theorem RS.SuperCommAlgebra.Mod.tmulOE_balanced_eoe {S : SuperCommAlgebra} (M N : S.Mod) (b : S.even) (m : M.odd) (n : N.even) : ((M.tmulOE N) ((M.actEO b) m)) n = ((M.tmulOE N) m) ((N.actEE b) n)

Balancing at parity pattern even-odd-even.

theorem RS.SuperCommAlgebra.Mod.tmulOE_balanced_oee {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.even) : ((M.tmulOE N) ((M.actOE c) m)) n = ((M.tmulEO N) m) ((N.actOE c) n)

Balancing at parity pattern odd-even-even.

theorem RS.SuperCommAlgebra.Mod.tmulEO_balanced_ooo {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.odd) : ((M.tmulEO N) ((M.actOO c) m)) n = -((M.tmulOE N) m) ((N.actOO c) n)

Balancing at parity pattern odd-odd-odd: both arguments are odd, so the Koszul sign appears.

The action on the canonical map

theorem RS.SuperCommAlgebra.Mod.actEE_tmulEE {S : SuperCommAlgebra} (M N : S.Mod) (a : S.even) (m : M.even) (n : N.even) : ((M.tensor N).actEE a) (((M.tmulEE N) m) n) = ((M.tmulEE N) ((M.actEE a) m)) n

An even scalar acts on the left factor, even times even.

theorem RS.SuperCommAlgebra.Mod.actEE_tmulOO {S : SuperCommAlgebra} (M N : S.Mod) (a : S.even) (m : M.odd) (n : N.odd) : ((M.tensor N).actEE a) (((M.tmulOO N) m) n) = ((M.tmulOO N) ((M.actEO a) m)) n

An even scalar acts on the left factor, odd times odd.

theorem RS.SuperCommAlgebra.Mod.actEO_tmulEO {S : SuperCommAlgebra} (M N : S.Mod) (a : S.even) (m : M.even) (n : N.odd) : ((M.tensor N).actEO a) (((M.tmulEO N) m) n) = ((M.tmulEO N) ((M.actEE a) m)) n

An even scalar acts on the left factor, even times odd.

theorem RS.SuperCommAlgebra.Mod.actEO_tmulOE {S : SuperCommAlgebra} (M N : S.Mod) (a : S.even) (m : M.odd) (n : N.even) : ((M.tensor N).actEO a) (((M.tmulOE N) m) n) = ((M.tmulOE N) ((M.actEO a) m)) n

An even scalar acts on the left factor, odd times even.

theorem RS.SuperCommAlgebra.Mod.actOE_tmulEE {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.even) : ((M.tensor N).actOE c) (((M.tmulEE N) m) n) = ((M.tmulOE N) ((M.actOE c) m)) n

An odd scalar acts on the left factor, even times even.

theorem RS.SuperCommAlgebra.Mod.actOE_tmulOO {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.odd) : ((M.tensor N).actOE c) (((M.tmulOO N) m) n) = ((M.tmulEO N) ((M.actOO c) m)) n

An odd scalar acts on the left factor, odd times odd.

theorem RS.SuperCommAlgebra.Mod.actOO_tmulEO {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.even) (n : N.odd) : ((M.tensor N).actOO c) (((M.tmulEO N) m) n) = ((M.tmulOO N) ((M.actOE c) m)) n

An odd scalar acts on the left factor, even times odd.

theorem RS.SuperCommAlgebra.Mod.actOO_tmulOE {S : SuperCommAlgebra} (M N : S.Mod) (c : S.odd) (m : M.odd) (n : N.even) : ((M.tensor N).actOO c) (((M.tmulOE N) m) n) = ((M.tmulEE N) ((M.actOO c) m)) n

An odd scalar acts on the left factor, odd times even.

The universal property

noncomputable def RS.SuperCommAlgebra.Mod.liftEven {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (fee : M.even →ₗ[ℂ] N.even →ₗ[ℂ] P) (foo : M.odd →ₗ[ℂ] N.odd →ₗ[ℂ] P) (hee : ∀ (b : S.even) (m : M.even) (n : N.even), (fee ((M.actEE b) m)) n = (fee m) ((N.actEE b) n)) (hoo : ∀ (b : S.even) (m : M.odd) (n : N.odd), (foo ((M.actEO b) m)) n = (foo m) ((N.actEO b) n)) (hoeo : ∀ (c : S.odd) (m : M.even) (n : N.odd), (foo ((M.actOE c) m)) n = (fee m) ((N.actOO c) n)) (hooe : ∀ (c : S.odd) (m : M.odd) (n : N.even), (fee ((M.actOO c) m)) n = -(foo m) ((N.actOE c) n)) : (M.tensor N).even →ₗ[ℂ] P

The even-degree lift: a pair of ℂ-bilinear maps out of the even-even and odd-odd blocks, balanced against the four even-degree relator families, factors through the even part of the tensor product.

Equations

• M.liftEven N fee foo hee hoo hoeo hooe = (M.balEven N).liftQ ((TensorProduct.lift fee).coprod (TensorProduct.lift foo)) ⋯

noncomputable def RS.SuperCommAlgebra.Mod.liftOdd {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (feo : M.even →ₗ[ℂ] N.odd →ₗ[ℂ] P) (foe : M.odd →ₗ[ℂ] N.even →ₗ[ℂ] P) (heeo : ∀ (b : S.even) (m : M.even) (n : N.odd), (feo ((M.actEE b) m)) n = (feo m) ((N.actEO b) n)) (heoe : ∀ (b : S.even) (m : M.odd) (n : N.even), (foe ((M.actEO b) m)) n = (foe m) ((N.actEE b) n)) (hoee : ∀ (c : S.odd) (m : M.even) (n : N.even), (foe ((M.actOE c) m)) n = (feo m) ((N.actOE c) n)) (hooo : ∀ (c : S.odd) (m : M.odd) (n : N.odd), (feo ((M.actOO c) m)) n = -(foe m) ((N.actOO c) n)) : (M.tensor N).odd →ₗ[ℂ] P

The odd-degree lift: a pair of ℂ-bilinear maps out of the even-odd and odd-even blocks, balanced against the four odd-degree relator families, factors through the odd part of the tensor product.

Equations

• M.liftOdd N feo foe heeo heoe hoee hooo = (M.balOdd N).liftQ ((TensorProduct.lift feo).coprod (TensorProduct.lift foe)) ⋯

@[simp]

theorem RS.SuperCommAlgebra.Mod.liftEven_tmulEE {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (fee : M.even →ₗ[ℂ] N.even →ₗ[ℂ] P) (foo : M.odd →ₗ[ℂ] N.odd →ₗ[ℂ] P) (hee : ∀ (b : S.even) (m : M.even) (n : N.even), (fee ((M.actEE b) m)) n = (fee m) ((N.actEE b) n)) (hoo : ∀ (b : S.even) (m : M.odd) (n : N.odd), (foo ((M.actEO b) m)) n = (foo m) ((N.actEO b) n)) (hoeo : ∀ (c : S.odd) (m : M.even) (n : N.odd), (foo ((M.actOE c) m)) n = (fee m) ((N.actOO c) n)) (hooe : ∀ (c : S.odd) (m : M.odd) (n : N.even), (fee ((M.actOO c) m)) n = -(foo m) ((N.actOE c) n)) (m : M.even) (n : N.even) : (M.liftEven N fee foo hee hoo hoeo hooe) (((M.tmulEE N) m) n) = (fee m) n

The even-degree lift computes on even-even products.

@[simp]

theorem RS.SuperCommAlgebra.Mod.liftEven_tmulOO {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (fee : M.even →ₗ[ℂ] N.even →ₗ[ℂ] P) (foo : M.odd →ₗ[ℂ] N.odd →ₗ[ℂ] P) (hee : ∀ (b : S.even) (m : M.even) (n : N.even), (fee ((M.actEE b) m)) n = (fee m) ((N.actEE b) n)) (hoo : ∀ (b : S.even) (m : M.odd) (n : N.odd), (foo ((M.actEO b) m)) n = (foo m) ((N.actEO b) n)) (hoeo : ∀ (c : S.odd) (m : M.even) (n : N.odd), (foo ((M.actOE c) m)) n = (fee m) ((N.actOO c) n)) (hooe : ∀ (c : S.odd) (m : M.odd) (n : N.even), (fee ((M.actOO c) m)) n = -(foo m) ((N.actOE c) n)) (m : M.odd) (n : N.odd) : (M.liftEven N fee foo hee hoo hoeo hooe) (((M.tmulOO N) m) n) = (foo m) n

The even-degree lift computes on odd-odd products.

@[simp]

theorem RS.SuperCommAlgebra.Mod.liftOdd_tmulEO {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (feo : M.even →ₗ[ℂ] N.odd →ₗ[ℂ] P) (foe : M.odd →ₗ[ℂ] N.even →ₗ[ℂ] P) (heeo : ∀ (b : S.even) (m : M.even) (n : N.odd), (feo ((M.actEE b) m)) n = (feo m) ((N.actEO b) n)) (heoe : ∀ (b : S.even) (m : M.odd) (n : N.even), (foe ((M.actEO b) m)) n = (foe m) ((N.actEE b) n)) (hoee : ∀ (c : S.odd) (m : M.even) (n : N.even), (foe ((M.actOE c) m)) n = (feo m) ((N.actOE c) n)) (hooo : ∀ (c : S.odd) (m : M.odd) (n : N.odd), (feo ((M.actOO c) m)) n = -(foe m) ((N.actOO c) n)) (m : M.even) (n : N.odd) : (M.liftOdd N feo foe heeo heoe hoee hooo) (((M.tmulEO N) m) n) = (feo m) n

The odd-degree lift computes on even-odd products.

@[simp]

theorem RS.SuperCommAlgebra.Mod.liftOdd_tmulOE {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (feo : M.even →ₗ[ℂ] N.odd →ₗ[ℂ] P) (foe : M.odd →ₗ[ℂ] N.even →ₗ[ℂ] P) (heeo : ∀ (b : S.even) (m : M.even) (n : N.odd), (feo ((M.actEE b) m)) n = (feo m) ((N.actEO b) n)) (heoe : ∀ (b : S.even) (m : M.odd) (n : N.even), (foe ((M.actEO b) m)) n = (foe m) ((N.actEE b) n)) (hoee : ∀ (c : S.odd) (m : M.even) (n : N.even), (foe ((M.actOE c) m)) n = (feo m) ((N.actOE c) n)) (hooo : ∀ (c : S.odd) (m : M.odd) (n : N.odd), (feo ((M.actOO c) m)) n = -(foe m) ((N.actOO c) n)) (m : M.odd) (n : N.even) : (M.liftOdd N feo foe heeo heoe hoee hooo) (((M.tmulOE N) m) n) = (foe m) n

The odd-degree lift computes on odd-even products.

theorem RS.SuperCommAlgebra.Mod.liftEven_unique {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (g g' : (M.tensor N).even →ₗ[ℂ] P) (hE : ∀ (m : M.even) (n : N.even), g (((M.tmulEE N) m) n) = g' (((M.tmulEE N) m) n)) (hO : ∀ (m : M.odd) (n : N.odd), g (((M.tmulOO N) m) n) = g' (((M.tmulOO N) m) n)) : g = g'

Uniqueness in even degree: the even part of the tensor product is generated by the even-even and odd-odd products.

theorem RS.SuperCommAlgebra.Mod.liftOdd_unique {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (g g' : (M.tensor N).odd →ₗ[ℂ] P) (hE : ∀ (m : M.even) (n : N.odd), g (((M.tmulEO N) m) n) = g' (((M.tmulEO N) m) n)) (hO : ∀ (m : M.odd) (n : N.even), g (((M.tmulOE N) m) n) = g' (((M.tmulOE N) m) n)) : g = g'

Uniqueness in odd degree: the odd part of the tensor product is generated by the even-odd and odd-even products.

theorem RS.SuperCommAlgebra.Mod.exists_unique_liftEven {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (fee : M.even →ₗ[ℂ] N.even →ₗ[ℂ] P) (foo : M.odd →ₗ[ℂ] N.odd →ₗ[ℂ] P) (hee : ∀ (b : S.even) (m : M.even) (n : N.even), (fee ((M.actEE b) m)) n = (fee m) ((N.actEE b) n)) (hoo : ∀ (b : S.even) (m : M.odd) (n : N.odd), (foo ((M.actEO b) m)) n = (foo m) ((N.actEO b) n)) (hoeo : ∀ (c : S.odd) (m : M.even) (n : N.odd), (foo ((M.actOE c) m)) n = (fee m) ((N.actOO c) n)) (hooe : ∀ (c : S.odd) (m : M.odd) (n : N.even), (fee ((M.actOO c) m)) n = -(foo m) ((N.actOE c) n)) : ∃! g : (M.tensor N).even →ₗ[ℂ] P, (∀ (m : M.even) (n : N.even), g (((M.tmulEE N) m) n) = (fee m) n) ∧ ∀ (m : M.odd) (n : N.odd), g (((M.tmulOO N) m) n) = (foo m) n

The universal property in even degree: a balanced pair of ℂ-bilinear maps out of the even-even and odd-odd blocks factors uniquely through the even part of the tensor product.

theorem RS.SuperCommAlgebra.Mod.exists_unique_liftOdd {S : SuperCommAlgebra} (M N : S.Mod) {P : Type v} [AddCommGroup P] [Module ℂ P] (feo : M.even →ₗ[ℂ] N.odd →ₗ[ℂ] P) (foe : M.odd →ₗ[ℂ] N.even →ₗ[ℂ] P) (heeo : ∀ (b : S.even) (m : M.even) (n : N.odd), (feo ((M.actEE b) m)) n = (feo m) ((N.actEO b) n)) (heoe : ∀ (b : S.even) (m : M.odd) (n : N.even), (foe ((M.actEO b) m)) n = (foe m) ((N.actEE b) n)) (hoee : ∀ (c : S.odd) (m : M.even) (n : N.even), (foe ((M.actOE c) m)) n = (feo m) ((N.actOE c) n)) (hooo : ∀ (c : S.odd) (m : M.odd) (n : N.odd), (feo ((M.actOO c) m)) n = -(foe m) ((N.actOO c) n)) : ∃! g : (M.tensor N).odd →ₗ[ℂ] P, (∀ (m : M.even) (n : N.odd), g (((M.tmulEO N) m) n) = (feo m) n) ∧ ∀ (m : M.odd) (n : N.even), g (((M.tmulOE N) m) n) = (foe m) n

The universal property in odd degree: a balanced pair of ℂ-bilinear maps out of the even-odd and odd-even blocks factors uniquely through the odd part of the tensor product.