Pi types of modules #
This file defines constructors for linear maps whose domains or codomains are pi types.
It contains theorems relating these to each other, as well as to
Main definitions #
pi construction for linear functions. From a family of linear functions it produces a linear
function into a family of modules.
The projections from a family of modules are linear maps.
Linear map between the function spaces
I → M₂ and
I → M₃, induced by a linear map
The linear equivalence between linear functions on a finite product of modules and families of functions on these modules. See note [bundled maps over different rings].
This is used as the ext lemma instead of
LinearMap.pi_ext for reasons explained in
note [partially-applied ext lemmas].
J are disjoint index sets, the product of the kernels of the
Jth projections of
φ is linearly equivalent to the product over
A version of
Set.pi for submodules. Given an index set
I and a family of submodules
p : (i : ι) → Submodule R (φ i),
pi I s is the submodule of dependent functions
f : (i : ι) → φ i such that
f i belongs to
p a whenever
i ∈ I.
Combine a family of linear equivalences into a linear equivalence of
Transport dependent functions through an equivalence of the base space.
Transporting dependent functions through an equivalence of the base, expressed as a "simplification".
Linear equivalence between linear functions
Rⁿ → M and
Mⁿ. The spaces
are represented as
ι → R and
ι → M, respectively, where
ι is a finite type.
This as an
S-linear equivalence, under the assumption that
S acts on
M commuting with
R is commutative, we can take this to be the usual action with
S = R.
S = ℕ shows that the equivalence is additive.
See note [bundled maps over different rings].
Bundled versions of
While the same thing could be achieved using
LinearMap.pi ![f₁, f₂, f₃], this is not
definitionally equal to the result using
Fin.cases and function
application do not commute definitionally.
Versions for when
f₁ f₂ f₃ are bilinear maps are also provided.