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].
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
Transport dependent functions through an equivalence of the base space.
equiv.Pi_congr_left' as a
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].
equiv.sum_arrow_equiv_prod_arrow as a linear equivalence.
ι has a unique element, then
ι → M is linearly equivalent to
Linear equivalence between dependent functions
Π i : fin 2, M i and
M 0 × M 1.
Linear equivalence between vectors in
M² = fin 2 → M and
M × M.
function.extend s f 0 as a bundled linear map.
Bundled versions of
The idea of these definitions is to be able to define a map as
x ↦ ![f₁ x, f₂ x, f₃ x], where
f₁ f₂ f₃ are already linear maps, as
f₁.vec_cons $ f₂.vec_cons $ f₃.vec_cons $ vec_empty.
While the same thing could be achieved using
linear_map.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.
The linear map defeq to
Non-dependent version of
pi.smul_comm_class. Lean gets confused by the dependent instance if
this is not present.
The empty bilinear map defeq to