Generators and products of generators of the symmetric algebra

SymmetricAlgebra R M is generated as an algebra by the image of ι R M, and the range of a lift is the subalgebra its generators' images generate. TensorAlgebra.symRingCon_le identifies the ring congruences containing TensorAlgebra.symRingCon, and TensorAlgebra.symRingCon_toAddCon_le_ker says which additive maps out of the tensor algebra descend to the symmetric algebra. SymmetricAlgebra.ιMulti R M κ multiplies κ-indexed generators; its span is the Fintype.card κ-th power of the submodule LinearMap.range (ι R M) (SymmetricAlgebra.span_range_ιMulti), as for ExteriorAlgebra.ιMulti. [UPSTREAM] All belong in Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean.

Implementation notes

The body of TensorAlgebra.symRingCon is not exposed, so TensorAlgebra.symRingCon_le, which upstream is RingCon.ringConGen_le applied to that body, goes through SymmetricAlgebra.lift into the quotient by the congruence. That quotient is shown commutative by the argument of mathlib's CommSemiring (SymmetricAlgebra R M) instance.

@[simp]

theorem SymmetricAlgebra.adjoin_range_ι {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Algebra.adjoin R (Set.range ⇑(ι R M)) = ⊤

@[simp]

theorem SymmetricAlgebra.range_lift {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {f : M →ₗ[R] A} : (lift f).range = Algebra.adjoin R (Set.range ⇑f)

theorem SymmetricAlgebra.algHom_ι {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) : (algHom R M) ((TensorAlgebra.ι R) x) = (ι R M) x

theorem TensorAlgebra.symRingCon_le {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {c : RingCon (TensorAlgebra R M)} : symRingCon R M ≤ c ↔ ∀ (x y : M), c ((ι R) x * (ι R) y) ((ι R) y * (ι R) x)

A ring congruence on the tensor algebra contains symRingCon exactly when it identifies ι R x * ι R y with ι R y * ι R x.

theorem TensorAlgebra.symRingCon_toAddCon_le_ker {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_3} [AddZeroClass N] (f : TensorAlgebra R M →+ N) : (symRingCon R M).toAddCon ≤ AddCon.ker f ↔ ∀ (a b : TensorAlgebra R M) (x y : M), f (a * ((ι R) x * (ι R) y) * b) = f (a * ((ι R) y * (ι R) x) * b)

An additive map out of the tensor algebra is constant on the classes of symRingCon exactly when it cannot see the order of two adjacent generators in any two-sided context.

def SymmetricAlgebra.ιMulti (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (κ : Type u_3) [Fintype κ] : MultilinearMap R (fun (x : κ) => M) (SymmetricAlgebra R M)

The product of κ-indexed generators, x ↦ ∏ i, ι R M (x i), as a multilinear map. It is symmetric (SymmetricAlgebra.ιMulti_perm); the symmetric algebra sibling of ExteriorAlgebra.ιMulti and TensorAlgebra.tprod.

Equations

• SymmetricAlgebra.ιMulti R M κ = (MultilinearMap.mkPiAlgebra R κ (SymmetricAlgebra R M)).compLinearMap fun (x : κ) => SymmetricAlgebra.ι R M

theorem SymmetricAlgebra.ιMulti_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {κ : Type u_3} [Fintype κ] (x : κ → M) : (ιMulti R M κ) x = ∏ i : κ, (ι R M) (x i)

theorem SymmetricAlgebra.ιMulti_perm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {κ : Type u_3} [Fintype κ] (x : κ → M) (σ : Equiv.Perm κ) : ((ιMulti R M κ) fun (i : κ) => x (σ i)) = (ιMulti R M κ) x

theorem SymmetricAlgebra.ιMulti_mul_ιMulti {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {κ : Type u_3} [Fintype κ] {κ' : Type u_4} [Fintype κ'] (x : κ → M) (y : κ' → M) : (ιMulti R M κ) x * (ιMulti R M κ') y = (ιMulti R M (κ ⊕ κ')) (Sum.elim x y)

theorem SymmetricAlgebra.algHom_tprod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) : (algHom R M) ((TensorAlgebra.tprod R M n) x) = (ιMulti R M (Fin n)) x

theorem SymmetricAlgebra.ιMulti_range (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (κ : Type u_3) [Fintype κ] : Set.range ⇑(ιMulti R M κ) ⊆ ↑((ι R M).range ^ Fintype.card κ)

theorem SymmetricAlgebra.span_range_ιMulti (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (κ : Type u_3) [Fintype κ] : Submodule.span R (Set.range ⇑(ιMulti R M κ)) = (ι R M).range ^ Fintype.card κ

The products of Fintype.card κ generators span the corresponding power of the submodule LinearMap.range (ι R M); the sibling of ExteriorAlgebra.ιMulti_span_fixedDegree.