Base Change for Symmetric Multilinear Maps

In this file we contruct the base change for symmetric multilinear maps.

Main definitions

• SymmetricMap.baseChange: the base change of a symmetric multilinear map M [Σ^ι]→ₗ[R] N to (A ⊗[R] M) [Σ^ι]→ₗ[A] (A ⊗[R] N).

theorem MultilinearMap.baseChange_hom_ext {R : Type u_1} [CommSemiring R] {ι' : Type u_3} {M₁ : ι' → Type u_4} [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] {A : Type u_8} [CommSemiring A] [Algebra R A] {N' : Type u_9} [AddCommMonoid N'] [Module A N'] [Finite ι'] {f g : MultilinearMap A (fun (i : ι') => TensorProduct R A (M₁ i)) N'} (h : ∀ (v : (i : ι') → M₁ i), (f fun (i : ι') => 1 ⊗ₜ[R] v i) = g fun (i : ι') => 1 ⊗ₜ[R] v i) : f = g

theorem MultilinearMap.baseChange_hom_ext_iff {R : Type u_1} [CommSemiring R] {ι' : Type u_3} {M₁ : ι' → Type u_4} [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] {A : Type u_8} [CommSemiring A] [Algebra R A] {N' : Type u_9} [AddCommMonoid N'] [Module A N'] [Finite ι'] {f g : MultilinearMap A (fun (i : ι') => TensorProduct R A (M₁ i)) N'} : f = g ↔ ∀ (v : (i : ι') → M₁ i), (f fun (i : ι') => 1 ⊗ₜ[R] v i) = g fun (i : ι') => 1 ⊗ₜ[R] v i

def MultilinearMap.restrictFin {R : Type u_1} [CommSemiring R] {N : Type u_6} [AddCommMonoid N] [Module R N] {n : ℕ} {M₁ : Fin (n + 1) → Type u_10} [(i : Fin (n + 1)) → AddCommMonoid (M₁ i)] [(i : Fin (n + 1)) → Module R (M₁ i)] (f : MultilinearMap R M₁ N) (p : M₁ (Fin.last n)) : MultilinearMap R (fun (i : Fin n) => M₁ i.castSucc) N

Restrict a multilinear map on Fin (n + 1) to a multilinear map on Fin n along a chosen p : M₁ (Fin.last n).

Equations

• f.restrictFin p = { toFun := fun (v : (i : Fin n) → M₁ i.castSucc) => f fun (i : Fin (n + 1)) => Fin.lastCases p v i, map_update_add' := ⋯, map_update_smul' := ⋯ }

def MultilinearMap.restrictFinₗ {R : Type u_1} [CommSemiring R] {N : Type u_6} [AddCommMonoid N] [Module R N] {n : ℕ} {M₁ : Fin (n + 1) → Type u_10} [(i : Fin (n + 1)) → AddCommMonoid (M₁ i)] [(i : Fin (n + 1)) → Module R (M₁ i)] (f : MultilinearMap R M₁ N) : M₁ (Fin.last n) →ₗ[R] MultilinearMap R (fun (i : Fin n) => M₁ i.castSucc) N

restrictFin as linear map.

Equations

• f.restrictFinₗ = { toFun := fun (p : M₁ (Fin.last n)) => f.restrictFin p, map_add' := ⋯, map_smul' := ⋯ }

def MultilinearMap.restrictFinₗₗ {R : Type u_1} [CommSemiring R] {N : Type u_6} [AddCommMonoid N] [Module R N] {n : ℕ} {M₁ : Fin (n + 1) → Type u_10} [(i : Fin (n + 1)) → AddCommMonoid (M₁ i)] [(i : Fin (n + 1)) → Module R (M₁ i)] : MultilinearMap R M₁ N →ₗ[R] M₁ (Fin.last n) →ₗ[R] MultilinearMap R (fun (i : Fin n) => M₁ i.castSucc) N

restrictFin as a bilinear map.

Equations

• MultilinearMap.restrictFinₗₗ = { toFun := fun (f : MultilinearMap R M₁ N) => f.restrictFinₗ, map_add' := ⋯, map_smul' := ⋯ }

def MultilinearMap.baseChangeFinAux {R : Type u_1} [CommSemiring R] {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] {n : ℕ} {M₁ : Fin (n + 1) → Type u_10} [(i : Fin (n + 1)) → AddCommMonoid (M₁ i)] [(i : Fin (n + 1)) → Module R (M₁ i)] (ih : MultilinearMap R (fun (i : Fin n) => M₁ i.castSucc) N →ₗ[R] MultilinearMap A (fun (i : Fin n) => TensorProduct R A (M₁ i.castSucc)) (TensorProduct R A N)) (f : MultilinearMap R M₁ N) (v : (i : Fin n) → TensorProduct R A (M₁ i.castSucc)) : M₁ (Fin.last n) →ₗ[R] TensorProduct R A N

The induction step.

Equations

• MultilinearMap.baseChangeFinAux ih f v = { toFun := fun (p : M₁ (Fin.last n)) => (ih ((MultilinearMap.restrictFinₗₗ f) p)) v, map_add' := ⋯, map_smul' := ⋯ }

def MultilinearMap.baseChangeFinAuxMultilinear {R : Type u_1} [CommSemiring R] {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] {n : ℕ} {M₁ : Fin (n + 1) → Type u_10} [(i : Fin (n + 1)) → AddCommMonoid (M₁ i)] [(i : Fin (n + 1)) → Module R (M₁ i)] (ih : MultilinearMap R (fun (i : Fin n) => M₁ i.castSucc) N →ₗ[R] MultilinearMap A (fun (i : Fin n) => TensorProduct R A (M₁ i.castSucc)) (TensorProduct R A N)) (f : MultilinearMap R M₁ N) : MultilinearMap A (fun (i : Fin n) => TensorProduct R A (M₁ i.castSucc)) (M₁ (Fin.last n) →ₗ[R] TensorProduct R A N)

The induction step as a multilinear map.

Equations

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

def MultilinearMap.baseChangeFinAuxMultilinearₗ {R : Type u_1} [CommSemiring R] {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] {n : ℕ} {M₁ : Fin (n + 1) → Type u_10} [(i : Fin (n + 1)) → AddCommMonoid (M₁ i)] [(i : Fin (n + 1)) → Module R (M₁ i)] (ih : MultilinearMap R (fun (i : Fin n) => M₁ i.castSucc) N →ₗ[R] MultilinearMap A (fun (i : Fin n) => TensorProduct R A (M₁ i.castSucc)) (TensorProduct R A N)) : MultilinearMap R M₁ N →ₗ[R] MultilinearMap A (fun (i : Fin n) => TensorProduct R A (M₁ i.castSucc)) (M₁ (Fin.last n) →ₗ[R] TensorProduct R A N)

The induction step as a linear map to multilinear maps.

Equations

• MultilinearMap.baseChangeFinAuxMultilinearₗ ih = { toFun := fun (f : MultilinearMap R M₁ N) => MultilinearMap.baseChangeFinAuxMultilinear ih f, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def MultilinearMap.baseChangeFin (R : Type u_1) [CommSemiring R] (N : Type u_6) [AddCommMonoid N] [Module R N] (A : Type u_8) [CommSemiring A] [Algebra R A] (n : ℕ) (M₁ : Fin n → Type u_10) [(i : Fin n) → AddCommMonoid (M₁ i)] [(i : Fin n) → Module R (M₁ i)] : MultilinearMap R M₁ N →ₗ[R] MultilinearMap A (fun (i : Fin n) => TensorProduct R A (M₁ i)) (TensorProduct R A N)

Base change for multilinear maps with a finite indexing type. Here we use Fin n as a special case so that we can define the map inductively.

Equations

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

theorem MultilinearMap.baseChangeFin_apply_one_tmul {R : Type u_1} [CommSemiring R] {n : ℕ} {M₂ : Fin n → Type u_5} [(i : Fin n) → AddCommMonoid (M₂ i)] [(i : Fin n) → Module R (M₂ i)] {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] (f : MultilinearMap R M₂ N) (v : (i : Fin n) → M₂ i) : (((baseChangeFin R N A n M₂) f) fun (i : Fin n) => 1 ⊗ₜ[R] v i) = 1 ⊗ₜ[R] f v

@[simp]

theorem MultilinearMap.baseChangeFin_apply_tmul {R : Type u_1} [CommSemiring R] {n : ℕ} {M₂ : Fin n → Type u_5} [(i : Fin n) → AddCommMonoid (M₂ i)] [(i : Fin n) → Module R (M₂ i)] {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] (f : MultilinearMap R M₂ N) (c : Fin n → A) (v : (i : Fin n) → M₂ i) : (((baseChangeFin R N A n M₂) f) fun (i : Fin n) => c i ⊗ₜ[R] v i) = (∏ i : Fin n, c i) ⊗ₜ[R] f v

noncomputable def MultilinearMap.baseChangeOfEquiv (R : Type u_1) [CommSemiring R] {ι' : Type u_3} (M₁ : ι' → Type u_4) [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] {n : ℕ} (N : Type u_6) [AddCommMonoid N] [Module R N] (A : Type u_8) [CommSemiring A] [Algebra R A] (e : ι' ≃ Fin n) : MultilinearMap R M₁ N →ₗ[R] MultilinearMap A (fun (i : ι') => TensorProduct R A (M₁ i)) (TensorProduct R A N)

Base change for multilinear maps with a (finite) indexing type, with a chosen equiv ι ≃ Fin n.

Equations

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

@[simp]

theorem MultilinearMap.baseChangeOfEquiv_apply_tmul {R : Type u_1} [CommSemiring R] {ι' : Type u_3} {M₁ : ι' → Type u_4} [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] {n : ℕ} {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] [Fintype ι'] (e : ι' ≃ Fin n) (f : MultilinearMap R M₁ N) (c : ι' → A) (v : (i : ι') → M₁ i) : (((baseChangeOfEquiv R M₁ N A e) f) fun (i : ι') => c i ⊗ₜ[R] v i) = (∏ i : ι', c i) ⊗ₜ[R] f v

theorem MultilinearMap.baseChangeOfEquiv_eq {R : Type u_1} [CommSemiring R] {ι' : Type u_3} {M₁ : ι' → Type u_4} [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] {n : ℕ} {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] (e₁ e₂ : ι' ≃ Fin n) : baseChangeOfEquiv R M₁ N A e₁ = baseChangeOfEquiv R M₁ N A e₂

baseChangeOfEquiv is actually independent of the Equiv chosen.

noncomputable def MultilinearMap.baseChangeOfTrunc (R : Type u_1) [CommSemiring R] {ι' : Type u_3} (M₁ : ι' → Type u_4) [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] {n : ℕ} (N : Type u_6) [AddCommMonoid N] [Module R N] (A : Type u_8) [CommSemiring A] [Algebra R A] (e : Trunc (ι' ≃ Fin n)) : MultilinearMap R M₁ N →ₗ[R] MultilinearMap A (fun (i : ι') => TensorProduct R A (M₁ i)) (TensorProduct R A N)

Base change for multilinear maps indexed by a finite type, given by a term of Trunc (ι ≃ Fin n).

Equations

• MultilinearMap.baseChangeOfTrunc R M₁ N A e = Trunc.lift (MultilinearMap.baseChangeOfEquiv R M₁ N A) ⋯ e

noncomputable def MultilinearMap.baseChange (R : Type u_1) [CommSemiring R] {ι' : Type u_3} (M₁ : ι' → Type u_4) [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] (N : Type u_6) [AddCommMonoid N] [Module R N] (A : Type u_8) [CommSemiring A] [Algebra R A] [Finite ι'] : MultilinearMap R M₁ N →ₗ[R] MultilinearMap A (fun (i : ι') => TensorProduct R A (M₁ i)) (TensorProduct R A N)

Base change for multilinear maps indexed by a finite type.

Equations

• MultilinearMap.baseChange R M₁ N A = MultilinearMap.baseChangeOfTrunc R M₁ N A (Trunc.mk (Finite.equivFin ι'))

@[simp]

theorem MultilinearMap.baseChange_apply_tmul {R : Type u_1} [CommSemiring R] {ι' : Type u_3} {M₁ : ι' → Type u_4} [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] [Fintype ι'] (f : MultilinearMap R M₁ N) (c : ι' → A) (v : (i : ι') → M₁ i) : (((baseChange R M₁ N A) f) fun (i : ι') => c i ⊗ₜ[R] v i) = (∏ i : ι', c i) ⊗ₜ[R] f v

@[simp]

theorem MultilinearMap.baseChange_apply_one_tmul {R : Type u_1} [CommSemiring R] {ι' : Type u_3} {M₁ : ι' → Type u_4} [(i : ι') → AddCommMonoid (M₁ i)] [(i : ι') → Module R (M₁ i)] {N : Type u_6} [AddCommMonoid N] [Module R N] {A : Type u_8} [CommSemiring A] [Algebra R A] [Finite ι'] (f : MultilinearMap R M₁ N) (v : (i : ι') → M₁ i) : (((baseChange R M₁ N A) f) fun (i : ι') => 1 ⊗ₜ[R] v i) = 1 ⊗ₜ[R] f v

theorem SymmetricMap.baseChange_hom_ext {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_7} {A : Type u_8} [CommSemiring A] [Algebra R A] {N' : Type u_9} [AddCommMonoid N'] [Module A N'] [Finite ι] {f g : (TensorProduct R A M) [Σ^ι]→ₗ[A] N'} (h : ∀ (v : ι → M), (f fun (i : ι) => 1 ⊗ₜ[R] v i) = g fun (i : ι) => 1 ⊗ₜ[R] v i) : f = g

theorem SymmetricMap.baseChange_hom_ext_iff {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_7} {A : Type u_8} [CommSemiring A] [Algebra R A] {N' : Type u_9} [AddCommMonoid N'] [Module A N'] [Finite ι] {f g : (TensorProduct R A M) [Σ^ι]→ₗ[A] N'} : f = g ↔ ∀ (v : ι → M), (f fun (i : ι) => 1 ⊗ₜ[R] v i) = g fun (i : ι) => 1 ⊗ₜ[R] v i

noncomputable def SymmetricMap.baseChange (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_6) [AddCommMonoid N] [Module R N] (ι : Type u_7) (A : Type u_8) [CommSemiring A] [Algebra R A] [Finite ι] : M [Σ^ι]→ₗ[R] N →ₗ[R] (TensorProduct R A M) [Σ^ι]→ₗ[A] (TensorProduct R A N)

Base change for symmetric maps with a finite indexing type.

Equations

• SymmetricMap.baseChange R M N ι A = { toFun := fun (f : M [Σ^ι]→ₗ[R] N) => SymmetricMap.mk' ((MultilinearMap.baseChange R (fun (x : ι) => M) N A) ↑f) ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SymmetricMap.baseChange_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_6} [AddCommMonoid N] [Module R N] {ι : Type u_7} {A : Type u_8} [CommSemiring A] [Algebra R A] [Fintype ι] (f : M [Σ^ι]→ₗ[R] N) (c : ι → A) (v : ι → M) : (((baseChange R M N ι A) f) fun (i : ι) => c i ⊗ₜ[R] v i) = (∏ i : ι, c i) ⊗ₜ[R] f v

@[simp]

theorem SymmetricMap.baseChange_apply_one_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_6} [AddCommMonoid N] [Module R N] {ι : Type u_7} {A : Type u_8} [CommSemiring A] [Algebra R A] [Finite ι] (f : M [Σ^ι]→ₗ[R] N) (v : ι → M) : (((baseChange R M N ι A) f) fun (i : ι) => 1 ⊗ₜ[R] v i) = 1 ⊗ₜ[R] f v