Pi types of semimodules #
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.
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].
J are disjoint index sets, the product of the kernels of the
Jth projections of
φ is linearly equivalent to the product over
- linear_map.infi_ker_proj_equiv R φ hd hu = linear_equiv.of_linear (linear_map.pi (λ (i : ↥I), (linear_map.proj ↑i).comp (⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker).subtype)) (linear_map.cod_restrict (⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker) (linear_map.pi (λ (i : ι), dite (i ∈ I) (λ (h : i ∈ I), linear_map.proj ⟨i, h⟩) (λ (h : i ∉ I), 0))) _) _ _
diag i j is the identity map if
i = j. Otherwise it is the constant 0 map.
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
f i belongs to
p a whenever
i ∈ I.
Combine a family of linear equivalences into a linear equivalence of
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].