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.

Equations

• LinearMap.pi f = { toFun := fun (c : M₂) (i : ι) => (f i) c, map_add' := ⋯, map_smul' := ⋯ }

@[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.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: known here as LinearMap.proj, this construction is in other categories called eval, for example Pi.evalMonoidHom, Pi.evalRingHom.

Equations

• LinearMap.proj i = { toFun := Function.eval i, map_add' := ⋯, map_smul' := ⋯ }

@[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

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₃.

Equations

• f.compLeft I = { toFun := fun (h : I → M₂) => ⇑f ∘ h, map_add' := ⋯, map_smul' := ⋯ }

@[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.

Equations

• LinearMap.single R φ i = { toFun := Pi.single i, map_add' := ⋯, map_smul' := ⋯ }

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].

Equations

• One or more equations did not get rendered due to their size.

@[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 {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [CommSemiring R] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : (lsum R M R) (single R M) = 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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• LinearMap.diag i j = Function.update 0 i LinearMap.id j

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.

Equations

• Submodule.pi I p = { carrier := I.pi fun (i : ι) => ↑(p i), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[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

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• LinearEquiv.piCongrLeft' R φ e = { toFun := (Equiv.piCongrLeft' φ e).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.piCongrLeft' φ e).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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

@[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)

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

Equations

• LinearEquiv.piCongrLeft R φ e = (LinearEquiv.piCongrLeft' R φ e.symm).symm

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.

Equations

• LinearEquiv.piCurry R α = { toFun := (Equiv.piCurry α).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.piCurry α).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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

Equations

• LinearEquiv.piOptionEquivProd R = { toFun := Equiv.piOptionEquivProd.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := Equiv.piOptionEquivProd.invFun, left_inv := ⋯, right_inv := ⋯ }

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].

Equations

• LinearEquiv.piRing R M ι S = (LinearMap.lsum R (fun (x : ι) => R) S).symm ≪≫ₗ LinearEquiv.piCongrRight fun (x : ι) => LinearMap.ringLmapEquivSelf R S M

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• LinearEquiv.funUnique ι R M = { toFun := (Equiv.funUnique ι M).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.funUnique ι M).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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.

Equations

• LinearEquiv.piFinTwo R M = { toFun := (piFinTwoEquiv M).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (piFinTwoEquiv M).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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.

Equations

• LinearEquiv.finTwoArrow R M = { toFun := (finTwoArrowEquiv M).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (finTwoArrowEquiv M).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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]

@[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)

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.

Equations

• Function.ExtendByZero.linearMap R s = { toFun := fun (f : ι → R) => Function.extend s f 0, map_add' := ⋯, map_smul' := ⋯ }

@[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.

Equations

• Fin.consLinearEquiv R M = { toFun := (Fin.consEquiv M).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Fin.consEquiv M).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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

Equations

• LinearMap.vecEmpty = { toFun := fun (x : M) => ![], map_add' := ⋯, map_smul' := ⋯ }

@[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₃.

Equations

• f.vecCons g = ↑(Fin.consLinearEquiv R fun (x : Fin n.succ) => M₂) ∘ₗ f.prod g

@[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] → [inst : Module R N] → Prop) (motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [inst : 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'], (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'], (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

Equations

• LinearMap.vecEmpty₂ = { toFun := fun (x : M) => LinearMap.vecEmpty, map_add' := ⋯, map_smul' := ⋯ }

@[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₃

Equations

• f.vecCons₂ g = { toFun := fun (m : M) => (f m).vecCons (g m), map_add' := ⋯, map_smul' := ⋯ }

@[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] → [inst : Module R N] → Prop) (motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [inst : 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'], (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'], (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.