# mathlib3documentation

linear_algebra.pi

# 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:
• 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) :
= (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₂] [ 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 : ι), =
@[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)
@[protected]
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 = 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 : ι), (φ 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
@[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 : ι), (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 : ι), (φ i)] [finite ι] [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)] [finite ι] [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)] [finite ι] [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)] [finite ι] [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), ≃ₗ[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 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 : ι), (φ i)] {I : set ι} {p : Π (i : ι), (φ 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 : ι), (φ i)] (p : Π (i : ι), (φ i)) :
@[simp]
theorem submodule.pi_top {R : Type u} {ι : Type x} [semiring R] {φ : ι Type u_1} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (s : set ι) :
(λ (i : ι), ) =
theorem submodule.pi_mono {R : Type u} {ι : Type x} [semiring R] {φ : ι Type u_1} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] {p q : Π (i : ι), (φ i)} {s : set ι} (h : (i : ι), i s p i q i) :
p q
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 ι] [finite ι] :
( (i : ι), (p i)) =
theorem submodule.le_comap_single_pi {R : Type u} {ι : Type x} [semiring R] {φ : ι Type u_1} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] [decidable_eq ι] (p : Π (i : ι), (φ i)) {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] × Π (i : ι), M (option.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 = 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] [ 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 linear_equiv.fun_unique_apply (ι : Type u_1) (R : Type u_2) (M : Type u_3) [unique ι] [semiring R] [ M] :
def linear_equiv.fun_unique (ι : Type u_1) (R : Type u_2) (M : Type u_3) [unique ι] [semiring R] [ M] :
M) ≃ₗ[R] M

If ι has a unique element, then ι → M is linearly equivalent to M.

Equations
@[simp]
theorem linear_equiv.fun_unique_symm_apply (ι : Type u_1) (R : Type u_2) (M : Type u_3) [unique ι] [semiring R] [ M] :
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), (M i)] :
M).symm) = λ (p : M 0 × M 1),
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), (M i)] :
(Π (i : fin 2), M i) ≃ₗ[R] M 0 × M 1

Linear equivalence between dependent functions Π i : fin 2, M i and M 0 × M 1.

Equations
@[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), (M i)] :
= λ (f : Π (i : fin 2), M i), (f 0, f 1)
def linear_equiv.fin_two_arrow (R : Type u) (M : Type v) [semiring R] [ M] :
(fin 2 M) ≃ₗ[R] M × M

Linear equivalence between vectors in M² = fin 2 → M and M × M.

Equations
@[simp]
theorem linear_equiv.fin_two_arrow_symm_apply (R : Type u) (M : Type v) [semiring R] [ M] :
.symm) = λ (x : M × M), ![x.fst, x.snd]
@[simp]
theorem linear_equiv.fin_two_arrow_apply (R : Type u) (M : Type v) [semiring 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) (ᾰ : η) :
= 0
noncomputable 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

### 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₃] [ M] [ M₃] :
M →ₗ[R] fin 0 M₃

The linear map defeq to matrix.vec_empty

Equations
@[simp]
theorem linear_map.vec_empty_apply {R : Type u} {M : Type v} {M₃ : Type y} [semiring R] [add_comm_monoid M₃] [ M] [ M₃] (m : M) :
def linear_map.vec_cons {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {n : } (f : M →ₗ[R] M₂) (g : M →ₗ[R] fin n M₂) :
M →ₗ[R] fin n.succ 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₃.

Equations
@[simp]
theorem linear_map.vec_cons_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {n : } (f : M →ₗ[R] M₂) (g : M →ₗ[R] fin n M₂) (m : M) :
(f.vec_cons g) m = matrix.vec_cons (f m) (g m)
@[simp]
theorem linear_map.vec_empty₂_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (m : M) :
def linear_map.vec_empty₂ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] :
M →ₗ[R] M₂ →ₗ[R] fin 0 M₃

The empty bilinear map defeq to matrix.vec_empty

Equations
@[simp]
theorem linear_map.vec_cons₂_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] {n : } (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] fin n M₃) (m : M) :
(f.vec_cons₂ g) m = (f m).vec_cons (g m)
def linear_map.vec_cons₂ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] {n : } (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] fin n M₃) :
M →ₗ[R] M₂ →ₗ[R] fin n.succ 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₃

Equations