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 linear_map.ker.
Main definitions #
- pi types in the codomain:
- pi types in the domain:
linear_map.diag
def
linear_map.pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i) :
pi construction for linear functions. From a family of linear functions it produces a linear
function into a family of modules.
theorem
linear_map.ker_pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i) :
linear_map.ker (linear_map.pi f) = ⨅ (i : ι), linear_map.ker (f i)
theorem
linear_map.pi_zero
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
linear_map.pi (λ (i : ι), 0) = 0
theorem
linear_map.pi_comp
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M₃]
[module R M₃]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(g : M₃ →ₗ[R] M₂) :
(linear_map.pi f).comp g = linear_map.pi (λ (i : ι), (f i).comp g)
def
linear_map.proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(i : ι) :
The projections from a family of modules are linear maps.
Note: known here as linear_map.proj, this construction is in other categories called eval, for
example pi.eval_monoid_hom, pi.eval_ring_hom.
Equations
- linear_map.proj i = {to_fun := function.eval i, map_add' := _, map_smul' := _}
@[simp]
theorem
linear_map.coe_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(i : ι) :
⇑(linear_map.proj i) = function.eval i
theorem
linear_map.proj_apply
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(i : ι)
(b : Π (i : ι), φ i) :
⇑(linear_map.proj i) b = b i
theorem
linear_map.proj_pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(i : ι) :
(linear_map.proj i).comp (linear_map.pi f) = f i
theorem
linear_map.infi_ker_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
(⨅ (i : ι), linear_map.ker (linear_map.proj i)) = ⊥
@[protected]
def
linear_map.comp_left
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M₃]
[module R M₃]
(f : M₂ →ₗ[R] M₃)
(I : Type u_1) :
Linear map between the function spaces I → M₂ and I → M₃, induced by a linear map f
between M₂ and M₃.
theorem
linear_map.apply_single
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[add_comm_monoid M]
[module R M]
[decidable_eq ι]
(f : Π (i : ι), φ i →ₗ[R] M)
(i j : ι)
(x : φ i) :
def
linear_map.single
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
The linear_map version of add_monoid_hom.single and pi.single.
@[simp]
theorem
linear_map.coe_single
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
⇑(linear_map.single i) = pi.single i
def
linear_map.lsum
(R : Type u)
{M : Type v}
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[module R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[module S M]
[smul_comm_class R S M] :
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].
@[simp]
theorem
linear_map.lsum_apply
(R : Type u)
{M : Type v}
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[module R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[module S M]
[smul_comm_class R S M]
(f : Π (i : ι), φ i →ₗ[R] M) :
⇑(linear_map.lsum R φ S) f = finset.univ.sum (λ (i : ι), (f i).comp (linear_map.proj i))
@[simp]
theorem
linear_map.lsum_symm_apply
(R : Type u)
{M : Type v}
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[module R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[module S M]
[smul_comm_class R S M]
(f : (Π (i : ι), φ i) →ₗ[R] M)
(i : ι) :
⇑((linear_map.lsum R φ S).symm) f i = f.comp (linear_map.single i)
@[simp]
theorem
linear_map.lsum_single
{ι : Type u_1}
{R : Type u_2}
[fintype ι]
[decidable_eq ι]
[comm_ring R]
{M : ι → Type u_3}
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), module R (M i)] :
theorem
linear_map.pi_ext
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[finite ι]
[decidable_eq ι]
[add_comm_monoid M]
[module R M]
{f g : (Π (i : ι), φ i) →ₗ[R] M}
(h : ∀ (i : ι) (x : φ i), ⇑f (pi.single i x) = ⇑g (pi.single i x)) :
f = g
theorem
linear_map.pi_ext_iff
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[finite ι]
[decidable_eq ι]
[add_comm_monoid M]
[module R M]
{f g : (Π (i : ι), φ i) →ₗ[R] M} :
@[ext]
theorem
linear_map.pi_ext'
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[finite ι]
[decidable_eq ι]
[add_comm_monoid M]
[module R M]
{f g : (Π (i : ι), φ i) →ₗ[R] M}
(h : ∀ (i : ι), f.comp (linear_map.single i) = g.comp (linear_map.single i)) :
f = g
This is used as the ext lemma instead of linear_map.pi_ext for reasons explained in
note [partially-applied ext lemmas].
theorem
linear_map.pi_ext'_iff
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[finite ι]
[decidable_eq ι]
[add_comm_monoid M]
[module R M]
{f g : (Π (i : ι), φ i) →ₗ[R] M} :
f = g ↔ ∀ (i : ι), f.comp (linear_map.single i) = g.comp (linear_map.single i)
def
linear_map.infi_ker_proj_equiv
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{I J : set ι}
[decidable_pred (λ (i : ι), i ∈ I)]
(hd : disjoint I J)
(hu : set.univ ⊆ I ∪ J) :
If I and J are disjoint index sets, the product of the kernels of the Jth 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.ker (linear_map.proj i)).subtype)) (linear_map.cod_restrict (⨅ (i : ι) (H : i ∈ J), linear_map.ker (linear_map.proj i)) (linear_map.pi (λ (i : ι), dite (i ∈ I) (λ (h : i ∈ I), linear_map.proj ⟨i, h⟩) (λ (h : i ∉ I), 0))) _) _ _
def
linear_map.diag
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i j : ι) :
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
theorem
linear_map.update_apply
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(c : M₂)
(i j : ι)
(b : M₂ →ₗ[R] φ i) :
⇑(function.update f i b j) c = function.update (λ (i : ι), ⇑(f i) c) i (⇑b c) j
def
submodule.pi
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(I : set ι)
(p : Π (i : ι), submodule R (φ i)) :
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.
theorem
submodule.binfi_comap_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{I : set ι}
{p : Π (i : ι), submodule R (φ i)} :
(⨅ (i : ι) (H : i ∈ I), submodule.comap (linear_map.proj i) (p i)) = submodule.pi I p
theorem
submodule.infi_comap_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{p : Π (i : ι), submodule R (φ i)} :
(⨅ (i : ι), submodule.comap (linear_map.proj i) (p i)) = submodule.pi set.univ p
theorem
submodule.supr_map_single
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{p : Π (i : ι), submodule R (φ i)}
[decidable_eq ι]
[finite ι] :
(⨆ (i : ι), submodule.map (linear_map.single i) (p i)) = submodule.pi set.univ p
theorem
submodule.le_comap_single_pi
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(p : Π (i : ι), submodule R (φ i))
{i : ι} :
p i ≤ submodule.comap (linear_map.single i) (submodule.pi set.univ p)
def
linear_equiv.Pi_congr_right
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), module R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i) :
Combine a family of linear equivalences into a linear equivalence of pi-types.
This is equiv.Pi_congr_right as a linear_equiv
@[simp]
theorem
linear_equiv.Pi_congr_right_apply
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), module R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i)
(f : Π (i : ι), φ i)
(i : ι) :
⇑(linear_equiv.Pi_congr_right e) f i = ⇑(e i) (f i)
@[simp]
theorem
linear_equiv.Pi_congr_right_refl
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
linear_equiv.Pi_congr_right (λ (j : ι), linear_equiv.refl R (φ j)) = linear_equiv.refl R (Π (i : ι), φ i)
@[simp]
theorem
linear_equiv.Pi_congr_right_symm
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), module R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i) :
(linear_equiv.Pi_congr_right e).symm = linear_equiv.Pi_congr_right (λ (i : ι), (e i).symm)
@[simp]
theorem
linear_equiv.Pi_congr_right_trans
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
{χ : ι → Type u_3}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), module R (ψ i)]
[Π (i : ι), add_comm_monoid (χ i)]
[Π (i : ι), module R (χ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i)
(f : Π (i : ι), ψ i ≃ₗ[R] χ i) :
(linear_equiv.Pi_congr_right e).trans (linear_equiv.Pi_congr_right f) = linear_equiv.Pi_congr_right (λ (i : ι), (e i).trans (f i))
def
linear_equiv.Pi_congr_left'
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[semiring R]
(φ : ι → Type u_1)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(e : ι ≃ ι') :
Transport dependent functions through an equivalence of the base space.
This is equiv.Pi_congr_left' as a linear_equiv.
Equations
- linear_equiv.Pi_congr_left' R φ e = {to_fun := (equiv.Pi_congr_left' φ e).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.Pi_congr_left' φ e).inv_fun, left_inv := _, right_inv := _}
def
linear_equiv.Pi_congr_left
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[semiring R]
(φ : ι → Type u_1)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(e : ι' ≃ ι) :
Transporting dependent functions through an equivalence of the base, expressed as a "simplification".
This is equiv.Pi_congr_left as a linear_equiv
Equations
- linear_equiv.Pi_congr_left R φ e = (linear_equiv.Pi_congr_left' R φ e.symm).symm
def
linear_equiv.pi_option_equiv_prod
(R : Type u)
[semiring R]
{ι : Type u_1}
{M : option ι → Type u_2}
[Π (i : option ι), add_comm_group (M i)]
[Π (i : option ι), module R (M i)] :
(Π (i : option ι), M i) ≃ₗ[R] M option.none × Π (i : ι), M (option.some i)
This is equiv.pi_option_equiv_prod as a linear_equiv
Equations
- linear_equiv.pi_option_equiv_prod R = {to_fun := equiv.pi_option_equiv_prod.to_fun, map_add' := _, map_smul' := _, inv_fun := equiv.pi_option_equiv_prod.inv_fun, left_inv := _, right_inv := _}
def
linear_equiv.pi_ring
(R : Type u)
(M : Type v)
(ι : Type x)
[semiring R]
(S : Type u_4)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R S M] :
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_congr_right (λ (i : ι), linear_map.ring_lmap_equiv_self R S M))
@[simp]
theorem
linear_equiv.pi_ring_apply
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
(S : Type u_4)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R S M]
(f : (ι → R) →ₗ[R] M)
(i : ι) :
⇑(linear_equiv.pi_ring R M ι S) f i = ⇑f (pi.single i 1)
@[simp]
theorem
linear_equiv.pi_ring_symm_apply
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
(S : Type u_4)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R S M]
(f : ι → M)
(g : ι → R) :
⇑(⇑((linear_equiv.pi_ring R M ι S).symm) f) g = finset.univ.sum (λ (i : ι), g i • f i)
def
linear_equiv.sum_arrow_lequiv_prod_arrow
(α : Type u_1)
(β : Type u_2)
(R : Type u_3)
(M : Type u_4)
[semiring R]
[add_comm_monoid M]
[module R M] :
equiv.sum_arrow_equiv_prod_arrow as a linear equivalence.
Equations
- linear_equiv.sum_arrow_lequiv_prod_arrow α β R M = {to_fun := (equiv.sum_arrow_equiv_prod_arrow α β M).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.sum_arrow_equiv_prod_arrow α β M).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.fun_unique_apply
(ι : Type u_1)
(R : Type u_2)
(M : Type u_3)
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M] :
def
linear_equiv.fun_unique
(ι : Type u_1)
(R : Type u_2)
(M : Type u_3)
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M] :
If ι has a unique element, then ι → M is linearly equivalent to M.
Equations
- linear_equiv.fun_unique ι R M = {to_fun := (equiv.fun_unique ι M).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.fun_unique ι M).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.fun_unique_symm_apply
(ι : Type u_1)
(R : Type u_2)
(M : Type u_3)
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M] :
⇑((linear_equiv.fun_unique ι R M).symm) = λ (x : M) (b : ι), x
def
linear_equiv.pi_fin_two
(R : Type u)
[semiring R]
(M : fin 2 → Type v)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)] :
Linear equivalence between dependent functions Π i : fin 2, M i and M 0 × M 1.
Equations
- linear_equiv.pi_fin_two R M = {to_fun := (pi_fin_two_equiv M).to_fun, map_add' := _, map_smul' := _, inv_fun := (pi_fin_two_equiv M).inv_fun, left_inv := _, right_inv := _}
def
linear_equiv.fin_two_arrow
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[module R M] :
Linear equivalence between vectors in M² = fin 2 → M and M × M.
Equations
- linear_equiv.fin_two_arrow R M = {to_fun := (fin_two_arrow_equiv M).to_fun, map_add' := _, map_smul' := _, inv_fun := (fin_two_arrow_equiv M).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.fin_two_arrow_symm_apply
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
linear_equiv.fin_two_arrow_apply
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[module R M] :
⇑(linear_equiv.fin_two_arrow R M) = λ (f : fin 2 → M), (f 0, f 1)
@[simp]
theorem
function.extend_by_zero.linear_map_apply
(R : Type u)
{ι η : Type x}
[semiring R]
(s : ι → η)
(f : ι → R)
(ᾰ : η) :
⇑(function.extend_by_zero.linear_map R s) f ᾰ = function.extend s f 0 ᾰ
noncomputable
def
function.extend_by_zero.linear_map
(R : Type u)
{ι η : Type x}
[semiring R]
(s : ι → η) :
function.extend s f 0 as a bundled linear map.
Equations
- function.extend_by_zero.linear_map R s = {to_fun := λ (f : ι → R), function.extend s f 0, map_add' := _, map_smul' := _}
Bundled versions of matrix.vec_cons and matrix.vec_empty #
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 linear_map.vec_cons, as fin.cases and function
application do not commute definitionally.
Versions for when f₁ f₂ f₃ are bilinear maps are also provided.
def
linear_map.vec_empty
{R : Type u}
{M : Type v}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module R M₃] :
The linear map defeq to matrix.vec_empty
Equations
- linear_map.vec_empty = {to_fun := λ (m : M), matrix.vec_empty, map_add' := _, map_smul' := _}
@[simp]
theorem
linear_map.vec_empty_apply
{R : Type u}
{M : Type v}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module R M₃]
(m : M) :
@[simp]
theorem
linear_map.vec_empty₂_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(m : M) :
def
linear_map.vec_empty₂
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃] :
The empty bilinear map defeq to matrix.vec_empty
Equations
- linear_map.vec_empty₂ = {to_fun := λ (m : M), linear_map.vec_empty, map_add' := _, map_smul' := _}
@[simp]
theorem
linear_map.vec_cons₂_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
{n : ℕ}
(f : M →ₗ[R] M₂ →ₗ[R] M₃)
(g : M →ₗ[R] M₂ →ₗ[R] fin n → M₃)
(m : M) :
def
linear_map.vec_cons₂
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
{n : ℕ}
(f : M →ₗ[R] M₂ →ₗ[R] M₃)
(g : M →ₗ[R] M₂ →ₗ[R] fin n → M₃) :
A bilinear map into fin n.succ → M₃ can be built out of a map into M₃ and a map into
fin n → M₃