Symmetric tensor power of a semimodule over a commutative semiring

We define the nth symmetric tensor power of M as the TensorPower quotiented by the relation that the tprod of n elements is equal to the tprod of the same elements permuted by a permutation of Fin n. We denote this space by Sym[R]^n M, and the canonical multilinear map from M ^ n to Sym[R]^n M by ⨂ₛ[R] i, f i.

Main definitions:

• SymmetricPower.module: the symmetric tensor power is a module over R.

TODO:

• Grading: show that there is a map Sym[R]^i M × Sym[R]^j M → Sym[R]^(i + j) M that is associative and commutative, and that n ↦ Sym[R]^n M is a graded (semi)ring and algebra.
• Universal property: linear maps from Sym[R]^n M to N correspond to symmetric multilinear maps M ^ n to N.
• Relate to homogneous (multivariate) polynomials of degree n.

inductive SymmetricPower.Rel (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : TensorPower R n M → TensorPower R n M → Prop

The relation on the nᵗʰ tensor power of M that two tensors are equal if they are related by a permutation of Fin n.

• perm {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} (e : Equiv.Perm (Fin n)) (f : Fin n → M) : Rel R M n ((PiTensorProduct.tprod R) fun (i : Fin n) => f i) ((PiTensorProduct.tprod R) fun (i : Fin n) => f (e i))

noncomputable def SymmetricPower (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : Type (max u v)

The symmetric tensor power of a semimodule M over a commutative semiring R is the quotient of the nᵗʰ tensor power by the relation that two tensors are equal if they are related by a permutation of Fin n.

Equations

• SymmetricPower R M n = (addConGen (SymmetricPower.Rel R M n)).Quotient

def TensorProduct.«termSym[_]^__» : Lean.ParserDescr

The symmetric tensor power of a semimodule M over a commutative semiring R is the quotient of the nᵗʰ tensor power by the relation that two tensors are equal if they are related by a permutation of Fin n.

Equations

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

noncomputable instance SymmetricPower.instAddCommMonoid (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : AddCommMonoid (SymmetricPower R M n)

Equations

• SymmetricPower.instAddCommMonoid R M n = (addConGen (SymmetricPower.Rel R M n)).addCommMonoid

noncomputable def SymmetricPower.mk' (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : TensorPower R n M →+ SymmetricPower R M n

The canonical map from the nᵗʰ tensor power to the nᵗʰ symmetric tensor power.

Equations

• SymmetricPower.mk' R M n = (addConGen (SymmetricPower.Rel R M n)).mk'

theorem SymmetricPower.mk'_induction {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} {C : SymmetricPower R M n → Prop} (ih : ∀ (x : TensorPower R n M), C ((mk' R M n) x)) (x : SymmetricPower R M n) : C x

theorem SymmetricPower.mk'_inductionOn {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} {C : SymmetricPower R M n → Prop} (x : SymmetricPower R M n) (ih : ∀ (x : TensorPower R n M), C ((mk' R M n) x)) : C x

theorem SymmetricPower.smulAux' {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} (r : R) (x y : TensorPower R n M) (h : Rel R M n x y) : (addConGen (Rel R M n)) (r • x) (r • y)

theorem SymmetricPower.smulAux {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} {R₁ : Type u₁} [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] (r₁ : R₁) (x y : TensorPower R n M) (h : Rel R M n x y) : (addConGen (Rel R M n)) (r₁ • x) (r₁ • y)

noncomputable instance SymmetricPower.smul (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) {R₁ : Type u₁} [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] : SMul R₁ (SymmetricPower R M n)

Equations

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

theorem SymmetricPower.smul_def {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} {R₁ : Type u₁} [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] (r : R₁) (x : TensorPower R n M) : r • (mk' R M n) x = (mk' R M n) (r • x)

instance SymmetricPower.instIsScalarTower (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) {R₁ : Type u₁} [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] {R₂ : Type u₂} [Monoid R₂] [DistribMulAction R₂ R] [SMulCommClass R₂ R R] [SMul R₁ R₂] [IsScalarTower R₁ R₂ R] : IsScalarTower R₁ R₂ (SymmetricPower R M n)

noncomputable instance SymmetricPower.module (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) (R₁ : Type u₁) [Semiring R₁] [Module R₁ R] [SMulCommClass R₁ R R] : Module R₁ (SymmetricPower R M n)

Equations

• SymmetricPower.module R M n R₁ = { toSMul := SymmetricPower.smul R M n, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable instance SymmetricPower.instModule (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : Module R (SymmetricPower R M n)

Equations

• SymmetricPower.instModule R M n = SymmetricPower.module R M n R

noncomputable def SymmetricPower.mk (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : TensorPower R n M →ₗ[R] SymmetricPower R M n

The canonical map from the nᵗʰ tensor power to the nᵗʰ symmetric tensor power.

Equations

• SymmetricPower.mk R M n = { toFun := (↑(addConGen (SymmetricPower.Rel R M n)).mk').toFun, map_add' := ⋯, map_smul' := ⋯ }

theorem SymmetricPower.mk_induction (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) {C : SymmetricPower R M n → Prop} (ih : ∀ (x : TensorPower R n M), C ((mk R M n) x)) (x : SymmetricPower R M n) : C x

theorem SymmetricPower.mk_inductionOn (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) {C : SymmetricPower R M n → Prop} (x : SymmetricPower R M n) (ih : ∀ (x : TensorPower R n M), C ((mk R M n) x)) : C x

noncomputable def SymmetricPower.tprod (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} : M [Σ^Fin n]→ₗ[R] (SymmetricPower R M n)

The multilinear map that takes n elements of M and returns their symmetric tensor product. Denoted ⨂ₛ[R] i, f i.

Equations

• SymmetricPower.tprod R = { toMultilinearMap := (SymmetricPower.mk R M n).compMultilinearMap (PiTensorProduct.tprod R), map_perm_apply' := ⋯ }

def SymmetricPower.«term⨂ₛ[_]_,_» : Lean.ParserDescr

The multilinear map that takes n elements of M and returns their symmetric tensor product. Denoted ⨂ₛ[R] i, f i.

Equations

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

def SymmetricPower.«term⨂ₛ[_]_,_».«delab_app.DFunLike.coe» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

@[simp]

theorem SymmetricPower.tprod_perm_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} (e : Equiv.Perm (Fin n)) (f : Fin n → M) : (⨂ₛ[R] (i : Fin n), f (e i)) = (tprod R) f

theorem SymmetricPower.range_mk (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : LinearMap.range (mk R M n) = ⊤

theorem SymmetricPower.span_tprod_eq_top (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : Submodule.span R (Set.range ⇑(tprod R)) = ⊤

The pure tensors (i.e. the elements of the image of SymmetricPower.tprod) span the symmetric tensor product.

theorem SymmetricPower.inductionOn {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} {C : SymmetricPower R M n → Prop} (x : SymmetricPower R M n) (zero : C 0) (smul_tprod : ∀ (r : R) (x : Fin n → M), C (r • (tprod R) x)) (add : ∀ (x y : SymmetricPower R M n), C x → C y → C (x + y)) : C x

theorem SymmetricPower.induction {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {n : ℕ} {C : SymmetricPower R M n → Prop} (zero : C 0) (smul_tprod : ∀ (r : R) (x : Fin n → M), C (r • (tprod R) x)) (add : ∀ (x y : SymmetricPower R M n), C x → C y → C (x + y)) (x : SymmetricPower R M n) : C x

theorem SymmetricPower.addHom_ext {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] {n : ℕ} {f g : SymmetricPower R M n →+ N} (h : ∀ (r : R) (x : Fin n → M), f (r • (tprod R) x) = g (r • (tprod R) x)) : f = g

theorem SymmetricPower.addHom_ext_iff {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] {n : ℕ} {f g : SymmetricPower R M n →+ N} : f = g ↔ ∀ (r : R) (x : Fin n → M), f (r • (tprod R) x) = g (r • (tprod R) x)

theorem SymmetricPower.hom_ext {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {n : ℕ} {f g : SymmetricPower R M n →ₗ[R] N} (h : ∀ (x : Fin n → M), f ((tprod R) x) = g ((tprod R) x)) : f = g

theorem SymmetricPower.hom_ext_iff {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {n : ℕ} {f g : SymmetricPower R M n →ₗ[R] N} : f = g ↔ ∀ (x : Fin n → M), f ((tprod R) x) = g ((tprod R) x)

noncomputable def SymmetricPower.liftAux {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {n : ℕ} (f : M [Σ^Fin n]→ₗ[R] N) : SymmetricPower R M n →ₗ[R] N

Equations

• SymmetricPower.liftAux f = { toFun := (↑((addConGen (SymmetricPower.Rel R M n)).lift ↑(PiTensorProduct.lift ↑f) ⋯)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SymmetricPower.liftAux_tprod {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {n : ℕ} (f : M [Σ^Fin n]→ₗ[R] N) (x : Fin n → M) : (liftAux f) ((tprod R) x) = f x

noncomputable def SymmetricPower.lift (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type v₁) [AddCommMonoid N] [Module R N] (n : ℕ) : M [Σ^Fin n]→ₗ[R] N ≃ₗ[R] SymmetricPower R M n →ₗ[R] N

Equations

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

@[simp]

theorem SymmetricPower.lift_tprod {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {n : ℕ} (f : M [Σ^Fin n]→ₗ[R] N) (x : Fin n → M) : ((lift R M N n) f) ((tprod R) x) = f x

@[simp]

theorem SymmetricPower.lift_symm_coe {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {n : ℕ} (f : SymmetricPower R M n →ₗ[R] N) : ⇑((lift R M N n).symm f) = ⇑f ∘ ⇑(tprod R)

noncomputable def SymmetricPower.map {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (n : ℕ) (f : M →ₗ[R] N) : SymmetricPower R M n →ₗ[R] SymmetricPower R N n

Equations

• SymmetricPower.map n f = (SymmetricPower.lift R M (SymmetricPower R N n) n) ((SymmetricPower.tprod R).compLinearMap f)

@[simp]

theorem SymmetricPower.map_tprod (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type v₁) [AddCommMonoid N] [Module R N] (n : ℕ) (f : M →ₗ[R] N) (x : Fin n → M) : (map n f) ((tprod R) x) = ⨂ₛ[R] (i : Fin n), f (x i)

@[simp]

theorem SymmetricPower.map_id (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ) : map n LinearMap.id = LinearMap.id

Functoriality of map.

theorem SymmetricPower.map_comp {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {P : Type v₂} [AddCommMonoid P] [Module R P] (n : ℕ) (f : N →ₗ[R] P) (g : M →ₗ[R] N) : map n (f ∘ₗ g) = map n f ∘ₗ map n g

Functoriality of map.

@[simp]

theorem SymmetricPower.map_map_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {P : Type v₂} [AddCommMonoid P] [Module R P] (n : ℕ) (f : N →ₗ[R] P) (g : M →ₗ[R] N) (x : SymmetricPower R M n) : (map n f) ((map n g) x) = (map n (f ∘ₗ g)) x

noncomputable def SymmetricPower.mapLinearEquiv {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (n : ℕ) (e : M ≃ₗ[R] N) : SymmetricPower R M n ≃ₗ[R] SymmetricPower R N n

map converts linear equiv to linear equiv.

Equations

• SymmetricPower.mapLinearEquiv n e = LinearEquiv.ofLinear (SymmetricPower.map n ↑e) (SymmetricPower.map n ↑e.symm) ⋯ ⋯

@[simp]

theorem SymmetricPower.mapLinearEquiv_coe (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type v₁) [AddCommMonoid N] [Module R N] (n : ℕ) (e : M ≃ₗ[R] N) : ↑(mapLinearEquiv n e) = map n ↑e

@[simp]

theorem SymmetricPower.mapLinearEquiv_coe' (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type v₁) [AddCommMonoid N] [Module R N] (n : ℕ) (e : M ≃ₗ[R] N) : ⇑(mapLinearEquiv n e) = ⇑(map n ↑e)

@[simp]

theorem SymmetricPower.mapLinearEquiv_symm (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type v₁) [AddCommMonoid N] [Module R N] (n : ℕ) (e : M ≃ₗ[R] N) : (mapLinearEquiv n e).symm = mapLinearEquiv n e.symm

noncomputable def SymmetricPower.mul (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (i j : ℕ) : SymmetricPower R M i →ₗ[R] SymmetricPower R M j →ₗ[R] SymmetricPower R M (i + j)

Equations

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

def SymmetricPower.«term_✱_» : Lean.TrailingParserDescr

Equations

• SymmetricPower.«term_✱_» = Lean.ParserDescr.trailingNode `SymmetricPower.«term_✱_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "✱") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem SymmetricPower.map_mul {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (i j : ℕ) (f : M →ₗ[R] N) : (mul R M i j).compr₂ (map (i + j) f) = (mul R N i j).compl₁₂ (map i f) (map j f)

@[simp]

theorem SymmetricPower.map_mul_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {i j : ℕ} (f : M →ₗ[R] N) (x : SymmetricPower R M i) (y : SymmetricPower R M j) : (map (i + j) f) (((mul R M i j) x) y) = ((mul R N i j) ((map i f) x)) ((map j f) y)

@[simp]

theorem SymmetricPower.map_mul_one_one {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x y : SymmetricPower R M 1) : (map 2 f) (((mul R M 1 1) x) y) = ((mul R N 1 1) ((map 1 f) x)) ((map 1 f) y)

@[simp]

theorem SymmetricPower.map_mul_one_two {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x : SymmetricPower R M 1) (y : SymmetricPower R M 2) : (map 3 f) (((mul R M 1 2) x) y) = ((mul R N 1 2) ((map 1 f) x)) ((map 2 f) y)

@[simp]

theorem SymmetricPower.map_mul_two_one {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x : SymmetricPower R M 2) (y : SymmetricPower R M 1) : (map 3 f) (((mul R M 2 1) x) y) = ((mul R N 2 1) ((map 2 f) x)) ((map 1 f) y)

@[simp]

theorem SymmetricPower.map_mul_one_three {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x : SymmetricPower R M 1) (y : SymmetricPower R M 3) : (map 4 f) (((mul R M 1 3) x) y) = ((mul R N 1 3) ((map 1 f) x)) ((map 3 f) y)

@[simp]

theorem SymmetricPower.map_mul_two_two {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x y : SymmetricPower R M 2) : (map 4 f) (((mul R M 2 2) x) y) = ((mul R N 2 2) ((map 2 f) x)) ((map 2 f) y)

@[simp]

theorem SymmetricPower.map_mul_three_one {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x : SymmetricPower R M 3) (y : SymmetricPower R M 1) : (map 4 f) (((mul R M 3 1) x) y) = ((mul R N 3 1) ((map 3 f) x)) ((map 1 f) y)

noncomputable def SymmetricPower.zero_equiv (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : SymmetricPower R M 0 ≃ₗ[R] R

Equations

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

@[simp]

theorem SymmetricPower.zero_equiv_apply (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (a✝ : (addConGen (Rel R M 0)).Quotient) : (zero_equiv R M) a✝ = ((addConGen (Rel R M 0)).lift ↑(PiTensorProduct.lift ↑((SymmetricMap.ofIsEmpty R M R (Fin 0)).symm 1)) ⋯) a✝

@[simp]

theorem SymmetricPower.zero_equiv_symm_apply (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (r : R) : (zero_equiv R M).symm r = r • (tprod R) ![]

noncomputable def SymmetricPower.one_equiv (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : SymmetricPower R M 1 ≃ₗ[R] M

Equations

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

@[simp]

theorem SymmetricPower.one_equiv_symm_apply (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (m : M) : (one_equiv R M).symm m = (tprod R) ![m]

@[simp]

theorem SymmetricPower.one_equiv_apply (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (a✝ : (addConGen (Rel R M 1)).Quotient) : (one_equiv R M) a✝ = ((addConGen (Rel R M 1)).lift ↑(PiTensorProduct.lift ↑((SymmetricMap.ofSubsingleton R M M 0).symm 1)) ⋯) a✝

noncomputable def SymmetricPower.toBaseChange (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) : SymmetricPower R M n →ₗ[R] SymmetricPower A (TensorProduct R A M) n

Equations

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

@[simp]

theorem SymmetricPower.toBaseChange_tprod (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (A : Type w) [CommSemiring A] [Algebra R A] {n : ℕ} (x : Fin n → M) : (toBaseChange R M A n) ((tprod R) x) = ⨂ₛ[A] (i : Fin n), 1 ⊗ₜ[R] x i

noncomputable def SymmetricPower.baseChange (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) : TensorProduct R A (SymmetricPower R M n) ≃ₗ[A] SymmetricPower A (TensorProduct R A M) n

Equations

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

@[simp]

theorem SymmetricPower.baseChange_tmul_tprod (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] {n : ℕ} (r : A) (x : Fin n → M) : (baseChange R M A n) (r ⊗ₜ[R] (tprod R) x) = r • ⨂ₛ[A] (i : Fin n), 1 ⊗ₜ[R] x i

theorem SymmetricPower.baseChange_one_tmul_tprod (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (A : Type w) [CommSemiring A] [Algebra R A] {n : ℕ} (x : Fin n → M) : (baseChange R M A n) (1 ⊗ₜ[R] (tprod R) x) = ⨂ₛ[A] (i : Fin n), 1 ⊗ₜ[R] x i

theorem SymmetricPower.map_comp_toBaseChange {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) (f : M →ₗ[R] N) : ↑R (map n (LinearMap.baseChange A f)) ∘ₗ toBaseChange R M A n = toBaseChange R N A n ∘ₗ map n f

theorem SymmetricPower.map_toBaseChange_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (A : Type w) [CommSemiring A] [Algebra R A] {n : ℕ} (f : M →ₗ[R] N) (x : SymmetricPower R M n) : (map n (LinearMap.baseChange A f)) ((toBaseChange R M A n) x) = (toBaseChange R N A n) ((map n f) x)

theorem SymmetricPower.map_comp_baseChange {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) (f : M →ₗ[R] N) : map n (LinearMap.baseChange A f) ∘ₗ ↑(baseChange R M A n) = ↑(baseChange R N A n) ∘ₗ LinearMap.baseChange A (map n f)

Naturality of baseChange.

theorem SymmetricPower.map_baseChange_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type v₁} [AddCommMonoid N] [Module R N] {A : Type w} [CommSemiring A] [Algebra R A] {n : ℕ} (f : M →ₗ[R] N) (x : TensorProduct R A (SymmetricPower R M n)) : (map n (LinearMap.baseChange A f)) ((baseChange R M A n) x) = (baseChange R N A n) ((LinearMap.baseChange A (map n f)) x)

theorem SymmetricPower.toBaseChange_of_isScalarTower (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (A : Type w) [CommSemiring A] [Algebra R A] (B : Type w₁) [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (n : ℕ) : ↑R (toBaseChange R M B n) = ↑R (map n ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M)) ∘ₗ ↑R (toBaseChange A (TensorProduct R A M) B n) ∘ₗ toBaseChange R M A n

theorem SymmetricPower.toBaseChange_apply_of_isScalarTower {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (A : Type w) [CommSemiring A] [Algebra R A] (B : Type w₁) [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] {n : ℕ} (x : SymmetricPower R M n) : (toBaseChange R M B n) x = (map n ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M)) ((toBaseChange A (TensorProduct R A M) B n) ((toBaseChange R M A n) x))

@[simp]

theorem SymmetricPower.mul_tprod_tprod (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (i j : ℕ) (v : Fin i → M) (w : Fin j → M) : ((mul R M i j) ((tprod R) v)) ((tprod R) w) = (tprod R) (Fin.append v w)

noncomputable instance SymmetricPower.instOne (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) : One (SymmetricPower R A n)

Equations

• SymmetricPower.instOne R A n = { one := (SymmetricPower.tprod R) 1 }

theorem SymmetricPower.one_def (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) : 1 = (tprod R) 1

noncomputable def SymmetricPower.eval (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) : SymmetricPower R A n →ₗ[R] A

Equations

• SymmetricPower.eval R A n = (SymmetricPower.lift R A A n) (mkPiAlgebra R (Fin n) A)

@[simp]

theorem SymmetricPower.eval_tprod (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) (v : Fin n → A) : (eval R A n) ((tprod R) v) = ∏ i : Fin n, v i

@[simp]

theorem SymmetricPower.eval_one (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (n : ℕ) : (eval R A n) 1 = 1

@[simp]

theorem SymmetricPower.eval_mul (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (i j : ℕ) : (mul R A i j).compr₂ (eval R A (i + j)) = (LinearMap.mul R A).compl₁₂ (eval R A i) (eval R A j)

@[simp]

theorem SymmetricPower.eval_mul_apply (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (i j : ℕ) (v : SymmetricPower R A i) (w : SymmetricPower R A j) : (eval R A (i + j)) (((mul R A i j) v) w) = (eval R A i) v * (eval R A j) w

@[simp]

theorem SymmetricPower.eval_mul_one_one (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (v w : SymmetricPower R A 1) : (eval R A 2) (((mul R A 1 1) v) w) = (eval R A 1) v * (eval R A 1) w

@[simp]

theorem SymmetricPower.eval_mul_two_one (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (v : SymmetricPower R A 2) (w : SymmetricPower R A 1) : (eval R A 3) (((mul R A 2 1) v) w) = (eval R A 2) v * (eval R A 1) w

@[simp]

theorem SymmetricPower.eval_mul_one_two (R : Type u) [CommSemiring R] (A : Type w) [CommSemiring A] [Algebra R A] (v : SymmetricPower R A 1) (w : SymmetricPower R A 2) : (eval R A 3) (((mul R A 1 2) v) w) = (eval R A 1) v * (eval R A 2) w

noncomputable def SymmetricPower.evalSelf (R : Type u) [CommSemiring R] (n : ℕ) : SymmetricPower R R n ≃ₗ[R] R

Equations

• SymmetricPower.evalSelf R n = LinearEquiv.ofLinear (SymmetricPower.eval R R n) (LinearMap.smulRight 1 1) ⋯ ⋯

@[simp]

theorem SymmetricPower.evalSelf_coe (R : Type u) [CommSemiring R] (n : ℕ) : ↑(evalSelf R n) = eval R R n

@[simp]

theorem SymmetricPower.evalSelf_coe' (R : Type u) [CommSemiring R] (n : ℕ) : ⇑(evalSelf R n) = ⇑(eval R R n)

noncomputable def SymmetricPower.cast (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (i j : ℕ) (h : i = j) : SymmetricPower R M i ≃ₗ[R] SymmetricPower R M j

Equations

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

@[simp]

theorem SymmetricPower.cast_tprod (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] {i j : ℕ} (h : i = j) (v : Fin i → M) : (cast R M i j h) ((tprod R) v) = ⨂ₛ[R] (x : Fin j), v (Fin.cast ⋯ x)

@[simp]

theorem SymmetricPower.cast_rfl (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (i : ℕ) : cast R M i i ⋯ = LinearEquiv.refl R (SymmetricPower R M i)

@[simp]

theorem SymmetricPower.cast_coe (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] {i j : ℕ} (h : i = j) : ⇑(cast R M i j h) = _root_.cast ⋯

@[simp]

theorem SymmetricPower.cast_symm (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] {i j : ℕ} (h : i = j) : (cast R M i j h).symm = cast R M j i ⋯

@[simp]

theorem SymmetricPower.cast_trans (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] {i j k : ℕ} (h₁ : i = j) (h₂ : j = k) : cast R M i j h₁ ≪≫ₗ cast R M j k h₂ = cast R M i k ⋯

noncomputable instance SymmetricPower.instOneOfNatNat (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : One (SymmetricPower R M 0)

Equations

• SymmetricPower.instOneOfNatNat R M = { one := (SymmetricPower.tprod R) ![] }

theorem SymmetricPower.one_def' (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : 1 = (tprod R) ![]

theorem SymmetricPower.mul_comm' (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (i j : ℕ) : mul R M i j = (mul R M j i).flip.compr₂ ↑(cast R M (j + i) (i + j) ⋯)

theorem SymmetricPower.mul_one' (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (i : ℕ) : (mul R M i 0).flip 1 = LinearMap.id

@[simp]

theorem SymmetricPower.mul_one_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {i : ℕ} (x : SymmetricPower R M i) : ((mul R M i 0) x) 1 = x

theorem SymmetricPower.one_mul' (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (j : ℕ) : (mul R M 0 j) 1 = ↑(cast R M j (0 + j) ⋯)

theorem SymmetricPower.cast_one_mul (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (j : ℕ) : ↑(cast R M (0 + j) j ⋯) ∘ₗ (mul R M 0 j) 1 = LinearMap.id

theorem SymmetricPower.mul_assoc' (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] {i j k : ℕ} (x : SymmetricPower R M i) (y : SymmetricPower R M j) (z : SymmetricPower R M k) : (cast R M (i + j + k) (i + (j + k)) ⋯) (((mul R M (i + j) k) (((mul R M i j) x) y)) z) = ((mul R M i (j + k)) x) (((mul R M j k) y) z)

noncomputable instance SymmetricPower.gMul (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : GradedMonoid.GMul fun (n : ℕ) => SymmetricPower R M n

Equations

• SymmetricPower.gMul R M = { mul := fun {i j : ℕ} (x : SymmetricPower R M i) (y : SymmetricPower R M j) => ((SymmetricPower.mul R M i j) x) y }

noncomputable instance SymmetricPower.gOne (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : GradedMonoid.GOne fun (n : ℕ) => SymmetricPower R M n

Equations

• SymmetricPower.gOne R M = { one := 1 }

theorem SymmetricPower.mul_def' (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (x y : GradedMonoid fun (n : ℕ) => SymmetricPower R M n) : GradedMonoid.GMul.mul x.snd y.snd = ((mul R M x.fst y.fst) x.snd) y.snd

theorem SymmetricPower.gradedMonoid_eq_of_cast {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {a b : GradedMonoid fun (n : ℕ) => SymmetricPower R M n} (h₁ : a.fst = b.fst) (h₂ : (cast R M a.fst b.fst h₁) a.snd = b.snd) : a = b

noncomputable instance SymmetricPower.gCommMonoid (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : GradedMonoid.GCommMonoid fun (n : ℕ) => SymmetricPower R M n

Equations

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

def SymmetricPower.«termGSym[_]_» : Lean.ParserDescr

Equations

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

noncomputable instance instAddCommGroupSymmetricPower (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] (n : ℕ) : AddCommGroup (SymmetricPower R M n)

Equations

• instAddCommGroupSymmetricPower R M n = (addConGen (SymmetricPower.Rel R M n)).addCommGroup