# 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 LinearMap.ker.

## Main definitions #

• pi types in the codomain:
• LinearMap.pi
• LinearMap.single
• pi types in the domain:
• LinearMap.proj
• LinearMap.diag
def LinearMap.pi {R : Type u} {M₂ : Type w} {ι : Type x} [] [] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ 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
• = let __src := Pi.addHom fun (i : ι) => (f i).toAddHom; { toFun := fun (c : M₂) (i : ι) => (f i) c, map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.pi_apply {R : Type u} {M₂ : Type w} {ι : Type x} [] [] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι) :
(LinearMap.pi f) c i = (f i) c
theorem LinearMap.ker_pi {R : Type u} {M₂ : Type w} {ι : Type x} [] [] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) :
= ⨅ (i : ι), LinearMap.ker (f i)
theorem LinearMap.pi_eq_zero {R : Type u} {M₂ : Type w} {ι : Type x} [] [] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) :
∀ (i : ι), f i = 0
theorem LinearMap.pi_zero {R : Type u} {M₂ : Type w} {ι : Type x} [] [] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
(LinearMap.pi fun (i : ι) => 0) = 0
theorem LinearMap.pi_comp {R : Type u} {M₂ : Type w} {M₃ : Type y} {ι : Type x} [] [] [Module R M₂] [] [Module R M₃] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) :
∘ₗ g = LinearMap.pi fun (i : ι) => f i ∘ₗ g
def LinearMap.proj {R : Type u} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) :
((i : ι) → φ i) →ₗ[R] φ i

The projections from a family of modules are linear maps.

Note: known here as LinearMap.proj, this construction is in other categories called eval, for example Pi.evalMonoidHom, Pi.evalRingHom.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.coe_proj {R : Type u} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) :
=
theorem LinearMap.proj_apply {R : Type u} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i) :
b = b i
theorem LinearMap.proj_pi {R : Type u} {M₂ : Type w} {ι : Type x} [] [] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (i : ι) :
= f i
theorem LinearMap.iInf_ker_proj {R : Type u} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
⨅ (i : ι), =
instance LinearMap.CompatibleSMul.pi (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) [] [] [] [SMul R M] [SMul R N] [Module S M] [Module S N] [] :
LinearMap.CompatibleSMul M (ιN) R S
Equations
• =
@[simp]
theorem LinearMap.compLeft_apply {R : Type u} {M₂ : Type w} {M₃ : Type y} [] [] [Module R M₂] [] [Module R M₃] (f : M₂ →ₗ[R] M₃) (I : Type u_1) (h : IM₂) :
∀ (a : I), (f.compLeft I) h a = (f h) a
def LinearMap.compLeft {R : Type u} {M₂ : Type w} {M₃ : Type y} [] [] [Module R M₂] [] [Module R M₃] (f : M₂ →ₗ[R] M₃) (I : Type u_1) :
(IM₂) →ₗ[R] IM₃

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

Equations
• f.compLeft I = let __src := f.toAddMonoidHom.compLeft I; { toFun := fun (h : IM₂) => f h, map_add' := , map_smul' := }
Instances For
theorem LinearMap.apply_single {R : Type u} {M : Type v} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] [Module R M] [] (f : (i : ι) → φ i →ₗ[R] M) (i : ι) (j : ι) (x : φ i) :
(f j) (Pi.single i x j) = Pi.single i ((f i) x) j
def LinearMap.single {R : Type u} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) :
φ i →ₗ[R] (i : ι) → φ i

The LinearMap version of AddMonoidHom.single and Pi.single.

Equations
• = let __src := ; { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.coe_single {R : Type u} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) :
=
@[simp]
theorem LinearMap.lsum_symm_apply (R : Type u) {M : Type v} {ι : Type x} [] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (S : Type u_1) [] [Module R M] [] [] [] [Module S M] [] (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) :
(LinearMap.lsum R φ S).symm f i = f ∘ₗ
def LinearMap.lsum (R : Type u) {M : Type v} {ι : Type x} [] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (S : Type u_1) [] [Module R M] [] [] [] [Module 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.lsum_apply (R : Type u) {M : Type v} {ι : Type x} [] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (S : Type u_1) [] [Module R M] [] [] [] [Module S M] [] (f : (i : ι) → φ i →ₗ[R] M) :
(LinearMap.lsum R φ S) f = i : ι, f i ∘ₗ
@[simp]
theorem LinearMap.lsum_single {ι : Type u_1} {R : Type u_2} [] [] [] {M : ιType u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] :
(LinearMap.lsum R M R) LinearMap.single = LinearMap.id
theorem LinearMap.pi_ext {R : Type u} {M : Type v} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] [] [] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} (h : ∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)) :
f = g
theorem LinearMap.pi_ext_iff {R : Type u} {M : Type v} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] [] [] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} :
f = g ∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)
theorem LinearMap.pi_ext'_iff {R : Type u} {M : Type v} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] [] [] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} :
f = g ∀ (i : ι), f ∘ₗ = g ∘ₗ
theorem LinearMap.pi_ext' {R : Type u} {M : Type v} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] [] [] [Module R M] {f : ((i : ι) → φ i) →ₗ[R] M} {g : ((i : ι) → φ i) →ₗ[R] M} (h : ∀ (i : ι), f ∘ₗ = g ∘ₗ ) :
f = g

This is used as the ext lemma instead of LinearMap.pi_ext for reasons explained in note [partially-applied ext lemmas].

def LinearMap.iInfKerProjEquiv (R : Type u) {ι : Type x} [] (φ : ιType i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {J : Set ι} [DecidablePred fun (i : ι) => i I] (hd : Disjoint I J) (hu : Set.univ I J) :
(⨅ iJ, ) ≃ₗ[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
• One or more equations did not get rendered due to their size.
Instances For
def LinearMap.diag {R : Type u} {ι : Type x} [] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) (j : ι) :
φ i →ₗ[R] φ j

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

Equations
Instances For
theorem LinearMap.update_apply {R : Type u} {M₂ : Type w} {ι : Type x} [] [] [Module R M₂] {φ : ιType i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι) (j : ι) (b : M₂ →ₗ[R] φ i) :
(Function.update f i b j) c = Function.update (fun (i : ι) => (f i) c) i (b c) j
theorem LinearMap.pi_apply_eq_sum_univ {R : Type u} {M₂ : Type w} {ι : Type x} [] [] [Module R M₂] [] [] (f : (ιR) →ₗ[R] M₂) (x : ιR) :
f x = i : ι, x i f fun (j : ι) => if i = j then 1 else 0

A linear map f applied to x : ι → R can be computed using the image under f of elements of the canonical basis.

def Submodule.pi {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ 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
• = { carrier := I.pi fun (i : ι) => (p i), add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem Submodule.mem_pi {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} {x : (i : ι) → φ i} :
x iI, x i p i
@[simp]
theorem Submodule.coe_pi {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} :
(Submodule.pi I p) = I.pi fun (i : ι) => (p i)
@[simp]
theorem Submodule.pi_empty {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (p : (i : ι) → Submodule R (φ i)) :
@[simp]
theorem Submodule.pi_top {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (s : Set ι) :
(Submodule.pi s fun (i : ι) => ) =
theorem Submodule.pi_mono {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} {q : (i : ι) → Submodule R (φ i)} {s : Set ι} (h : is, p i q i) :
theorem Submodule.biInf_comap_proj {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} :
iI, Submodule.comap (p i) =
theorem Submodule.iInf_comap_proj {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} :
⨅ (i : ι), Submodule.comap (p i) = Submodule.pi Set.univ p
theorem Submodule.iSup_map_single {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} [] [] :
⨆ (i : ι), Submodule.map (p i) = Submodule.pi Set.univ p
theorem Submodule.le_comap_single_pi {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (p : (i : ι) → Submodule R (φ i)) {i : ι} :
def LinearEquiv.piCongrRight {R : Type u} {ι : Type x} [] {φ : ιType u_1} {ψ : ιType u_2} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → AddCommMonoid (ψ 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.piCongrRight as a LinearEquiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.piCongrRight_apply {R : Type u} {ι : Type x} [] {φ : ιType u_1} {ψ : ιType u_2} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f : (i : ι) → φ i) (i : ι) :
f i = (e i) (f i)
@[simp]
theorem LinearEquiv.piCongrRight_refl {R : Type u} {ι : Type x} [] {φ : ιType u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
(LinearEquiv.piCongrRight fun (j : ι) => LinearEquiv.refl R (φ j)) = LinearEquiv.refl R ((i : ι) → φ i)
@[simp]
theorem LinearEquiv.piCongrRight_symm {R : Type u} {ι : Type x} [] {φ : ιType u_1} {ψ : ιType u_2} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i) :
.symm = LinearEquiv.piCongrRight fun (i : ι) => (e i).symm
@[simp]
theorem LinearEquiv.piCongrRight_trans {R : Type u} {ι : Type x} [] {φ : ιType u_1} {ψ : ιType u_2} {χ : ιType u_3} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] [(i : ι) → AddCommMonoid (χ i)] [(i : ι) → Module R (χ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f : (i : ι) → ψ i ≃ₗ[R] χ i) :
= LinearEquiv.piCongrRight fun (i : ι) => e i ≪≫ₗ f i
@[simp]
theorem LinearEquiv.piCongrLeft'_apply (R : Type u) {ι : Type x} {ι' : Type x'} [] (φ : ιType u_1) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (e : ι ι') :
∀ (a : (a : ι) → φ a) (b : ι'), a b = a (e.symm b)
@[simp]
theorem LinearEquiv.piCongrLeft'_symm_apply (R : Type u) {ι : Type x} {ι' : Type x'} [] (φ : ιType u_1) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (e : ι ι') :
∀ (a : (b : ι') → φ (e.symm b)) (a_1 : ι), .symm a a_1 = a (e a_1)
def LinearEquiv.piCongrLeft' (R : Type u) {ι : Type x} {ι' : Type x'} [] (φ : ιType u_1) [(i : ι) → AddCommMonoid (φ 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.piCongrLeft' as a LinearEquiv.

Equations
• = let __src := ; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
def LinearEquiv.piCongrLeft (R : Type u) {ι : Type x} {ι' : Type x'} [] (φ : ιType u_1) [(i : ι) → AddCommMonoid (φ 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.piCongrLeft as a LinearEquiv

Equations
Instances For
def LinearEquiv.piCurry (R : Type u) [] {ι : Type u_4} {κ : ιType u_5} (α : (i : ι) → κ iType u_6) [(i : ι) → (k : κ i) → AddCommMonoid (α i k)] [(i : ι) → (k : κ i) → Module R (α i k)] :
((i : ) → α i.fst i.snd) ≃ₗ[R] (i : ι) → (j : κ i) → α i j

Equiv.piCurry as a LinearEquiv.

Equations
• = let __spread.0 := ; { toFun := __spread.0.toFun, map_add' := , map_smul' := , invFun := __spread.0.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.piCurry_apply (R : Type u) [] {ι : Type u_4} {κ : ιType u_5} (α : (i : ι) → κ iType u_6) [(i : ι) → (k : κ i) → AddCommMonoid (α i k)] [(i : ι) → (k : κ i) → Module R (α i k)] (f : (x : (i : ι) × κ i) → α x.fst x.snd) :
f =
@[simp]
theorem LinearEquiv.piCurry_symm_apply (R : Type u) [] {ι : Type u_4} {κ : ιType u_5} (α : (i : ι) → κ iType u_6) [(i : ι) → (k : κ i) → AddCommMonoid (α i k)] [(i : ι) → (k : κ i) → Module R (α i k)] (f : (a : ι) → (b : κ a) → α a b) :
.symm f =
def LinearEquiv.piOptionEquivProd (R : Type u) [] {ι : Type u_4} {M : Type u_5} [(i : ) → AddCommGroup (M i)] [(i : ) → Module R (M i)] :
((i : ) → M i) ≃ₗ[R] M none × ((i : ι) → M (some i))

This is Equiv.piOptionEquivProd as a LinearEquiv

Equations
• = let __src := Equiv.piOptionEquivProd; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
def LinearEquiv.piRing (R : Type u) (M : Type v) (ι : Type x) [] (S : Type u_4) [] [] [] [] [Module R M] [Module 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
Instances For
@[simp]
theorem LinearEquiv.piRing_apply {R : Type u} {M : Type v} {ι : Type x} [] (S : Type u_4) [] [] [] [] [Module R M] [Module S M] [] (f : (ιR) →ₗ[R] M) (i : ι) :
(LinearEquiv.piRing R M ι S) f i = f (Pi.single i 1)
@[simp]
theorem LinearEquiv.piRing_symm_apply {R : Type u} {M : Type v} {ι : Type x} [] (S : Type u_4) [] [] [] [] [Module R M] [Module S M] [] (f : ιM) (g : ιR) :
((LinearEquiv.piRing R M ι S).symm f) g = i : ι, g i f i
def LinearEquiv.sumArrowLequivProdArrow (α : Type u_5) (β : Type u_6) (R : Type u_7) (M : Type u_8) [] [] [Module R M] :
(α βM) ≃ₗ[R] (αM) × (βM)

Equiv.sumArrowEquivProdArrow as a linear equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.sumArrowLequivProdArrow_apply_fst {R : Type u} {M : Type v} [] [] [Module R M] {α : Type u_5} {β : Type u_6} (f : α βM) (a : α) :
( f).1 a = f (Sum.inl a)
@[simp]
theorem LinearEquiv.sumArrowLequivProdArrow_apply_snd {R : Type u} {M : Type v} [] [] [Module R M] {α : Type u_5} {β : Type u_6} (f : α βM) (b : β) :
( f).2 b = f (Sum.inr b)
@[simp]
theorem LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl {R : Type u} {M : Type v} [] [] [Module R M] {α : Type u_5} {β : Type u_6} (f : αM) (g : βM) (a : α) :
.symm (f, g) (Sum.inl a) = f a
@[simp]
theorem LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr {R : Type u} {M : Type v} [] [] [Module R M] {α : Type u_5} {β : Type u_6} (f : αM) (g : βM) (b : β) :
.symm (f, g) (Sum.inr b) = g b
@[simp]
theorem LinearEquiv.funUnique_symm_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [] [] [] [Module R M] :
.symm = uniqueElim
def LinearEquiv.funUnique (ι : Type u_5) (R : Type u_6) (M : Type u_7) [] [] [] [Module R M] :
(ιM) ≃ₗ[R] M

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

Equations
• = let __src := ; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.funUnique_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [] [] [] [Module R M] :
= Function.eval default
@[simp]
theorem LinearEquiv.piFinTwo_symm_apply (R : Type u) [] (M : Fin 2Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] :
.symm = fun (p : M 0 × M 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
def LinearEquiv.piFinTwo (R : Type u) [] (M : Fin 2Type v) [(i : Fin 2) → AddCommMonoid (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
• = let __src := ; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.piFinTwo_apply (R : Type u) [] (M : Fin 2Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] :
= fun (f : (i : Fin 2) → M i) => (f 0, f 1)
@[simp]
theorem LinearEquiv.finTwoArrow_apply (R : Type u) (M : Type v) [] [] [Module R M] :
= fun (f : Fin 2M) => (f 0, f 1)
@[simp]
theorem LinearEquiv.finTwoArrow_symm_apply (R : Type u) (M : Type v) [] [] [Module R M] :
.symm = fun (x : M × M) => ![x.1, x.2]
def LinearEquiv.finTwoArrow (R : Type u) (M : Type v) [] [] [Module R M] :
(Fin 2M) ≃ₗ[R] M × M

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Function.ExtendByZero.linearMap_apply (R : Type u) {ι : Type x} {η : Type x} [] (s : ιη) (f : ιR) :
∀ (a : η), f a = Function.extend s f 0 a
noncomputable def Function.ExtendByZero.linearMap (R : Type u) {ι : Type x} {η : Type x} [] (s : ιη) :
(ιR) →ₗ[R] ηR

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

Equations
• = let __src := ; { toFun := fun (f : ιR) => , map_add' := , map_smul' := }
Instances For

### Bundled versions of Matrix.vecCons and Matrix.vecEmpty#

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₁.vecCons <| f₂.vecCons <| f₃.vecCons <| vecEmpty.

While the same thing could be achieved using LinearMap.pi ![f₁, f₂, f₃], this is not definitionally equal to the result using LinearMap.vecCons, as Fin.cases and function application do not commute definitionally.

Versions for when f₁ f₂ f₃ are bilinear maps are also provided.

def LinearMap.vecEmpty {R : Type u} {M : Type v} {M₃ : Type y} [] [] [] [Module R M] [Module R M₃] :
M →ₗ[R] Fin 0M₃

The linear map defeq to Matrix.vecEmpty

Equations
• LinearMap.vecEmpty = { toFun := fun (x : M) => ![], map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.vecEmpty_apply {R : Type u} {M : Type v} {M₃ : Type y} [] [] [] [Module R M] [Module R M₃] (m : M) :
LinearMap.vecEmpty m = ![]
def LinearMap.vecCons {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] {n : } (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin nM₂) :
M →ₗ[R] Fin n.succM₂

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
• f.vecCons g = { toFun := fun (m : M) => Matrix.vecCons (f m) (g m), map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.vecCons_apply {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] {n : } (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin nM₂) (m : M) :
(f.vecCons g) m = Matrix.vecCons (f m) (g m)
@[simp]
theorem LinearMap.vecEmpty₂_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] :
∀ (x : M), LinearMap.vecEmpty₂ x = LinearMap.vecEmpty
def LinearMap.vecEmpty₂ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] :
M →ₗ[R] M₂ →ₗ[R] Fin 0M₃

The empty bilinear map defeq to Matrix.vecEmpty

Equations
• LinearMap.vecEmpty₂ = { toFun := fun (x : M) => LinearMap.vecEmpty, map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.vecCons₂_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] {n : } (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] Fin nM₃) (m : M) :
(f.vecCons₂ g) m = (f m).vecCons (g m)
def LinearMap.vecCons₂ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] {n : } (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] Fin nM₃) :
M →ₗ[R] M₂ →ₗ[R] Fin n.succM₃

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
• f.vecCons₂ g = { toFun := fun (m : M) => (f m).vecCons (g m), map_add' := , map_smul' := }
Instances For