doc-next-gen

Mathlib.LinearAlgebra.Pi

Module docstring

{"# 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

","### 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.

"}

LinearMap.pi definition
(f : (i : ι) → M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (i : ι) → φ i
Full source 
/-- `pi` construction for linear functions. From a family of linear functions it produces a linear
function into a family of modules. -/
def pi (f : (i : ι) → M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (i : ι) → φ i :=
  { Pi.addHom fun i => (f i).toAddHom with
    toFun := fun c i => f i c
    map_smul' := fun _ _ => funext fun i => (f i).map_smul _ _ }
Linear map into a product space
Informal description
Given a family of linear maps \( f_i : M_2 \to \varphi_i \) for each \( i \) in an index set \( \iota \), the function `LinearMap.pi` constructs a linear map from \( M_2 \) to the product space \( \prod_{i \in \iota} \varphi_i \), defined by \( c \mapsto (f_i(c))_{i \in \iota} \).
LinearMap.pi_apply theorem
(f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι) : pi f c i = f i c
Full source 
@[simp]
theorem pi_apply (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι) : pi f c i = f i c :=
  rfl
Component-wise Evaluation of Linear Map into Product Space
Informal description
For a family of linear maps \( f_i : M_2 \to \varphi_i \) indexed by \( i \in \iota \), the evaluation of the linear map \( \pi f \) at \( c \in M_2 \) in the \( i \)-th component is equal to \( f_i(c) \), i.e., \( (\pi f)(c)_i = f_i(c) \).
LinearMap.ker_pi theorem
(f : (i : ι) → M₂ →ₗ[R] φ i) : ker (pi f) = ⨅ i : ι, ker (f i)
Full source 
theorem ker_pi (f : (i : ι) → M₂ →ₗ[R] φ i) : ker (pi f) = ⨅ i : ι, ker (f i) := by
  ext c; simp [funext_iff]
Kernel of Linear Map into Product Space as Intersection of Kernels
Informal description
For a family of linear maps \( f_i : M_2 \to \varphi_i \) indexed by \( i \in \iota \), the kernel of the linear map \( \pi f : M_2 \to \prod_{i \in \iota} \varphi_i \) is equal to the intersection of the kernels of the individual maps \( f_i \), i.e., \[ \ker(\pi f) = \bigcap_{i \in \iota} \ker(f_i). \]
LinearMap.pi_eq_zero theorem
(f : (i : ι) → M₂ →ₗ[R] φ i) : pi f = 0 ↔ ∀ i, f i = 0
Full source 
theorem pi_eq_zero (f : (i : ι) → M₂ →ₗ[R] φ i) : pipi f = 0 ↔ ∀ i, f i = 0 := by
  simp only [LinearMap.ext_iff, pi_apply, funext_iff]
  exact ⟨fun h a b => h b a, fun h a b => h b a⟩
Zero Criterion for Linear Map into Product Space
Informal description
For a family of linear maps \( f_i : M_2 \to \varphi_i \) indexed by \( i \in \iota \), the linear map \( \pi f : M_2 \to \prod_{i \in \iota} \varphi_i \) is the zero map if and only if each \( f_i \) is the zero map. In other words, \[ \pi f = 0 \leftrightarrow \forall i \in \iota, f_i = 0. \]
LinearMap.pi_zero theorem
: pi (fun _ => 0 : (i : ι) → M₂ →ₗ[R] φ i) = 0
Full source 
theorem pi_zero : pi (fun _ => 0 : (i : ι) → M₂ →ₗ[R] φ i) = 0 := by ext; rfl
Zero Construction Yields Zero Map in Product Space
Informal description
The linear map $\pi f : M_2 \to \prod_{i \in \iota} \varphi_i$ constructed from the family of zero maps $f_i = 0$ for each $i \in \iota$ is itself the zero map.
LinearMap.pi_comp theorem
(f : (i : ι) → M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) : (pi f).comp g = pi fun i => (f i).comp g
Full source 
theorem pi_comp (f : (i : ι) → M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) :
    (pi f).comp g = pi fun i => (f i).comp g :=
  rfl
Composition of Product Linear Map with Another Linear Map
Informal description
Let $R$ be a ring, $\iota$ an index set, and $\{\varphi_i\}_{i \in \iota}$ a family of $R$-modules. Given a family of $R$-linear maps $f_i : M_2 \to \varphi_i$ for each $i \in \iota$ and an $R$-linear map $g : M_3 \to M_2$, the composition of the product map $\pi f : M_2 \to \prod_{i \in \iota} \varphi_i$ with $g$ equals the product map formed by composing each $f_i$ with $g$. That is, \[ (\pi f) \circ g = \pi \left( \lambda i, f_i \circ g \right). \]
LinearMap.proj definition
(i : ι) : ((i : ι) → φ i) →ₗ[R] φ i
Full source 
/-- 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`. -/
def proj (i : ι) : ((i : ι) → φ i) →ₗ[R] φ i where
  toFun := Function.eval i
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
Projection linear map
Informal description
For each index $i$ in the index set $\iota$, the projection map $\text{proj}_i$ is a linear map from the product space $\prod_{i \in \iota} \phi_i$ to the component space $\phi_i$. Specifically, $\text{proj}_i$ evaluates a function $b$ at the index $i$, i.e., $\text{proj}_i(b) = b(i)$.
LinearMap.coe_proj theorem
(i : ι) : ⇑(proj i : ((i : ι) → φ i) →ₗ[R] φ i) = Function.eval i
Full source 
@[simp]
theorem coe_proj (i : ι) : ⇑(proj i : ((i : ι) → φ i) →ₗ[R] φ i) = Function.eval i :=
  rfl
Projection Map as Evaluation Function
Informal description
For any index $i$ in the index set $\iota$, the underlying function of the projection linear map $\text{proj}_i$ from the product space $\prod_{i \in \iota} \phi_i$ to $\phi_i$ is equal to the evaluation function at $i$, i.e., $\text{proj}_i(b) = b(i)$ for all $b \in \prod_{i \in \iota} \phi_i$.
LinearMap.proj_apply theorem
(i : ι) (b : (i : ι) → φ i) : (proj i : ((i : ι) → φ i) →ₗ[R] φ i) b = b i
Full source 
theorem proj_apply (i : ι) (b : (i : ι) → φ i) : (proj i : ((i : ι) → φ i) →ₗ[R] φ i) b = b i :=
  rfl
Projection Map Evaluation: $\text{proj}_i(b) = b(i)$
Informal description
For any index $i$ in the index set $\iota$ and any element $b$ in the product space $\prod_{i \in \iota} \phi_i$, the application of the projection linear map $\text{proj}_i$ to $b$ equals the evaluation of $b$ at $i$, i.e., $\text{proj}_i(b) = b(i)$.
LinearMap.proj_pi theorem
(f : (i : ι) → M₂ →ₗ[R] φ i) (i : ι) : (proj i).comp (pi f) = f i
Full source 
@[simp]
theorem proj_pi (f : (i : ι) → M₂ →ₗ[R] φ i) (i : ι) : (proj i).comp (pi f) = f i := rfl
Composition of Projection with Pi Map: \( \text{proj}_i \circ \pi f = f_i \)
Informal description
For any family of linear maps \( f_i : M_2 \to \varphi_i \) indexed by \( i \in \iota \), and for any index \( i \in \iota \), the composition of the projection map \( \text{proj}_i \) with the linear map \( \pi f \) (constructed from the family \( f \)) equals \( f_i \). That is, \( \text{proj}_i \circ \pi f = f_i \).
LinearMap.pi_proj theorem
: pi proj = LinearMap.id (R := R) (M := ∀ i, φ i)
Full source 
@[simp]
theorem pi_proj : pi proj = LinearMap.id (R := R) (M := ∀ i, φ i) := rfl
Identity via Projections: $\pi(\text{proj}_i) = \text{id}$
Informal description
The linear map $\pi$ constructed from the family of projection maps $\text{proj}_i$ is equal to the identity map on the product space $\prod_{i \in \iota} \varphi_i$.
LinearMap.pi_proj_comp theorem
(f : M₂ →ₗ[R] ∀ i, φ i) : pi (proj · ∘ₗ f) = f
Full source 
@[simp]
theorem pi_proj_comp (f : M₂ →ₗ[R] ∀ i, φ i) : pi (projproj · ∘ₗ f) = f := rfl
Reconstruction of Linear Map via Projections: $\pi (\text{proj}_i \circ f) = f$
Informal description
For any linear map $f \colon M_2 \to \prod_{i \in \iota} \varphi_i$ over a ring $R$, the composition of the projection maps $\text{proj}_i$ with $f$ reconstructs $f$ itself when combined via the $\pi$ construction. That is, $\pi (\text{proj}_i \circ f) = f$.
LinearMap.proj_surjective theorem
(i : ι) : Surjective (proj i : ((i : ι) → φ i) →ₗ[R] φ i)
Full source 
theorem proj_surjective (i : ι) : Surjective (proj i : ((i : ι) → φ i) →ₗ[R] φ i) :=
  surjective_eval i
Surjectivity of Projection Linear Maps on Pi Types
Informal description
For any index $i$ in the index set $\iota$, the projection map $\text{proj}_i : \prod_{i \in \iota} \phi_i \to \phi_i$ is surjective. That is, for every element $y \in \phi_i$, there exists an element $x \in \prod_{i \in \iota} \phi_i$ such that $\text{proj}_i(x) = y$.
LinearMap.iInf_ker_proj theorem
: (⨅ i, ker (proj i : ((i : ι) → φ i) →ₗ[R] φ i) : Submodule R ((i : ι) → φ i)) = ⊥
Full source 
theorem iInf_ker_proj : (⨅ i, ker (proj i : ((i : ι) → φ i) →ₗ[R] φ i) :
    Submodule R ((i : ι) → φ i)) = ⊥ :=
  bot_unique <|
    SetLike.le_def.2 fun a h => by
      simp only [mem_iInf, mem_ker, proj_apply] at h
      exact (mem_bot _).2 (funext fun i => h i)
Trivial Intersection of Kernels of Projection Maps on Pi Modules
Informal description
For a family of modules $\{\phi_i\}_{i \in \iota}$ over a ring $R$, the intersection of the kernels of all projection maps $\text{proj}_i : \prod_{i \in \iota} \phi_i \to \phi_i$ is the trivial submodule $\{0\}$. In other words, $\bigcap_{i \in \iota} \ker(\text{proj}_i) = \bot$.
LinearMap.CompatibleSMul.pi instance
(R S M N ι : Type*) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [SMul R M] [SMul R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul M (ι → N) R S
Full source 
instance CompatibleSMul.pi (R S M N ι : Type*) [Semiring S]
    [AddCommMonoid M] [AddCommMonoid N] [SMul R M] [SMul R N] [Module S M] [Module S N]
    [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul M (ι → N) R S where
  map_smul f r m := by ext i; apply ((LinearMap.proj i).comp f).map_smul_of_tower
Compatibility of Scalar Multiplication with Function Spaces
Informal description
For any types $R$, $S$, $M$, $N$, and $\iota$, given a semiring $S$, additive commutative monoids $M$ and $N$, scalar multiplication operations of $R$ on $M$ and $N$, module structures of $S$ on $M$ and $N$, and a compatible scalar multiplication structure between $M$ and $N$ over $R$ and $S$, there exists a compatible scalar multiplication structure between $M$ and the function space $\iota \to N$ over $R$ and $S$.
LinearMap.compLeft definition
(f : M₂ →ₗ[R] M₃) (I : Type*) : (I → M₂) →ₗ[R] I → M₃
Full source 
/-- Linear map between the function spaces `I → M₂` and `I → M₃`, induced by a linear map `f`
between `M₂` and `M₃`. -/
@[simps]
protected def compLeft (f : M₂ →ₗ[R] M₃) (I : Type*) : (I → M₂) →ₗ[R] I → M₃ :=
  { f.toAddMonoidHom.compLeft I with
    toFun := fun h => f ∘ h
    map_smul' := fun c h => by
      ext x
      exact f.map_smul' c (h x) }
Left composition with a linear map
Informal description
Given a linear map \( f : M_2 \to M_3 \) over a ring \( R \) and an index type \( I \), the linear map \( \text{compLeft} \) maps a function \( h : I \to M_2 \) to the composition \( f \circ h : I \to M_3 \). This operation preserves the linear structure, meaning it respects addition and scalar multiplication.
LinearMap.apply_single theorem
[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) : ι → M) j
Full source 
theorem apply_single [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) : ι → M) j :=
  Pi.apply_single (fun i => f i) (fun i => (f i).map_zero) _ _ _
Evaluation of Linear Maps on Single Elements in Pi Types
Informal description
Let $R$ be a ring, $M$ an additive commutative monoid with an $R$-module structure, $\iota$ a decidable index type, and $(\phi_i)_{i \in \iota}$ a family of $R$-modules. Given a family of linear maps $f_i : \phi_i \to M$ for each $i \in \iota$, and elements $i, j \in \iota$ and $x \in \phi_i$, we have: \[ f_j(\text{Pi.single}_i(x)_j) = \text{Pi.single}_i(f_i(x))_j \] where $\text{Pi.single}_i(x)$ denotes the function that is $x$ at $i$ and zero elsewhere.
LinearMap.single definition
[DecidableEq ι] (i : ι) : φ i →ₗ[R] (i : ι) → φ i
Full source 
/-- The `LinearMap` version of `AddMonoidHom.single` and `Pi.single`. -/
def single [DecidableEq ι] (i : ι) : φ i →ₗ[R] (i : ι) → φ i :=
  { AddMonoidHom.single φ i with
    toFun := Pi.single i
    map_smul' := Pi.single_smul i }
Linear single map
Informal description
For a decidable index type $\iota$ and a family of $R$-modules $(\phi_i)_{i \in \iota}$, the linear map $\text{single}_i : \phi_i \to \bigoplus_{j \in \iota} \phi_j$ is defined as the linear extension of the function that maps an element $x \in \phi_i$ to the tuple $(0, \ldots, 0, x, 0, \ldots, 0)$ where $x$ appears in the $i$-th position. This is the linear algebra version of the single function in the additive monoid homomorphism context.
LinearMap.single_apply theorem
[DecidableEq ι] {i : ι} (v : φ i) : single R φ i v = Pi.single i v
Full source 
lemma single_apply [DecidableEq ι] {i : ι} (v : φ i) :
    single R φ i v = Pi.single i v :=
  rfl
Single Linear Map Equals Pi Single Function
Informal description
For a decidable index type $\iota$ and a family of $R$-modules $(\phi_i)_{i \in \iota}$, given an index $i \in \iota$ and an element $v \in \phi_i$, the linear map $\text{single}_i(v)$ is equal to the function $\text{Pi.single}_i(v)$, which maps $v$ to the tuple $(0, \ldots, 0, v, 0, \ldots, 0)$ where $v$ appears in the $i$-th position.
LinearMap.coe_single theorem
[DecidableEq ι] (i : ι) : ⇑(single R φ i : φ i →ₗ[R] (i : ι) → φ i) = Pi.single i
Full source 
@[simp]
theorem coe_single [DecidableEq ι] (i : ι) :
    ⇑(single R φ i : φ i →ₗ[R] (i : ι) → φ i) = Pi.single i :=
  rfl
Coefficient Function of Linear Single Map Equals Pi Single Function
Informal description
For a decidable index type $\iota$ and a family of $R$-modules $(\phi_i)_{i \in \iota}$, the underlying function of the linear map $\text{single}_i : \phi_i \to \bigoplus_{j \in \iota} \phi_j$ is equal to the function $\text{Pi.single}_i$, which maps an element $x \in \phi_i$ to the tuple $(0, \ldots, 0, x, 0, \ldots, 0)$ where $x$ appears in the $i$-th position.
LinearMap.proj_comp_single_same theorem
(i : ι) : (proj i).comp (single R φ i) = id
Full source 
theorem proj_comp_single_same (i : ι) : (proj i).comp (single R φ i) = id :=
  LinearMap.ext <| Pi.single_eq_same i
Composition of Projection and Single Maps Yields Identity
Informal description
For any index $i$ in the index set $\iota$, the composition of the projection map $\text{proj}_i$ with the single map $\text{single}_i$ is equal to the identity map on $\phi_i$, i.e., $\text{proj}_i \circ \text{single}_i = \text{id}$.
LinearMap.proj_comp_single_ne theorem
(i j : ι) (h : i ≠ j) : (proj i).comp (single R φ j) = 0
Full source 
theorem proj_comp_single_ne (i j : ι) (h : i ≠ j) : (proj i).comp (single R φ j) = 0 :=
  LinearMap.ext <| Pi.single_eq_of_ne h
Composition of Projection and Single Maps for Distinct Indices is Zero
Informal description
For any distinct indices $i$ and $j$ in the index set $\iota$, the composition of the projection map $\text{proj}_i$ with the linear single map $\text{single}_j$ is the zero linear map, i.e., $\text{proj}_i \circ \text{single}_j = 0$.
LinearMap.iSup_range_single_le_iInf_ker_proj theorem
(I J : Set ι) (h : Disjoint I J) : ⨆ i ∈ I, range (single R φ i) ≤ ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i)
Full source 
theorem iSup_range_single_le_iInf_ker_proj (I J : Set ι) (h : Disjoint I J) :
    ⨆ i ∈ I, range (single R φ i) ≤ ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i) := by
  refine iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 ?_
  simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
  rintro b - j hj
  rw [proj_comp_single_ne R φ j i, zero_apply]
  rintro rfl
  exact h.le_bot ⟨hi, hj⟩
Inclusion of Single Map Ranges in Projection Kernels for Disjoint Index Sets
Informal description
Let $I$ and $J$ be disjoint subsets of the index set $\iota$. Then the supremum of the ranges of the single maps $\text{single}_i$ for $i \in I$ is contained in the infimum of the kernels of the projection maps $\text{proj}_i$ for $i \in J$. In other words: \[ \bigcup_{i \in I} \text{range}(\text{single}_i) \subseteq \bigcap_{i \in J} \ker(\text{proj}_i). \]
LinearMap.iInf_ker_proj_le_iSup_range_single theorem
{I : Finset ι} {J : Set ι} (hu : Set.univ ⊆ ↑I ∪ J) : ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i) ≤ ⨆ i ∈ I, range (single R φ i)
Full source 
theorem iInf_ker_proj_le_iSup_range_single {I : Finset ι} {J : Set ι} (hu : Set.univSet.univ ⊆ ↑I ∪ J) :
    ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i) ≤ ⨆ i ∈ I, range (single R φ i) :=
  SetLike.le_def.2
    (by
      intro b hb
      simp only [mem_iInf, mem_ker, proj_apply] at hb
      rw [←
        show (∑ i ∈ I, Pi.single i (b i)) = b by
          ext i
          rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
          refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
          intro hiI
          rw [Pi.single_eq_same]
          exact hb _ ((hu trivial).resolve_left hiI)]
      exact sum_mem_biSup fun i _ => mem_range_self (single R φ i) (b i))
Inclusion of Infimum of Projection Kernels in Supremum of Single Ranges
Informal description
Let $I$ be a finite subset and $J$ be a subset of the index set $\iota$ such that the entire universe is covered by $I \cup J$. Then the infimum of the kernels of the projection maps $\text{proj}_i$ for $i \in J$ is contained in the supremum of the ranges of the single maps $\text{single}_i$ for $i \in I$. In other words: \[ \bigcap_{i \in J} \ker(\text{proj}_i) \subseteq \sum_{i \in I} \text{range}(\text{single}_i). \]
LinearMap.iSup_range_single_eq_iInf_ker_proj theorem
{I J : Set ι} (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) (hI : Set.Finite I) : ⨆ i ∈ I, range (single R φ i) = ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i)
Full source 
theorem iSup_range_single_eq_iInf_ker_proj {I J : Set ι} (hd : Disjoint I J)
    (hu : Set.univSet.univ ⊆ I ∪ J) (hI : Set.Finite I) :
    ⨆ i ∈ I, range (single R φ i) = ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i) := by
  refine le_antisymm (iSup_range_single_le_iInf_ker_proj _ _ _ _ hd) ?_
  have : Set.univSet.univ ⊆ ↑hI.toFinset ∪ J := by rwa [hI.coe_toFinset]
  refine le_trans (iInf_ker_proj_le_iSup_range_single R φ this) (iSup_mono fun i => ?_)
  rw [Set.Finite.mem_toFinset]
Equality of Single Map Ranges and Projection Kernels for Finite Covering Index Sets
Informal description
Let $I$ and $J$ be disjoint subsets of an index set $\iota$ such that their union covers the entire set $\iota$, and $I$ is finite. Then the supremum of the ranges of the single linear maps $\text{single}_i : \phi_i \to \prod_{j \in \iota} \phi_j$ for $i \in I$ equals the infimum of the kernels of the projection maps $\text{proj}_i : \prod_{j \in \iota} \phi_j \to \phi_i$ for $i \in J$. In other words: \[ \bigcup_{i \in I} \text{range}(\text{single}_i) = \bigcap_{i \in J} \ker(\text{proj}_i). \]
LinearMap.iSup_range_single theorem
[Finite ι] : ⨆ i, range (single R φ i) = ⊤
Full source 
theorem iSup_range_single [Finite ι] : ⨆ i, range (single R φ i) = ⊤ := by
  cases nonempty_fintype ι
  convert top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_single R φ _)
  · rename_i i
    exact ((@iSup_pos _ _ _ fun _ => range <| single R φ i) <| Finset.mem_univ i).symm
  · rw [Finset.coe_univ, Set.union_empty]
Supremum of Single Map Ranges Covers Entire Space for Finite Index Sets
Informal description
For a finite index set $\iota$ and a family of $R$-modules $(\phi_i)_{i \in \iota}$, the supremum of the ranges of the single linear maps $\text{single}_i : \phi_i \to \prod_{j \in \iota} \phi_j$ for all $i \in \iota$ equals the entire space $\prod_{j \in \iota} \phi_j$. In other words: \[ \bigcup_{i \in \iota} \text{range}(\text{single}_i) = \prod_{j \in \iota} \phi_j. \]
LinearMap.disjoint_single_single theorem
(I J : Set ι) (h : Disjoint I J) : Disjoint (⨆ i ∈ I, range (single R φ i)) (⨆ i ∈ J, range (single R φ i))
Full source 
theorem disjoint_single_single (I J : Set ι) (h : Disjoint I J) :
    Disjoint (⨆ i ∈ I, range (single R φ i)) (⨆ i ∈ J, range (single R φ i)) := by
  refine
    Disjoint.mono (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
      (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) ?_
  simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply,
    funext_iff]
  rintro b ⟨hI, hJ⟩ i
  classical
    by_cases hiI : i ∈ I
    · by_cases hiJ : i ∈ J
      · exact (h.le_bot ⟨hiI, hiJ⟩).elim
      · exact hJ i hiJ
    · exact hI i hiI
Disjointness of Single Map Ranges for Disjoint Index Sets
Informal description
Let $I$ and $J$ be disjoint subsets of an index set $\iota$. Then the ranges of the single linear maps $\text{single}_i$ for $i \in I$ are disjoint from the ranges of the single linear maps $\text{single}_j$ for $j \in J$. In other words, the supremum of the ranges $\bigsqcup_{i \in I} \text{range}(\text{single}_i)$ is disjoint from the supremum of the ranges $\bigsqcup_{j \in J} \text{range}(\text{single}_j)$.
LinearMap.lsum definition
(S) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M] : ((i : ι) → φ i →ₗ[R] M) ≃ₗ[S] ((i : ι) → φ i) →ₗ[R] M
Full source 
/-- 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]. -/
@[simps symm_apply]
def lsum (S) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M]
    [SMulCommClass R S M] : ((i : ι) → φ i →ₗ[R] M) ≃ₗ[S] ((i : ι) → φ i) →ₗ[R] M where
  toFun f := ∑ i : ι, (f i).comp (proj i)
  invFun f i := f.comp (single R φ i)
  map_add' f g := by simp only [Pi.add_apply, add_comp, Finset.sum_add_distrib]
  map_smul' c f := by simp only [Pi.smul_apply, smul_comp, Finset.smul_sum, RingHom.id_apply]
  left_inv f := by
    ext i x
    simp [apply_single]
  right_inv f := by
    ext x
    suffices f (∑ j, Pi.single j (x j)) = f x by simpa [apply_single]
    rw [Finset.univ_sum_single]
Linear Sum Equivalence for Families of Linear Maps
Informal description
Given a finite index set $\iota$, a commutative ring $R$, and a family of $R$-modules $(\phi_i)_{i \in \iota}$, the linear equivalence `LinearMap.lsum` maps a family of linear maps $(f_i : \phi_i \to M)_{i \in \iota}$ to the linear map $\sum_{i \in \iota} (f_i \circ \text{proj}_i)$, where $\text{proj}_i$ is the projection onto the $i$-th component. Conversely, it maps a linear map $f : \prod_{i \in \iota} \phi_i \to M$ to the family of linear maps $(f \circ \text{single}_i)_{i \in \iota}$, where $\text{single}_i$ is the inclusion of $\phi_i$ into the product. This equivalence is also $S$-linear when $M$ is an $S$-module and the actions of $R$ and $S$ on $M$ commute.
LinearMap.lsum_apply theorem
(S) [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).comp (proj i)
Full source 
@[simp]
theorem lsum_apply (S) [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).comp (proj i) := rfl
Linear Sum Map as Sum of Compositions with Projections
Informal description
Let $R$ be a ring, $M$ an $R$-module, $\iota$ a finite index set, and $(\phi_i)_{i \in \iota}$ a family of $R$-modules. Given a family of linear maps $(f_i : \phi_i \to M)_{i \in \iota}$, the linear sum map $\text{lsum}_R \phi S f$ is equal to the sum over $\iota$ of the compositions $f_i \circ \text{proj}_i$, where $\text{proj}_i$ is the projection onto the $i$-th component. In other words: \[ \text{lsum}_R \phi S f = \sum_{i \in \iota} (f_i \circ \text{proj}_i) \]
LinearMap.lsum_piSingle theorem
(S) [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
Full source 
theorem lsum_piSingle (S) [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 := by
  simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']
Evaluation of Linear Sum Map on Single Elements
Informal description
Let $R$ be a ring, $M$ an $R$-module, $\iota$ a finite index set, and $(\phi_i)_{i \in \iota}$ a family of $R$-modules. Given a family of linear maps $(f_i : \phi_i \to M)_{i \in \iota}$, the linear sum map $\text{lsum}_R \phi S f$ evaluated at the single element $\text{Pi.single}_i(x)$ (which is $x$ in the $i$-th component and zero elsewhere) equals $f_i(x)$. In other words, for any $i \in \iota$ and $x \in \phi_i$, we have: \[ \text{lsum}_R \phi S f (\text{Pi.single}_i(x)) = f_i(x) \]
LinearMap.lsum_single theorem
{ι R : Type*} [Fintype ι] [DecidableEq ι] [CommSemiring R] {M : ι → Type*} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : LinearMap.lsum R M R (LinearMap.single R M) = LinearMap.id
Full source 
@[simp high]
theorem lsum_single {ι R : Type*} [Fintype ι] [DecidableEq ι] [CommSemiring R] {M : ι → Type*}
    [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :
    LinearMap.lsum R M R (LinearMap.single R M) = LinearMap.id :=
  LinearMap.ext fun x => by simp [Finset.univ_sum_single]
Identity of Linear Sum Equivalence for Single Maps on Direct Sum
Informal description
Let $\iota$ be a finite type with decidable equality, $R$ a commutative semiring, and $(M_i)_{i \in \iota}$ a family of $R$-modules. Then the linear sum equivalence applied to the family of linear single maps $( \text{single}_i : M_i \to \bigoplus_{j \in \iota} M_j )_{i \in \iota}$ yields the identity map on $\bigoplus_{i \in \iota} M_i$. In other words, $\text{lsum}_R M R (\text{single}_R M) = \text{id}$, where: - $\text{single}_i$ is the canonical inclusion of $M_i$ into the direct sum, - $\text{lsum}$ is the linear sum equivalence that combines a family of linear maps into a single linear map on the direct sum, - $\text{id}$ is the identity linear map on $\bigoplus_{i \in \iota} M_i$.
LinearMap.pi_ext theorem
(h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) : f = g
Full source 
theorem pi_ext (h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) : f = g :=
  toAddMonoidHom_injective <| AddMonoidHom.functions_ext _ _ _ h
Extensionality of Linear Maps on Direct Sum via Single Components
Informal description
Let $R$ be a commutative semiring, and let $\{\phi_i\}_{i \in \iota}$ and $M$ be families of $R$-modules. Given two linear maps $f, g \colon \bigoplus_{i \in \iota} \phi_i \to M$, if for every index $i \in \iota$ and every element $x \in \phi_i$ we have $f(\text{single}_i(x)) = g(\text{single}_i(x))$, where $\text{single}_i(x)$ is the element of $\bigoplus_{i \in \iota} \phi_i$ with $x$ in the $i$-th position and zero elsewhere, then $f = g$.
LinearMap.pi_ext_iff theorem
: f = g ↔ ∀ i x, f (Pi.single i x) = g (Pi.single i x)
Full source 
theorem pi_ext_iff : f = g ↔ ∀ i x, f (Pi.single i x) = g (Pi.single i x) :=
  ⟨fun h _ _ => h ▸ rfl, pi_ext⟩
Equivalence of Linear Map Equality and Equality on Single Components
Informal description
Let $R$ be a commutative semiring, and let $\{\phi_i\}_{i \in \iota}$ and $M$ be families of $R$-modules. For two linear maps $f, g \colon \bigoplus_{i \in \iota} \phi_i \to M$, the following are equivalent: 1. $f = g$, 2. For every index $i \in \iota$ and every element $x \in \phi_i$, we have $f(\text{single}_i(x)) = g(\text{single}_i(x))$, where $\text{single}_i(x)$ is the element of $\bigoplus_{i \in \iota} \phi_i$ with $x$ in the $i$-th position and zero elsewhere.
LinearMap.pi_ext' theorem
(h : ∀ i, f.comp (single R φ i) = g.comp (single R φ i)) : f = g
Full source 
/-- This is used as the ext lemma instead of `LinearMap.pi_ext` for reasons explained in
note [partially-applied ext lemmas]. -/
@[ext]
theorem pi_ext' (h : ∀ i, f.comp (single R φ i) = g.comp (single R φ i)) : f = g := by
  refine pi_ext fun i x => ?_
  convert LinearMap.congr_fun (h i) x
Extensionality of Linear Maps via Composition with Single Components
Informal description
Let $R$ be a commutative semiring, and let $\{\phi_i\}_{i \in \iota}$ be a family of $R$-modules. Given two linear maps $f, g \colon \bigoplus_{i \in \iota} \phi_i \to M$, if for every index $i \in \iota$ the composition $f \circ \text{single}_i$ equals $g \circ \text{single}_i$, where $\text{single}_i \colon \phi_i \to \bigoplus_{j \in \iota} \phi_j$ is the canonical inclusion map, then $f = g$.
LinearMap.iInfKerProjEquiv definition
{I J : Set ι} [DecidablePred fun i => i ∈ I] (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) : (⨅ i ∈ J, ker (proj i : ((i : ι) → φ i) →ₗ[R] φ i) : Submodule R ((i : ι) → φ i)) ≃ₗ[R] (i : I) → φ i
Full source 
/-- If `I` and `J` are disjoint index sets, the product of the kernels of the `J`th projections of
`φ` is linearly equivalent to the product over `I`. -/
def iInfKerProjEquiv {I J : Set ι} [DecidablePred fun i => i ∈ I] (hd : Disjoint I J)
    (hu : Set.univSet.univ ⊆ I ∪ J) :
    (⨅ i ∈ J, ker (proj i : ((i : ι) → φ i) →ₗ[R] φ i) :
    Submodule R ((i : ι) → φ i)) ≃ₗ[R] (i : I) → φ i := by
  refine
    LinearEquiv.ofLinear (pi fun i => (proj (i : ι)).comp (Submodule.subtype _))
      (codRestrict _ (pi fun i => if h : i ∈ I then proj (⟨i, h⟩ : I) else 0) ?_) ?_ ?_
  · intro b
    simp only [mem_iInf, mem_ker, funext_iff, proj_apply, pi_apply]
    intro j hjJ
    have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩
    rw [dif_neg this, zero_apply]
  · simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop]
    ext b ⟨j, hj⟩
    simp only [dif_pos, Function.comp_apply, Function.eval_apply, LinearMap.codRestrict_apply,
      LinearMap.coe_comp, LinearMap.coe_proj, LinearMap.pi_apply, Submodule.subtype_apply,
      Subtype.coe_prop]
    rfl
  · ext1 ⟨b, hb⟩
    apply Subtype.ext
    ext j
    have hb : ∀ i ∈ J, b i = 0 := by
      simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb
    simp only [comp_apply, pi_apply, id_apply, proj_apply, subtype_apply, codRestrict_apply]
    split_ifs with h
    · rfl
    · exact (hb _ <| (hu trivial).resolve_left h).symm
Linear equivalence between intersection of kernels and product over disjoint index set
Informal description
Given two disjoint index sets $I$ and $J$ whose union covers the entire index set $\iota$, the submodule $\bigcap_{i \in J} \ker(\text{proj}_i)$ (where $\text{proj}_i$ is the projection map from the product space $\prod_{i \in \iota} \phi_i$ to $\phi_i$) is linearly equivalent to the product space $\prod_{i \in I} \phi_i$. More precisely, the equivalence is constructed by restricting the projection maps $\text{proj}_i$ for $i \in I$ to the submodule $\bigcap_{i \in J} \ker(\text{proj}_i)$, and then assembling these restricted projections into a linear map to $\prod_{i \in I} \phi_i$. The inverse map is given by extending a family of elements in $\prod_{i \in I} \phi_i$ to the full product space by setting the components indexed by $J$ to zero.
LinearMap.diag definition
(i j : ι) : φ i →ₗ[R] φ j
Full source 
/-- `diag i j` is the identity map if `i = j`. Otherwise it is the constant 0 map. -/
def diag (i j : ι) : φ i →ₗ[R] φ j :=
  @Function.update ι (fun j => φ i →ₗ[R] φ j) _ 0 i id j
Diagonal linear map between components of a product space
Informal description
For each pair of indices $i$ and $j$ in the index set $\iota$, the linear map $\text{diag}_{i,j} : \phi_i \to \phi_j$ is defined as the identity map when $i = j$ and the zero map otherwise.
LinearMap.update_apply theorem
(f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i j : ι) (b : M₂ →ₗ[R] φ i) : (update f i b j) c = update (fun i => f i c) i (b c) j
Full source 
theorem update_apply (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i j : ι) (b : M₂ →ₗ[R] φ i) :
    (update f i b j) c = update (fun i => f i c) i (b c) j := by
  by_cases h : j = i
  · rw [h, update_self, update_self]
  · rw [update_of_ne h, update_of_ne h]
Evaluation-Update Commutation for Linear Maps
Informal description
Let $R$ be a commutative ring, $\iota$ an index set, and $\{\phi_i\}_{i \in \iota}$ a family of $R$-modules. Given a family of linear maps $f = (f_i : M_2 \to \phi_i)_{i \in \iota}$, a vector $c \in M_2$, indices $i,j \in \iota$, and a linear map $b : M_2 \to \phi_i$, then evaluating the updated family $f$ (with $f_i$ replaced by $b$) at index $j$ and vector $c$ equals updating the evaluation map $i \mapsto f_i(c)$ at index $i$ with value $b(c)$ and then evaluating at $j$. In symbols: $$(\text{update}\, f\, i\, b\, j)\, c = \text{update}\, (\lambda i, f_i c)\, i\, (b c)\, j$$
LinearMap.single_eq_pi_diag theorem
(i : ι) : single R φ i = pi (diag i)
Full source 
theorem single_eq_pi_diag (i : ι) : single R φ i = pi (diag i) := by
  ext x j
  convert (update_apply 0 x i j _).symm
  rfl
Single Map as Composition of Diagonal and Projection
Informal description
For any index $i$ in the index set $\iota$, the linear map $\text{single}_i : \phi_i \to \prod_{j \in \iota} \phi_j$ is equal to the composition of the diagonal map $\text{diag}_i : \phi_i \to \prod_{j \in \iota} \phi_j$ (which maps $x \in \phi_i$ to $(x)_{j \in \iota}$) with the projection map $\pi : \prod_{j \in \iota} \phi_j \to \phi_i$. In symbols: $$\text{single}_i = \pi \circ \text{diag}_i$$
LinearMap.ker_single theorem
(i : ι) : ker (single R φ i) = ⊥
Full source 
theorem ker_single (i : ι) : ker (single R φ i) = ⊥ :=
  ker_eq_bot_of_injective <| Pi.single_injective _ _
Trivial Kernel of Linear Single Map
Informal description
For any index $i$ in the decidable type $\iota$, the kernel of the linear map $\text{single}_i : \phi_i \to \bigoplus_{j \in \iota} \phi_j$ is trivial, i.e., $\ker(\text{single}_i) = \{0\}$.
LinearMap.proj_comp_single theorem
(i j : ι) : (proj i).comp (single R φ j) = diag j i
Full source 
theorem proj_comp_single (i j : ι) : (proj i).comp (single R φ j) = diag j i := by
  rw [single_eq_pi_diag, proj_pi]
Composition Identity: $\text{proj}_i \circ \text{single}_j = \text{diag}_{j,i}$
Informal description
For any indices $i$ and $j$ in the index set $\iota$, the composition of the projection map $\text{proj}_i$ with the single map $\text{single}_j$ equals the diagonal map $\text{diag}_{j,i}$. In symbols: $$ \text{proj}_i \circ \text{single}_j = \text{diag}_{j,i} $$
LinearMap.pi_apply_eq_sum_univ theorem
[Fintype ι] (f : (ι → R) →ₗ[R] M₂) (x : ι → R) : f x = ∑ i, x i • f fun j => if i = j then 1 else 0
Full source 
/-- A linear map `f` applied to `x : ι → R` can be computed using the image under `f` of elements
of the canonical basis. -/
theorem pi_apply_eq_sum_univ [Fintype ι] (f : (ι → R) →ₗ[R] M₂) (x : ι → R) :
    f x = ∑ i, x i • f fun j => if i = j then 1 else 0 := by
  conv_lhs => rw [pi_eq_sum_univ x, map_sum]
  refine Finset.sum_congr rfl (fun _ _ => ?_)
  rw [map_smul]
Linear map evaluation via basis expansion
Informal description
Let $R$ be a ring, $\iota$ a finite type, and $M₂$ an $R$-module. For any linear map $f \colon (\iota \to R) \to M₂$ and any vector $x \in \iota \to R$, the value of $f$ at $x$ can be expressed as: \[ f(x) = \sum_{i \in \iota} x_i \cdot f(\delta_i) \] where $\delta_i \colon \iota \to R$ is the function defined by $\delta_i(j) = 1$ if $i = j$ and $0$ otherwise.
Submodule.pi definition
(I : Set ι) (p : (i : ι) → Submodule R (φ i)) : Submodule R ((i : ι) → φ i)
Full source 
/-- 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`. -/
@[simps]
def pi (I : Set ι) (p : (i : ι) → Submodule R (φ i)) : Submodule R ((i : ι) → φ i) where
  carrier := Set.pi I fun i => p i
  zero_mem' i _ := (p i).zero_mem
  add_mem' {_ _} hx hy i hi := (p i).add_mem (hx i hi) (hy i hi)
  smul_mem' c _ hx i hi := (p i).smul_mem c (hx i hi)
Submodule of functions with restricted values
Informal description
For an index set $I$ and a family of submodules $p_i \subseteq \varphi_i$ for each $i \in \iota$, the submodule $\pi_I p$ consists of all functions $f \colon \iota \to \bigcup_i \varphi_i$ such that $f(i) \in p_i$ for every $i \in I$.
Submodule.mem_pi theorem
: x ∈ pi I p ↔ ∀ i ∈ I, x i ∈ p i
Full source 
@[simp]
theorem mem_pi : x ∈ pi I px ∈ pi I p ↔ ∀ i ∈ I, x i ∈ p i :=
  Iff.rfl
Characterization of Membership in Pi Submodule
Informal description
An element $x$ belongs to the submodule $\pi_I p$ if and only if for every index $i \in I$, the component $x_i$ belongs to the submodule $p_i$.
Submodule.pi_empty theorem
(p : (i : ι) → Submodule R (φ i)) : pi ∅ p = ⊤
Full source 
@[simp]
theorem pi_empty (p : (i : ι) → Submodule R (φ i)) : pi ∅ p = ⊤ :=
  SetLike.coe_injective <| Set.empty_pi _
Submodule of Empty Index Set is Entire Space
Informal description
For any family of submodules $p_i \subseteq \varphi_i$ indexed by $i \in \iota$, the submodule of functions restricted to the empty index set is the entire space, i.e., $\pi_\emptyset p = \top$.
Submodule.pi_top theorem
(s : Set ι) : (pi s fun i : ι ↦ (⊤ : Submodule R (φ i))) = ⊤
Full source 
@[simp]
theorem pi_top (s : Set ι) : (pi s fun i : ι ↦ (⊤ : Submodule R (φ i))) = ⊤ :=
  SetLike.coe_injective <| Set.pi_univ _
Top Submodule Characterization for Function Space with Unrestricted Components
Informal description
For any set $s$ of indices, the submodule of functions $\pi_s$ where each component is in the top submodule $\top$ of $\varphi_i$ is equal to the top submodule $\top$ of the function space $\prod_{i \in \iota} \varphi_i$.
Submodule.pi_univ_bot theorem
: (pi Set.univ fun i : ι ↦ (⊥ : Submodule R (φ i))) = ⊥
Full source 
@[simp]
theorem pi_univ_bot : (pi Set.univ fun i : ι ↦ (⊥ : Submodule R (φ i))) = ⊥ :=
  le_bot_iff.mp fun _ h ↦ funext fun i ↦ h i trivial
Bottom Submodule Characterization for Function Space with Trivial Components
Informal description
For any family of submodules $\varphi_i$ indexed by $i \in \iota$, the submodule of functions restricted to the entire index set $\iota$ where each component is the bottom submodule $\bot$ is equal to the bottom submodule $\bot$ of the function space $\prod_{i \in \iota} \varphi_i$.
Submodule.pi_mono theorem
{s : Set ι} (h : ∀ i ∈ s, p i ≤ q i) : pi s p ≤ pi s q
Full source 
@[gcongr]
theorem pi_mono {s : Set ι} (h : ∀ i ∈ s, p i ≤ q i) : pi s p ≤ pi s q :=
  Set.pi_mono h
Monotonicity of Submodule Restriction in Pi Types
Informal description
For any subset $s$ of the index set $\iota$, if for every $i \in s$ the submodule $p_i$ is contained in $q_i$, then the submodule $\pi_s p$ of functions with values in $p_i$ for $i \in s$ is contained in the submodule $\pi_s q$ of functions with values in $q_i$ for $i \in s$.
Submodule.biInf_comap_proj theorem
: ⨅ i ∈ I, comap (proj i : ((i : ι) → φ i) →ₗ[R] φ i) (p i) = pi I p
Full source 
theorem biInf_comap_proj :
    ⨅ i ∈ I, comap (proj i : ((i : ι) → φ i) →ₗ[R] φ i) (p i) = pi I p := by
  ext x
  simp
Infimum of Precomposed Projections Equals Restricted Pi Submodule
Informal description
For any subset $I$ of the index set $\iota$, the infimum of the submodules obtained by precomposing the projection maps $\text{proj}_i \colon \prod_{j \in \iota} \phi_j \to \phi_i$ with the submodules $p_i$ is equal to the submodule of all functions $f \colon \iota \to \bigcup_{j \in \iota} \phi_j$ such that $f(i) \in p_i$ for every $i \in I$. In other words, \[ \bigsqcap_{i \in I} \text{comap}(\text{proj}_i, p_i) = \pi_I p. \]
Submodule.iInf_comap_proj theorem
: ⨅ i, comap (proj i : ((i : ι) → φ i) →ₗ[R] φ i) (p i) = pi Set.univ p
Full source 
theorem iInf_comap_proj :
    ⨅ i, comap (proj i : ((i : ι) → φ i) →ₗ[R] φ i) (p i) = pi Set.univ p := by
  ext x
  simp
Infimum of Precomposed Projections Equals Universal Pi Submodule
Informal description
The infimum of the submodules obtained by precomposing the projection maps $\text{proj}_i \colon \prod_{i \in \iota} \phi_i \to \phi_i$ with the submodules $p_i$ is equal to the submodule of all functions $f \colon \iota \to \bigcup_i \phi_i$ such that $f(i) \in p_i$ for every $i \in \iota$. In other words, \[ \bigsqcap_i \text{comap}(\text{proj}_i, p_i) = \pi_{\text{univ}} p. \]
Submodule.le_comap_single_pi theorem
[DecidableEq ι] (p : (i : ι) → Submodule R (φ i)) {I i} : p i ≤ Submodule.comap (LinearMap.single R φ i : φ i →ₗ[R] _) (Submodule.pi I p)
Full source 
theorem le_comap_single_pi [DecidableEq ι] (p : (i : ι) → Submodule R (φ i)) {I i} :
    p i ≤ Submodule.comap (LinearMap.single R φ i : φ i →ₗ[R] _) (Submodule.pi I p) := by
  intro x hx
  rw [Submodule.mem_comap, Submodule.mem_pi]
  rintro j -
  rcases eq_or_ne j i with rfl | hne <;> simp [*]
Inclusion of Submodule in Preimage of Pi Submodule under Single Map
Informal description
Let $\iota$ be a decidable index type, $R$ a ring, and $(\varphi_i)_{i \in \iota}$ a family of $R$-modules. For any family of submodules $(p_i)_{i \in \iota}$ where $p_i \subseteq \varphi_i$, any index set $I \subseteq \iota$, and any index $i \in \iota$, the submodule $p_i$ is contained in the preimage of the submodule $\pi_I p$ under the linear map $\text{single}_i : \varphi_i \to \bigoplus_{j \in \iota} \varphi_j$. In other words, for any $x \in p_i$, the element $\text{single}_i(x)$ belongs to $\pi_I p$.
Submodule.iSup_map_single_le theorem
[DecidableEq ι] : ⨆ i, map (LinearMap.single R φ i) (p i) ≤ pi I p
Full source 
theorem iSup_map_single_le [DecidableEq ι] :
    ⨆ i, map (LinearMap.single R φ i) (p i) ≤ pi I p :=
  iSup_le fun _ => map_le_iff_le_comap.mpr <| le_comap_single_pi _
Supremum of Images under Single Maps is Contained in Pi Submodule
Informal description
Let $\iota$ be a decidable index type, $R$ a ring, and $(\varphi_i)_{i \in \iota}$ a family of $R$-modules. For any family of submodules $(p_i)_{i \in \iota}$ where $p_i \subseteq \varphi_i$ and any index set $I \subseteq \iota$, the supremum of the images of $p_i$ under the linear maps $\text{single}_i : \varphi_i \to \bigoplus_{j \in \iota} \varphi_j$ is contained in the submodule $\pi_I p$ of functions $f \colon \iota \to \bigcup_i \varphi_i$ such that $f(i) \in p_i$ for every $i \in I$. In other words, \[ \bigsqcup_i \text{map}(\text{single}_i, p_i) \subseteq \pi_I p. \]
Submodule.iSup_map_single theorem
[DecidableEq ι] [Finite ι] : ⨆ i, map (LinearMap.single R φ i : φ i →ₗ[R] (i : ι) → φ i) (p i) = pi Set.univ p
Full source 
theorem iSup_map_single [DecidableEq ι] [Finite ι] :
    ⨆ i, map (LinearMap.single R φ i : φ i →ₗ[R] (i : ι) → φ i) (p i) = pi Set.univ p := by
  cases nonempty_fintype ι
  refine iSup_map_single_le.antisymm fun x hx => ?_
  rw [← Finset.univ_sum_single x]
  exact sum_mem_iSup fun i => mem_map_of_mem (hx i trivial)
Equality of Supremum of Single Maps and Full Pi Submodule for Finite Index Sets
Informal description
Let $\iota$ be a finite decidable index type, $R$ a ring, and $(\varphi_i)_{i \in \iota}$ a family of $R$-modules. For any family of submodules $(p_i)_{i \in \iota}$ where $p_i \subseteq \varphi_i$, the supremum of the images of $p_i$ under the linear maps $\text{single}_i : \varphi_i \to \bigoplus_{j \in \iota} \varphi_j$ equals the submodule $\pi_{\text{univ}} p$ of all functions $f \colon \iota \to \bigcup_i \varphi_i$ such that $f(i) \in p_i$ for every $i \in \iota$. In other words, \[ \bigsqcup_i \text{map}(\text{single}_i, p_i) = \pi_{\text{univ}} p. \]
LinearEquiv.piCongrRight definition
(e : (i : ι) → φ i ≃ₗ[R] ψ i) : ((i : ι) → φ i) ≃ₗ[R] (i : ι) → ψ i
Full source 
/-- Combine a family of linear equivalences into a linear equivalence of `pi`-types.

This is `Equiv.piCongrRight` as a `LinearEquiv` -/
def piCongrRight (e : (i : ι) → φ i ≃ₗ[R] ψ i) : ((i : ι) → φ i) ≃ₗ[R] (i : ι) → ψ i :=
  { AddEquiv.piCongrRight fun j => (e j).toAddEquiv with
    toFun := fun f i => e i (f i)
    invFun := fun f i => (e i).symm (f i)
    map_smul' := fun c f => by ext; simp }
Linear equivalence of product spaces via component-wise linear equivalences
Informal description
Given a family of linear equivalences \( e_i : \phi_i \simeq \psi_i \) for each \( i \) in an index set \( \iota \), the function constructs a linear equivalence between the product spaces \( \prod_{i \in \iota} \phi_i \) and \( \prod_{i \in \iota} \psi_i \). The equivalence maps a function \( f \) in the product space to the function \( \lambda i, e_i (f i) \), and its inverse maps \( g \) to \( \lambda i, e_i^{-1} (g i) \).
LinearEquiv.piCongrRight_apply theorem
(e : (i : ι) → φ i ≃ₗ[R] ψ i) (f i) : piCongrRight e f i = e i (f i)
Full source 
@[simp]
theorem piCongrRight_apply (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f i) :
    piCongrRight e f i = e i (f i) := rfl
Component-wise Application of Linear Equivalence on Product Space
Informal description
Given a family of linear equivalences \( e_i : \phi_i \simeq \psi_i \) for each \( i \) in an index set \( \iota \), the linear equivalence \(\text{piCongrRight } e\) maps a function \( f \in \prod_{i \in \iota} \phi_i \) to the function \( (\text{piCongrRight } e) f \in \prod_{i \in \iota} \psi_i \) such that for each \( i \in \iota \), the \(i\)-th component satisfies \( (\text{piCongrRight } e) f \, i = e_i (f \, i) \).
LinearEquiv.piCongrRight_refl theorem
: (piCongrRight fun j => refl R (φ j)) = refl _ _
Full source 
@[simp]
theorem piCongrRight_refl : (piCongrRight fun j => refl R (φ j)) = refl _ _ :=
  rfl
Identity Component-wise Linear Equivalence Yields Identity on Product Space
Informal description
The linear equivalence constructed by applying the identity linear equivalence to each component of a product space is equal to the identity linear equivalence on the entire product space. That is, for any family of modules $\phi_j$ over a ring $R$, we have: \[ \text{piCongrRight} (\lambda j, \text{refl}_R (\phi_j)) = \text{refl}_{(\Pi j, \phi_j)} \]
LinearEquiv.piCongrRight_symm theorem
(e : (i : ι) → φ i ≃ₗ[R] ψ i) : (piCongrRight e).symm = piCongrRight fun i => (e i).symm
Full source 
@[simp]
theorem piCongrRight_symm (e : (i : ι) → φ i ≃ₗ[R] ψ i) :
    (piCongrRight e).symm = piCongrRight fun i => (e i).symm :=
  rfl
Inverse of Component-wise Linear Equivalence on Product Space
Informal description
Given a family of linear equivalences \( e_i : \phi_i \simeq \psi_i \) for each \( i \) in an index set \( \iota \), the inverse of the linear equivalence \(\text{piCongrRight } e\) is equal to the linear equivalence obtained by taking the inverse of each component equivalence \( e_i \). That is, \[ (\text{piCongrRight } e)^{-1} = \text{piCongrRight } (\lambda i, (e_i)^{-1}). \]
LinearEquiv.piCongrRight_trans theorem
(e : (i : ι) → φ i ≃ₗ[R] ψ i) (f : (i : ι) → ψ i ≃ₗ[R] χ i) : (piCongrRight e).trans (piCongrRight f) = piCongrRight fun i => (e i).trans (f i)
Full source 
@[simp]
theorem piCongrRight_trans (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f : (i : ι) → ψ i ≃ₗ[R] χ i) :
    (piCongrRight e).trans (piCongrRight f) = piCongrRight fun i => (e i).trans (f i) :=
  rfl
Composition of Product Space Linear Equivalences via Component-wise Composition
Informal description
Given a family of linear equivalences \( e_i : \phi_i \simeq \psi_i \) and another family \( f_i : \psi_i \simeq \chi_i \) for each \( i \) in an index set \( \iota \), the composition of the product space equivalences \( \prod_{i \in \iota} \phi_i \simeq \prod_{i \in \iota} \psi_i \) and \( \prod_{i \in \iota} \psi_i \simeq \prod_{i \in \iota} \chi_i \) is equal to the product space equivalence \( \prod_{i \in \iota} \phi_i \simeq \prod_{i \in \iota} \chi_i \) obtained by composing each component equivalence \( e_i \) with \( f_i \).
LinearEquiv.piCongrLeft' definition
(e : ι ≃ ι') : ((i' : ι) → φ i') ≃ₗ[R] (i : ι') → φ <| e.symm i
Full source 
/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft'` as a `LinearEquiv`. -/
@[simps +simpRhs]
def piCongrLeft' (e : ι ≃ ι') : ((i' : ι) → φ i') ≃ₗ[R] (i : ι') → φ <| e.symm i :=
  { Equiv.piCongrLeft' φ e with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }
Linear equivalence of dependent functions under index equivalence
Informal description
Given a ring $R$, an index type $\iota$, an index type $\iota'$, and for each $i \in \iota$ an $R$-module $\varphi_i$, the linear equivalence `LinearEquiv.piCongrLeft'` maps between the space of dependent functions $\Pi_{i' \in \iota} \varphi_{i'}$ and the space of dependent functions $\Pi_{i \in \iota'} \varphi_{e^{-1}(i)}$, where $e : \iota \simeq \iota'$ is an equivalence between the index types. This equivalence preserves addition and scalar multiplication.
LinearEquiv.piCongrLeft definition
(e : ι' ≃ ι) : ((i' : ι') → φ (e i')) ≃ₗ[R] (i : ι) → φ i
Full source 
/-- Transporting dependent functions through an equivalence of the base,
expressed as a "simplification".

This is `Equiv.piCongrLeft` as a `LinearEquiv` -/
def piCongrLeft (e : ι' ≃ ι) : ((i' : ι') → φ (e i')) ≃ₗ[R] (i : ι) → φ i :=
  (piCongrLeft' R φ e.symm).symm
Linear equivalence of dependent functions under index equivalence (reverse direction)
Informal description
Given a ring $R$, an index type $\iota$, an index type $\iota'$, and for each $i \in \iota$ an $R$-module $\varphi_i$, the linear equivalence `LinearEquiv.piCongrLeft` maps between the space of dependent functions $\Pi_{i' \in \iota'} \varphi_{e(i')}$ and the space of dependent functions $\Pi_{i \in \iota} \varphi_i$, where $e : \iota' \simeq \iota$ is an equivalence between the index types. This equivalence preserves addition and scalar multiplication.
LinearEquiv.piCurry definition
{ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*) [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)] : (Π i : Sigma κ, α i.1 i.2) ≃ₗ[R] Π i j, α i j
Full source 
/-- `Equiv.piCurry` as a `LinearEquiv`. -/
def piCurry {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*)
    [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)] :
    (Π i : Sigma κ, α i.1 i.2) ≃ₗ[R] Π i j, α i j where
  __ := Equiv.piCurry α
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
Linear equivalence between dependent product and doubly-indexed functions
Informal description
Given a ring $R$, an index type $\iota$, and for each $i \in \iota$ an index type $\kappa_i$, and for each $i \in \iota$ and $k \in \kappa_i$ an $R$-module $\alpha_{i,k}$, the linear equivalence `LinearEquiv.piCurry` maps between the space of functions $\Pi_{(i,k) \in \Sigma \kappa} \alpha_{i,k}$ (where $\Sigma \kappa$ is the dependent sum) and the space of doubly-indexed functions $\Pi_{i \in \iota} \Pi_{k \in \kappa_i} \alpha_{i,k}$. This equivalence preserves addition and scalar multiplication.
LinearEquiv.piCurry_apply theorem
{ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*) [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)] (f : ∀ x : Σ i, κ i, α x.1 x.2) : piCurry R α f = Sigma.curry f
Full source 
@[simp] theorem piCurry_apply {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*)
    [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)]
    (f : ∀ x : Σ i, κ i, α x.1 x.2) :
    piCurry R α f = Sigma.curry f :=
  rfl
Application of Linear Currying Equivalence for Doubly-Indexed Modules
Informal description
Let $R$ be a ring, $\iota$ an index type, and for each $i \in \iota$, let $\kappa_i$ be another index type. For each $i \in \iota$ and $k \in \kappa_i$, let $\alpha_{i,k}$ be an $R$-module. Given a function $f : \prod_{(i,k) \in \Sigma \kappa} \alpha_{i,k}$ (where $\Sigma \kappa$ is the dependent sum type), the linear equivalence `piCurry` maps $f$ to the curried function $\mathrm{curry}(f) : \prod_{i \in \iota} \prod_{k \in \kappa_i} \alpha_{i,k}$.
LinearEquiv.piCurry_symm_apply theorem
{ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*) [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)] (f : ∀ a b, α a b) : (piCurry R α).symm f = Sigma.uncurry f
Full source 
@[simp] theorem piCurry_symm_apply {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*)
    [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)]
    (f : ∀ a b, α a b) :
    (piCurry R α).symm f = Sigma.uncurry f :=
  rfl
Inverse of Linear Currying Equivalence for Doubly-Indexed Modules
Informal description
Let $R$ be a ring, $\iota$ an index type, and for each $i \in \iota$, let $\kappa_i$ be another index type. For each $i \in \iota$ and $k \in \kappa_i$, let $\alpha_{i,k}$ be an $R$-module. Given a doubly-indexed function $f : \prod_{i \in \iota} \prod_{k \in \kappa_i} \alpha_{i,k}$, the inverse of the linear equivalence `piCurry` maps $f$ to the function $\Sigma.\text{uncurry}\, f$ on the dependent sum type $\Sigma \kappa$, where $\Sigma.\text{uncurry}\, f (x) = f x.1 x.2$ for $x \in \Sigma \kappa$.
LinearEquiv.piOptionEquivProd definition
{ι : Type*} {M : Option ι → Type*} [(i : Option ι) → AddCommMonoid (M i)] [(i : Option ι) → Module R (M i)] : ((i : Option ι) → M i) ≃ₗ[R] M none × ((i : ι) → M (some i))
Full source 
/-- This is `Equiv.piOptionEquivProd` as a `LinearEquiv` -/
def piOptionEquivProd {ι : Type*} {M : Option ι → Type*} [(i : Option ι) → AddCommMonoid (M i)]
    [(i : Option ι) → Module R (M i)] :
    ((i : Option ι) → M i) ≃ₗ[R] M none × ((i : ι) → M (some i)) :=
  { Equiv.piOptionEquivProd with
    map_add' := by simp [funext_iff]
    map_smul' := by simp [funext_iff] }
Linear equivalence between pi types over `Option ι` and product of modules
Informal description
Given a type `ι`, a family of modules `M : Option ι → Type*` indexed by `Option ι`, and a ring `R` such that each `M i` is an `R`-module, the linear equivalence `LinearEquiv.piOptionEquivProd` maps a function `f : (i : Option ι) → M i` to the pair `(f none, λ i, f (some i))`. This is the linear algebra version of the bijection `Equiv.piOptionEquivProd`.
LinearEquiv.piRing definition
: ((ι → R) →ₗ[R] M) ≃ₗ[S] ι → M
Full source 
/-- 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]. -/
def piRing : ((ι → R) →ₗ[R] M) ≃ₗ[S] ι → M :=
  (LinearMap.lsum R (fun _ : ι => R) S).symm.trans
    (piCongrRight fun _ => LinearMap.ringLmapEquivSelf R S M)
Linear equivalence between linear functionals on $R^\iota$ and $\iota$-indexed families in $M$
Informal description
Given a finite index set $\iota$, a commutative ring $R$, and an $R$-module $M$ that is also an $S$-module with commuting $R$ and $S$ actions, the linear equivalence `LinearEquiv.piRing` establishes an $S$-linear isomorphism between the space of $R$-linear maps from $\iota \to R$ to $M$ and the space of functions $\iota \to M$. Specifically: - The forward map takes a linear map $f : (\iota \to R) \to M$ to the function $\lambda i, f(\text{single}_i(1))$, where $\text{single}_i(1)$ is the function that is $1$ at $i$ and $0$ elsewhere. - The inverse map takes a function $g : \iota \to M$ to the linear map $\lambda h, \sum_{i} h(i) \cdot g(i)$.
LinearEquiv.piRing_apply theorem
(f : (ι → R) →ₗ[R] M) (i : ι) : piRing R M ι S f i = f (Pi.single i 1)
Full source 
@[simp]
theorem piRing_apply (f : (ι → R) →ₗ[R] M) (i : ι) : piRing R M ι S f i = f (Pi.single i 1) :=
  rfl
Evaluation of Linear Equivalence $\text{piRing}$ at Basis Vector $\text{single}_i(1)$
Informal description
For any $R$-linear map $f \colon (\iota \to R) \to M$ and any index $i \in \iota$, the $i$-th component of the image of $f$ under the linear equivalence $\text{piRing}$ is equal to $f$ evaluated at the function $\text{single}_i(1)$, where $\text{single}_i(1)$ is the function that takes value $1$ at $i$ and $0$ elsewhere. In symbols: \[ \text{piRing}(f)(i) = f(\text{single}_i(1)) \]
LinearEquiv.piRing_symm_apply theorem
(f : ι → M) (g : ι → R) : (piRing R M ι S).symm f g = ∑ i, g i • f i
Full source 
@[simp]
theorem piRing_symm_apply (f : ι → M) (g : ι → R) : (piRing R M ι S).symm f g = ∑ i, g i • f i := by
  simp [piRing, LinearMap.lsum_apply]
Inverse of $\text{piRing}$ as Sum of Scalar Multiples
Informal description
For any function $f \colon \iota \to M$ and any function $g \colon \iota \to R$, the inverse of the linear equivalence $\text{piRing}_{R,M,\iota,S}$ applied to $f$ and evaluated at $g$ is equal to the sum $\sum_{i \in \iota} g(i) \cdot f(i)$, where $\cdot$ denotes the scalar multiplication in the $R$-module $M$.
LinearEquiv.sumArrowLequivProdArrow definition
(α β R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] : (α ⊕ β → M) ≃ₗ[R] (α → M) × (β → M)
Full source 
/-- `Equiv.sumArrowEquivProdArrow` as a linear equivalence.
-/
def sumArrowLequivProdArrow (α β R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] :
    (α ⊕ β → M) ≃ₗ[R] (α → M) × (β → M) :=
  { Equiv.sumArrowEquivProdArrow α β
      M with
    map_add' := by
      intro f g
      ext <;> rfl
    map_smul' := by
      intro r f
      ext <;> rfl }
Linear equivalence between functions on a sum type and product of function spaces
Informal description
Given types $\alpha$ and $\beta$, a semiring $R$, and an $R$-module $M$, the linear equivalence $\text{sumArrowLequivProdArrow}$ establishes an isomorphism between the space of functions from the disjoint union $\alpha \oplus \beta$ to $M$ and the product space $(\alpha \to M) \times (\beta \to M)$. This equivalence preserves addition and scalar multiplication, making it a linear isomorphism.
LinearEquiv.sumArrowLequivProdArrow_apply_fst theorem
{α β} (f : α ⊕ β → M) (a : α) : (sumArrowLequivProdArrow α β R M f).1 a = f (Sum.inl a)
Full source 
@[simp]
theorem sumArrowLequivProdArrow_apply_fst {α β} (f : α ⊕ β → M) (a : α) :
    (sumArrowLequivProdArrow α β R M f).1 a = f (Sum.inl a) :=
  rfl
Evaluation of First Component in Linear Equivalence for Sum Types
Informal description
For any types $\alpha$ and $\beta$, a semiring $R$, and an $R$-module $M$, given a function $f \colon \alpha \oplus \beta \to M$ and an element $a \in \alpha$, the first component of the linear equivalence $\text{sumArrowLequivProdArrow}_{\alpha,\beta,R,M}$ applied to $f$, evaluated at $a$, equals $f$ evaluated at the left injection $\text{Sum.inl}(a)$. In other words, $(\text{sumArrowLequivProdArrow}_{\alpha,\beta,R,M}(f))_1(a) = f(\text{inl}(a))$.
LinearEquiv.sumArrowLequivProdArrow_apply_snd theorem
{α β} (f : α ⊕ β → M) (b : β) : (sumArrowLequivProdArrow α β R M f).2 b = f (Sum.inr b)
Full source 
@[simp]
theorem sumArrowLequivProdArrow_apply_snd {α β} (f : α ⊕ β → M) (b : β) :
    (sumArrowLequivProdArrow α β R M f).2 b = f (Sum.inr b) :=
  rfl
Evaluation of Second Component in Linear Equivalence for Sum Types
Informal description
For any types $\alpha$ and $\beta$, a semiring $R$, and an $R$-module $M$, given a function $f \colon \alpha \oplus \beta \to M$ and an element $b \in \beta$, the second component of the linear equivalence $\text{sumArrowLequivProdArrow}_{\alpha,\beta,R,M}$ applied to $f$, evaluated at $b$, equals $f$ evaluated at the right injection $\text{Sum.inr}(b)$. In other words, $(\text{sumArrowLequivProdArrow}_{\alpha,\beta,R,M}(f))_2(b) = f(\text{inr}(b))$.
LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl theorem
{α β} (f : α → M) (g : β → M) (a : α) : ((sumArrowLequivProdArrow α β R M).symm (f, g)) (Sum.inl a) = f a
Full source 
@[simp]
theorem sumArrowLequivProdArrow_symm_apply_inl {α β} (f : α → M) (g : β → M) (a : α) :
    ((sumArrowLequivProdArrow α β R M).symm (f, g)) (Sum.inl a) = f a :=
  rfl
Evaluation of Inverse Linear Equivalence on Left Injection
Informal description
Let $\alpha$ and $\beta$ be types, $R$ a semiring, and $M$ an $R$-module. For any functions $f \colon \alpha \to M$ and $g \colon \beta \to M$, and any element $a \in \alpha$, the inverse of the linear equivalence $\text{sumArrowLequivProdArrow}_{\alpha,\beta,R,M}$ applied to $(f, g)$ and evaluated at $\text{Sum.inl}(a)$ equals $f(a)$. In other words, $(\text{sumArrowLequivProdArrow}_{\alpha,\beta,R,M}^{-1}(f, g))(\text{inl}(a)) = f(a)$.
LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr theorem
{α β} (f : α → M) (g : β → M) (b : β) : ((sumArrowLequivProdArrow α β R M).symm (f, g)) (Sum.inr b) = g b
Full source 
@[simp]
theorem sumArrowLequivProdArrow_symm_apply_inr {α β} (f : α → M) (g : β → M) (b : β) :
    ((sumArrowLequivProdArrow α β R M).symm (f, g)) (Sum.inr b) = g b :=
  rfl
Evaluation of Inverse Linear Equivalence on Right Injection
Informal description
Let $\alpha$ and $\beta$ be types, $R$ a semiring, and $M$ an $R$-module. For any functions $f \colon \alpha \to M$ and $g \colon \beta \to M$, and any element $b \in \beta$, the inverse of the linear equivalence $\text{sumArrowLequivProdArrow}$ applied to $(f, g)$ and evaluated at $\text{Sum.inr}(b)$ equals $g(b)$. In other words, $(\text{sumArrowLequivProdArrow}_{\alpha,\beta,R,M}^{-1}(f, g))(\text{inr}(b)) = g(b)$.
LinearEquiv.funUnique definition
(ι R M : Type*) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] : (ι → M) ≃ₗ[R] M
Full source 
/-- If `ι` has a unique element, then `ι → M` is linearly equivalent to `M`. -/
@[simps +simpRhs -fullyApplied symm_apply]
def funUnique (ι R M : Type*) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] :
    (ι → M) ≃ₗ[R] M :=
  { Equiv.funUnique ι M with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }
Linear equivalence between function space and module for unique domain
Informal description
Given a type $\iota$ with a unique element, a semiring $R$, and an $R$-module $M$, the space of functions $\iota \to M$ is linearly equivalent to $M$ itself. The equivalence is given by evaluating at the unique element of $\iota$.
LinearEquiv.funUnique_apply theorem
(ι R M : Type*) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] : (funUnique ι R M : (ι → M) → M) = eval default
Full source 
@[simp]
theorem funUnique_apply (ι R M : Type*) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] :
    (funUnique ι R M : (ι → M) → M) = eval default := rfl
Evaluation of Linear Equivalence for Unique Domain at Default Element
Informal description
For a type $\iota$ with a unique element, a semiring $R$, and an $R$-module $M$, the linear equivalence `funUnique` from the function space $\iota \to M$ to $M$ is given by evaluation at the default (unique) element of $\iota$. That is, for any $f : \iota \to M$, we have $\text{funUnique}(f) = f(\text{default})$.
LinearEquiv.piFinTwo definition
(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
Full source 
/-- Linear equivalence between dependent functions `(i : Fin 2) → M i` and `M 0 × M 1`. -/
@[simps +simpRhs -fullyApplied symm_apply]
def piFinTwo (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 :=
  { piFinTwoEquiv M with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }
Linear equivalence between dependent functions on `Fin 2` and their product
Informal description
The linear equivalence between the space of dependent functions `(i : Fin 2) → M i` and the product space `M 0 × M 1`, where each `M i` is an `R`-module. This equivalence maps a function `f` to the pair `(f 0, f 1)` and preserves addition and scalar multiplication.
LinearEquiv.piFinTwo_apply theorem
(M : Fin 2 → Type v) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] : (piFinTwo R M : ((i : Fin 2) → M i) → M 0 × M 1) = fun f => (f 0, f 1)
Full source 
@[simp]
theorem piFinTwo_apply (M : Fin 2 → Type v)
    [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] :
    (piFinTwo R M : ((i : Fin 2) → M i) → M 0 × M 1) = fun f => (f 0, f 1) := rfl
Linear equivalence $\text{piFinTwo}$ maps a function to its evaluations at $0$ and $1$
Informal description
For a family of $R$-modules $M_i$ indexed by $i \in \text{Fin } 2$ (i.e., $i = 0,1$), the linear equivalence $\text{piFinTwo}$ maps a function $f \colon (i : \text{Fin } 2) \to M_i$ to the pair $(f(0), f(1)) \in M_0 \times M_1$.
LinearEquiv.finTwoArrow definition
: (Fin 2 → M) ≃ₗ[R] M × M
Full source 
/-- Linear equivalence between vectors in `M² = Fin 2 → M` and `M × M`. -/
@[simps! -fullyApplied]
def finTwoArrow : (Fin 2 → M) ≃ₗ[R] M × M :=
  { finTwoArrowEquiv M, piFinTwo R fun _ => M with }
Linear equivalence between `Fin 2 → M` and `M × M`
Informal description
The linear equivalence between the space of functions from the two-element type `Fin 2` to an `R`-module `M` and the product module `M × M`. This equivalence maps a function `f` to the pair `(f 0, f 1)` and preserves addition and scalar multiplication.
Function.ExtendByZero.linearMap definition
: (ι → R) →ₗ[R] η → R
Full source 
/-- `Function.extend s f 0` as a bundled linear map. -/
@[simps]
noncomputable def Function.ExtendByZero.linearMap : (ι → R) →ₗ[R] η → R :=
  { Function.ExtendByZero.hom R s with
    toFun := fun f => Function.extend s f 0
    map_smul' := fun r f => by simpa using Function.extend_smul r s f 0 }
Extension by zero linear map
Informal description
The linear map that extends a function \( f \colon \iota \to R \) by zero to a function \( \eta \to R \). Specifically, for any \( x \in \eta \), if \( x \) is in the image of \( s \colon \iota \to \eta \), then the output is \( f(s^{-1}(x)) \); otherwise, the output is \( 0 \).
Fin.consLinearEquiv definition
{n : ℕ} (M : Fin n.succ → Type*) [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] : (M 0 × Π i, M (Fin.succ i)) ≃ₗ[R] (Π i, M i)
Full source 
/-- `Fin.consEquiv` as a continuous linear equivalence. -/
@[simps]
def Fin.consLinearEquiv
    {n : ℕ} (M : Fin n.succ → Type*) [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] :
    (M 0 × Π i, M (Fin.succ i)) ≃ₗ[R] (Π i, M i) where
  __ := Fin.consEquiv M
  map_add' x y := funext <| Fin.cases rfl (by simp)
  map_smul' c x := funext <| Fin.cases rfl (by simp)
Linear equivalence between product and function modules via cons construction
Informal description
For a natural number $n$ and a family of modules $M_i$ indexed by $i \in \{0, \dots, n\}$ over a semiring $R$, the linear equivalence $\text{Fin.consLinearEquiv}$ establishes an isomorphism between the product module $M_0 \times \prod_{i} M_{i+1}$ and the module of functions $\prod_{i} M_i$. This equivalence is defined using the constructor $\text{Fin.consEquiv}$ and preserves addition and scalar multiplication.
LinearMap.vecEmpty definition
: M →ₗ[R] Fin 0 → M₃
Full source 
/-- The linear map defeq to `Matrix.vecEmpty` -/
def LinearMap.vecEmpty : M →ₗ[R] Fin 0 → M₃ where
  toFun _ := Matrix.vecEmpty
  map_add' _ _ := Subsingleton.elim _ _
  map_smul' _ _ := Subsingleton.elim _ _
Empty vector linear map
Informal description
The linear map from a module $M$ to the trivial module $\text{Fin}\ 0 \to M₃$, which is definitionally equal to the empty vector $\text{Matrix.vecEmpty}$. For any element $m \in M$, the application of this map to $m$ yields the empty vector $[]$.
LinearMap.vecEmpty_apply theorem
(m : M) : (LinearMap.vecEmpty : M →ₗ[R] Fin 0 → M₃) m = ![]
Full source 
@[simp]
theorem LinearMap.vecEmpty_apply (m : M) : (LinearMap.vecEmpty : M →ₗ[R] Fin 0 → M₃) m = ![] :=
  rfl
Empty Vector Linear Map Yields Empty Vector: $\text{vecEmpty}\ m = []$
Informal description
For any element $m$ in a module $M$ over a semiring $R$, the application of the empty vector linear map $\text{vecEmpty}$ to $m$ yields the empty vector $[]$ in the module $\text{Fin}\ 0 \to M₃$.
LinearMap.vecCons definition
{n} (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin n → M₂) : M →ₗ[R] Fin n.succ → M₂
Full source 
/-- A linear map into `Fin n.succ → M₃` can be built out of a map into `M₃` and a map into
`Fin n → M₃`. -/
def LinearMap.vecCons {n} (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin n → M₂) : M →ₗ[R] Fin n.succ → M₂ :=
  Fin.consLinearEquivFin.consLinearEquiv R (fun _ : Fin n.succ => M₂) ∘ₗ f.prod g
Linear map construction via vector cons
Informal description
Given a linear map $f : M \to M₂$ and a linear map $g : M \to \text{Fin}\ n \to M₂$, the linear map $\text{vecCons}\ f\ g : M \to \text{Fin}\ (n+1) \to M₂$ is constructed by combining $f$ and $g$ using the linear equivalence $\text{Fin.consLinearEquiv}$. Specifically, for any $m \in M$, the result is the vector $\text{vecCons}\ (f\ m)\ (g\ m)$ in $\text{Fin}\ (n+1) \to M₂$.
LinearMap.vecCons_apply theorem
{n} (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin n → M₂) (m : M) : f.vecCons g m = Matrix.vecCons (f m) (g m)
Full source 
@[simp]
theorem LinearMap.vecCons_apply {n} (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin n → M₂) (m : M) :
    f.vecCons g m = Matrix.vecCons (f m) (g m) :=
  rfl
Application of Vector Cons Linear Map: $\text{vecCons}\ f\ g\ m = \text{vecCons}\ (f\ m)\ (g\ m)$
Informal description
For any linear maps $f \colon M \to M₂$ and $g \colon M \to \text{Fin}\ n \to M₂$, and for any element $m \in M$, the application of the linear map $\text{vecCons}\ f\ g$ to $m$ is equal to the vector $\text{vecCons}\ (f\ m)\ (g\ m)$ in $\text{Fin}\ (n+1) \to M₂$.
Module.pi_induction theorem
{ι : Type v} [Finite ι] (motive : ∀ (N : Type u) [AddCommMonoid N] [Module R N], Prop) (motive' : ∀ (N : Type (max u v)) [AddCommMonoid N] [Module R N], Prop) (equiv : ∀ {N : Type u} {N' : Type (max u v)} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'], (N ≃ₗ[R] N') → motive N → motive' N') (equiv' : ∀ {N N' : Type (max u v)} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'], (N ≃ₗ[R] N') → motive' N → motive' N') (unit : motive PUnit) (prod : ∀ {N : Type u} {N' : Type (max u v)} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [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)
Full source 
/--
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.
-/
@[elab_as_elim]
lemma Module.pi_induction {ι : Type v} [Finite ι]
    (motive : ∀ (N : Type u) [AddCommMonoid N] [Module R N], Prop)
    (motive' : ∀ (N : Type (max u v)) [AddCommMonoid N] [Module R N], Prop)
    (equiv : ∀ {N : Type u} {N' : Type (max u v)} [AddCommMonoid N] [AddCommMonoid N']
      [Module R N] [Module R N'], (N ≃ₗ[R] N') → motive N → motive' N')
    (equiv' : ∀ {N N' : Type (max u v)} [AddCommMonoid N] [AddCommMonoid N']
      [Module R N] [Module R N'], (N ≃ₗ[R] N') → motive' N → motive' N')
    (unit : motive PUnit) (prod : ∀ {N : Type u} {N' : Type (max u v)} [AddCommMonoid N]
      [AddCommMonoid N'] [Module R N] [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) := by
  classical
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)
Induction Principle for Properties of Finite Product Modules
Informal description
Let $R$ be a ring, $\iota$ a finite type, and for each $i \in \iota$, let $M_i$ be an $R$-module. Suppose we have: 1. A property `motive` of $R$-modules in `Type u` and a property `motive'` of $R$-modules in `Type (max u v)`, where `motive'` is equivalent to `motive` under linear equivalence (via `equiv` and `equiv'`). 2. The property `motive` holds for the zero module (i.e., `motive PUnit` holds). 3. For any $R$-modules $N$ (in `Type u`) and $N'$ (in `Type (max u v)`), if `motive N` and `motive' N'` hold, then `motive' (N × N')` holds. Then, if `motive (M i)` holds for each $i \in \iota$, it follows that `motive' (Π i, M i)` holds.
LinearMap.vecEmpty₂ definition
: M →ₗ[R] M₂ →ₗ[R] Fin 0 → M₃
Full source 
/-- The empty bilinear map defeq to `Matrix.vecEmpty` -/
@[simps]
def LinearMap.vecEmpty₂ : M →ₗ[R] M₂ →ₗ[R] Fin 0 → M₃ where
  toFun _ := LinearMap.vecEmpty
  map_add' _ _ := LinearMap.ext fun _ => Subsingleton.elim _ _
  map_smul' _ _ := LinearMap.ext fun _ => Subsingleton.elim _ _
Empty vector bilinear map
Informal description
The bilinear map from modules $M$ and $M₂$ to the trivial module $\text{Fin}\ 0 \to M₃$, which is definitionally equal to the empty vector $\text{Matrix.vecEmpty}$. For any elements $m \in M$ and $m₂ \in M₂$, the application of this map to $(m, m₂)$ yields the empty vector $[]$.
LinearMap.vecCons₂ definition
{n} (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃) : M →ₗ[R] M₂ →ₗ[R] Fin n.succ → M₃
Full source 
/-- A bilinear map into `Fin n.succ → M₃` can be built out of a map into `M₃` and a map into
`Fin n → M₃` -/
@[simps]
def LinearMap.vecCons₂ {n} (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃) :
    M →ₗ[R] M₂ →ₗ[R] Fin n.succ → M₃ where
  toFun m := LinearMap.vecCons (f m) (g m)
  map_add' x y :=
    LinearMap.ext fun z => by
      simp only [f.map_add, g.map_add, LinearMap.add_apply, LinearMap.vecCons_apply,
        Matrix.cons_add_cons (f x z)]
  map_smul' r x := LinearMap.ext fun z => by simp [Matrix.smul_cons r (f x z)]
Bilinear map construction via vector cons
Informal description
Given a bilinear map $f : M \to M₂ \to M₃$ and a bilinear map $g : M \to M₂ \to \text{Fin}\ n \to M₃$, the bilinear map $\text{vecCons₂}\ f\ g : M \to M₂ \to \text{Fin}\ (n+1) \to M₃$ is constructed by combining $f$ and $g$ using the vector cons operation. Specifically, for any $m \in M$ and $m₂ \in M₂$, the result is the vector $\text{vecCons}\ (f\ m\ m₂)\ (g\ m\ m₂)$ in $\text{Fin}\ (n+1) \to M₃$.
Module.pi_induction' theorem
{ι : Type v} [Finite ι] (R : Type*) [Ring R] (motive : ∀ (N : Type u) [AddCommGroup N] [Module R N], Prop) (motive' : ∀ (N : Type (max u v)) [AddCommGroup N] [Module R N], Prop) (equiv : ∀ {N : Type u} {N' : Type (max u v)} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'], (N ≃ₗ[R] N') → motive N → motive' N') (equiv' : ∀ {N N' : Type (max u v)} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'], (N ≃ₗ[R] N') → motive' N → motive' N') (unit : motive PUnit) (prod : ∀ {N : Type u} {N' : Type (max u v)} [AddCommGroup N] [AddCommGroup N'] [Module R N] [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)
Full source 
/-- A variant of `Module.pi_induction` that assumes `AddCommGroup` instead of `AddCommMonoid`. -/
@[elab_as_elim]
lemma Module.pi_induction' {ι : Type v} [Finite ι] (R : Type*) [Ring R]
    (motive : ∀ (N : Type u) [AddCommGroup N] [Module R N], Prop)
    (motive' : ∀ (N : Type (max u v)) [AddCommGroup N] [Module R N], Prop)
    (equiv : ∀ {N : Type u} {N' : Type (max u v)} [AddCommGroup N] [AddCommGroup N']
      [Module R N] [Module R N'], (N ≃ₗ[R] N') → motive N → motive' N')
    (equiv' : ∀ {N N' : Type (max u v)} [AddCommGroup N] [AddCommGroup N']
      [Module R N] [Module R N'], (N ≃ₗ[R] N') → motive' N → motive' N')
    (unit : motive PUnit) (prod : ∀ {N : Type u} {N' : Type (max u v)} [AddCommGroup N]
      [AddCommGroup N'] [Module R N] [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) := by
  classical
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)
Induction Principle for Finite Product Modules with Additive Commutative Group Structure
Informal description
Let $R$ be a ring, $\iota$ a finite type, and for each $i \in \iota$, let $M_i$ be an $R$-module with an additive commutative group structure. Given two predicates `motive` and `motive'` on $R$-modules, suppose: 1. `motive` is preserved under linear equivalence for modules in universe `u`, 2. `motive'` is preserved under linear equivalence for modules in universe `max u v`, 3. `motive` holds for the trivial module `PUnit`, 4. `motive` and `motive'` are compatible with products, 5. `motive` holds for each $M_i$. Then `motive'` holds for the product module $\Pi_{i \in \iota} M_i$.