Documentation

Linglib.Core.LinearAlgebra.TensorPower.Symmetric

The universal property of the symmetric tensor power #

A multilinear map f : (ι → M) → N invariant under permutations of its arguments descends to a linear map SymmetricPower.lift f hf : Sym[R] ι M →ₗ[R] N, and linear maps out of Sym[R] ι M are determined by their values on ⨂ₛ[R] i, x i (SymmetricPower.ext). This is the universal property TODO of Mathlib/LinearAlgebra/TensorPower/Symmetric.lean.

Implementation notes #

The symmetry hypothesis has the shape of the field SymmetricMap.map_perm' of mathlib4#41426, whose dependent mathlib4#41444 packages lift as a linear equivalence out of symmetric multilinear maps. This file is a stand-in until those land.

source
@[simp]
theorem SymmetricPower.mk_tprod {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : ι → M) :
(mk R ι M) ((PiTensorProduct.tprod R) x) = (tprod R) x
source
def SymmetricPower.lift {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : ι) => M) N) (hf : ∀ (x : ι → M) (σ : Equiv.Perm ι), (f fun (i : ι) => x (σ i)) = f x) :
SymmetricPower R ι M →ₗ[R] N

A multilinear map (ι → M) → N invariant under permutations of its arguments descends to a linear map Sym[R] ι M →ₗ[R] N.

Equations
  • SymmetricPower.lift f hf = { toFun := ⇑((addConGen (SymmetricPower.Rel R ι M)).lift (PiTensorProduct.lift f).toAddMonoidHom ⋯), map_add' := ⋯, map_smul' := ⋯ }
Instances For
    source
    @[simp]
    theorem SymmetricPower.lift_tprod {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : MultilinearMap R (fun (x : ι) => M) N} {hf : ∀ (x : ι → M) (σ : Equiv.Perm ι), (f fun (i : ι) => x (σ i)) = f x} (x : ι → M) :
    (lift f hf) ((tprod R) x) = f x
    source
    @[simp]
    theorem SymmetricPower.lift_comp_tprod {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : MultilinearMap R (fun (x : ι) => M) N} {hf : ∀ (x : ι → M) (σ : Equiv.Perm ι), (f fun (i : ι) => x (σ i)) = f x} :
    (lift f hf).compMultilinearMap (tprod R) = f
    source
    theorem SymmetricPower.ext {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {g₁ g₂ : SymmetricPower R ι M →ₗ[R] N} (h : g₁.compMultilinearMap (tprod R) = g₂.compMultilinearMap (tprod R)) :
    g₁ = g₂

    Two linear maps out of Sym[R] ι M that agree on ⨂ₛ[R] i, x i are equal.

    source
    theorem SymmetricPower.ext_iff {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {g₁ g₂ : SymmetricPower R ι M →ₗ[R] N} :
    g₁ = g₂ ↔ g₁.compMultilinearMap (tprod R) = g₂.compMultilinearMap (tprod R)