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
def
linear_map.pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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₂]
[semimodule R M₂]
[add_comm_monoid M₃]
[semimodule R M₃]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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 : ι), semimodule R (φ i)]
(i : ι) :
The projections from a family of modules are linear maps.
@[simp]
theorem
linear_map.coe_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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 : ι), semimodule 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₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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 : ι), semimodule R (φ i)] :
(⨅ (i : ι), (linear_map.proj i).ker) = ⊥
theorem
linear_map.apply_single
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[add_comm_monoid M]
[semimodule 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 : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[semimodule R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[semimodule 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 : ι), semimodule R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[semimodule R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[semimodule 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 : ι), semimodule R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[semimodule R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[semimodule 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 : ι), semimodule R (φ i)]
[fintype ι]
[decidable_eq ι]
[add_comm_monoid M]
[semimodule 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 : ι), semimodule R (φ i)]
[fintype ι]
[decidable_eq ι]
[add_comm_monoid M]
[semimodule 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 : ι), semimodule R (φ i)]
[fintype ι]
[decidable_eq ι]
[add_comm_monoid M]
[semimodule 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 : ι), semimodule R (φ i)]
[fintype ι]
[decidable_eq ι]
[add_comm_monoid M]
[semimodule 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 : ι), semimodule 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 : ι), semimodule 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₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule 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]
theorem
submodule.coe_pi
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
{I : set ι}
{p : Π (i : ι), submodule R (φ i)} :
↑(submodule.pi I p) = I.pi (λ (i : ι), ↑(p i))
theorem
submodule.binfi_comap_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule R (φ i)]
{p : Π (i : ι), submodule R (φ i)}
[decidable_eq ι]
[fintype ι] :
(⨆ (i : ι), submodule.map (linear_map.single i) (p i)) = submodule.pi set.univ p
@[simp]
theorem
linear_equiv.pi_symm_apply
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), semimodule R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i)
(f : Π (i : ι), ψ i)
(i : ι) :
@[simp]
theorem
linear_equiv.pi_apply
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), semimodule R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i)
(f : Π (i : ι), φ i)
(i : ι) :
⇑(linear_equiv.pi e) f i = ⇑(e i) (f i)
def
linear_equiv.pi
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), semimodule R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i) :
Combine a family of linear equivalences into a linear equivalence of pi-types.
def
linear_equiv.pi_ring
(R : Type u)
(M : Type v)
(ι : Type x)
[semiring R]
(S : Type u_3)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[semimodule R M]
[semimodule 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 (λ (i : ι), linear_map.ring_lmap_equiv_self R M S))
@[simp]
theorem
linear_equiv.pi_ring_apply
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
(S : Type u_3)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[semimodule R M]
[semimodule 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_3)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[semimodule R M]
[semimodule S M]
[smul_comm_class R S M]
(f : ι → M)
(g : ι → R) :