Documentation

TauCeti.LinearAlgebra.Multilinear.Curry

Currying the first argument of a multilinear map into its values #

A multilinear map f in n + 1 arguments determines the multilinear map in the last n arguments whose value at (m₁, …, mₙ) is the linear map m₀ ↦ f (m₀, m₁, …, mₙ). This gives a linear equivalence TauCeti.multilinearCurryFirstEquiv. It differs from Mathlib's multilinearCurryLeftEquiv, which curries the first argument outside, into linear maps valued in multilinear maps, and is the first-argument counterpart of multilinearCurryRightEquiv.

Cochains with values in linear maps out of an algebra arise in this way from cochains with one more argument, which is how scalar Hochschild cochains are compared with cochains valued in the dual bimodule.

Main definitions #

source
def TauCeti.multilinearCurryFirstEquiv (R : Type u_1) {n : ℕ} (M : Fin (n + 1) → Type u_2) (N : Type u_3) [CommSemiring R] [(i : Fin (n + 1)) → AddCommMonoid (M i)] [(i : Fin (n + 1)) → Module R (M i)] [AddCommMonoid N] [Module R N] :
((Π (a : Fin (n + 1)), M a) →ₘₗ[R] N) ≃ₗ[R] (Π (i : Fin n), M i.succ) →ₘₗ[R] M 0 →ₗ[R] N

Currying the first argument of a multilinear map into its values: f ↦ ((m₁, …, mₙ) ↦ (m₀ ↦ f (m₀, m₁, …, mₙ))).

Instances For
    source
    @[simp]
    theorem TauCeti.multilinearCurryFirstEquiv_apply_apply {R : Type u_1} {n : ℕ} {M : Fin (n + 1) → Type u_2} {N : Type u_3} [CommSemiring R] [(i : Fin (n + 1)) → AddCommMonoid (M i)] [(i : Fin (n + 1)) → Module R (M i)] [AddCommMonoid N] [Module R N] (f : (Π (a : Fin (n + 1)), M a) →ₘₗ[R] N) (m : (i : Fin n) → M i.succ) (x : M 0) :
    (((multilinearCurryFirstEquiv R M N) f) m) x = f (Fin.cons x m)

    The curried map evaluates f on the tuple with x prepended.

    source
    @[simp]
    theorem TauCeti.multilinearCurryFirstEquiv_symm_apply {R : Type u_1} {n : ℕ} {M : Fin (n + 1) → Type u_2} {N : Type u_3} [CommSemiring R] [(i : Fin (n + 1)) → AddCommMonoid (M i)] [(i : Fin (n + 1)) → Module R (M i)] [AddCommMonoid N] [Module R N] (g : (Π (i : Fin n), M i.succ) →ₘₗ[R] M 0 →ₗ[R] N) (m : (i : Fin (n + 1)) → M i) :
    ((multilinearCurryFirstEquiv R M N).symm g) m = (g (Fin.tail m)) (m 0)

    The uncurried map evaluates on the last n entries and then on the first one.