Basics on bilinear maps #
This file provides basics on bilinear maps. The most general form considered are maps that are
semilinear in both arguments. They are of type M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
, where M
and N
are modules over R
and S
respectively, P
is a module over both R₂
and S₂
with
commuting actions, and ρ₁₂ : R →+* R₂
and σ₁₂ : S →+* S₂
.
Main declarations #
LinearMap.mk₂
: a constructor for bilinear maps, taking an unbundled function together with proof witnesses of bilinearityLinearMap.flip
: turns a bilinear mapM × N → P
intoN × M → P
LinearMap.lflip
: given a linear map fromM
toN →ₗ[R] P
, i.e., a bilinear mapM → N → P
, change the order of variables and get a linear map fromN
toM →ₗ[R] P
.LinearMap.lcomp
: composition of a given linear mapM → N
with a linear mapN → P
as a linear map fromNₗ →ₗ[R] Pₗ
toM →ₗ[R] Pₗ
LinearMap.llcomp
: composition of linear maps as a bilinear map from(M →ₗ[R] N) × (N →ₗ[R] P)
toM →ₗ[R] P
LinearMap.compl₂
: composition of a linear mapQ → N
and a bilinear mapM → N → P
to form a bilinear mapM → Q → P
.LinearMap.compr₂
: composition of a linear mapP → Q
and a bilinear mapM → N → P
to form a bilinear mapM → N → Q
.LinearMap.lsmul
: scalar multiplication as a bilinear mapR × M → M
Tags #
bilinear
Create a bilinear map from a function that is semilinear in each component.
See mk₂'
and mk₂
for the linear case.
Equations
Instances For
Create a bilinear map from a function that is linear in each component.
See mk₂
for the special case where both arguments come from modules over the same ring.
Equations
Instances For
Given a linear map from M
to linear maps from N
to P
, i.e., a bilinear map from M × N
to
P
, change the order of variables and get a linear map from N
to linear maps from M
to P
.
Equations
Instances For
Restricting a bilinear map in the second entry
Equations
Instances For
Restricting a bilinear map in both components
Equations
Instances For
If B : M → N → Pₗ
is R
-S
bilinear and R'
and S'
are compatible scalar multiplications,
then the restriction of scalars is a R'
-S'
bilinear map.
Equations
Instances For
Given a linear map from M
to linear maps from N
to P
, i.e., a bilinear map M → N → P
,
change the order of variables and get a linear map from N
to linear maps from M
to P
.
Equations
Instances For
Create a bilinear map from a function that is linear in each component.
This is a shorthand for mk₂'
for the common case when R = S
.
Equations
Instances For
Composing a given linear map M → N
with a linear map N → P
as a linear map from
Nₗ →ₗ[R] Pₗ
to M →ₗ[R] Pₗ
.
Equations
Instances For
Composing a semilinear map M → N
and a semilinear map N → P
to form a semilinear map
M → P
is itself a linear map.
Equations
Instances For
Composing linear maps as a bilinear map from (M →ₗ[R] N) × (N →ₗ[R] P)
to M →ₗ[R] P
Equations
Instances For
Composing a linear map Q → N
and a bilinear map M → N → P
to
form a bilinear map M → Q → P
.
Equations
Instances For
Composing linear maps Q → M
and Q' → N
with a bilinear map M → N → P
to
form a bilinear map Q → Q' → P
.
Equations
Instances For
Composing a linear map P → Q
and a bilinear map M → N → P
to
form a bilinear map M → N → Q
.
Equations
Instances For
A version of Function.Injective.comp
for composition of a bilinear map with a linear map.
A version of Function.Surjective.comp
for composition of a bilinear map with a linear map.
A version of Function.Surjective.comp
for composition of a bilinear map with a linear map.
A version of Function.Bijective.comp
for composition of a bilinear map with a linear map.
Scalar multiplication as a bilinear map R → M → M
.
Equations
Instances For
A shorthand for the type of R
-bilinear Nₗ
-valued maps on M
.
Equations
Instances For
For convenience, a shorthand for the type of bilinear forms from M
to R
.
Equations
Instances For
Restrict the scalars and range of a linear map.
Equations
Instances For
Restrict the scalars, domains, and range of a bilinear map.