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} [Semiring R] [AddCommMonoid M₂] [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.

@[simp]

theorem LinearMap.pi_apply {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι) : (pi f) c i = (f i) c

theorem LinearMap.ker_pi {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) : ker (pi f) = ⨅ (i : ι), ker (f i)

theorem LinearMap.pi_eq_zero {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) : pi f = 0 ↔ ∀ (i : ι), f i = 0

theorem LinearMap.pi_zero {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] : (pi fun (x : ι) => 0) = 0

theorem LinearMap.pi_comp {R : Type u} {M₂ : Type w} {M₃ : Type y} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) : pi f ∘ₗ g = pi fun (i : ι) => f i ∘ₗ g

def LinearMap.const {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] : M₂ →ₗ[R] ι → M₂

The constant linear map, taking x to Function.const ι x.

@[simp]

theorem LinearMap.const_apply {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] (x : M₂) : const x = Function.const ι x

def LinearMap.proj {R : Type u} {ι : Type x} [Semiring R] {φ : ι → 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: this definition would be called Pi.evalLinearMap if we followed the pattern established by Pi.evalAddHom, Pi.evalMonoidHom, Pi.evalRingHom, ...

@[simp]

theorem LinearMap.coe_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : ⇑(proj i) = Function.eval i

@[simp]

theorem LinearMap.toAddMonoidHom_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : (proj i).toAddMonoidHom = Pi.evalAddMonoidHom φ i

theorem LinearMap.proj_apply {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i) : (proj i) b = b i

@[simp]

theorem LinearMap.proj_pi {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (i : ι) : proj i ∘ₗ pi f = f i

@[simp]

theorem LinearMap.pi_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] : pi proj = id

@[simp]

theorem LinearMap.pi_proj_comp {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : M₂ →ₗ[R] (i : ι) → φ i) : (pi fun (x : ι) => proj x ∘ₗ f) = f

theorem LinearMap.proj_surjective {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : Function.Surjective ⇑(proj i)

theorem LinearMap.iInf_ker_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] : ⨅ (i : ι), ker (proj i) = ⊥

instance LinearMap.CompatibleSMul.pi (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [SMul R M] [SMul R N] [Module S M] [Module S N] [CompatibleSMul M N R S] : CompatibleSMul M (ι → N) R S

def LinearMap.compLeft {R : Type u} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid 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₃.

@[simp]

theorem LinearMap.compLeft_apply {R : Type u} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] (f : M₂ →ₗ[R] M₃) (I : Type u_1) (h : I → M₂) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝

theorem LinearMap.apply_single {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [AddCommMonoid M] [Module R M] [DecidableEq ι] (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} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : φ i →ₗ[R] (i : ι) → φ i

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

theorem LinearMap.single_apply (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {i : ι} (v : φ i) : (single R φ i) v = Pi.single i v

@[simp]

theorem LinearMap.coe_single (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : ⇑(single R φ i) = Pi.single i

theorem LinearMap.proj_comp_single_same (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : proj i ∘ₗ single R φ i = id

theorem LinearMap.proj_comp_single_ne (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i j : ι) (h : i ≠ j) : proj i ∘ₗ single R φ j = 0

theorem LinearMap.iSup_range_single_le_iInf_ker_proj (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (I J : Set ι) (h : Disjoint I J) : ⨆ i ∈ I, range (single R φ i) ≤ ⨅ i ∈ J, ker (proj i)

theorem LinearMap.iInf_ker_proj_le_iSup_range_single (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {I : Finset ι} {J : Set ι} (hu : Set.univ ⊆ ↑I ∪ J) : ⨅ i ∈ J, ker (proj i) ≤ ⨆ i ∈ I, range (single R φ i)

theorem LinearMap.iSup_range_single_eq_iInf_ker_proj (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {I J : Set ι} (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) (hI : I.Finite) : ⨆ i ∈ I, range (single R φ i) = ⨅ i ∈ J, ker (proj i)

theorem LinearMap.iSup_range_single (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] : ⨆ (i : ι), range (single R φ i) = ⊤

theorem LinearMap.disjoint_single_single (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (I J : Set ι) (h : Disjoint I J) : Disjoint (⨆ i ∈ I, range (single R φ i)) (⨆ i ∈ J, range (single R φ i))

def LinearMap.lsum (R : Type u) {M : Type v} {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass 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].

@[simp]

theorem LinearMap.lsum_symm_apply (R : Type u) {M : Type v} {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M] (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) : (lsum R φ S).symm f i = f ∘ₗ single R φ i

@[simp]

theorem LinearMap.lsum_apply (R : Type u) {M : Type v} {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M] (f : (i : ι) → φ i →ₗ[R] M) : (lsum R φ S) f = ∑ i : ι, f i ∘ₗ proj i

theorem LinearMap.lsum_piSingle (R : Type u) {M : Type v} {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (S : Type u_1) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M] (f : (i : ι) → φ i →ₗ[R] M) (i : ι) (x : φ i) : ((lsum R φ S) f) (Pi.single i x) = (f i) x

@[simp]

theorem LinearMap.lsum_single (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (S : Type u_1) [Fintype ι] [Semiring S] [(i : ι) → Module S (φ i)] [∀ (i : ι), SMulCommClass R S (φ i)] : (lsum R φ S) (single R φ) = id

theorem LinearMap.pi_ext {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] [AddCommMonoid 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 LinearMap.pi_ext_iff {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] [AddCommMonoid 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)

theorem LinearMap.pi_ext' {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] [AddCommMonoid M] [Module R M] {f g : ((i : ι) → φ i) →ₗ[R] M} (h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i) : f = g

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

theorem LinearMap.pi_ext'_iff {R : Type u} {M : Type v} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] [AddCommMonoid M] [Module R M] {f g : ((i : ι) → φ i) →ₗ[R] M} : f = g ↔ ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i

def LinearMap.iInfKerProjEquiv (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I J : Set ι} [DecidablePred fun (i : ι) => i ∈ I] (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) : ↥(⨅ i ∈ J, ker (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.

def LinearMap.diag {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i j : ι) : φ i →ₗ[R] φ j

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

theorem LinearMap.update_apply {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type i} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (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.single_eq_pi_diag (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : single R φ i = pi (diag i)

theorem LinearMap.ker_single (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : ker (single R φ i) = ⊥

theorem LinearMap.proj_comp_single (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i j : ι) : proj i ∘ₗ single R φ j = diag j i

theorem LinearMap.pi_apply_eq_sum_univ {R : Type u} {M₂ : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [DecidableEq ι] [Fintype ι] (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} [Semiring R] {φ : ι → 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.

@[simp]

theorem Submodule.coe_pi {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (I : Set ι) (p : (i : ι) → Submodule R (φ i)) : ↑(pi I p) = I.pi fun (i : ι) => ↑(p i)

@[simp]

theorem Submodule.mem_pi {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} {x : (i : ι) → φ i} : x ∈ pi I p ↔ ∀ i ∈ I, x i ∈ p i

@[simp]

theorem Submodule.pi_empty {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (p : (i : ι) → Submodule R (φ i)) : pi ∅ p = ⊤

@[simp]

theorem Submodule.pi_top {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (s : Set ι) : (pi s fun (i : ι) => ⊤) = ⊤

@[simp]

theorem Submodule.pi_univ_bot {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] : (pi Set.univ fun (i : ι) => ⊥) = ⊥

theorem Submodule.pi_mono {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p q : (i : ι) → Submodule R (φ i)} {s : Set ι} (h : ∀ i ∈ s, p i ≤ q i) : pi s p ≤ pi s q

theorem Submodule.biInf_comap_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} : ⨅ i ∈ I, comap (LinearMap.proj i) (p i) = pi I p

theorem Submodule.iInf_comap_proj {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} : ⨅ (i : ι), comap (LinearMap.proj i) (p i) = pi Set.univ p

theorem Submodule.le_comap_single_pi {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (p : (i : ι) → Submodule R (φ i)) {I : Set ι} {i : ι} : p i ≤ comap (LinearMap.single R φ i) (pi I p)

theorem Submodule.iSup_map_single_le {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} [DecidableEq ι] : ⨆ (i : ι), map (LinearMap.single R φ i) (p i) ≤ pi I p

theorem Submodule.iSup_map_single {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} [DecidableEq ι] [Finite ι] : ⨆ (i : ι), map (LinearMap.single R φ i) (p i) = pi Set.univ p

theorem LinearMap.ker_compLeft {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (I : Type u_1) : ker (f.compLeft I) = Submodule.pi Set.univ fun (x : I) => ker f

theorem LinearMap.range_compLeft {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (I : Type u_1) : range (f.compLeft I) = Submodule.pi Set.univ fun (x : I) => range f

def LinearEquiv.piCongrRight {R : Type u} {ι : Type x} [Semiring R] {φ : ι → 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

@[simp]

theorem LinearEquiv.piCongrRight_apply {R : Type u} {ι : Type x} [Semiring R] {φ : ι → 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 : ι) : (piCongrRight e) f i = (e i) (f i)

@[simp]

theorem LinearEquiv.piCongrRight_refl {R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] : (piCongrRight fun (j : ι) => refl R (φ j)) = refl R ((i : ι) → φ i)

@[simp]

theorem LinearEquiv.piCongrRight_symm {R : Type u} {ι : Type x} [Semiring R] {φ : ι → 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) : (piCongrRight e).symm = piCongrRight fun (i : ι) => (e i).symm

@[simp]

theorem LinearEquiv.piCongrRight_trans {R : Type u} {ι : Type x} [Semiring R] {φ : ι → 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) : piCongrRight e ≪≫ₗ piCongrRight f = piCongrRight fun (i : ι) => e i ≪≫ₗ f i

def LinearEquiv.piCongrLeft' (R : Type u) {ι : Type x} {ι' : Type x'} [Semiring R] (φ : ι → 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.

@[simp]

theorem LinearEquiv.piCongrLeft'_apply (R : Type u) {ι : Type x} {ι' : Type x'} [Semiring R] (φ : ι → Type u_1) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (e : ι ≃ ι') (a✝ : (a : ι) → φ a) (b : ι') : (piCongrLeft' R φ e) a✝ b = a✝ (e.symm b)

@[simp]

theorem LinearEquiv.piCongrLeft'_symm_apply (R : Type u) {ι : Type x} {ι' : Type x'} [Semiring R] (φ : ι → Type u_1) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (e : ι ≃ ι') (a✝ : (b : ι') → φ (e.symm b)) (a : ι) : (piCongrLeft' R φ e).symm a✝ a = (Equiv.piCongrLeft' φ e).symm a✝ a

def LinearEquiv.piCongrLeft (R : Type u) {ι : Type x} {ι' : Type x'} [Semiring R] (φ : ι → 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

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

Equiv.piCurry as a LinearEquiv.

@[simp]

theorem LinearEquiv.piCurry_apply (R : Type u) [Semiring R] {ι : Type u_4} {κ : ι → Type u_5} (α : (i : ι) → κ i → Type u_6) [(i : ι) → (k : κ i) → AddCommMonoid (α i k)] [(i : ι) → (k : κ i) → Module R (α i k)] (f : (x : (i : ι) × κ i) → α x.fst x.snd) : (piCurry R α) f = Sigma.curry f

@[simp]

theorem LinearEquiv.piCurry_symm_apply (R : Type u) [Semiring R] {ι : Type u_4} {κ : ι → Type u_5} (α : (i : ι) → κ i → Type u_6) [(i : ι) → (k : κ i) → AddCommMonoid (α i k)] [(i : ι) → (k : κ i) → Module R (α i k)] (f : (a : ι) → (b : κ a) → α a b) : (piCurry R α).symm f = Sigma.uncurry f

def LinearEquiv.piOptionEquivProd (R : Type u) [Semiring R] {ι : Type u_4} {M : Option ι → Type u_5} [(i : Option ι) → AddCommMonoid (M i)] [(i : Option ι) → Module R (M i)] : ((i : Option ι) → M i) ≃ₗ[R] M none × ((i : ι) → M (some i))

This is Equiv.piOptionEquivProd as a LinearEquiv

def LinearEquiv.piRing (R : Type u) (M : Type v) (ι : Type x) [Semiring R] (S : Type u_4) [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass 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].

@[simp]

theorem LinearEquiv.piRing_apply {R : Type u} {M : Type v} {ι : Type x} [Semiring R] (S : Type u_4) [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : (ι → R) →ₗ[R] M) (i : ι) : (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} [Semiring R] (S : Type u_4) [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : ι → M) (g : ι → R) : ((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) [Semiring R] [AddCommMonoid M] [Module R M] : (α ⊕ β → M) ≃ₗ[R] (α → M) × (β → M)

Equiv.sumArrowEquivProdArrow as a linear equivalence.

@[simp]

theorem LinearEquiv.sumArrowLequivProdArrow_apply_fst {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : α ⊕ β → M) (a : α) : ((sumArrowLequivProdArrow α β R M) f).1 a = f (Sum.inl a)

@[simp]

theorem LinearEquiv.sumArrowLequivProdArrow_apply_snd {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : α ⊕ β → M) (b : β) : ((sumArrowLequivProdArrow α β R M) f).2 b = f (Sum.inr b)

@[simp]

theorem LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : α → M) (g : β → M) (a : α) : (sumArrowLequivProdArrow α β R M).symm (f, g) (Sum.inl a) = f a

@[simp]

theorem LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : α → M) (g : β → M) (b : β) : (sumArrowLequivProdArrow α β R M).symm (f, g) (Sum.inr b) = g b

def LinearEquiv.funUnique (ι : Type u_5) (R : Type u_6) (M : Type u_7) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] : (ι → M) ≃ₗ[R] M

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

@[simp]

theorem LinearEquiv.funUnique_symm_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] : ⇑(funUnique ι R M).symm = uniqueElim

@[simp]

theorem LinearEquiv.funUnique_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] : ⇑(funUnique ι R M) = Function.eval default

def LinearEquiv.piFinTwo (R : Type u) [Semiring R] (M : Fin 2 → Type 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.

@[simp]

theorem LinearEquiv.piFinTwo_symm_apply (R : Type u) [Semiring R] (M : Fin 2 → Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] : ⇑(piFinTwo R M).symm = fun (p : M 0 × M 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)

@[simp]

theorem LinearEquiv.piFinTwo_apply (R : Type u) [Semiring R] (M : Fin 2 → Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] : ⇑(piFinTwo R M) = fun (f : (i : Fin 2) → M i) => (f 0, f 1)

def LinearEquiv.finTwoArrow (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : (Fin 2 → M) ≃ₗ[R] M × M

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

@[simp]

theorem LinearEquiv.finTwoArrow_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : ⇑(finTwoArrow R M) = fun (f : Fin 2 → M) => (f 0, f 1)

@[simp]

theorem LinearEquiv.finTwoArrow_symm_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : ⇑(finTwoArrow R M).symm = fun (x : M × M) => ![x.1, x.2]

theorem Pi.mem_span_range_single_inl_iff {R : Type u} {ι : Type x} {ι' : Type x'} [DecidableEq ι] [DecidableEq ι'] [Fintype ι] [Semiring R] {x : ι ⊕ ι' → R} : x ∈ Submodule.span R (Set.range fun (i : ι) => single (Sum.inl i) 1) ↔ ∀ (k : ι'), x (Sum.inr k) = 0

noncomputable def Function.ExtendByZero.linearMap (R : Type u) {ι η : Type x} [Semiring R] (s : ι → η) : (ι → R) →ₗ[R] η → R

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

@[simp]

theorem Function.ExtendByZero.linearMap_apply (R : Type u) {ι η : Type x} [Semiring R] (s : ι → η) (f : ι → R) (a✝ : η) : (linearMap R s) f a✝ = extend s f 0 a✝

def Fin.consLinearEquiv (R : Type u) {n : ℕ} (M : Fin n.succ → Type u_1) [Semiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [(i : Fin n.succ) → Module R (M i)] : (M 0 × ((i : Fin n) → M i.succ)) ≃ₗ[R] (i : Fin n.succ) → M i

Fin.consEquiv as a continuous linear equivalence.

@[simp]

theorem Fin.consLinearEquiv_symm_apply (R : Type u) {n : ℕ} (M : Fin n.succ → Type u_1) [Semiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [(i : Fin n.succ) → Module R (M i)] (a✝ : (i : Fin (n + 1)) → M i) : (consLinearEquiv R M).symm a✝ = (consEquiv M).invFun a✝

@[simp]

theorem Fin.consLinearEquiv_apply (R : Type u) {n : ℕ} (M : Fin n.succ → Type u_1) [Semiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [(i : Fin n.succ) → Module R (M i)] (a✝ : M 0 × ((i : Fin n) → M i.succ)) (i : Fin (n + 1)) : (consLinearEquiv R M) a✝ i = (consEquiv M).toFun a✝ i

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} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module R M₃] : M →ₗ[R] Fin 0 → M₃

The linear map defeq to Matrix.vecEmpty

@[simp]

theorem LinearMap.vecEmpty_apply {R : Type u} {M : Type v} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module R M₃] (m : M) : vecEmpty m = ![]

def LinearMap.vecCons {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid 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₃.

@[simp]

theorem LinearMap.vecCons_apply {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {n : ℕ} (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin n → M₂) (m : M) : (f.vecCons g) m = Matrix.vecCons (f m) (g m)

theorem Module.pi_induction (R : Type u) [Semiring R] {ι : Type v} [Finite ι] (motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop) (motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop) (equiv : ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N') (equiv' : ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N') (unit : motive PUnit.{u + 1}) (prod : ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')) (M : ι → Type u) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (h : ∀ (i : ι), motive (M i)) : motive' ((i : ι) → M i)

To show a property motive of modules holds for arbitrary finite products of modules, it suffices to show

1. motive is stable under isomorphism.
2. motive holds for the zero module.
3. motive holds for M × N if it holds for both M and N.

Since we need to apply motive to modules in Type u and in Type (max u v), there is a second motive' argument which is required to be equivalent to motive up to universe lifting by equiv.

See Module.pi_induction' for a version where motive assumes AddCommGroup instead.

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

The empty bilinear map defeq to Matrix.vecEmpty

@[simp]

theorem LinearMap.vecEmpty₂_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (x✝ : M) : vecEmpty₂ x✝ = vecEmpty

def LinearMap.vecCons₂ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid 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₃

@[simp]

theorem LinearMap.vecCons₂_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid 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.vecCons₂ g) m = (f m).vecCons (g m)

theorem Module.pi_induction' {ι : Type v} [Finite ι] (R : Type u_1) [Ring R] (motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop) (motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop) (equiv : ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N') (equiv' : ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N') (unit : motive PUnit.{u + 1}) (prod : ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')) (M : ι → Type u) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (h : ∀ (i : ι), motive (M i)) : motive' ((i : ι) → M i)

A variant of Module.pi_induction that assumes AddCommGroup instead of AddCommMonoid.