Pi types of modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.ker (linear_map.pi f) = ⨅ (i : ι), linear_map.ker (f i)
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.ker (linear_map.proj i)) = ⊥
@[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].
Equations
- linear_map.lsum R φ S = {to_fun := λ (f : Π (i : ι), φ i →ₗ[R] M), finset.univ.sum (λ (i : ι), (f i).comp (linear_map.proj i)), map_add' := _, map_smul' := _, inv_fun := λ (f : (Π (i : ι), φ i) →ₗ[R] M) (i : ι), f.comp (linear_map.single i), left_inv := _, right_inv := _}
@[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) :
(↥⨅ (i : ι) (H : i ∈ J), linear_map.ker (linear_map.proj i)) ≃ₗ[R] Π (i : ↥I), φ ↑i
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)) :
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 ι]
[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 := _}
@[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)] :
(Π (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.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) = λ (x : M) (b : ι), x
@[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) :
@[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₃