Documentation

Mathlib.LinearAlgebra.Alternating.Curry

Currying alternating forms #

In this file we define AlternatingMap.curryLeft which interprets an alternating map in n + 1 variables as a linear map in the 0th variable taking values in the alternating maps in n variables.

source
def AlternatingMap.curryLeft {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) :
M →ₗ[R] M [⋀^Fin n]→ₗ[R] N

Given an alternating map f in n+1 variables, split the first variable to obtain a linear map into alternating maps in n variables, given by x ↦ (m ↦ f (Matrix.vecCons x m)). It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.

This is MultilinearMap.curryLeft for AlternatingMap. See also AlternatingMap.curryLeftLinearMap.

Instances For
    source
    @[simp]
    theorem AlternatingMap.curryLeft_apply_toMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M) :
    ↑(f.curryLeft m) = (↑f).curryLeft m
    source
    @[simp]
    theorem AlternatingMap.curryLeft_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (x : M) (v : Fin n → M) :
    (f.curryLeft x) v = f (Matrix.vecCons x v)
    source
    @[simp]
    theorem AlternatingMap.curryLeft_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} :
    curryLeft 0 = 0
    source
    @[simp]
    theorem AlternatingMap.curryLeft_add {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f g : M [⋀^Fin n.succ]→ₗ[R] N) :
    (f + g).curryLeft = f.curryLeft + g.curryLeft
    source
    @[simp]
    theorem AlternatingMap.curryLeft_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (r : R) (f : M [⋀^Fin n.succ]→ₗ[R] N) :
    (r • f).curryLeft = r • f.curryLeft
    source
    def AlternatingMap.curryLeftLinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} :
    M [⋀^Fin n.succ]→ₗ[R] N →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N

    AlternatingMap.curryLeft as a LinearMap. This is a separate definition as dot notation does not work for this version.

    Instances For
      source
      @[simp]
      theorem AlternatingMap.curryLeftLinearMap_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) :
      curryLeftLinearMap f = f.curryLeft
      source
      @[simp]
      theorem AlternatingMap.curryLeft_same {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ.succ]→ₗ[R] N) (m : M) :
      (f.curryLeft m).curryLeft m = 0

      Currying with the same element twice gives the zero map.

      source
      @[simp]
      theorem AlternatingMap.curryLeft_compAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {N₂ : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R N₂] {n : ℕ} (g : N →ₗ[R] N₂) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M) :
      (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m)
      source
      @[simp]
      theorem AlternatingMap.curryLeft_compLinearMap {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M] [Module R M₂] [Module R N] {n : ℕ} (g : M₂ →ₗ[R] M) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M₂) :
      (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g