mathlib documentation

linear_algebra.pi

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 #

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) :
M₂ →ₗ[R] Π (i : ι), φ i

pi construction for linear functions. From a family of linear functions it produces a linear function into a family of modules.

Equations
@[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 : ι) :
(Π (i : ι), φ i) →ₗ[R] φ i

The projections from a family of modules are linear maps.

Equations
@[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 : ι) :
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) :
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 : ι) :
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) :
(f j) (pi.single i x j) = pi.single i ((f i) x) j
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 : ι) :
φ i →ₗ[R] Π (i : ι), φ i

The linear_map version of add_monoid_hom.single and pi.single.

Equations
@[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 : ι) :
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] :
(Π (i : ι), φ i →ₗ[R] M) ≃ₗ[S] (Π (i : ι), φ i) →ₗ[R] 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
@[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 : ι) :
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} :
f = g ∀ (i : ι) (x : φ i), f (pi.single i x) = g (pi.single i x)
@[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) :
(⨅ (i : ι) (H : i J), (linear_map.proj i).ker) ≃ₗ[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
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 : ι) :
φ i →ₗ[R] φ j

diag i j is the identity map if i = j. Otherwise it is the constant 0 map.

Equations
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.

Equations
@[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 Ix 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)} :
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 ι] :
@[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 : ι) :
((linear_equiv.pi e).symm) f i = ((e i).symm) (f 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) :
(Π (i : ι), φ i) ≃ₗ[R] Π (i : ι), ψ i

Combine a family of linear equivalences into a linear equivalence of pi-types.

Equations
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] :
((ι → R) →ₗ[R] M) ≃ₗ[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
@[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) :
(((linear_equiv.pi_ring R M ι S).symm) f) g = ∑ (i : ι), g i f i