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 linear_map.ker
.
Main definitions #
- pi types in the codomain:
- pi types in the domain:
linear_map.diag
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_map
version of add_monoid_hom.single
and pi.single
.
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 linear_map.pi_ext
for reasons explained in
note [partially-applied ext lemmas].
If I
and J
are disjoint index sets, the product of the kernels of the J
th projections of
φ
is linearly equivalent to the product over I
.
Equations
- 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.
Equations
- linear_map.diag i j = function.update 0 i linear_map.id j
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 pi
-types.
Linear equivalence between linear functions Rⁿ → M
and Mⁿ
. The spaces Rⁿ
and Mⁿ
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
.
When R
is commutative, we can take this to be the usual action with S = R
.
Otherwise, S = ℕ
shows that the equivalence is additive.
See note [bundled maps over different rings].
Equations
- linear_equiv.pi_ring R M ι S = (linear_map.lsum R (λ (i : ι), R) S).symm.trans (linear_equiv.pi (λ (i : ι), linear_map.ring_lmap_equiv_self R M S))