Symmetric Multilinear Maps

In this file we define symmetric multilinear maps bewteen modules as a module itself.

Main definitions

• SymmetricMap R M N ι: the symmetric R-multilinear maps from ι → M to N.

structure SymmetricMap (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] (ι : Type u') extends MultilinearMap R (fun (x : ι) => M) N : Type (max (max u' v) w)

An symmetric map from ι → M to N, denoted M [Σ^ι]→ₗ[R] N, is a multilinear map that stays the same when its arguments are permuted.

• toFun : (ι → M) → N
• map_update_add' [DecidableEq ι] (m : ι → M) (i : ι) (x y : M) : (↑self).toFun (Function.update m i (x + y)) = (↑self).toFun (Function.update m i x) + (↑self).toFun (Function.update m i y)
• map_update_smul' [DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M) : (↑self).toFun (Function.update m i (c • x)) = c • (↑self).toFun (Function.update m i x)
• map_perm_apply' (v : ι → M) (e : Equiv.Perm ι) : ((↑self).toFun fun (i : ι) => v (e i)) = (↑self).toFun v

  The map is symmetric: if the arguments of v are permuted, the result does not change.

def «term_[Σ^_]→ₗ[_]_» : Lean.TrailingParserDescr

An symmetric map from ι → M to N, denoted M [Σ^ι]→ₗ[R] N, is a multilinear map that stays the same when its arguments are permuted.

Equations

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

instance SymmetricMap.instFunLikeForall {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : FunLike (M [Σ^ι]→ₗ[R] N) (ι → M) N

Equations

• SymmetricMap.instFunLikeForall = { coe := fun (f : M [Σ^ι]→ₗ[R] N) => (↑f).toFun, coe_injective' := ⋯ }

@[simp]

theorem SymmetricMap.map_update_add {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) [DecidableEq ι] (g : ι → M) (c : ι) (x y : M) : f (Function.update g c (x + y)) = f (Function.update g c x) + f (Function.update g c y)

@[simp]

theorem SymmetricMap.map_update_smul {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) [DecidableEq ι] (g : ι → M) (c : ι) (r : R) (x : M) : f (Function.update g c (r • x)) = r • f (Function.update g c x)

theorem SymmetricMap.map_coord_zero {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) {g : ι → M} (c : ι) (h : g c = 0) : f g = 0

@[simp]

theorem SymmetricMap.map_update_zero {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) [DecidableEq ι] (g : ι → M) (c : ι) : f (Function.update g c 0) = 0

@[simp]

theorem SymmetricMap.map_zero {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) [Nonempty ι] : f 0 = 0

theorem SymmetricMap.congrFun {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {f g : M [Σ^ι]→ₗ[R] N} (h : f = g) (x : ι → M) : f x = g x

theorem SymmetricMap.congrArg {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) {x y : ι → M} (h : x = y) : f x = f y

theorem SymmetricMap.coe_injective {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : Function.Injective DFunLike.coe

theorem SymmetricMap.coe_inj {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {f g : M [Σ^ι]→ₗ[R] N} : ⇑f = ⇑g ↔ f = g

theorem SymmetricMap.ext {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {f g : M [Σ^ι]→ₗ[R] N} (h : ∀ (x : ι → M), f x = g x) : f = g

theorem SymmetricMap.ext_iff {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {f g : M [Σ^ι]→ₗ[R] N} : f = g ↔ ∀ (x : ι → M), f x = g x

instance SymmetricMap.instCoeMultilinearMap {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : Coe (M [Σ^ι]→ₗ[R] N) (MultilinearMap R (fun (x : ι) => M) N)

Equations

• SymmetricMap.instCoeMultilinearMap = { coe := fun (f : M [Σ^ι]→ₗ[R] N) => ↑f }

theorem SymmetricMap.toMultilinearMap_injective {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : Function.Injective toMultilinearMap

@[simp]

theorem SymmetricMap.coe_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) : ⇑↑f = ⇑f

@[simp]

theorem SymmetricMap.coe_mk {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : MultilinearMap R (fun (x : ι) => M) N) (h : ∀ (v : ι → M) (e : Equiv.Perm ι), (f.toFun fun (i : ι) => v (e i)) = f.toFun v) : ⇑{ toMultilinearMap := f, map_perm_apply' := h } = ⇑f

@[simp]

theorem SymmetricMap.map_perm_apply {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) (e : Equiv.Perm ι) (x : ι → M) : (f fun (i : ι) => x (e i)) = f x

@[simp]

theorem SymmetricMap.comp_domDomCongr {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) (e : Equiv.Perm ι) : MultilinearMap.domDomCongr e ↑f = ↑f

def SymmetricMap.mk' {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : MultilinearMap R (fun (x : ι) => M) N) (h : ∀ (e : ι ≃ ι), MultilinearMap.domDomCongr e f = f) : M [Σ^ι]→ₗ[R] N

Equations

• SymmetricMap.mk' f h = { toMultilinearMap := f, map_perm_apply' := ⋯ }

instance SymmetricMap.instAdd {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : Add (M [Σ^ι]→ₗ[R] N)

Equations

• SymmetricMap.instAdd = { add := fun (f g : M [Σ^ι]→ₗ[R] N) => { toMultilinearMap := ↑f + ↑g, map_perm_apply' := ⋯ } }

@[simp]

theorem SymmetricMap.add_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f g : M [Σ^ι]→ₗ[R] N) : ⇑(f + g) = ⇑f + ⇑g

theorem SymmetricMap.coe_add {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f g : M [Σ^ι]→ₗ[R] N) : ↑(f + g) = ↑f + ↑g

instance SymmetricMap.instZero {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : Zero (M [Σ^ι]→ₗ[R] N)

Equations

• SymmetricMap.instZero = { zero := { toMultilinearMap := 0, map_perm_apply' := ⋯ } }

@[simp]

theorem SymmetricMap.zero_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : ⇑0 = 0

theorem SymmetricMap.coe_zero {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : ↑0 = 0

@[simp]

theorem SymmetricMap.mk_zero {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (h : ∀ (v : ι → M) (e : Equiv.Perm ι), (MultilinearMap.toFun 0 fun (i : ι) => v (e i)) = MultilinearMap.toFun 0 v) : { toMultilinearMap := 0, map_perm_apply' := h } = 0

instance SymmetricMap.instSMul {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] : SMul S (M [Σ^ι]→ₗ[R] N)

Equations

• SymmetricMap.instSMul = { smul := fun (c : S) (f : M [Σ^ι]→ₗ[R] N) => { toMultilinearMap := c • ↑f, map_perm_apply' := ⋯ } }

@[simp]

theorem SymmetricMap.smul_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) {S : Type u_1} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (c : S) : ⇑(c • f) = c • ⇑f

theorem SymmetricMap.coe_smul {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) {S : Type u_1} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (c : S) : ↑(c • f) = c • ↑f

theorem SymmetricMap.coeFn_smul {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (c : S) (f : M [Σ^ι]→ₗ[R] N) : ⇑(c • f) = c • ⇑f

instance SymmetricMap.instSMulCommClass {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] {T : Type u_2} [Monoid T] [DistribMulAction T N] [SMulCommClass R T N] [SMulCommClass S T N] : SMulCommClass S T (M [Σ^ι]→ₗ[R] N)

instance SymmetricMap.instIsCentralScalar {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] [DistribMulAction Sᵐᵒᵖ N] [IsCentralScalar S N] : IsCentralScalar S (M [Σ^ι]→ₗ[R] N)

instance SymmetricMap.instAddCommMonoid {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} : AddCommMonoid (M [Σ^ι]→ₗ[R] N)

Equations

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

instance SymmetricMap.instDistribMulAction {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] : DistribMulAction S (M [Σ^ι]→ₗ[R] N)

Equations

• SymmetricMap.instDistribMulAction = { toSMul := SymmetricMap.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

instance SymmetricMap.instModule {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Semiring S] [Module S N] [SMulCommClass R S N] : Module S (M [Σ^ι]→ₗ[R] N)

The space of multilinear maps over an algebra over R is a module over R, for the pointwise addition and scalar multiplication.

Equations

• SymmetricMap.instModule = { toDistribMulAction := SymmetricMap.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

instance SymmetricMap.instNoZeroSMulDivisors {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Semiring S] [Module S N] [SMulCommClass R S N] [NoZeroSMulDivisors S N] : NoZeroSMulDivisors S (M [Σ^ι]→ₗ[R] N)

def SymmetricMap.toMultilinearMapLM {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Semiring S] [Module S N] [SMulCommClass R S N] : M [Σ^ι]→ₗ[R] N →ₗ[S] MultilinearMap R (fun (x : ι) => M) N

Embedding of symmetric maps into multilinear maps as a linear map.

Equations

• SymmetricMap.toMultilinearMapLM = { toFun := SymmetricMap.toMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SymmetricMap.toMultilinearMapLM_apply {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {S : Type u_1} [Semiring S] [Module S N] [SMulCommClass R S N] (self : M [Σ^ι]→ₗ[R] N) : toMultilinearMapLM self = ↑self

def SymmetricMap.compLinearMap {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : N [Σ^ι]→ₗ[R] P) (g : M →ₗ[R] N) : M [Σ^ι]→ₗ[R] P

Equations

• f.compLinearMap g = { toMultilinearMap := (↑f).compLinearMap fun (x : ι) => g, map_perm_apply' := ⋯ }

@[simp]

theorem SymmetricMap.compLinearMap_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : N [Σ^ι]→ₗ[R] P) (g : M →ₗ[R] N) : ⇑(f.compLinearMap g) = ⇑f ∘ fun (x : ι → M) (i : ι) => g (x i)

theorem SymmetricMap.compLinearMap_apply {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : N [Σ^ι]→ₗ[R] P) (g : M →ₗ[R] N) (x : ι → M) : (f.compLinearMap g) x = f (⇑g ∘ x)

def SymmetricMap.compLinearMapAddHom {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (P : Type w') [AddCommMonoid P] [Module R P] (ι : Type u') (f : M →ₗ[R] N) : N [Σ^ι]→ₗ[R] P →+ M [Σ^ι]→ₗ[R] P

Equations

• SymmetricMap.compLinearMapAddHom P ι f = { toFun := fun (g : N [Σ^ι]→ₗ[R] P) => g.compLinearMap f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SymmetricMap.compLinearMapAddHom_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : M →ₗ[R] N) : ⇑(compLinearMapAddHom P ι f) = fun (x : N [Σ^ι]→ₗ[R] P) => x.compLinearMap f

theorem SymmetricMap.compLinearMapAddHom_apply {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : M →ₗ[R] N) (g : N [Σ^ι]→ₗ[R] P) : (compLinearMapAddHom P ι f) g = g.compLinearMap f

theorem SymmetricMap.compLinearMap_add {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f₁ f₂ : N [Σ^ι]→ₗ[R] P) (g : M →ₗ[R] N) : (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

def SymmetricMap.compLinearMapₗ {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (P : Type w') [AddCommMonoid P] [Module R P] (ι : Type u') (S : Type u_1) [Semiring S] [Module S P] [SMulCommClass R S P] (f : M →ₗ[R] N) : N [Σ^ι]→ₗ[R] P →ₗ[S] M [Σ^ι]→ₗ[R] P

Equations

• SymmetricMap.compLinearMapₗ P ι S f = { toFun := (↑(SymmetricMap.compLinearMapAddHom P ι f)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SymmetricMap.compLinearMapₗ_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (S : Type u_1) [Semiring S] [Module S P] [SMulCommClass R S P] [Module R S] (f : M →ₗ[R] N) : ⇑(compLinearMapₗ P ι S f) = fun (x : N [Σ^ι]→ₗ[R] P) => x.compLinearMap f

theorem SymmetricMap.compLinearMapₗ_apply {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (S : Type u_1) [Semiring S] [Module S P] [SMulCommClass R S P] [Module R S] (f : M →ₗ[R] N) (g : N [Σ^ι]→ₗ[R] P) : (compLinearMapₗ P ι S f) g = g.compLinearMap f

def LinearMap.compSymmetricMap {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : N →ₗ[R] P) (g : M [Σ^ι]→ₗ[R] N) : M [Σ^ι]→ₗ[R] P

Equations

• f.compSymmetricMap g = { toMultilinearMap := f.compMultilinearMap ↑g, map_perm_apply' := ⋯ }

@[simp]

theorem LinearMap.compSymmetricMap_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : N →ₗ[R] P) (g : M [Σ^ι]→ₗ[R] N) : ⇑(f.compSymmetricMap g) = ⇑f ∘ ⇑g

theorem LinearMap.compSymmetricMap_apply {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : N →ₗ[R] P) (g : M [Σ^ι]→ₗ[R] N) (x : ι → M) : (f.compSymmetricMap g) x = f (g x)

def LinearMap.compSymmetricMapAddHom {R : Type u} [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] (ι : Type u') (f : N →ₗ[R] P) : M [Σ^ι]→ₗ[R] N →+ M [Σ^ι]→ₗ[R] P

Equations

• LinearMap.compSymmetricMapAddHom M ι f = { toFun := f.compSymmetricMap, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LinearMap.compSymmetricMapAddHom_coe {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (f : N →ₗ[R] P) : ⇑(compSymmetricMapAddHom M ι f) = f.compSymmetricMap

def LinearMap.compSymmetricMapₗ {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type w'} [AddCommMonoid P] [Module R P] {ι : Type u'} (S : Type u_1) [Semiring S] [Module S N] [SMulCommClass R S N] [Module S P] [SMulCommClass R S P] [CompatibleSMul N P S R] (f : N →ₗ[R] P) : M [Σ^ι]→ₗ[R] N →ₗ[S] M [Σ^ι]→ₗ[R] P

Equations

• LinearMap.compSymmetricMapₗ S f = { toFun := (↑(LinearMap.compSymmetricMapAddHom M ι f)).toFun, map_add' := ⋯, map_smul' := ⋯ }

def SymmetricMap.ofIsEmpty (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] (ι : Type u') [IsEmpty ι] : M [Σ^ι]→ₗ[R] N ≃+ N

Equations

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

@[simp]

theorem SymmetricMap.ofIsEmpty_symm_apply_apply (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] (ι : Type u') [IsEmpty ι] (n : N) (x✝ : ι → M) : ((ofIsEmpty R M N ι).symm n) x✝ = n

@[simp]

theorem SymmetricMap.ofIsEmpty_apply (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] (ι : Type u') [IsEmpty ι] (f : M [Σ^ι]→ₗ[R] N) : (ofIsEmpty R M N ι) f = f fun (a : ι) => isEmptyElim a

def SymmetricMap.ofSubsingleton (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] {ι : Type u'} [Subsingleton ι] (i : ι) : M [Σ^ι]→ₗ[R] N ≃+ (M →ₗ[R] N)

Equations

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

@[simp]

theorem SymmetricMap.ofSubsingleton_apply_apply (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] {ι : Type u'} [Subsingleton ι] (i : ι) (f : M [Σ^ι]→ₗ[R] N) (m : M) : ((ofSubsingleton R M N i) f) m = f (Function.const ι m)

@[simp]

theorem SymmetricMap.ofSubsingleton_symm_apply_apply (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] {ι : Type u'} [Subsingleton ι] (i : ι) (f : M →ₗ[R] N) (x : ι → M) : ((ofSubsingleton R M N i).symm f) x = f (x i)

def SymmetricMap.isUnique (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] (ι : Type u') [Unique ι] : M [Σ^ι]→ₗ[R] N ≃+ (M →ₗ[R] N)

Equations

• SymmetricMap.isUnique R M N ι = SymmetricMap.ofSubsingleton R M N default

@[simp]

theorem SymmetricMap.isUnique_apply_apply (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] (ι : Type u') [Unique ι] (f : M [Σ^ι]→ₗ[R] N) (m : M) : ((isUnique R M N ι) f) m = f (Function.const ι m)

@[simp]

theorem SymmetricMap.isUnique_symm_apply_apply (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] (ι : Type u') [Unique ι] (f : M →ₗ[R] N) (x : ι → M) : ((isUnique R M N ι).symm f) x = f (x default)

def SymmetricMap.restrictScalars {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (S : Type u_1) [Semiring S] [SMul S R] [Module S M] [Module S N] [IsScalarTower S R M] [IsScalarTower S R N] (f : M [Σ^ι]→ₗ[R] N) : M [Σ^ι]→ₗ[S] N

Equations

• SymmetricMap.restrictScalars S f = { toMultilinearMap := MultilinearMap.restrictScalars S ↑f, map_perm_apply' := ⋯ }

def SymmetricMap.domDomCongr {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {ι' : Type u₁} (e : ι ≃ ι') (f : M [Σ^ι]→ₗ[R] N) : M [Σ^ι']→ₗ[R] N

Equations

• SymmetricMap.domDomCongr e f = { toMultilinearMap := MultilinearMap.domDomCongr e ↑f, map_perm_apply' := ⋯ }

@[simp]

theorem SymmetricMap.domDomCongr_apply {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {ι' : Type u₁} (e : ι ≃ ι') (f : M [Σ^ι]→ₗ[R] N) (v : ι' → M) : (domDomCongr e f) v = f fun (i : ι) => v (e i)

theorem SymmetricMap.domDomCongr_trans {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {ι' : Type u₁} {ι'' : Type u₂} (e₁ : ι ≃ ι') (e₂ : ι' ≃ ι'') (f : M [Σ^ι]→ₗ[R] N) : domDomCongr (e₁.trans e₂) f = domDomCongr e₂ (domDomCongr e₁ f)

@[simp]

theorem SymmetricMap.domDomCongr_refl {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} (f : M [Σ^ι]→ₗ[R] N) : domDomCongr (Equiv.refl ι) f = f

def SymmetricMap.domDomCongrLinearEquiv (R : Type u) [Semiring R] (M : Type v) [AddCommMonoid M] [Module R M] (N : Type w) [AddCommMonoid N] [Module R N] {ι : Type u'} {ι' : Type u₁} (S : Type u_1) [Semiring S] [Module S N] [SMulCommClass R S N] (e : ι ≃ ι') : M [Σ^ι]→ₗ[R] N ≃ₗ[S] M [Σ^ι']→ₗ[R] N

Equations

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

@[simp]

theorem SymmetricMap.domDomCongrLinearEquiv_apply {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} {ι' : Type u₁} (S : Type u_1) [Semiring S] [Module S N] [SMulCommClass R S N] (e : ι ≃ ι') (f : M [Σ^ι]→ₗ[R] N) (v : ι' → M) : ((domDomCongrLinearEquiv R M N S e) f) v = f fun (i : ι) => v (e i)

theorem map_smul_univ {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {ι : Type u'} [Fintype ι] (f : M [Σ^ι]→ₗ[R] N) (c : ι → R) (v : ι → M) : (f fun (i : ι) => c i • v i) = (∏ i : ι, c i) • f v

def mkPiAlgebra (R : Type u) [CommSemiring R] (ι : Type u') (A : Type w') [CommSemiring A] [Algebra R A] [Fintype ι] : A [Σ^ι]→ₗ[R] A

Equations

• mkPiAlgebra R ι A = { toMultilinearMap := MultilinearMap.mkPiAlgebra R ι A, map_perm_apply' := ⋯ }

@[simp]

theorem mkPiAlgebra_apply (R : Type u) [CommSemiring R] (ι : Type u') (A : Type w') [CommSemiring A] [Algebra R A] [Fintype ι] (v : ι → A) : (mkPiAlgebra R ι A) v = ∏ i : ι, v i