# mathlibdocumentation

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 #

• pi types in the codomain:
• linear_map.pi
• linear_map.single
• pi types in the domain:
• linear_map.proj
• linear_map.diag
def linear_map.pi {R : Type u} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M₂] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ 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₂] [ M₂] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M₂ →ₗ[R] φ i) (c : M₂) (i : ι) :
c i = (f i) c
theorem linear_map.ker_pi {R : Type u} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M₂] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M₂ →ₗ[R] φ i) :
.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₂] [ M₂] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M₂ →ₗ[R] φ i) :
∀ (i : ι), f i = 0
theorem linear_map.pi_zero {R : Type u} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M₂] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ 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₂] [ M₂] [add_comm_monoid M₃] [ M₃] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) :
.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 : ι), (φ 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 : ι), (φ i)] (i : ι) :
theorem linear_map.proj_apply {R : Type u} {ι : Type x} [semiring R] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (i : ι) (b : Π (i : ι), φ i) :
b = b i
theorem linear_map.proj_pi {R : Type u} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M₂] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M₂ →ₗ[R] φ i) (i : ι) :
.comp = f i
theorem linear_map.infi_ker_proj {R : Type u} {ι : Type x} [semiring R] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] :
(⨅ (i : ι), .ker) =
@[simp]
theorem linear_map.comp_left_apply {R : Type u} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [ M₂] [add_comm_monoid M₃] [ 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₂] [ M₂] [add_comm_monoid M₃] [ 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 : ι), (φ i)] [ M] [decidable_eq ι] (f : Π (i : ι), φ i →ₗ[R] M) (i j : ι) (x : φ i) :
(f j) x j) = ((f i) x) j
def linear_map.single {R : Type u} {ι : Type x} [semiring R] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ 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 : ι), (φ 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 : ι), (φ i)] (S : Type u_1) [ M] [fintype ι] [decidable_eq ι] [semiring S] [ M] [ 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 : ι), (φ i)] (S : Type u_1) [ M] [fintype ι] [decidable_eq ι] [semiring S] [ M] [ M] (f : Π (i : ι), φ i →ₗ[R] M) :
φ S) f = ∑ (i : ι), (f i).comp
@[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 : ι), (φ i)] (S : Type u_1) [ M] [fintype ι] [decidable_eq ι] [semiring S] [ M] [ M] (f : (Π (i : ι), φ i) →ₗ[R] M) (i : ι) :
φ S).symm) f i = f.comp
theorem linear_map.pi_ext {R : Type u} {M : Type v} {ι : Type x} [semiring R] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] [fintype ι] [decidable_eq ι] [ M] {f g : (Π (i : ι), φ i) →ₗ[R] M} (h : ∀ (i : ι) (x : φ i), f x) = g 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 : ι), (φ i)] [fintype ι] [decidable_eq ι] [ M] {f g : (Π (i : ι), φ i) →ₗ[R] M} :
f = g ∀ (i : ι) (x : φ i), f x) = g 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 : ι), (φ i)] [fintype ι] [decidable_eq ι] [ M] {f g : (Π (i : ι), φ i) →ₗ[R] M} (h : ∀ (i : ι), f.comp = g.comp ) :
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 : ι), (φ i)] [fintype ι] [decidable_eq ι] [ M] {f g : (Π (i : ι), φ i) →ₗ[R] M} :
f = g ∀ (i : ι), f.comp = g.comp
def linear_map.infi_ker_proj_equiv (R : Type u) {ι : Type x} [semiring R] (φ : ι → Type i) [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] {I J : set ι} [decidable_pred (λ (i : ι), i I)] (hd : J) (hu : set.univ I J) :
(⨅ (i : ι) (H : i J), .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 : ι), (φ 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₂] [ M₂] {φ : ι → Type i} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] [decidable_eq ι] (f : Π (i : ι), M₂ →ₗ[R] φ i) (c : M₂) (i j : ι) (b : M₂ →ₗ[R] φ i) :
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 : ι), (φ i)] (I : set ι) (p : Π (i : ι), (φ i)) :
(Π (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 : ι), (φ i)] {I : set ι} {p : Π (i : ι), (φ i)} {x : Π (i : ι), φ i} :
x 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 : ι), (φ i)] {I : set ι} {p : Π (i : ι), (φ 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 : ι), (φ i)] {I : set ι} {p : Π (i : ι), (φ i)} :
(⨅ (i : ι) (H : i I), (p i)) = p
theorem submodule.infi_comap_proj {R : Type u} {ι : Type x} [semiring R] {φ : ι → Type u_1} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] {p : Π (i : ι), (φ i)} :
(⨅ (i : ι), (p i)) =
theorem submodule.supr_map_single {R : Type u} {ι : Type x} [semiring R] {φ : ι → Type u_1} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] {p : Π (i : ι), (φ i)} [decidable_eq ι] [fintype ι] :
(⨆ (i : ι), (p i)) =
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 : ι), (φ i)] [Π (i : ι), add_comm_monoid (ψ i)] [Π (i : ι), (ψ 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 : ι), (φ i)] [Π (i : ι), add_comm_monoid (ψ i)] [Π (i : ι), (ψ i)] (e : Π (i : ι), φ i ≃ₗ[R] ψ i) (f : Π (i : ι), φ i) (i : ι) :
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 : ι), (φ i)] :
linear_equiv.Pi_congr_right (λ (j : ι), (φ j)) = (Π (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 : ι), (φ i)] [Π (i : ι), add_comm_monoid (ψ i)] [Π (i : ι), (ψ i)] (e : Π (i : ι), φ i ≃ₗ[R] ψ i) :
= 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 : ι), (φ i)] [Π (i : ι), add_comm_monoid (ψ i)] [Π (i : ι), (ψ i)] [Π (i : ι), add_comm_monoid (χ i)] [Π (i : ι), (χ i)] (e : Π (i : ι), φ i ≃ₗ[R] ψ i) (f : Π (i : ι), ψ i ≃ₗ[R] χ i) :
= 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 : ι), (φ 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 : ι), (φ i)] (e : ι ι') (ᾰ : Π (b : ι'), φ ((e.symm) b)) (a : ι) :
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 : ι), (φ i)] (e : ι ι') (ᾰ : Π (a : ι), φ a) (b : ι') :
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 : ι), (φ 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_option_equiv_prod (R : Type u) [semiring R] {ι : Type u_1} {M : Type u_2} [Π (i : option ι), add_comm_group (M i)] [Π (i : option ι), (M i)] :
(Π (i : option ι), M i) ≃ₗ[R] M none × Π (i : ι), M (some i)

This is equiv.pi_option_equiv_prod 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] [ M] [ M] [ 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] [ M] [ M] [ M] (f : (ι → R) →ₗ[R] M) (i : ι) :
ι S) f i = f 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] [ M] [ M] [ M] (f : ι → M) (g : ι → 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] [ 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] [ M] {α : Type u_1} {β : Type u_2} (f : α β → M) (a : α) :
( 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] [ M] {α : Type u_1} {β : Type u_2} (f : α β → M) (b : β) :
( 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] [ M] {α : Type u_1} {β : Type u_2} (f : α → M) (g : β → M) (a : α) :
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] [ M] {α : Type u_1} {β : Type u_2} (f : α → M) (g : β → M) (b : β) :
M).symm) (f, g) (sum.inr b) = g b
@[simp]
theorem function.extend_by_zero.linear_map_apply (R : Type u) {ι η : Type x} [semiring R] (s : ι → η) (f : ι → R) (ᾰ : η) :
= 0
def function.extend_by_zero.linear_map (R : Type u) {ι η : Type x} [semiring R] (s : ι → η) :
(ι → R) →ₗ[R] η → R

function.extend s f 0 as a bundled linear map.

Equations