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) :
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)] :
@[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)
@[protected]
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 = 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 : ι), 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 : ι) :
@[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 : ι), module 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)] [finite ι] [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)] [finite ι] [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)] [finite ι] [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)] [finite ι] [decidable_eq ι] [add_comm_monoid M] [module R M] {f g : (Π (i : ι), φ i) →ₗ[R] M} :
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.ker (linear_map.proj i)) ≃ₗ[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 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 : ι), module R (φ i)] {I : set ι} {p : Π (i : ι), submodule R (φ i)} :
(submodule.pi 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 : ι), module R (φ i)] (p : Π (i : ι), submodule R (φ i)) :
@[simp]
theorem submodule.pi_top {R : Type u} {ι : Type x} [semiring R] {φ : ι Type u_1} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (s : set ι) :
submodule.pi s (λ (i : ι), ) =
theorem submodule.pi_mono {R : Type u} {ι : Type x} [semiring R] {φ : ι Type u_1} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] {p q : Π (i : ι), submodule R (φ i)} {s : set ι} (h : (i : ι), i s p i q 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 ι] [finite ι] :
theorem submodule.le_comap_single_pi {R : Type u} {ι : Type x} [semiring R] {φ : ι Type u_1} [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] [decidable_eq ι] (p : Π (i : ι), submodule R (φ i)) {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 : ι), 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 = 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] [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 : β) :
def linear_equiv.fun_unique (ι : Type u_1) (R : Type u_2) (M : Type u_3) [unique ι] [semiring R] [add_comm_monoid M] [module 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] [add_comm_monoid M] [module R M] :
((linear_equiv.fun_unique ι R 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), module R (M i)] :
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), module R (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), module R (M i)] :
(linear_equiv.pi_fin_two R M) = λ (f : Π (i : fin 2), M i), (f 0, f 1)
def linear_equiv.fin_two_arrow (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module 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] [add_comm_monoid M] [module R M] :
((linear_equiv.fin_two_arrow 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] [add_comm_monoid M] [module R M] :
(linear_equiv.fin_two_arrow 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) (ᾰ : η) :
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] [add_comm_monoid M₃] [module R M] [module R 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] [add_comm_monoid M₃] [module R M] [module R M₃] (m : M) :
def linear_map.vec_cons {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₂] [module R M] [module R 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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (m : M) :
def linear_map.vec_empty₂ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R 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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R 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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R 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