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.
@[simp]
theorem
linear_map.pi_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)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(c : M₂)
(i : ι) :
⇑(linear_map.pi f) c i = ⇑(f i) c
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.pi f).ker = ⨅ (i : ι), (f i).ker
theorem
linear_map.pi_eq_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)]
(f : Π (i : ι), M₂ →ₗ[R] φ i) :
linear_map.pi f = 0 ↔ ∀ (i : ι), f i = 0
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.proj i).ker) = ⊥
@[simp]
theorem
linear_map.comp_left_apply
{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)
(h : I → M₂)
(ᾰ : 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 = ∑ (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)
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)]
[fintype ι]
[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)]
[fintype ι]
[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)]
[fintype ι]
[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)]
[fintype ι]
[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.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))) _) _ _
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)) :
submodule R (Π (i : ι), φ 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.
@[simp]
theorem
submodule.mem_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)}
{x : Π (i : ι), φ i} :
x ∈ submodule.pi I p ↔ ∀ (i : ι), i ∈ I → x i ∈ p i
@[simp, norm_cast]
theorem
submodule.coe_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)} :
↑(submodule.pi I p) = I.pi (λ (i : ι), ↑(p i))
@[simp]
theorem
submodule.pi_empty
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(p : Π (i : ι), submodule R (φ i)) :
submodule.pi ∅ p = ⊤
@[simp]
theorem
submodule.pi_top
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(s : set ι) :
submodule.pi s (λ (i : ι), ⊤) = ⊤
theorem
submodule.pi_mono
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{p q : Π (i : ι), submodule R (φ i)}
{s : set ι}
(h : ∀ (i : ι), i ∈ s → p i ≤ q i) :
submodule.pi s p ≤ submodule.pi s q
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 ι]
[fintype ι] :
(⨆ (i : ι), submodule.map (linear_map.single i) (p 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 := _}
@[simp]
theorem
linear_equiv.Pi_congr_left'_symm_apply
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[semiring R]
(φ : ι → Type u_1)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(e : ι ≃ ι')
(ᾰ : Π (b : ι'), φ (⇑(e.symm) b))
(a : ι) :
@[simp]
theorem
linear_equiv.Pi_congr_left'_apply
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[semiring R]
(φ : ι → Type u_1)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(e : ι ≃ ι')
(ᾰ : Π (a : ι), φ a)
(b : ι') :
⇑(linear_equiv.Pi_congr_left' R φ e) ᾰ b = ᾰ (⇑(e.symm) b)
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)] :
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) :
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.sum_arrow_lequiv_prod_arrow_apply_fst
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{α : Type u_1}
{β : Type u_2}
(f : α ⊕ β → M)
(a : α) :
(⇑(linear_equiv.sum_arrow_lequiv_prod_arrow α β R M) f).fst a = f (sum.inl a)
@[simp]
theorem
linear_equiv.sum_arrow_lequiv_prod_arrow_apply_snd
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{α : Type u_1}
{β : Type u_2}
(f : α ⊕ β → M)
(b : β) :
(⇑(linear_equiv.sum_arrow_lequiv_prod_arrow α β R M) f).snd b = f (sum.inr b)
@[simp]
theorem
linear_equiv.sum_arrow_lequiv_prod_arrow_symm_apply_inl
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{α : Type u_1}
{β : Type u_2}
(f : α → M)
(g : β → M)
(a : α) :
⇑((linear_equiv.sum_arrow_lequiv_prod_arrow α β R M).symm) (f, g) (sum.inl a) = f a
@[simp]
theorem
linear_equiv.sum_arrow_lequiv_prod_arrow_symm_apply_inr
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{α : Type u_1}
{β : Type u_2}
(f : α → M)
(g : β → M)
(b : β) :
⇑((linear_equiv.sum_arrow_lequiv_prod_arrow α β R M).symm) (f, g) (sum.inr b) = g b
@[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) = function.const ι
@[simp]
theorem
linear_equiv.pi_fin_two_symm_apply
(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_equiv.pi_fin_two R M).symm) = λ (p : M 0 × M 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
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 := _}
@[simp]
theorem
linear_equiv.pi_fin_two_apply
(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_equiv.pi_fin_two R M) = λ (f : Π (i : fin 2), M i), (f 0, f 1)
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) :
def
linear_map.vec_cons
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{n : ℕ}
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] fin n → M₂) :
A linear map into fin n.succ → M₃ can be built out of a map into M₃ and a map into
fin n → M₃.
@[simp]
theorem
linear_map.vec_cons_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{n : ℕ}
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] fin n → M₂)
(m : M) :
@[protected, instance]
def
function.has_vadd
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[has_vadd R M] :
has_vadd R (ι → M)
Equations
@[protected, instance]
def
function.has_scalar
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[has_scalar R M] :
has_scalar R (ι → M)
Non-dependent version of pi.has_scalar. Lean gets confused by the dependent instance if this
is not present.
Equations
@[protected, instance]
def
function.smul_comm_class
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{M : Type u_4}
[has_scalar α M]
[has_scalar β M]
[smul_comm_class α β M] :
smul_comm_class α β (ι → M)
Non-dependent version of pi.smul_comm_class. Lean gets confused by the dependent instance if
this is not present.
@[protected, instance]
def
function.vadd_comm_class
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{M : Type u_4}
[has_vadd α M]
[has_vadd β M]
[vadd_comm_class α β M] :
vadd_comm_class α β (ι → 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₃