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 #
MultilinearMap R M₁ M₂
is the space of multilinear maps from∀ (i : ι), M₁ i
toM₂
.f.map_smul
is the multiplicativity of the multilinear mapf
along each coordinate.f.map_add
is the additivity of the multilinear mapf
along each coordinate.f.map_smul_univ
expresses the multiplicativity off
over all coordinates at the same time, writingf (fun i => c i • m i)
as(∏ i, c i) • f m
.f.map_add_univ
expresses the additivity off
over all coordinates at the same time, writingf (m + m')
as the sum over all subsetss
ofι
off (s.piecewise m m')
.f.map_sum
expressesf (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)
as the sum off (g₁ (r 1), ..., gₙ (r n))
wherer
ranges over all possible functions.
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:
- fixing a vector
m : ∀ (j : ι - i), M₁ j.val
, and then choosing separately thei
-th coordinate - fixing a vector
m : ∀j, M₁ j
, and then modifying itsi
-th coordinate
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:
- Requiring
DecidableEq ι
as an argument toMultilinearMap
(as we did originally). - Using
Classical.decEq ι
in the statement ofmap_add'
andmap_smul'
. - Quantifying over all possible
DecidableEq ι
instances in the statement ofmap_add'
andmap_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.
Multilinear maps over the ring R
, from ∀ i, M₁ i
to M₂
where M₁ i
and M₂
are modules
over R
.
- toFun : ((i : ι) → M₁ i) → M₂
The underlying multivariate function of a multilinear map.
- map_add' : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), self.toFun (Function.update m i (x + y)) = self.toFun (Function.update m i x) + self.toFun (Function.update m i y)
A multilinear map is additive in every argument.
- map_smul' : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), self.toFun (Function.update m i (c • x)) = c • self.toFun (Function.update m i x)
A multilinear map is compatible with scalar multiplication in every argument.
Instances For
A multilinear map is additive in every argument.
A multilinear map is compatible with scalar multiplication in every argument.
Equations
- MultilinearMap.instFunLikeForall = { coe := fun (f : MultilinearMap R M₁ M₂) => f.toFun, coe_injective' := ⋯ }
Equations
- MultilinearMap.instAdd = { add := fun (f f' : MultilinearMap R M₁ M₂) => { toFun := fun (x : (i : ι) → M₁ i) => f x + f' x, map_add' := ⋯, map_smul' := ⋯ } }
Equations
- MultilinearMap.instZero = { zero := { toFun := fun (x : (i : ι) → M₁ i) => 0, map_add' := ⋯, map_smul' := ⋯ } }
Equations
- MultilinearMap.instInhabited = { default := 0 }
Equations
- MultilinearMap.instSMul = { smul := fun (c : R') (f : MultilinearMap A M₁ M₂) => { toFun := fun (m : (i : ι) → M₁ i) => c • f m, map_add' := ⋯, map_smul' := ⋯ } }
Equations
- MultilinearMap.addCommMonoid = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
Coercion of a multilinear map to a function as an additive monoid homomorphism.
Equations
- MultilinearMap.coeAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
Instances For
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
- f.toLinearMap m i = { toFun := fun (x : M₁ i) => f (Function.update m i x), map_add' := ⋯, map_smul' := ⋯ }
Instances For
The cartesian product of two multilinear maps, as a multilinear map.
Equations
- f.prod g = { toFun := fun (m : (i : ι) → M₁ i) => (f m, g m), map_add' := ⋯, map_smul' := ⋯ }
Instances For
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
- MultilinearMap.pi f = { toFun := fun (m : (i : ι) → M₁ i) (i : ι') => (f i) m, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Equivalence between linear maps M₂ →ₗ[R] M₃
and one-multilinear maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constant map is multilinear when ι
is empty.
Equations
- MultilinearMap.constOfIsEmpty R M₁ m = { toFun := Function.const ((i : ι) → M₁ i) m, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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
Instances For
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.
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.
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.
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.
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
- g.compLinearMap f = { toFun := fun (m : (i : ι) → M₁ i) => g fun (i : ι) => (f i) (m i), map_add' := ⋯, map_smul' := ⋯ }
Instances For
Composing a multilinear map twice with a linear map in each argument is the same as composing with their composition.
Composing the zero multilinear map with a linear map in each argument.
Composing a multilinear map with the identity linear map in each argument.
Composing with a family of surjective linear maps is injective.
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.
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.
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
.
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
.
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.
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.
Restrict the codomain of a multilinear map to a submodule.
This is the multilinear version of LinearMap.codRestrict
.
Equations
- f.codRestrict p h = { toFun := fun (v : (i : ι) → M₁ i) => ⟨f v, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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
- MultilinearMap.restrictScalars R f = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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
- MultilinearMap.domDomCongr σ m = { toFun := fun (v : ι₂ → M₂) => m fun (i : ι₁) => v (σ i), map_add' := ⋯, map_smul' := ⋯ }
Instances For
MultilinearMap.domDomCongr
as an equivalence.
This is declared separately because it does not work with dot notation.
Equations
- MultilinearMap.domDomCongrEquiv σ = { toFun := MultilinearMap.domDomCongr σ, invFun := MultilinearMap.domDomCongr σ.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
The results of applying domDomCongr
to two maps are equal if
and only if those maps are.
If {a // P a}
is a subtype of ι
and if we fix an element z
of (i : {a // ¬ P a}) → M₁ i
,
then a multilinear map on M₁
defines a multilinear map on the restriction of M₁
to
{a // P a}
, by fixing the arguments out of {a // P a}
equal to the values of z
.
Given a multilinear map f
on (i : ι) → M i
, a (decidable) predicate P
on ι
and
an element z
of (i : {a // ¬ P a}) → M₁ i
, construct a multilinear map on
(i : {a // P a}) → M₁ i)
whose value at x
is f
evaluated at the vector with i
th coordinate
x i
if P i
and z i
otherwise.
The naming is similar to MultilinearMap.domDomCongr
: here we are applying the restriction to the
domain of the domain.
For a linear map version, see MultilinearMap.domDomRestrictₗ
.
Equations
- f.domDomRestrict P z = { toFun := fun (x : (i : { a : ι // P a }) → M₁ ↑i) => f fun (j : ι) => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The "derivative" of a multilinear map, as a linear map from (i : ι) → M₁ i
to M₂
.
For continuous multilinear maps, this will indeed be the derivative.
Equations
- f.linearDeriv x = ∑ i : ι, f.toLinearMap x i ∘ₗ LinearMap.proj i
Instances For
Composing a multilinear map with a linear map gives again a multilinear map.
Instances For
The multilinear version of LinearMap.subtype_comp_codRestrict
The multilinear version of LinearMap.comp_codRestrict
Equations
- MultilinearMap.instDistribMulActionOfSMulCommClass = Function.Injective.distribMulAction MultilinearMap.coeAddMonoidHom ⋯ ⋯
The space of multilinear maps over an algebra over R
is a module over R
, for the pointwise
addition and scalar multiplication.
Equations
- MultilinearMap.instModule = Function.Injective.module S MultilinearMap.coeAddMonoidHom ⋯ ⋯
Equations
- ⋯ = ⋯
Linear equivalence between linear maps M₂ →ₗ[R] M₃
and one-multilinear maps MultilinearMap R (fun _ : ι ↦ M₂) M₃
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dependent version of MultilinearMap.domDomCongrLinearEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
MultilinearMap.domDomCongr
as a LinearEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a predicate P
, one may associate to a multilinear map f
a multilinear map
from the elements satisfying P
to the multilinear maps on elements not satisfying P
.
In other words, splitting the variables into two subsets one gets a multilinear map into
multilinear maps.
This is a linear map version of the function MultilinearMap.domDomRestrict
.
Equations
Instances For
One of the components of the iterated derivative of a multilinear map. Given a bijection e
between a type α
(typically Fin k
) and a subset s
of ι
, this component is a multilinear map
of k
vectors v₁, ..., vₖ
, mapping them to f (x₁, (v_{e.symm 2})₂, x₃, ...)
, where at
indices i
in s
one uses the i
-th coordinate of the vector v_{e.symm i}
and otherwise one
uses the i
-th coordinate of a reference vector x
.
This is multilinear in the components of x
outside of s
, and in the v_j
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The k
-th iterated derivative of a multilinear map f
at the point x
. It is a multilinear
map of k
vectors v₁, ..., vₖ
(with the same type as x
), mapping them
to ∑ f (x₁, (v_{i₁})₂, x₃, ...)
, where at each index j
one uses either xⱼ
or one
of the (vᵢ)ⱼ
, and each vᵢ
has to be used exactly once.
The sum is parameterized by the embeddings of Fin k
in the index type ι
(or, equivalently,
by the subsets s
of ι
of cardinality k
and then the bijections between Fin k
and s
).
For the continuous version, see ContinuousMultilinearMap.iteratedFDeriv
.
Equations
Instances For
If f
is a collection of linear maps, then the construction MultilinearMap.compLinearMap
sending a multilinear map g
to g (f₁ ⬝ , ..., fₙ ⬝ )
is linear in g
.
Equations
- MultilinearMap.compLinearMapₗ f = { toFun := fun (g : MultilinearMap R M₁' M₂) => g.compLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
If f
is a collection of linear maps, then the construction MultilinearMap.compLinearMap
sending a multilinear map g
to g (f₁ ⬝ , ..., fₙ ⬝ )
is linear in g
and multilinear in
f₁, ..., fₙ
.
Equations
- MultilinearMap.compLinearMapMultilinear = { toFun := MultilinearMap.compLinearMapₗ, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Let M₁ᵢ
and M₁ᵢ'
be two families of R
-modules and M₂
an R
-module.
Let us denote Π i, M₁ᵢ
and Π i, M₁ᵢ'
by M
and M'
respectively.
If g
is a multilinear map M' → M₂
, then g
can be reinterpreted as a multilinear
map from Π i, M₁ᵢ ⟶ M₁ᵢ'
to M ⟶ M₂
via (fᵢ) ↦ v ↦ g(fᵢ vᵢ)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If one multiplies by c i
the coordinates in a finset s
, then the image under a multilinear
map is multiplied by ∏ i ∈ 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.
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
.
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
- MultilinearMap.mkPiAlgebra R ι A = { toFun := fun (m : ι → A) => ∏ i : ι, m i, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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
- MultilinearMap.mkPiAlgebraFin R n A = { toFun := fun (m : Fin n → A) => (List.ofFn m).prod, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Given an R
-multilinear map f
taking values in R
, f.smulRight z
is the map
sending m
to f m • z
.
Equations
- f.smulRight z = (LinearMap.id.smulRight z).compMultilinearMap f
Instances For
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
- MultilinearMap.mkPiRing R ι z = (MultilinearMap.mkPiAlgebra R ι R).smulRight z
Instances For
Equations
- MultilinearMap.instNeg = { neg := fun (f : MultilinearMap R M₁ M₂) => { toFun := fun (m : (i : ι) → M₁ i) => -f m, map_add' := ⋯, map_smul' := ⋯ } }
Equations
- MultilinearMap.instSub = { sub := fun (f g : MultilinearMap R M₁ M₂) => { toFun := fun (m : (i : ι) → M₁ i) => f m - g m, map_add' := ⋯, map_smul' := ⋯ } }
Equations
- MultilinearMap.instAddCommGroup = AddCommGroup.mk ⋯
This calculates the differences between the values of a multilinear map at
two arguments that differ on a finset s
of ι
. It requires a
linear order on ι
in order to express the result.
This expresses the difference between the values of a multilinear map
at two points "close to x
" in terms of the "derivative" of the multilinear map at x
and of "second-order" terms.
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 #
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
Instances For
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
Instances For
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.curryLeft
and f.uncurryLeft
. Use these
unless you need the full framework of linear equivs.
Equations
- multilinearCurryLeftEquiv R M M₂ = { toFun := MultilinearMap.curryLeft, map_add' := ⋯, map_smul' := ⋯, invFun := LinearMap.uncurryLeft, left_inv := ⋯, right_inv := ⋯ }
Instances For
Right currying #
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
Instances For
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
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.curryRight
and f.uncurryRight
. Use these
unless you need the full framework of linear equivs.
Equations
- multilinearCurryRightEquiv R M M₂ = { toFun := MultilinearMap.curryRight, map_add' := ⋯, map_smul' := ⋯, invFun := MultilinearMap.uncurryRight, left_inv := ⋯, right_inv := ⋯ }
Instances For
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
Instances For
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
Instances For
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
- MultilinearMap.currySumEquiv R ι M₂ M' ι' = { toFun := MultilinearMap.currySum, map_add' := ⋯, map_smul' := ⋯, invFun := MultilinearMap.uncurrySum, left_inv := ⋯, right_inv := ⋯ }
Instances For
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
- MultilinearMap.curryFinFinset R M₂ M' hk hl = (MultilinearMap.domDomCongrLinearEquiv R R M' M₂ (finSumEquivOfFinset hk hl).symm).trans (MultilinearMap.currySumEquiv R (Fin k) M₂ M' (Fin l))
Instances For
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.
Instances For
The map is always nonempty. This lemma is needed to apply SubMulAction.zero_mem
.
The range of a multilinear map, closed under scalar multiplication.