mathlib documentation

linear_algebra.pi

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 #

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) :
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₂] [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 : ι) :
(Π (i : ι), φ i) →ₗ[R] φ 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
@[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 : ι) :
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) :
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 : ι) :
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) :
(f.comp_left I) h = (f h)
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) :
(I → M₂) →ₗ[R] I → M₃

Linear map between the function spaces I → M₂ and I → M₃, induced by a linear map f between M₂ and M₃.

Equations
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) :
(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 : ι), module 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 : ι), module 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 : ι), 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] :
(Π (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 : ι), 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 : ι) :
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} :
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 : ι), 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) :
(⨅ (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 : ι), module 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₂] [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.

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

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

This is equiv.Pi_congr_right as a linear_equiv

Equations
@[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 : ι) :
@[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) :
@[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) :
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 : ι ι') :
(Π (i' : ι), φ i') ≃ₗ[R] Π (i : ι'), φ ((e.symm) i)

Transport dependent functions through an equivalence of the base space.

This is equiv.Pi_congr_left' as a linear_equiv.

Equations
@[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 : ι) :
((linear_equiv.Pi_congr_left' R φ e).symm) a = cast _ (ᾰ (e 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 : ι' ι) :
(Π (i' : ι'), φ (e i')) ≃ₗ[R] Π (i : ι), φ i

Transporting dependent functions through an equivalence of the base, expressed as a "simplification".

This is equiv.Pi_congr_left as a linear_equiv

Equations
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] :
((ι → 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_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 = ∑ (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] :
β → M) ≃ₗ[R] (α → M) × (β → M)

equiv.sum_arrow_equiv_prod_arrow as a linear equivalence.

Equations
@[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 : α) :
@[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 : β) :
@[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 : α) :
@[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 : β) :