Documentation

Mathlib.LinearAlgebra.Multilinear.Basic

Multilinear maps #

We define multilinear maps as maps from ∀ (i : ι), M₁ i to M₂ which are linear in each coordinate. Here, M₁ i and M₂ are modules over a ring R, and ι is an arbitrary type (although some statements will require it to be a fintype). This space, denoted by MultilinearMap R M₁ M₂, inherits a module structure by pointwise addition and multiplication.

Main definitions #

We also register isomorphisms corresponding to currying or uncurrying variables, transforming a multilinear function f on n+1 variables into a linear function taking values in multilinear functions in n variables, and into a multilinear function in n variables taking values in linear functions. These operations are called f.curryLeft and f.curryRight respectively (with inverses f.uncurryLeft and f.uncurryRight). These operations induce linear equivalences between spaces of multilinear functions in n+1 variables and spaces of linear functions into multilinear functions in n variables (resp. multilinear functions in n variables taking values in linear functions), called respectively multilinearCurryLeftEquiv and multilinearCurryRightEquiv.

Implementation notes #

Expressing that a map is linear along the i-th coordinate when all other coordinates are fixed can be done in two (equivalent) different ways:

The second way is more artificial as the value of m at i is not relevant, but it has the advantage of avoiding subtype inclusion issues. This is the definition we use, based on Function.update that allows to change the value of m at i.

Note that the use of Function.update requires a DecidableEq ι term to appear somewhere in the statement of MultilinearMap.map_add' and MultilinearMap.map_smul'. Three possible choices are:

  1. Requiring DecidableEq ι as an argument to MultilinearMap (as we did originally).
  2. Using Classical.decEq ι in the statement of map_add' and map_smul'.
  3. Quantifying over all possible DecidableEq ι instances in the statement of map_add' and map_smul'.

Option 1 works fine, but puts unnecessary constraints on the user (the zero map certainly does not need decidability). Option 2 looks great at first, but in the common case when ι = Fin n it introduces non-defeq decidability instance diamonds within the context of proving map_add' and map_smul', of the form Fin.decidableEq n = Classical.decEq (Fin n). Option 3 of course does something similar, but of the form Fin.decidableEq n = _inst, which is much easier to clean up since _inst is a free variable and so the equality can just be substituted.

structure MultilinearMap (R : Type uR) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Type (max (max uι v₁) v₂)

Multilinear maps over the ring R, from ∀ i, M₁ i to M₂ where M₁ i and M₂ are modules over R.

Instances For
    instance MultilinearMap.instFunLikeMultilinearMapForAll {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
    FunLike (MultilinearMap R M₁ M₂) ((i : ι) → M₁ i) fun x => M₂
    Equations
    • MultilinearMap.instFunLikeMultilinearMapForAll = { coe := fun f => f.toFun, coe_injective' := (_ : ∀ (f g : MultilinearMap R M₁ M₂), (fun f => f.toFun) f = (fun f => f.toFun) gf = g) }
    @[simp]
    theorem MultilinearMap.toFun_eq_coe {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) :
    f.toFun = f
    @[simp]
    theorem MultilinearMap.coe_mk {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : ((i : ι) → M₁ i) → M₂) (h₁ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)) (h₂ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (Function.update m i (c x)) = c f (Function.update m i x)) :
    { toFun := f, map_add' := h₁, map_smul' := h₂ } = f
    theorem MultilinearMap.congr_fun {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {f : MultilinearMap R M₁ M₂} {g : MultilinearMap R M₁ M₂} (h : f = g) (x : (i : ι) → M₁ i) :
    f x = g x
    theorem MultilinearMap.congr_arg {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {x : (i : ι) → M₁ i} {y : (i : ι) → M₁ i} (h : x = y) :
    f x = f y
    theorem MultilinearMap.coe_injective {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
    Function.Injective FunLike.coe
    theorem MultilinearMap.coe_inj {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {f : MultilinearMap R M₁ M₂} {g : MultilinearMap R M₁ M₂} :
    f = g f = g
    theorem MultilinearMap.ext {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {f : MultilinearMap R M₁ M₂} {f' : MultilinearMap R M₁ M₂} (H : ∀ (x : (i : ι) → M₁ i), f x = f' x) :
    f = f'
    theorem MultilinearMap.ext_iff {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {f : MultilinearMap R M₁ M₂} {g : MultilinearMap R M₁ M₂} :
    f = g ∀ (x : (i : ι) → M₁ i), f x = g x
    @[simp]
    theorem MultilinearMap.mk_coe {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (h₁ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)) (h₂ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (Function.update m i (c x)) = c f (Function.update m i x)) :
    { toFun := f, map_add' := h₁, map_smul' := h₂ } = f
    @[simp]
    theorem MultilinearMap.map_add {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) (y : M₁ i) :
    f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
    @[simp]
    theorem MultilinearMap.map_smul {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i) :
    f (Function.update m i (c x)) = c f (Function.update m i x)
    theorem MultilinearMap.map_coord_zero {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {m : (i : ι) → M₁ i} (i : ι) (h : m i = 0) :
    f m = 0
    @[simp]
    theorem MultilinearMap.map_update_zero {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) :
    f (Function.update m i 0) = 0
    @[simp]
    theorem MultilinearMap.map_zero {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [Nonempty ι] :
    f 0 = 0
    instance MultilinearMap.instAddMultilinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
    Add (MultilinearMap R M₁ M₂)
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem MultilinearMap.add_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (f' : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) :
    ↑(f + f') m = f m + f' m
    instance MultilinearMap.instZeroMultilinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
    Zero (MultilinearMap R M₁ M₂)
    Equations
    • One or more equations did not get rendered due to their size.
    instance MultilinearMap.instInhabitedMultilinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
    Equations
    • MultilinearMap.instInhabitedMultilinearMap = { default := 0 }
    @[simp]
    theorem MultilinearMap.zero_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (m : (i : ι) → M₁ i) :
    0 m = 0
    instance MultilinearMap.instSMulMultilinearMap {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] {R' : Type u_1} {A : Type u_2} [Monoid R'] [Semiring A] [(i : ι) → Module A (M₁ i)] [DistribMulAction R' M₂] [Module A M₂] [SMulCommClass A R' M₂] :
    SMul R' (MultilinearMap A M₁ M₂)
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem MultilinearMap.smul_apply {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] {R' : Type u_1} {A : Type u_2} [Monoid R'] [Semiring A] [(i : ι) → Module A (M₁ i)] [DistribMulAction R' M₂] [Module A M₂] [SMulCommClass A R' M₂] (f : MultilinearMap A M₁ M₂) (c : R') (m : (i : ι) → M₁ i) :
    ↑(c f) m = c f m
    theorem MultilinearMap.coe_smul {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] {R' : Type u_1} {A : Type u_2} [Monoid R'] [Semiring A] [(i : ι) → Module A (M₁ i)] [DistribMulAction R' M₂] [Module A M₂] [SMulCommClass A R' M₂] (c : R') (f : MultilinearMap A M₁ M₂) :
    ↑(c f) = c f
    instance MultilinearMap.addCommMonoid {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem MultilinearMap.coeAddMonoidHom_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
    ∀ (a : MultilinearMap R M₁ M₂) (a_1 : (i : ι) → M₁ i), MultilinearMap.coeAddMonoidHom a a_1 = a a_1
    def MultilinearMap.coeAddMonoidHom {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
    MultilinearMap R M₁ M₂ →+ ((i : ι) → M₁ i) → M₂

    Coercion of a multilinear map to a function as an additive monoid homomorphism.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem MultilinearMap.coe_sum {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {α : Type u_1} (f : αMultilinearMap R M₁ M₂) (s : Finset α) :
      ↑(Finset.sum s fun a => f a) = Finset.sum s fun a => ↑(f a)
      theorem MultilinearMap.sum_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {α : Type u_1} (f : αMultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) {s : Finset α} :
      ↑(Finset.sum s fun a => f a) m = Finset.sum s fun a => ↑(f a) m
      @[simp]
      theorem MultilinearMap.toLinearMap_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) :
      ↑(MultilinearMap.toLinearMap f m i) x = f (Function.update m i x)
      def MultilinearMap.toLinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) :
      M₁ i →ₗ[R] M₂

      If f is a multilinear map, then f.toLinearMap m i is the linear map obtained by fixing all coordinates but i equal to those of m, and varying the i-th coordinate.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem MultilinearMap.prod_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₃) (m : (i : ι) → M₁ i) :
        ↑(MultilinearMap.prod f g) m = (f m, g m)
        def MultilinearMap.prod {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₃) :
        MultilinearMap R M₁ (M₂ × M₃)

        The cartesian product of two multilinear maps, as a multilinear map.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem MultilinearMap.pi_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → MultilinearMap R M₁ (M' i)) (m : (i : ι) → M₁ i) (i : ι') :
          ↑(MultilinearMap.pi f) m i = ↑(f i) m
          def MultilinearMap.pi {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → MultilinearMap R M₁ (M' i)) :
          MultilinearMap R M₁ ((i : ι') → M' i)

          Combine a family of multilinear maps with the same domain and codomains M' i into a multilinear map taking values in the space of functions ∀ i, M' i.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem MultilinearMap.ofSubsingleton_apply (R : Type uR) {ι : Type uι} (M₂ : Type v₂) [Semiring R] [AddCommMonoid M₂] [Module R M₂] [Subsingleton ι] (i' : ι) (f : ιM₂) :
            def MultilinearMap.ofSubsingleton (R : Type uR) {ι : Type uι} (M₂ : Type v₂) [Semiring R] [AddCommMonoid M₂] [Module R M₂] [Subsingleton ι] (i' : ι) :
            MultilinearMap R (fun x => M₂) M₂

            The evaluation map from ι → M₂ to M₂ is multilinear at a given i when ι is subsingleton.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem MultilinearMap.constOfIsEmpty_apply (R : Type uR) {ι : Type uι} (M₁ : ιType v₁) {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [IsEmpty ι] (m : M₂) :
              ↑(MultilinearMap.constOfIsEmpty R M₁ m) = Function.const ((i : ι) → M₁ i) m
              def MultilinearMap.constOfIsEmpty (R : Type uR) {ι : Type uι} (M₁ : ιType v₁) {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [IsEmpty ι] (m : M₂) :
              MultilinearMap R M₁ M₂

              The constant map is multilinear when ι is empty.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def MultilinearMap.restr {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M'] [Module R M₂] [Module R M'] {k : } {n : } (f : MultilinearMap R (fun x => M') M₂) (s : Finset (Fin n)) (hk : Finset.card s = k) (z : M') :
                MultilinearMap R (fun x => M') M₂

                Given a multilinear map f on n variables (parameterized by Fin n) and a subset s of k of these variables, one gets a new multilinear map on Fin k by varying these variables, and fixing the other ones equal to a given value z. It is denoted by f.restr s hk z, where hk is a proof that the cardinality of s is k. The implicit identification between Fin k and s that we use is the canonical (increasing) bijection.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem MultilinearMap.cons_add {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [Semiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M (Fin.succ i)) (x : M 0) (y : M 0) :
                  f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)

                  In the specific case of multilinear maps on spaces indexed by Fin (n+1), where one can build an element of ∀ (i : Fin (n+1)), M i using cons, one can express directly the additivity of a multilinear map along the first variable.

                  theorem MultilinearMap.cons_smul {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [Semiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M (Fin.succ i)) (c : R) (x : M 0) :
                  f (Fin.cons (c x) m) = c f (Fin.cons x m)

                  In the specific case of multilinear maps on spaces indexed by Fin (n+1), where one can build an element of ∀ (i : Fin (n+1)), M i using cons, one can express directly the multiplicativity of a multilinear map along the first variable.

                  theorem MultilinearMap.snoc_add {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [Semiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M (Fin.castSucc i)) (x : M (Fin.last n)) (y : M (Fin.last n)) :
                  f (Fin.snoc m (x + y)) = f (Fin.snoc m x) + f (Fin.snoc m y)

                  In the specific case of multilinear maps on spaces indexed by Fin (n+1), where one can build an element of ∀ (i : Fin (n+1)), M i using snoc, one can express directly the additivity of a multilinear map along the first variable.

                  theorem MultilinearMap.snoc_smul {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [Semiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M (Fin.castSucc i)) (c : R) (x : M (Fin.last n)) :
                  f (Fin.snoc m (c x)) = c f (Fin.snoc m x)

                  In the specific case of multilinear maps on spaces indexed by Fin (n+1), where one can build an element of ∀ (i : Fin (n+1)), M i using cons, one can express directly the multiplicativity of a multilinear map along the first variable.

                  def MultilinearMap.compLinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) (f : (i : ι) → M₁ i →ₗ[R] M₁' i) :
                  MultilinearMap R M₁ M₂

                  If g is a multilinear map and f is a collection of linear maps, then g (f₁ m₁, ..., fₙ mₙ) is again a multilinear map, that we call g.compLinearMap f.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem MultilinearMap.compLinearMap_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (m : (i : ι) → M₁ i) :
                    ↑(MultilinearMap.compLinearMap g f) m = g fun i => ↑(f i) (m i)
                    theorem MultilinearMap.compLinearMap_assoc {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] {M₁'' : ιType u_2} [(i : ι) → AddCommMonoid (M₁'' i)] [(i : ι) → Module R (M₁'' i)] (g : MultilinearMap R M₁'' M₂) (f₁ : (i : ι) → M₁' i →ₗ[R] M₁'' i) (f₂ : (i : ι) → M₁ i →ₗ[R] M₁' i) :

                    Composing a multilinear map twice with a linear map in each argument is the same as composing with their composition.

                    @[simp]
                    theorem MultilinearMap.zero_compLinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) :

                    Composing the zero multilinear map with a linear map in each argument.

                    @[simp]
                    theorem MultilinearMap.compLinearMap_id {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) :
                    (MultilinearMap.compLinearMap g fun x => LinearMap.id) = g

                    Composing a multilinear map with the identity linear map in each argument.

                    theorem MultilinearMap.compLinearMap_injective {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (hf : ∀ (i : ι), Function.Surjective ↑(f i)) :

                    Composing with a family of surjective linear maps is injective.

                    theorem MultilinearMap.compLinearMap_inj {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (hf : ∀ (i : ι), Function.Surjective ↑(f i)) (g₁ : MultilinearMap R M₁' M₂) (g₂ : MultilinearMap R M₁' M₂) :
                    @[simp]
                    theorem MultilinearMap.comp_linearEquiv_eq_zero_iff {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) (f : (i : ι) → M₁ i ≃ₗ[R] M₁' i) :
                    (MultilinearMap.compLinearMap g fun i => ↑(f i)) = 0 g = 0

                    Composing a multilinear map with a linear equiv on each argument gives the zero map if and only if the multilinear map is the zero map.

                    theorem MultilinearMap.map_piecewise_add {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (m' : (i : ι) → M₁ i) (t : Finset ι) :
                    f (Finset.piecewise t (m + m') m') = Finset.sum (Finset.powerset t) fun s => f (Finset.piecewise s m m')

                    If one adds to a vector m' another vector m, but only for coordinates in a finset t, then the image under a multilinear map f is the sum of f (s.piecewise m m') along all subsets s of t. This is mainly an auxiliary statement to prove the result when t = univ, given in map_add_univ, although it can be useful in its own right as it does not require the index set ι to be finite.

                    theorem MultilinearMap.map_add_univ {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] [Fintype ι] (m : (i : ι) → M₁ i) (m' : (i : ι) → M₁ i) :
                    f (m + m') = Finset.sum Finset.univ fun s => f (Finset.piecewise s m m')

                    Additivity of a multilinear map along all coordinates at the same time, writing f (m + m') as the sum of f (s.piecewise m m') over all sets s.

                    theorem MultilinearMap.map_sum_finset_aux {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ιType u_1} (g : (i : ι) → α iM₁ i) (A : (i : ι) → Finset (α i)) [DecidableEq ι] [Fintype ι] {n : } (h : (Finset.sum Finset.univ fun i => Finset.card (A i)) = n) :
                    (f fun i => Finset.sum (A i) fun j => g i j) = Finset.sum (Fintype.piFinset A) fun r => f fun i => g i (r i)

                    If f is multilinear, then f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ) is the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions with r 1 ∈ A₁, ..., r n ∈ Aₙ. This follows from multilinearity by expanding successively with respect to each coordinate. Here, we give an auxiliary statement tailored for an inductive proof. Use instead map_sum_finset.

                    theorem MultilinearMap.map_sum_finset {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ιType u_1} (g : (i : ι) → α iM₁ i) (A : (i : ι) → Finset (α i)) [DecidableEq ι] [Fintype ι] :
                    (f fun i => Finset.sum (A i) fun j => g i j) = Finset.sum (Fintype.piFinset A) fun r => f fun i => g i (r i)

                    If f is multilinear, then f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ) is the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions with r 1 ∈ A₁, ..., r n ∈ Aₙ. This follows from multilinearity by expanding successively with respect to each coordinate.

                    theorem MultilinearMap.map_sum {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ιType u_1} (g : (i : ι) → α iM₁ i) [DecidableEq ι] [Fintype ι] [(i : ι) → Fintype (α i)] :
                    (f fun i => Finset.sum Finset.univ fun j => g i j) = Finset.sum Finset.univ fun r => f fun i => g i (r i)

                    If f is multilinear, then f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ) is the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions r. This follows from multilinearity by expanding successively with respect to each coordinate.

                    theorem MultilinearMap.map_update_sum {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {α : Type u_2} [DecidableEq ι] (t : Finset α) (i : ι) (g : αM₁ i) (m : (i : ι) → M₁ i) :
                    f (Function.update m i (Finset.sum t fun a => g a)) = Finset.sum t fun a => f (Function.update m i (g a))
                    @[simp]
                    theorem MultilinearMap.codRestrict_apply_coe {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) (v : (i : ι) → M₁ i) :
                    ↑(↑(MultilinearMap.codRestrict f p h) v) = f v
                    def MultilinearMap.codRestrict {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) :
                    MultilinearMap R M₁ { x // x p }

                    Restrict the codomain of a multilinear map to a submodule.

                    This is the multilinear version of LinearMap.codRestrict.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def MultilinearMap.restrictScalars (R : Type uR) {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {A : Type u_1} [Semiring A] [SMul R A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [∀ (i : ι), IsScalarTower R A (M₁ i)] [IsScalarTower R A M₂] (f : MultilinearMap A M₁ M₂) :
                      MultilinearMap R M₁ M₂

                      Reinterpret an A-multilinear map as an R-multilinear map, if A is an algebra over R and their actions on all involved modules agree with the action of R on A.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem MultilinearMap.coe_restrictScalars (R : Type uR) {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] {A : Type u_1} [Semiring A] [SMul R A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [∀ (i : ι), IsScalarTower R A (M₁ i)] [IsScalarTower R A M₂] (f : MultilinearMap A M₁ M₂) :
                        @[simp]
                        theorem MultilinearMap.domDomCongr_apply {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : MultilinearMap R (fun x => M₂) M₃) (v : ι₂M₂) :
                        ↑(MultilinearMap.domDomCongr σ m) v = m fun i => v (σ i)
                        def MultilinearMap.domDomCongr {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : MultilinearMap R (fun x => M₂) M₃) :
                        MultilinearMap R (fun x => M₂) M₃

                        Transfer the arguments to a map along an equivalence between argument indices.

                        The naming is derived from Finsupp.domCongr, noting that here the permutation applies to the domain of the domain.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem MultilinearMap.domDomCongr_trans {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} (σ₁ : ι₁ ι₂) (σ₂ : ι₂ ι₃) (m : MultilinearMap R (fun x => M₂) M₃) :
                          theorem MultilinearMap.domDomCongr_mul {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} (σ₁ : Equiv.Perm ι₁) (σ₂ : Equiv.Perm ι₁) (m : MultilinearMap R (fun x => M₂) M₃) :
                          @[simp]
                          theorem MultilinearMap.domDomCongrEquiv_symm_apply {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : MultilinearMap R (fun x => M₂) M₃) :
                          @[simp]
                          theorem MultilinearMap.domDomCongrEquiv_apply {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : MultilinearMap R (fun x => M₂) M₃) :
                          def MultilinearMap.domDomCongrEquiv {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
                          MultilinearMap R (fun x => M₂) M₃ ≃+ MultilinearMap R (fun x => M₂) M₃

                          MultilinearMap.domDomCongr as an equivalence.

                          This is declared separately because it does not work with dot notation.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem MultilinearMap.domDomCongr_eq_iff {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (f : MultilinearMap R (fun x => M₂) M₃) (g : MultilinearMap R (fun x => M₂) M₃) :

                            The results of applying domDomCongr to two maps are equal if and only if those maps are.

                            def LinearMap.compMultilinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) :
                            MultilinearMap R M₁ M₃

                            Composing a multilinear map with a linear map gives again a multilinear map.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem LinearMap.coe_compMultilinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) :
                              @[simp]
                              theorem LinearMap.compMultilinearMap_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) :
                              ↑(LinearMap.compMultilinearMap g f) m = g (f m)
                              @[simp]
                              theorem LinearMap.subtype_compMultilinearMap_codRestrict {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) :

                              The multilinear version of LinearMap.subtype_comp_codRestrict

                              @[simp]
                              theorem LinearMap.compMultilinearMap_codRestrict {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (p : Submodule R M₃) (h : ∀ (c : M₂), g c p) :

                              The multilinear version of LinearMap.comp_codRestrict

                              @[simp]
                              theorem LinearMap.compMultilinearMap_domDomCongr {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} {M' : Type v'} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M'] [Module R M₂] [Module R M₃] [Module R M'] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R (fun x => M') M₂) :
                              instance MultilinearMap.instDistribMulActionMultilinearMapToAddMonoidAddCommMonoid {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Monoid S] [DistribMulAction S M₂] [Module R M₂] [SMulCommClass R S M₂] :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              instance MultilinearMap.instModuleMultilinearMapAddCommMonoid {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Semiring S] [Module S M₂] [Module R M₂] [SMulCommClass R S M₂] :
                              Module S (MultilinearMap R M₁ M₂)

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              instance MultilinearMap.instNoZeroSMulDivisorsMultilinearMapToZeroToMonoidWithZeroInstZeroMultilinearMapInstSMulMultilinearMapToMonoidToDistribMulAction {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Semiring S] [Module S M₂] [Module R M₂] [SMulCommClass R S M₂] [NoZeroSMulDivisors S M₂] :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[simp]
                              theorem MultilinearMap.domDomCongrLinearEquiv'_symm_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Semiring S] [Module S M₂] [Module R M₂] [SMulCommClass R S M₂] {ι' : Type u_1} (σ : ι ι') (f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂) :
                              ↑(LinearEquiv.symm (MultilinearMap.domDomCongrLinearEquiv' R S M₁ M₂ σ)) f = { toFun := f ↑(Equiv.piCongrLeft' M₁ σ), map_add' := (_ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), (f ↑(Equiv.piCongrLeft' M₁ σ)) (Function.update m i (x + y)) = (f ↑(Equiv.piCongrLeft' M₁ σ)) (Function.update m i x) + (f ↑(Equiv.piCongrLeft' M₁ σ)) (Function.update m i y)), map_smul' := (_ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), (f ↑(Equiv.piCongrLeft' M₁ σ)) (Function.update m i (c x)) = c (f ↑(Equiv.piCongrLeft' M₁ σ)) (Function.update m i x)) }
                              @[simp]
                              theorem MultilinearMap.domDomCongrLinearEquiv'_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Semiring S] [Module S M₂] [Module R M₂] [SMulCommClass R S M₂] {ι' : Type u_1} (σ : ι ι') (f : MultilinearMap R M₁ M₂) :
                              ↑(MultilinearMap.domDomCongrLinearEquiv' R S M₁ M₂ σ) f = { toFun := f (Equiv.piCongrLeft' M₁ σ).symm, map_add' := (_ : ∀ [inst : DecidableEq ι'] (m : (i : ι') → M₁ (σ.symm i)) (i : ι') (x y : M₁ (σ.symm i)), (f (Equiv.piCongrLeft' M₁ σ).symm) (Function.update m i (x + y)) = (f (Equiv.piCongrLeft' M₁ σ).symm) (Function.update m i x) + (f (Equiv.piCongrLeft' M₁ σ).symm) (Function.update m i y)), map_smul' := (_ : ∀ [inst : DecidableEq ι'] (m : (i : ι') → M₁ (σ.symm i)) (i : ι') (c : R) (x : M₁ (σ.symm i)), (f (Equiv.piCongrLeft' M₁ σ).symm) (Function.update m i (c x)) = c (f (Equiv.piCongrLeft' M₁ σ).symm) (Function.update m i x)) }
                              def MultilinearMap.domDomCongrLinearEquiv' (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Semiring S] [Module S M₂] [Module R M₂] [SMulCommClass R S M₂] {ι' : Type u_1} (σ : ι ι') :
                              MultilinearMap R M₁ M₂ ≃ₗ[S] MultilinearMap R (fun i => M₁ (σ.symm i)) M₂

                              The dependent version of MultilinearMap.domDomCongrLinearEquiv.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem MultilinearMap.constLinearEquivOfIsEmpty_symm_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Semiring S] [Module S M₂] [Module R M₂] [SMulCommClass R S M₂] [IsEmpty ι] (f : MultilinearMap R M₁ M₂) :
                                @[simp]
                                theorem MultilinearMap.constLinearEquivOfIsEmpty_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Semiring S] [Module S M₂] [Module R M₂] [SMulCommClass R S M₂] [IsEmpty ι] (m : M₂) :
                                def MultilinearMap.constLinearEquivOfIsEmpty (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [AddCommMonoid M₂] [Semiring S] [Module S M₂] [Module R M₂] [SMulCommClass R S M₂] [IsEmpty ι] :
                                M₂ ≃ₗ[S] MultilinearMap R M₁ M₂

                                The space of constant maps is equivalent to the space of maps that are multilinear with respect to an empty family.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem MultilinearMap.domDomCongrLinearEquiv_symm_apply (R : Type uR) (S : Type uS) (M₂ : Type v₂) (M₃ : Type v₃) [Semiring R] [AddCommMonoid M₂] [Semiring S] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
                                  ∀ (a : MultilinearMap R (fun x => M₂) M₃), ↑(LinearEquiv.symm (MultilinearMap.domDomCongrLinearEquiv R S M₂ M₃ σ)) a = Equiv.invFun (MultilinearMap.domDomCongrEquiv σ).toEquiv a
                                  @[simp]
                                  theorem MultilinearMap.domDomCongrLinearEquiv_apply (R : Type uR) (S : Type uS) (M₂ : Type v₂) (M₃ : Type v₃) [Semiring R] [AddCommMonoid M₂] [Semiring S] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
                                  ∀ (a : MultilinearMap R (fun x => M₂) M₃), ↑(MultilinearMap.domDomCongrLinearEquiv R S M₂ M₃ σ) a = Equiv.toFun (MultilinearMap.domDomCongrEquiv σ).toEquiv a
                                  def MultilinearMap.domDomCongrLinearEquiv (R : Type uR) (S : Type uS) (M₂ : Type v₂) (M₃ : Type v₃) [Semiring R] [AddCommMonoid M₂] [Semiring S] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
                                  MultilinearMap R (fun x => M₂) M₃ ≃ₗ[S] MultilinearMap R (fun x => M₂) M₃

                                  MultilinearMap.domDomCongr as a LinearEquiv.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem MultilinearMap.map_piecewise_smul {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (c : ιR) (m : (i : ι) → M₁ i) (s : Finset ι) :
                                    f (Finset.piecewise s (fun i => c i m i) m) = (Finset.prod s fun i => c i) f m

                                    If one multiplies by c i the coordinates in a finset s, then the image under a multilinear map is multiplied by ∏ i in s, c i. This is mainly an auxiliary statement to prove the result when s = univ, given in map_smul_univ, although it can be useful in its own right as it does not require the index set ι to be finite.

                                    theorem MultilinearMap.map_smul_univ {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [Fintype ι] (c : ιR) (m : (i : ι) → M₁ i) :
                                    (f fun i => c i m i) = (Finset.prod Finset.univ fun i => c i) f m

                                    Multiplicativity of a multilinear map along all coordinates at the same time, writing f (fun i => c i • m i) as (∏ i, c i) • f m.

                                    @[simp]
                                    theorem MultilinearMap.map_update_smul {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] [Fintype ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i) :
                                    f (Function.update (c m) i x) = c ^ (Fintype.card ι - 1) f (Function.update m i x)
                                    def MultilinearMap.mkPiAlgebra (R : Type uR) (ι : Type uι) [CommSemiring R] (A : Type u_1) [CommSemiring A] [Algebra R A] [Fintype ι] :
                                    MultilinearMap R (fun x => A) A

                                    Given an R-algebra A, mkPiAlgebra is the multilinear map on A^ι associating to m the product of all the m i.

                                    See also MultilinearMap.mkPiAlgebraFin for a version that works with a non-commutative algebra A but requires ι = Fin n.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem MultilinearMap.mkPiAlgebra_apply {R : Type uR} {ι : Type uι} [CommSemiring R] {A : Type u_1} [CommSemiring A] [Algebra R A] [Fintype ι] (m : ιA) :
                                      ↑(MultilinearMap.mkPiAlgebra R ι A) m = Finset.prod Finset.univ fun i => m i
                                      def MultilinearMap.mkPiAlgebraFin (R : Type uR) (n : ) [CommSemiring R] (A : Type u_1) [Semiring A] [Algebra R A] :
                                      MultilinearMap R (fun x => A) A

                                      Given an R-algebra A, mkPiAlgebraFin is the multilinear map on A^n associating to m the product of all the m i.

                                      See also MultilinearMap.mkPiAlgebra for a version that assumes [CommSemiring A] but works for A^ι with any finite type ι.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem MultilinearMap.mkPiAlgebraFin_apply {R : Type uR} {n : } [CommSemiring R] {A : Type u_1} [Semiring A] [Algebra R A] (m : Fin nA) :
                                        theorem MultilinearMap.mkPiAlgebraFin_apply_const {R : Type uR} {n : } [CommSemiring R] {A : Type u_1} [Semiring A] [Algebra R A] (a : A) :
                                        (↑(MultilinearMap.mkPiAlgebraFin R n A) fun x => a) = a ^ n
                                        def MultilinearMap.smulRight {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ R) (z : M₂) :
                                        MultilinearMap R M₁ M₂

                                        Given an R-multilinear map f taking values in R, f.smulRight z is the map sending m to f m • z.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem MultilinearMap.smulRight_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ R) (z : M₂) (m : (i : ι) → M₁ i) :
                                          ↑(MultilinearMap.smulRight f z) m = f m z
                                          def MultilinearMap.mkPiRing (R : Type uR) (ι : Type uι) {M₂ : Type v₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [Fintype ι] (z : M₂) :
                                          MultilinearMap R (fun x => R) M₂

                                          The canonical multilinear map on R^ι when ι is finite, associating to m the product of all the m i (multiplied by a fixed reference element z in the target module). See also mkPiAlgebra for a more general version.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem MultilinearMap.mkPiRing_apply {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [Fintype ι] (z : M₂) (m : ιR) :
                                            ↑(MultilinearMap.mkPiRing R ι z) m = (Finset.prod Finset.univ fun i => m i) z
                                            theorem MultilinearMap.mkPiRing_apply_one_eq_self {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [Fintype ι] (f : MultilinearMap R (fun x => R) M₂) :
                                            MultilinearMap.mkPiRing R ι (f fun x => 1) = f
                                            theorem MultilinearMap.mkPiRing_eq_iff {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [Fintype ι] {z₁ : M₂} {z₂ : M₂} :
                                            MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ z₁ = z₂
                                            theorem MultilinearMap.mkPiRing_zero {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [Fintype ι] :
                                            theorem MultilinearMap.mkPiRing_eq_zero_iff {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [Fintype ι] (z : M₂) :
                                            instance MultilinearMap.instNegMultilinearMapToAddCommMonoid {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
                                            Neg (MultilinearMap R M₁ M₂)
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            @[simp]
                                            theorem MultilinearMap.neg_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) :
                                            ↑(-f) m = -f m
                                            instance MultilinearMap.instSubMultilinearMapToAddCommMonoid {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
                                            Sub (MultilinearMap R M₁ M₂)
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            @[simp]
                                            theorem MultilinearMap.sub_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) :
                                            ↑(f - g) m = f m - g m
                                            instance MultilinearMap.instAddCommGroupMultilinearMapToAddCommMonoid {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
                                            Equations
                                            • MultilinearMap.instAddCommGroupMultilinearMapToAddCommMonoid = let src := MultilinearMap.addCommMonoid; AddCommGroup.mk (_ : ∀ (a b : MultilinearMap R M₁ M₂), a + b = b + a)
                                            @[simp]
                                            theorem MultilinearMap.map_neg {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) :
                                            f (Function.update m i (-x)) = -f (Function.update m i x)
                                            @[simp]
                                            theorem MultilinearMap.map_sub {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Semiring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) (y : M₁ i) :
                                            f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
                                            def MultilinearMap.piRingEquiv {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [Fintype ι] :
                                            M₂ ≃ₗ[R] MultilinearMap R (fun x => R) M₂

                                            When ι is finite, multilinear maps on R^ι with values in M₂ are in bijection with M₂, as such a multilinear map is completely determined by its value on the constant vector made of ones. We register this bijection as a linear equivalence in MultilinearMap.piRingEquiv.

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

                                              Currying #

                                              We associate to a multilinear map in n+1 variables (i.e., based on Fin n.succ) two curried functions, named f.curryLeft (which is a linear map on E 0 taking values in multilinear maps in n variables) and f.curryRight (which is a multilinear map in n variables taking values in linear maps on E 0). In both constructions, the variable that is singled out is 0, to take advantage of the operations cons and tail on Fin n. The inverse operations are called uncurryLeft and uncurryRight.

                                              We also register linear equiv versions of these correspondences, in multilinearCurryLeftEquiv and multilinearCurryRightEquiv.

                                              Left currying #

                                              def LinearMap.uncurryLeft {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun i => M (Fin.succ i)) M₂) :

                                              Given a linear map f from M 0 to multilinear maps on n variables, construct the corresponding multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (m 0) (tail m)

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem LinearMap.uncurryLeft_apply {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun i => M (Fin.succ i)) M₂) (m : (i : Fin (Nat.succ n)) → M i) :
                                                ↑(LinearMap.uncurryLeft f) m = ↑(f (m 0)) (Fin.tail m)
                                                def MultilinearMap.curryLeft {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) :
                                                M 0 →ₗ[R] MultilinearMap R (fun i => M (Fin.succ i)) M₂

                                                Given a multilinear map f in n+1 variables, split the first variable to obtain a linear map into multilinear maps in n variables, given by x ↦ (m ↦ f (cons x m)).

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem MultilinearMap.curryLeft_apply {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (x : M 0) (m : (i : Fin n) → M (Fin.succ i)) :
                                                  ↑(↑(MultilinearMap.curryLeft f) x) m = f (Fin.cons x m)
                                                  @[simp]
                                                  theorem LinearMap.curry_uncurryLeft {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun i => M (Fin.succ i)) M₂) :
                                                  @[simp]
                                                  theorem MultilinearMap.uncurry_curryLeft {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) :
                                                  def multilinearCurryLeftEquiv (R : Type uR) {n : } (M : Fin (Nat.succ n)Type v) (M₂ : Type v₂) [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] :
                                                  (M 0 →ₗ[R] MultilinearMap R (fun i => M (Fin.succ i)) M₂) ≃ₗ[R] MultilinearMap R M M₂

                                                  The space of multilinear maps on ∀ (i : Fin (n+1)), M i is canonically isomorphic to the space of linear maps from M 0 to the space of multilinear maps on ∀ (i : Fin n), M i.succ , by separating the first variable. We register this isomorphism as a linear isomorphism in multilinearCurryLeftEquiv R M M₂.

                                                  The direct and inverse maps are given by f.uncurryLeft and f.curryLeft. Use these unless you need the full framework of linear equivs.

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

                                                    Right currying #

                                                    def MultilinearMap.uncurryRight {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun i => M (Fin.castSucc i)) (M (Fin.last n) →ₗ[R] M₂)) :

                                                    Given a multilinear map f in n variables to the space of linear maps from M (last n) to M₂, construct the corresponding multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (init m) (m (last n))

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem MultilinearMap.uncurryRight_apply {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun i => M (Fin.castSucc i)) (M (Fin.last n) →ₗ[R] M₂)) (m : (i : Fin (Nat.succ n)) → M i) :
                                                      ↑(MultilinearMap.uncurryRight f) m = ↑(f (Fin.init m)) (m (Fin.last n))
                                                      def MultilinearMap.curryRight {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) :
                                                      MultilinearMap R (fun i => M (Fin.castSucc i)) (M (Fin.last n) →ₗ[R] M₂)

                                                      Given a multilinear map f in n+1 variables, split the last variable to obtain a multilinear map in n variables taking values in linear maps from M (last n) to M₂, given by m ↦ (x ↦ f (snoc m x)).

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem MultilinearMap.curryRight_apply {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M (Fin.castSucc i)) (x : M (Fin.last n)) :
                                                        ↑(↑(MultilinearMap.curryRight f) m) x = f (Fin.snoc m x)
                                                        @[simp]
                                                        theorem MultilinearMap.curry_uncurryRight {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun i => M (Fin.castSucc i)) (M (Fin.last n) →ₗ[R] M₂)) :
                                                        @[simp]
                                                        theorem MultilinearMap.uncurry_curryRight {R : Type uR} {n : } {M : Fin (Nat.succ n)Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) :
                                                        def multilinearCurryRightEquiv (R : Type uR) {n : } (M : Fin (Nat.succ n)Type v) (M₂ : Type v₂) [CommSemiring R] [(i : Fin (Nat.succ n)) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin (Nat.succ n)) → Module R (M i)] [Module R M₂] :
                                                        MultilinearMap R (fun i => M (Fin.castSucc i)) (M (Fin.last n) →ₗ[R] M₂) ≃ₗ[R] MultilinearMap R M M₂

                                                        The space of multilinear maps on ∀ (i : Fin (n+1)), M i is canonically isomorphic to the space of linear maps from the space of multilinear maps on ∀ (i : Fin n), M (castSucc i) to the space of linear maps on M (last n), by separating the last variable. We register this isomorphism as a linear isomorphism in multilinearCurryRightEquiv R M M₂.

                                                        The direct and inverse maps are given by f.uncurryRight and f.curryRight. Use these unless you need the full framework of linear equivs.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          def MultilinearMap.currySum {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun x => M') M₂) :
                                                          MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)

                                                          A multilinear map on ∀ i : ι ⊕ ι', M' defines a multilinear map on ∀ i : ι, M' taking values in the space of multilinear maps on ∀ i : ι', M'.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem MultilinearMap.currySum_apply {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun x => M') M₂) (u : ιM') (v : ι'M') :
                                                            ↑(↑(MultilinearMap.currySum f) u) v = f (Sum.elim u v)
                                                            def MultilinearMap.uncurrySum {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)) :
                                                            MultilinearMap R (fun x => M') M₂

                                                            A multilinear map on ∀ i : ι, M' taking values in the space of multilinear maps on ∀ i : ι', M' defines a multilinear map on ∀ i : ι ⊕ ι', M'.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[simp]
                                                              theorem MultilinearMap.uncurrySum_aux_apply {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)) (u : ι ι'M') :
                                                              ↑(MultilinearMap.uncurrySum f) u = ↑(f (u Sum.inl)) (u Sum.inr)
                                                              def MultilinearMap.currySumEquiv (R : Type uR) (ι : Type uι) (M₂ : Type v₂) (M' : Type v') [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] (ι' : Type u_1) :
                                                              MultilinearMap R (fun x => M') M₂ ≃ₗ[R] MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)

                                                              Linear equivalence between the space of multilinear maps on ∀ i : ι ⊕ ι', M' and the space of multilinear maps on ∀ i : ι, M' taking values in the space of multilinear maps on ∀ i : ι', M'.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                theorem MultilinearMap.coe_currySumEquiv {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} :
                                                                ↑(MultilinearMap.currySumEquiv R ι M₂ M' ι') = MultilinearMap.currySum
                                                                @[simp]
                                                                theorem MultilinearMap.coe_currySumEquiv_symm {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} :
                                                                ↑(LinearEquiv.symm (MultilinearMap.currySumEquiv R ι M₂ M' ι')) = MultilinearMap.uncurrySum
                                                                def MultilinearMap.curryFinFinset (R : Type uR) (M₂ : Type v₂) (M' : Type v') [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : Finset.card s = k) (hl : Finset.card s = l) :
                                                                MultilinearMap R (fun x => M') M₂ ≃ₗ[R] MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)

                                                                If s : Finset (Fin n) is a finite set of cardinality k and its complement has cardinality l, then the space of multilinear maps on fun i : Fin n => M' is isomorphic to the space of multilinear maps on fun i : Fin k => M' taking values in the space of multilinear maps on fun i : Fin l => M'.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[simp]
                                                                  theorem MultilinearMap.curryFinFinset_apply {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : Finset.card s = k) (hl : Finset.card s = l) (f : MultilinearMap R (fun x => M') M₂) (mk : Fin kM') (ml : Fin lM') :
                                                                  ↑(↑(↑(MultilinearMap.curryFinFinset R M₂ M' hk hl) f) mk) ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
                                                                  @[simp]
                                                                  theorem MultilinearMap.curryFinFinset_symm_apply {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : Finset.card s = k) (hl : Finset.card s = l) (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)) (m : Fin nM') :
                                                                  ↑(↑(LinearEquiv.symm (MultilinearMap.curryFinFinset R M₂ M' hk hl)) f) m = ↑(f fun i => m (↑(finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => m (↑(finSumEquivOfFinset hk hl) (Sum.inr i))
                                                                  theorem MultilinearMap.curryFinFinset_symm_apply_piecewise_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : Finset.card s = k) (hl : Finset.card s = l) (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)) (x : M') (y : M') :
                                                                  ↑(↑(LinearEquiv.symm (MultilinearMap.curryFinFinset R M₂ M' hk hl)) f) (Finset.piecewise s (fun x => x) fun x => y) = ↑(f fun x => x) fun x => y
                                                                  @[simp]
                                                                  theorem MultilinearMap.curryFinFinset_symm_apply_piecewise_const_aux {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : Finset.card s = k) (hl : Finset.card s = l) (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)) (x : M') (y : M') :
                                                                  (↑(f fun x => x) fun i => Finset.piecewise s (fun x => x) (fun x => y) (↑(finSumEquivOfFinset hk hl) (Sum.inr i))) = ↑(f fun x => x) fun x => y
                                                                  @[simp]
                                                                  theorem MultilinearMap.curryFinFinset_symm_apply_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : Finset.card s = k) (hl : Finset.card s = l) (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)) (x : M') :
                                                                  (↑(↑(LinearEquiv.symm (MultilinearMap.curryFinFinset R M₂ M' hk hl)) f) fun x => x) = ↑(f fun x => x) fun x => x
                                                                  theorem MultilinearMap.curryFinFinset_apply_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : Finset.card s = k) (hl : Finset.card s = l) (f : MultilinearMap R (fun x => M') M₂) (x : M') (y : M') :
                                                                  (↑(↑(↑(MultilinearMap.curryFinFinset R M₂ M' hk hl) f) fun x => x) fun x => y) = f (Finset.piecewise s (fun x => x) fun x => y)
                                                                  @[simp]
                                                                  theorem MultilinearMap.curryFinFinset_apply_const_aux {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : Finset.card s = k) (hl : Finset.card s = l) (f : MultilinearMap R (fun x => M') M₂) (x : M') (y : M') :
                                                                  (f fun i => Sum.elim (fun x => x) (fun x => y) ((finSumEquivOfFinset hk hl).symm i)) = f (Finset.piecewise s (fun x => x) fun x => y)
                                                                  def MultilinearMap.map {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Ring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : (i : ι) → Submodule R (M₁ i)) :

                                                                  The pushforward of an indexed collection of submodule p i ⊆ M₁ i by f : M₁ → M₂.

                                                                  Note that this is not a submodule - it is not closed under addition.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    theorem MultilinearMap.map_nonempty {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Ring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : (i : ι) → Submodule R (M₁ i)) :

                                                                    The map is always nonempty. This lemma is needed to apply SubMulAction.zero_mem.

                                                                    def MultilinearMap.range {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Ring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Nonempty ι] (f : MultilinearMap R M₁ M₂) :

                                                                    The range of a multilinear map, closed under scalar multiplication.

                                                                    Equations
                                                                    Instances For