Mathlib.LinearAlgebra.Basis.Defs

Basis structure

Full source

/-- A `Basis ι R M` for a module `M` is the type of `ι`-indexed `R`-bases of `M`.

The basis vectors are available as `DFunLike.coe (b : Basis ι R M) : ι → M`.
To turn a linear independent family of vectors spanning `M` into a basis, use `Basis.mk`.
They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
available as `Basis.repr`.
-/
structure Basis where
  /-- `Basis.ofRepr` constructs a basis given an assignment of coordinates to each vector. -/
  ofRepr ::
    /-- `repr` is the linear equivalence sending a vector `x` to its coordinates:
    the `c`s such that `x = ∑ i, c i`. -/
    repr : M ≃ₗ[R] ι →₀ R

Basis of a module

Informal description

A basis for a module $M$ over a ring $R$ indexed by a type $\iota$ is a structure that provides a linear equivalence between $M$ and the space of finitely supported functions from $\iota$ to $R$. The basis vectors are given by a function from $\iota$ to $M$, and the structure includes a representation isomorphism that maps any element of $M$ to its coordinates in the basis.

Basis.instInhabitedFinsupp instance

: Inhabited (Basis ι R (ι →₀ R))

Full source

instance : Inhabited (Basis ι R (ι →₀ R)) :=
  ⟨.ofRepr (LinearEquiv.refl _ _)⟩

Canonical Basis for Finitely Supported Functions

Informal description

For any indexing type $\iota$ and any ring $R$, the space of finitely supported functions $\iota \to_{\text{f}} R$ has a canonical basis structure.

Basis.repr_injective theorem

: Injective (repr : Basis ι R M → M ≃ₗ[R] ι →₀ R)

Full source

theorem repr_injective : Injective (repr : Basis ι R M → M ≃ₗ[R] ι →₀ R) := fun f g h => by
  cases f; cases g; congr

Injectivity of Basis Representation as Linear Equivalence

Informal description

The function that maps a basis to its representation as a linear equivalence is injective. That is, if two bases of a module $M$ over a ring $R$ indexed by $\iota$ induce the same linear equivalence $M \simeq_{\ell[R]} \iota \to_{\text{f}} R$, then the two bases are equal.

Basis.instFunLike instance

: FunLike (Basis ι R M) ι M

Full source

/-- `b i` is the `i`th basis vector. -/
instance instFunLike : FunLike (Basis ι R M) ι M where
  coe b i := b.repr.symm (Finsupp.single i 1)
  coe_injective' f g h := repr_injective <| LinearEquiv.symm_bijective.injective <|
    LinearEquiv.toLinearMap_injective <| by ext; exact congr_fun h _

Basis Vectors as Function Application

Informal description

For any basis $b$ of a module $M$ over a ring $R$ indexed by a type $\iota$, the basis vectors $b(i)$ for $i \in \iota$ can be treated as elements of $M$ via a function-like structure. This means that the basis $b$ can be applied to an index $i$ to obtain the corresponding basis vector in $M$.

Basis.coe_ofRepr theorem

(e : M ≃ₗ[R] ι →₀ R) : ⇑(ofRepr e) = fun i => e.symm (Finsupp.single i 1)

Full source

@[simp]
theorem coe_ofRepr (e : M ≃ₗ[R] ι →₀ R) : ⇑(ofRepr e) = fun i => e.symm (Finsupp.single i 1) :=
  rfl

Basis Vectors from Linear Equivalence via Single Functions

Informal description

Given a linear equivalence $e : M \simeq_{\ell[R]} \iota \to_{\text{f}} R$ between a module $M$ and the space of finitely supported functions from $\iota$ to $R$, the basis vectors of the corresponding basis $\text{ofRepr}(e)$ are given by applying the inverse of $e$ to the finitely supported function that is $1$ at index $i$ and $0$ elsewhere. In other words, for each $i \in \iota$, the basis vector $(\text{ofRepr}(e))(i)$ equals $e^{-1}(\text{single}(i, 1))$.

Basis.injective theorem

[Nontrivial R] : Injective b

Full source

protected theorem injective [Nontrivial R] : Injective b :=
  b.repr.symm.injective.comp fun _ _ => (Finsupp.single_left_inj (one_ne_zero : (1 : R) ≠ 0)).mp

Injectivity of Basis Vectors in Nontrivial Rings

Informal description

For any nontrivial ring $R$ and any basis $b$ of a module $M$ over $R$, the function $b : \iota \to M$ is injective. That is, if $b(i) = b(j)$ for some $i, j \in \iota$, then $i = j$.

Basis.repr_symm_single_one theorem

: b.repr.symm (Finsupp.single i 1) = b i

Full source

theorem repr_symm_single_one : b.repr.symm (Finsupp.single i 1) = b i :=
  rfl

Basis Vector Representation: $b.\text{repr}^{-1}(\text{single}_i(1)) = b(i)$

Informal description

For any basis $b$ of a module $M$ over a ring $R$, the inverse of the representation isomorphism $b.\text{repr}$ evaluated at the finitely supported function $\text{single}_i(1)$ (which is $1$ at index $i$ and $0$ elsewhere) equals the basis vector $b(i)$.

Basis.repr_symm_single theorem

: b.repr.symm (Finsupp.single i c) = c • b i

Full source

theorem repr_symm_single : b.repr.symm (Finsupp.single i c) = c • b i :=
  calc
    b.repr.symm (Finsupp.single i c) = b.repr.symm (c • Finsupp.single i (1 : R)) := by
      { rw [Finsupp.smul_single', mul_one] }
    _ = c • b i := by rw [LinearEquiv.map_smul, repr_symm_single_one]

Basis Representation Inverse of Single Function: $b.\text{repr}^{-1}(\text{single}_i(c)) = c \cdot b(i)$

Informal description

For any basis $b$ of a module $M$ over a ring $R$, the inverse of the representation isomorphism $b.\text{repr}$ evaluated at the finitely supported function $\text{single}_i(c)$ (which is $c$ at index $i$ and $0$ elsewhere) equals the scalar multiple $c \cdot b(i)$ of the basis vector $b(i)$. In other words, $b.\text{repr}^{-1}(\text{single}_i(c)) = c \cdot b(i)$.

Basis.repr_self theorem

: b.repr (b i) = Finsupp.single i 1

Full source

@[simp]
theorem repr_self : b.repr (b i) = Finsupp.single i 1 :=
  LinearEquiv.apply_symm_apply _ _

Coordinate Representation of Basis Vectors: $b.\text{repr}(b(i)) = \text{single}_i(1)$

Informal description

For a basis $b$ of a module $M$ over a ring $R$, the representation of the basis vector $b(i)$ under the coordinate isomorphism $b.\text{repr}$ is the finitely supported function that takes the value $1$ at index $i$ and $0$ elsewhere. In other words, $b.\text{repr}(b(i)) = \text{single}_i(1)$, where $\text{single}_i(1)$ denotes the function that is $1$ at $i$ and zero otherwise.

Basis.repr_self_apply theorem

(j) [Decidable (i = j)] : b.repr (b i) j = if i = j then 1 else 0

Full source

theorem repr_self_apply (j) [Decidable (i = j)] : b.repr (b i) j = if i = j then 1 else 0 := by
  rw [repr_self, Finsupp.single_apply]

Coordinate Representation of Basis Vectors at Index $j$: $b.\text{repr}(b(i))(j) = \delta_{ij}$

Informal description

For a basis $b$ of a module $M$ over a ring $R$, the coordinate representation of the basis vector $b(i)$ at index $j$ is given by: $$b.\text{repr}(b(i))(j) = \begin{cases} 1 & \text{if } i = j \\ 0 & \text{otherwise} \end{cases}$$

Basis.repr_symm_apply theorem

(v) : b.repr.symm v = Finsupp.linearCombination R b v

Full source

@[simp]
theorem repr_symm_apply (v) : b.repr.symm v = Finsupp.linearCombination R b v :=
  calc
    b.repr.symm v = b.repr.symm (v.sum Finsupp.single) := by simp
    _ = v.sum fun i vi => b.repr.symm (Finsupp.single i vi) := map_finsuppSum ..
    _ = Finsupp.linearCombination R b v := by simp only [repr_symm_single,
                                                         Finsupp.linearCombination_apply]

Inverse Basis Representation as Linear Combination

Informal description

For any basis $b$ of a module $M$ over a ring $R$, the inverse of the coordinate representation isomorphism $b.\text{repr}^{-1}$ applied to a finitely supported function $v : \iota \to_{\text{f}} R$ equals the linear combination of the basis vectors $b(i)$ with coefficients given by $v(i)$. In other words: $$ b.\text{repr}^{-1}(v) = \sum_{i \in \iota} v(i) \cdot b(i) $$

Basis.coe_repr_symm theorem

: ↑b.repr.symm = Finsupp.linearCombination R b

Full source

@[simp]
theorem coe_repr_symm : ↑b.repr.symm = Finsupp.linearCombination R b :=
  LinearMap.ext fun v => b.repr_symm_apply v

Inverse Basis Representation as Linear Combination Map

Informal description

For any basis $b$ of a module $M$ over a ring $R$, the underlying function of the inverse coordinate representation isomorphism $b.\text{repr}^{-1}$ is equal to the linear combination map $\text{Finsupp.linearCombination}_R b$, which constructs a vector in $M$ from a finitely supported function $v : \iota \to_{\text{f}} R$ via: $$ v \mapsto \sum_{i \in \iota} v(i) \cdot b(i) $$

Basis.repr_linearCombination theorem

(v) : b.repr (Finsupp.linearCombination _ b v) = v

Full source

@[simp]
theorem repr_linearCombination (v) : b.repr (Finsupp.linearCombination _ b v) = v := by
  rw [← b.coe_repr_symm]
  exact b.repr.apply_symm_apply v

Coordinate Representation of Linear Combination Matches Input Coefficients

Informal description

For any basis $b$ of a module $M$ over a ring $R$ and any finitely supported function $v : \iota \to_{\text{f}} R$, the coordinate representation of the linear combination $\sum_{i \in \iota} v(i) \cdot b(i)$ equals $v$. That is: $$ b.\text{repr}\left(\sum_{i \in \iota} v(i) \cdot b(i)\right) = v $$

Basis.linearCombination_repr theorem

: Finsupp.linearCombination _ b (b.repr x) = x

Full source

@[simp]
theorem linearCombination_repr : Finsupp.linearCombination _ b (b.repr x) = x := by
  rw [← b.coe_repr_symm]
  exact b.repr.symm_apply_apply x

Reconstruction of Vector from Basis Coordinates via Linear Combination

Informal description

For any basis $b$ of a module $M$ over a ring $R$ and any vector $x \in M$, the linear combination of the basis vectors $b(i)$ with coefficients given by the coordinates of $x$ in the basis $b$ (i.e., $b.\text{repr}(x)$) reconstructs the original vector $x$. More precisely, if $b.\text{repr}(x) = v \in \iota \to_{\text{f}} R$ is the coordinate representation of $x$, then: $$ \sum_{i \in \iota} v(i) \cdot b(i) = x $$

Basis.map definition

: Basis ι R M'

Full source

/-- Apply the linear equivalence `f` to the basis vectors. -/
@[simps]
protected def map : Basis ι R M' :=
  ofRepr (f.symm.trans b.repr)

Basis transformation via linear equivalence

Informal description

Given a basis `b` for a module `M` over a ring `R` indexed by `ι`, and a linear equivalence `f : M ≃ₗ[R] M'` to another module `M'`, the function `Basis.map` constructs a new basis for `M'` by applying `f` to each basis vector of `b`. Specifically, the new basis vectors are given by `f (b i)` for each `i : ι`, and the representation isomorphism for the new basis is obtained by composing the inverse of `f` with the representation isomorphism of `b`.

Basis.map_apply theorem

(i) : b.map f i = f (b i)

Full source

@[simp]
theorem map_apply (i) : b.map f i = f (b i) :=
  rfl

Image of Basis Vector under Linear Equivalence

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$ indexed by a type $\iota$, and let $f : M \simeq M'$ be a linear equivalence to another module $M'$. For any index $i \in \iota$, the $i$-th basis vector of the transformed basis $b.map f$ is equal to $f$ applied to the $i$-th basis vector of $b$, i.e., $(b.map f)(i) = f(b(i))$.

Basis.coe_map theorem

: (b.map f : ι → M') = f ∘ b

Full source

theorem coe_map : (b.map f : ι → M') = f ∘ b :=
  rfl

Function Representation of Mapped Basis: $(b.\text{map}\, f) = f \circ b$

Informal description

For a basis $b$ of a module $M$ over a ring $R$ indexed by $\iota$, and a linear equivalence $f : M \simeq M'$, the function representation of the mapped basis $b.\text{map}\, f$ is equal to the composition $f \circ b$. In other words, $(b.\text{map}\, f)(i) = f(b(i))$ for all $i \in \iota$.

Basis.reindex definition

: Basis ι' R M

Full source

/-- `b.reindex (e : ι ≃ ι')` is a basis indexed by `ι'` -/
def reindex : Basis ι' R M :=
  .ofRepr (b.repr.trans (Finsupp.domLCongr e))

Reindexed basis

Informal description

Given a basis `b` indexed by type `ι` for a module `M` over a ring `R`, and an equivalence `e : ι ≃ ι'` between index types, the basis `b.reindex e` is a new basis for `M` indexed by `ι'`. The basis vectors of the reindexed basis are given by `b (e.symm i')` for each `i' ∈ ι'`. The reindexing is implemented via the linear isomorphism `b.repr.trans (Finsupp.domLCongr e)`, which first maps an element of `M` to its coordinates in the original basis `b`, and then reindexes these coordinates using the equivalence `e`.

Basis.reindex_apply theorem

(i' : ι') : b.reindex e i' = b (e.symm i')

Full source

theorem reindex_apply (i' : ι') : b.reindex e i' = b (e.symm i') :=
  show (b.repr.trans (Finsupp.domLCongr e)).symm (Finsupp.single i' 1) =
    b.repr.symm (Finsupp.single (e.symm i') 1)
  by rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]

Reindexed Basis Vector Formula: $b.\text{reindex}\, e\, i' = b(e^{-1}(i'))$

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$ indexed by a type $\iota$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. For any $i' \in \iota'$, the $i'$-th basis vector of the reindexed basis $b.\text{reindex}\, e$ is equal to $b(e^{-1}(i'))$.

Basis.coe_reindex theorem

: (b.reindex e : ι' → M) = b ∘ e.symm

Full source

@[simp]
theorem coe_reindex : (b.reindex e : ι' → M) = b ∘ e.symm :=
  funext (b.reindex_apply e)

Reindexed Basis as Composition with Inverse Equivalence

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$ indexed by a type $\iota$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. Then the reindexed basis $b.\text{reindex}\, e$, when viewed as a function from $\iota'$ to $M$, is equal to the composition of the original basis $b$ with the inverse of the equivalence $e$, i.e., $$(b.\text{reindex}\, e) = b \circ e^{-1}.$$

Basis.repr_reindex_apply theorem

(i' : ι') : (b.reindex e).repr x i' = b.repr x (e.symm i')

Full source

theorem repr_reindex_apply (i' : ι') : (b.reindex e).repr x i' = b.repr x (e.symm i') :=
  show (Finsupp.domLCongr e : _ ≃ₗ[R] _) (b.repr x) i' = _ by simp

Coordinate Representation under Basis Reindexing

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$ indexed by $\iota$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. For any $x \in M$ and any $i' \in \iota'$, the $i'$-th coordinate of $x$ with respect to the reindexed basis $b.\text{reindex}\, e$ is equal to the $(e^{-1} i')$-th coordinate of $x$ with respect to the original basis $b$. In other words, $$(b.\text{reindex}\, e).\text{repr}\, x\, i' = b.\text{repr}\, x\, (e^{-1} i').$$

Basis.repr_reindex theorem

: (b.reindex e).repr x = (b.repr x).mapDomain e

Full source

@[simp]
theorem repr_reindex : (b.reindex e).repr x = (b.repr x).mapDomain e :=
  DFunLike.ext _ _ <| by simp [repr_reindex_apply]

Coordinate Representation Transformation under Basis Reindexing

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$ indexed by $\iota$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. For any $x \in M$, the coordinate representation of $x$ with respect to the reindexed basis $b.\text{reindex}\, e$ is equal to the finitely supported function obtained by applying the domain mapping $e$ to the coordinate representation of $x$ with respect to the original basis $b$. In other words, $$(b.\text{reindex}\, e).\text{repr}\, x = \text{mapDomain}\, e\, (b.\text{repr}\, x).$$

Basis.reindex_refl theorem

: b.reindex (Equiv.refl ι) = b

Full source

@[simp]
theorem reindex_refl : b.reindex (Equiv.refl ι) = b := by
  simp [reindex]

Reindexing a Basis with the Identity Equivalence Yields the Original Basis

Informal description

Given a basis $b$ indexed by type $\iota$ for a module $M$ over a ring $R$, reindexing $b$ with the identity equivalence $\text{Equiv.refl } \iota$ yields the original basis $b$.

Basis.range_reindex theorem

: Set.range (b.reindex e) = Set.range b

Full source

/-- `simp` can prove this as `Basis.coe_reindex` + `EquivLike.range_comp` -/
theorem range_reindex : Set.range (b.reindex e) = Set.range b := by
  simp [coe_reindex, range_comp]

Range Preservation under Basis Reindexing

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$ indexed by a type $\iota$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. Then the range of the reindexed basis $b.\text{reindex}\, e$ is equal to the range of the original basis $b$, i.e., $$\text{range}\, (b.\text{reindex}\, e) = \text{range}\, b.$$

Basis.equivFun definition

[Finite ι] (b : Basis ι R M) : M ≃ₗ[R] ι → R

Full source

/-- A module over `R` with a finite basis is linearly equivalent to functions from its basis to `R`.
-/
def Basis.equivFun [Finite ι] (b : Basis ι R M) : M ≃ₗ[R] ι → R :=
  LinearEquiv.trans b.repr
    ({ Finsupp.equivFunOnFinite with
        toFun := (↑)
        map_add' := Finsupp.coe_add
        map_smul' := Finsupp.coe_smul } :
      (ι →₀ R) ≃ₗ[R] ι → R)

Linear equivalence between a module and its coordinate functions for a finite basis

Informal description

Given a finite index type $\iota$, a ring $R$, and a module $M$ over $R$ with a basis $b : \text{Basis } \iota R M$, the linear equivalence $\text{Basis.equivFun } b$ maps any element $x \in M$ to its coordinates in the basis $b$ as a function $\iota \to R$. This is constructed by composing the basis representation isomorphism $b.\text{repr} : M \simeq (\iota \to_{\text{f}} R)$ with the canonical equivalence between finitely supported functions and all functions on a finite type.

Module.fintypeOfFintype definition

[Fintype ι] (b : Basis ι R M) [Fintype R] : Fintype M

Full source

/-- A module over a finite ring that admits a finite basis is finite. -/
def Module.fintypeOfFintype [Fintype ι] (b : Basis ι R M) [Fintype R] : Fintype M :=
  haveI := Classical.decEq ι
  Fintype.ofEquiv _ b.equivFun.toEquiv.symm

Finiteness of a module with finite basis over a finite ring

Informal description

Given a finite index type $\iota$, a finite ring $R$, and a module $M$ over $R$ with a basis $b : \text{Basis } \iota R M$, the module $M$ is finite. This is established by constructing a bijection between $M$ and the space of functions $\iota \to R$ using the basis representation.

Module.card_fintype theorem

[Fintype ι] (b : Basis ι R M) [Fintype R] [Fintype M] : card M = card R ^ card ι

Full source

theorem Module.card_fintype [Fintype ι] (b : Basis ι R M) [Fintype R] [Fintype M] :
    card M = card R ^ card ι := by
  classical
    calc
      card M = card (ι → R) := card_congr b.equivFun.toEquiv
      _ = card R ^ card ι := card_fun

Cardinality of Finite Module via Basis

Informal description

Let $M$ be a module over a ring $R$ with a finite basis indexed by a finite type $\iota$. If both $R$ and $M$ are finite types, then the cardinality of $M$ is equal to the cardinality of $R$ raised to the power of the cardinality of $\iota$, i.e., $|M| = |R|^{|\iota|}$.

Basis.equivFun_symm_apply theorem

[Fintype ι] (b : Basis ι R M) (x : ι → R) : b.equivFun.symm x = ∑ i, x i • b i

Full source

/-- Given a basis `v` indexed by `ι`, the canonical linear equivalence between `ι → R` and `M` maps
a function `x : ι → R` to the linear combination `∑_i x i • v i`. -/
@[simp]
theorem Basis.equivFun_symm_apply [Fintype ι] (b : Basis ι R M) (x : ι → R) :
    b.equivFun.symm x = ∑ i, x i • b i := by
  simp [Basis.equivFun, Finsupp.linearCombination_apply, sum_fintype, equivFunOnFinite]

Inverse Coordinate Representation as Linear Combination for Finite Bases

Informal description

Let $M$ be a module over a ring $R$ with a finite basis $b$ indexed by a finite type $\iota$. For any function $x : \iota \to R$, the inverse of the coordinate representation isomorphism $b.\text{equivFun}^{-1}$ maps $x$ to the linear combination $\sum_{i \in \iota} x(i) \cdot b(i)$.

Basis.equivFun_apply theorem

[Finite ι] (b : Basis ι R M) (u : M) : b.equivFun u = b.repr u

Full source

@[simp]
theorem Basis.equivFun_apply [Finite ι] (b : Basis ι R M) (u : M) : b.equivFun u = b.repr u :=
  rfl

Equality of Coordinate Function and Basis Representation for Finite Bases

Informal description

For a finite index type $\iota$, a ring $R$, a module $M$ over $R$, and a basis $b : \text{Basis } \iota R M$, the coordinate function $\text{Basis.equivFun } b$ evaluated at any vector $u \in M$ equals the representation of $u$ in the basis $b$, i.e., $b.\text{equivFun}(u) = b.\text{repr}(u)$.

Basis.map_equivFun theorem

[Finite ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).equivFun = f.symm.trans b.equivFun

Full source

@[simp]
theorem Basis.map_equivFun [Finite ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') :
    (b.map f).equivFun = f.symm.trans b.equivFun :=
  rfl

Equivariance of Coordinate Representation under Basis Transformation

Informal description

Let $M$ and $M'$ be modules over a ring $R$, with $\iota$ a finite indexing type. Given a basis $b$ of $M$ indexed by $\iota$ and a linear equivalence $f : M \simeq M'$, the coordinate representation isomorphism $(b.\text{map } f).\text{equivFun}$ for the transformed basis is equal to the composition $f^{-1} \circ b.\text{equivFun}$.

Basis.sum_equivFun theorem

[Fintype ι] (b : Basis ι R M) (u : M) : ∑ i, b.equivFun u i • b i = u

Full source

theorem Basis.sum_equivFun [Fintype ι] (b : Basis ι R M) (u : M) :
    ∑ i, b.equivFun u i • b i = u := by
  rw [← b.equivFun_symm_apply, b.equivFun.symm_apply_apply]

Reconstruction of Vector from Coordinates in Finite Basis

Informal description

Let $M$ be a module over a ring $R$ with a finite basis $b$ indexed by a finite type $\iota$. For any vector $u \in M$, the sum $\sum_{i \in \iota} (b.\text{equivFun}(u))(i) \cdot b(i)$ equals $u$, where $b.\text{equivFun}(u)$ gives the coordinates of $u$ in the basis $b$.

Basis.sum_repr theorem

[Fintype ι] (b : Basis ι R M) (u : M) : ∑ i, b.repr u i • b i = u

Full source

theorem Basis.sum_repr [Fintype ι] (b : Basis ι R M) (u : M) : ∑ i, b.repr u i • b i = u :=
  b.sum_equivFun u

Reconstruction of Vector from Coordinates in Finite Basis via `repr`

Informal description

Let $M$ be a module over a ring $R$ with a finite basis $b$ indexed by a finite type $\iota$. For any vector $u \in M$, the sum $\sum_{i \in \iota} (b.\text{repr}(u))(i) \cdot b(i)$ equals $u$, where $b.\text{repr}(u)$ gives the coordinates of $u$ in the basis $b$.

Basis.equivFun_self theorem

[Finite ι] [DecidableEq ι] (b : Basis ι R M) (i j : ι) : b.equivFun (b i) j = if i = j then 1 else 0

Full source

@[simp]
theorem Basis.equivFun_self [Finite ι] [DecidableEq ι] (b : Basis ι R M) (i j : ι) :
    b.equivFun (b i) j = if i = j then 1 else 0 := by rw [b.equivFun_apply, b.repr_self_apply]

Coordinate Function of Basis Vectors: $b.\text{equivFun}(b(i))(j) = \delta_{ij}$

Informal description

Let $\iota$ be a finite index type with decidable equality, $R$ a ring, and $M$ an $R$-module with a basis $b : \text{Basis } \iota R M$. For any indices $i, j \in \iota$, the coordinate function of the basis vector $b(i)$ at index $j$ satisfies: $$b.\text{equivFun}(b(i))(j) = \begin{cases} 1 & \text{if } i = j \\ 0 & \text{otherwise} \end{cases}$$

Basis.repr_sum_self theorem

[Fintype ι] (b : Basis ι R M) (c : ι → R) : b.repr (∑ i, c i • b i) = c

Full source

theorem Basis.repr_sum_self [Fintype ι] (b : Basis ι R M) (c : ι → R) :
    b.repr (∑ i, c i • b i) = c := by
  simp_rw [← b.equivFun_symm_apply, ← b.equivFun_apply, b.equivFun.apply_symm_apply]

Coordinate Representation of Linear Combination in Finite Basis

Informal description

Let $M$ be a module over a ring $R$ with a finite basis $b$ indexed by a finite type $\iota$. For any function $c : \iota \to R$, the coordinate representation of the linear combination $\sum_{i \in \iota} c(i) \cdot b(i)$ with respect to the basis $b$ is equal to $c$ itself. In other words, $b.\text{repr}(\sum_i c(i) \cdot b(i)) = c$.

Basis.ofEquivFun definition

[Finite ι] (e : M ≃ₗ[R] ι → R) : Basis ι R M

Full source

/-- Define a basis by mapping each vector `x : M` to its coordinates `e x : ι → R`,
as long as `ι` is finite. -/
def Basis.ofEquivFun [Finite ι] (e : M ≃ₗ[R] ι → R) : Basis ι R M :=
  .ofRepr <| e.trans <| LinearEquiv.symm <| Finsupp.linearEquivFunOnFinite R R ι

Basis from linear equivalence to function space

Informal description

Given a finite index type $\iota$ and a linear equivalence $e : M \simeq_{\ell[R]} \iota \to R$ between an $R$-module $M$ and the space of functions from $\iota$ to $R$, the function `Basis.ofEquivFun` constructs a basis for $M$ over $R$ indexed by $\iota$. The basis vectors are defined such that the coordinates of any $x \in M$ under this basis correspond to the values of $e(x) : \iota \to R$.

Basis.ofEquivFun_repr_apply theorem

[Finite ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) : (Basis.ofEquivFun e).repr x i = e x i

Full source

@[simp]
theorem Basis.ofEquivFun_repr_apply [Finite ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) :
    (Basis.ofEquivFun e).repr x i = e x i :=
  rfl

Coordinate Representation in Basis Constructed from Linear Equivalence

Informal description

For a finite index type $\iota$, a linear equivalence $e : M \simeq_{\ell[R]} \iota \to R$, and any $x \in M$ and $i \in \iota$, the $i$-th coordinate of $x$ with respect to the basis constructed from $e$ via `Basis.ofEquivFun` is equal to the $i$-th component of $e(x)$. In other words, $(Basis.ofEquivFun\, e).repr\, x\, i = e\, x\, i$.

Basis.coe_ofEquivFun theorem

 [Finite ι] [DecidableEq ι] (e : M ≃ₗ[R] ι → R) : (Basis.ofEquivFun e : ι → M) = fun i => e.symm (Pi.single i 1)

Full source

@[simp]
theorem Basis.coe_ofEquivFun [Finite ι] [DecidableEq ι] (e : M ≃ₗ[R] ι → R) :
    (Basis.ofEquivFun e : ι → M) = fun i => e.symm (Pi.single i 1) :=
  funext fun i =>
    e.injective <|
      funext fun j => by
        simp [Basis.ofEquivFun, ← Finsupp.single_eq_pi_single]

Basis vectors from linear equivalence: $(Basis.ofEquivFun e)(i) = e^{-1}(\delta_i)$

Informal description

Let $\iota$ be a finite index type with decidable equality, and let $e : M \simeq_{\ell[R]} \iota \to R$ be a linear equivalence between an $R$-module $M$ and the space of functions from $\iota$ to $R$. Then the basis vectors of the basis constructed by `Basis.ofEquivFun e` are given by $(Basis.ofEquivFun e)(i) = e^{-1}(\delta_i)$, where $\delta_i$ is the function $\iota \to R$ that takes the value $1$ at $i$ and $0$ elsewhere.

Basis.ofEquivFun_equivFun theorem

[Finite ι] (v : Basis ι R M) : Basis.ofEquivFun v.equivFun = v

Full source

@[simp]
theorem Basis.ofEquivFun_equivFun [Finite ι] (v : Basis ι R M) :
    Basis.ofEquivFun v.equivFun = v :=
  Basis.repr_injective <| by ext; rfl

Basis Reconstruction from Coordinate Equivalence

Informal description

For a finite index type $\iota$, a ring $R$, and a basis $v$ of an $R$-module $M$ indexed by $\iota$, the basis constructed from the linear equivalence $v.\text{equivFun} : M \simeq_{\ell[R]} \iota \to R$ via `Basis.ofEquivFun` is equal to $v$ itself.

Basis.equivFun_ofEquivFun theorem

[Finite ι] (e : M ≃ₗ[R] ι → R) : (Basis.ofEquivFun e).equivFun = e

Full source

@[simp]
theorem Basis.equivFun_ofEquivFun [Finite ι] (e : M ≃ₗ[R] ι → R) :
    (Basis.ofEquivFun e).equivFun = e := by
  ext j
  simp_rw [Basis.equivFun_apply, Basis.ofEquivFun_repr_apply]

Equivalence between Basis Construction and Original Linear Map

Informal description

For a finite index type $\iota$, a ring $R$, and a linear equivalence $e : M \simeq_{\ell[R]} \iota \to R$ between an $R$-module $M$ and the space of functions from $\iota$ to $R$, the coordinate function equivalence associated with the basis constructed from $e$ via `Basis.ofEquivFun` is equal to $e$ itself. In other words, if $b$ is the basis obtained from $e$, then $b.\text{equivFun} = e$.

Basis.ext theorem

{f₁ f₂ : M →ₛₗ[σ] M₁} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂

Full source

/-- Two linear maps are equal if they are equal on basis vectors. -/
theorem ext {f₁ f₂ : M →ₛₗ[σ] M₁} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂ := by
  ext x
  rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]
  simp only [map_sum, LinearMap.map_smulₛₗ, h]

Equality of Linear Maps on Basis Vectors

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$, and let $M₁$ be another module over a ring $R₁$ with a ring homomorphism $\sigma: R \to R₁$. For any two linear maps $f₁, f₂: M \to M₁$ with respect to $\sigma$, if $f₁(b(i)) = f₂(b(i))$ for all $i \in \iota$, then $f₁ = f₂$.

Basis.ext' theorem

{f₁ f₂ : M ≃ₛₗ[σ] M₁} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂

Full source

/-- Two linear equivs are equal if they are equal on basis vectors. -/
theorem ext' {f₁ f₂ : M ≃ₛₗ[σ] M₁} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂ := by
  ext x
  rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]
  simp only [map_sum, LinearEquiv.map_smulₛₗ, h]

Equality of Semilinear Equivalences on Basis Vectors

Informal description

Let $M$ and $M_1$ be modules over a ring $R$ with a ring homomorphism $\sigma: R \to R$, and let $b$ be a basis of $M$ indexed by $\iota$. For any two $\sigma$-semilinear equivalences $f_1, f_2: M \simeq_{\sigma} M_1$, if $f_1(b(i)) = f_2(b(i))$ for all basis vectors $b(i)$, then $f_1 = f_2$.

Basis.ext_elem_iff theorem

{x y : M} : x = y ↔ ∀ i, b.repr x i = b.repr y i

Full source

/-- Two elements are equal iff their coordinates are equal. -/
theorem ext_elem_iff {x y : M} : x = y ↔ ∀ i, b.repr x i = b.repr y i := by
  simp only [← DFunLike.ext_iff, EmbeddingLike.apply_eq_iff_eq]

Equality of Elements via Basis Coordinates

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$. For any two elements $x, y \in M$, we have $x = y$ if and only if their coordinates with respect to the basis $b$ are equal, i.e., for all $i \in \iota$, the $i$-th coordinate of $x$ equals the $i$-th coordinate of $y$.

Basis.repr_eq_iff theorem

{b : Basis ι R M} {f : M →ₗ[R] ι →₀ R} : ↑b.repr = f ↔ ∀ i, f (b i) = Finsupp.single i 1

Full source

theorem repr_eq_iff {b : Basis ι R M} {f : M →ₗ[R] ι →₀ R} :
    ↑b.repr = f ↔ ∀ i, f (b i) = Finsupp.single i 1 :=
  ⟨fun h i => h ▸ b.repr_self i, fun h => b.ext fun i => (b.repr_self i).trans (h i).symm⟩

Characterization of Basis Representation via Linear Maps: $b.\text{repr} = f \leftrightarrow \forall i, f(b(i)) = \text{single}_i(1)$

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$. For a linear map $f : M \to \iota \to_{\text{f}} R$ (where $\iota \to_{\text{f}} R$ denotes finitely supported functions from $\iota$ to $R$), the coordinate representation map $b.\text{repr}$ is equal to $f$ if and only if for every basis vector $b(i)$, the image $f(b(i))$ is the finitely supported function that takes the value $1$ at $i$ and $0$ elsewhere.

Basis.repr_eq_iff' theorem

{b : Basis ι R M} {f : M ≃ₗ[R] ι →₀ R} : b.repr = f ↔ ∀ i, f (b i) = Finsupp.single i 1

Full source

theorem repr_eq_iff' {b : Basis ι R M} {f : M ≃ₗ[R] ι →₀ R} :
    b.repr = f ↔ ∀ i, f (b i) = Finsupp.single i 1 :=
  ⟨fun h i => h ▸ b.repr_self i, fun h => b.ext' fun i => (b.repr_self i).trans (h i).symm⟩

Equality of Coordinate Representations via Basis Vectors: $b.\text{repr} = f \leftrightarrow \forall i, f(b(i)) = \text{single}_i(1)$

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$, and let $f : M \simeq_{\text{lin}} \iota \to_{\text{f}} R$ be a linear equivalence. Then the coordinate representation isomorphism $b.\text{repr}$ equals $f$ if and only if for every basis vector $b(i)$, the image $f(b(i))$ is the finitely supported function that takes the value $1$ at $i$ and $0$ elsewhere, i.e., $f(b(i)) = \text{single}_i(1)$ for all $i \in \iota$.

Basis.apply_eq_iff theorem

{b : Basis ι R M} {x : M} {i : ι} : b i = x ↔ b.repr x = Finsupp.single i 1

Full source

theorem apply_eq_iff {b : Basis ι R M} {x : M} {i : ι} : b i = x ↔ b.repr x = Finsupp.single i 1 :=
  ⟨fun h => h ▸ b.repr_self i, fun h => b.repr.injective ((b.repr_self i).trans h.symm)⟩

Basis Vector Equals Vector if and only if Coordinates are Single Nonzero at Index

Informal description

For a basis $b$ of a module $M$ over a ring $R$ indexed by a type $\iota$, a vector $x \in M$, and an index $i \in \iota$, the basis vector $b(i)$ equals $x$ if and only if the coordinate representation of $x$ under $b$ is the finitely supported function that takes the value $1$ at $i$ and $0$ elsewhere. In other words, $b(i) = x \leftrightarrow b.\text{repr}(x) = \text{single}_i(1)$.

Basis.repr_apply_eq theorem

 (f : M → ι → R) (hadd : ∀ x y, f (x + y) = f x + f y) (hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x)
  (f_eq : ∀ i, f (b i) = Finsupp.single i 1) (x : M) (i : ι) : b.repr x i = f x i

Full source

/-- An unbundled version of `repr_eq_iff` -/
theorem repr_apply_eq (f : M → ι → R) (hadd : ∀ x y, f (x + y) = f x + f y)
    (hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x) (f_eq : ∀ i, f (b i) = Finsupp.single i 1)
    (x : M) (i : ι) : b.repr x i = f x i := by
  let f_i : M →ₗ[R] R :=
    { toFun x := f x i
      map_add' _ _ := by rw [hadd, Pi.add_apply]
      map_smul' _ _ := by simp [hsmul, Pi.smul_apply] }
  have : Finsupp.lapplyFinsupp.lapply i ∘ₗ ↑b.repr = f_i := by
    refine b.ext fun j => ?_
    show b.repr (b j) i = f (b j) i
    rw [b.repr_self, f_eq]
  calc
    b.repr x i = f_i x := by
      { rw [← this]
        rfl }
    _ = f x i := rfl

Equality of Coordinate Functions on Basis Vectors: $b.\text{repr}(x)(i) = f(x)(i)$

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$. Given a function $f \colon M \to \iota \to R$ that is additive (i.e., $f(x + y) = f(x) + f(y)$ for all $x, y \in M$) and linear (i.e., $f(c \cdot x) = c \cdot f(x)$ for all $c \in R$ and $x \in M$), and satisfies $f(b(i)) = \text{single}_i(1)$ for all $i \in \iota$, then for any $x \in M$ and $i \in \iota$, the $i$-th coordinate of $x$ in the basis $b$ equals the $i$-th component of $f(x)$, i.e., $b.\text{repr}(x)(i) = f(x)(i)$.

Basis.mapCoeffs definition

(h : ∀ (c) (x : M), f c • x = c • x) : Basis ι R' M

Full source

/-- If `R` and `R'` are isomorphic rings that act identically on a module `M`,
then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module.

See also `Basis.algebraMapCoeffs` for the case where `f` is equal to `algebraMap`.
-/
@[simps +simpRhs]
def mapCoeffs (h : ∀ (c) (x : M), f c • x = c • x) : Basis ι R' M := by
  letI : Module R' R := Module.compHom R (↑f.symm : R' →+* R)
  haveI : IsScalarTower R' R M :=
    { smul_assoc := fun x y z => by
        change (f.symm x * y) • z = x • (y • z)
        rw [mul_smul, ← h, f.apply_symm_apply] }
  exact ofRepr <| (b.repr.restrictScalars R').trans <|
    Finsupp.mapRange.linearEquiv (Module.compHom.toLinearEquiv f.symm).symm

Basis transformation under ring isomorphism

Informal description

Given a ring isomorphism $f : R \to R'$ and a basis $b$ for a module $M$ over $R$, if the action of $R$ and $R'$ on $M$ is compatible via $f$ (i.e., $f(c) \cdot x = c \cdot x$ for all $c \in R$ and $x \in M$), then $b$ is also a basis for $M$ as an $R'$-module. The basis vectors remain unchanged under this transformation.

Basis.mapCoeffs_apply theorem

(i : ι) : b.mapCoeffs f h i = b i

Full source

theorem mapCoeffs_apply (i : ι) : b.mapCoeffs f h i = b i :=
  apply_eq_iff.mpr <| by simp

Basis Vectors Remain Unchanged Under Coefficient Mapping: $(b.\text{mapCoeffs}\,f\,h)(i) = b(i)$

Informal description

For any basis $b$ of a module $M$ over a ring $R$, any ring isomorphism $f : R \to R'$, and any index $i \in \iota$, the $i$-th basis vector of the transformed basis $b.\text{mapCoeffs}\,f\,h$ equals the original $i$-th basis vector $b(i)$. In other words, $(b.\text{mapCoeffs}\,f\,h)(i) = b(i)$.

Basis.coe_mapCoeffs theorem

: (b.mapCoeffs f h : ι → M) = b

Full source

@[simp]
theorem coe_mapCoeffs : (b.mapCoeffs f h : ι → M) = b :=
  funext <| b.mapCoeffs_apply f h

Coefficient Mapping Preserves Basis Vectors: $(b.\text{mapCoeffs}\,f\,h) = b$

Informal description

For any basis $b$ of a module $M$ over a ring $R$, any ring isomorphism $f : R \to R'$, and any compatibility condition $h$ ensuring that the scalar multiplication is preserved under $f$, the function representation of the transformed basis $b.\text{mapCoeffs}\,f\,h$ is equal to the original basis $b$ as a function from the index set $\iota$ to $M$.

Basis.reindexRange definition

: Basis (range b) R M

Full source

/-- `b.reindexRange` is a basis indexed by `range b`, the basis vectors themselves. -/
def reindexRange : Basis (range b) R M :=
  haveI := Classical.dec (Nontrivial R)
  if h : Nontrivial R then
    letI := h
    b.reindex (Equiv.ofInjective b (Basis.injective b))
  else
    letI : Subsingleton R := not_nontrivial_iff_subsingleton.mp h
    .ofRepr (Module.subsingletonEquiv R M (range b))

Basis reindexed by its range

Informal description

Given a basis `b : Basis ι R M`, the basis `b.reindexRange` is a basis indexed by the range of `b`, i.e., the set of all basis vectors `{b i | i ∈ ι}`. For each basis vector `b i` in the range, the corresponding basis vector in `b.reindexRange` is `b i` itself. The representation isomorphism of `b.reindexRange` maps any element `x ∈ M` to its coordinates with respect to this new indexing set.

Basis.reindexRange_repr_self theorem

(i : ι) : b.reindexRange.repr (b i) = Finsupp.single ⟨b i, mem_range_self i⟩ 1

Full source

theorem reindexRange_repr_self (i : ι) :
    b.reindexRange.repr (b i) = Finsupp.single ⟨b i, mem_range_self i⟩ 1 :=
  calc
    b.reindexRange.repr (b i) = b.reindexRange.repr (b.reindexRange ⟨b i, mem_range_self i⟩) :=
      congr_arg _ (b.reindexRange_self _ _).symm
    _ = Finsupp.single ⟨b i, mem_range_self i⟩ 1 := b.reindexRange.repr_self _

Coordinate Representation of Basis Vectors under Range Reindexing: $b.\text{reindexRange}.\text{repr}(b(i)) = \text{single}_{\langle b(i), \text{mem\_range\_self } i \rangle}(1)$

Informal description

For any basis $b$ of a module $M$ over a ring $R$ and any index $i \in \iota$, the coordinate representation of the basis vector $b(i)$ under the reindexed basis $b.\text{reindexRange}$ is the finitely supported function that takes the value $1$ at the index $\langle b(i), \text{mem\_range\_self } i \rangle$ (which represents $b(i)$ in the range of $b$) and $0$ elsewhere. In other words, $b.\text{reindexRange}.\text{repr}(b(i)) = \text{single}_{\langle b(i), \text{mem\_range\_self } i \rangle}(1)$.

Basis.reindexRange_apply theorem

(x : range b) : b.reindexRange x = x

Full source

@[simp]
theorem reindexRange_apply (x : range b) : b.reindexRange x = x := by
  rcases x with ⟨bi, ⟨i, rfl⟩⟩
  exact b.reindexRange_self i

Basis Vector Equality in Reindexed Basis

Informal description

For any element $x$ in the range of a basis $b : \text{Basis } \iota R M$, the basis vector $b.\text{reindexRange}(x)$ is equal to $x$ itself.

Basis.reindexRange_repr' theorem

(x : M) {bi : M} {i : ι} (h : b i = bi) : b.reindexRange.repr x ⟨bi, ⟨i, h⟩⟩ = b.repr x i

Full source

theorem reindexRange_repr' (x : M) {bi : M} {i : ι} (h : b i = bi) :
    b.reindexRange.repr x ⟨bi, ⟨i, h⟩⟩ = b.repr x i := by
  nontriviality
  subst h
  apply (b.repr_apply_eq (fun x i => b.reindexRange.repr x ⟨b i, _⟩) _ _ _ x i).symm
  · intro x y
    ext i
    simp only [Pi.add_apply, LinearEquiv.map_add, Finsupp.coe_add]
  · intro c x
    ext i
    simp only [Pi.smul_apply, LinearEquiv.map_smul, Finsupp.coe_smul]
  · intro i
    ext j
    simp only [reindexRange_repr_self]
    apply Finsupp.single_apply_left (f := fun i => (⟨b i, _⟩ : Set.range b))
    exact fun i j h => b.injective (Subtype.mk.inj h)

Equality of Coordinates in Original and Range-Reindexed Basis: $b.\text{reindexRange}.\text{repr}(x) \langle b_i, \langle i, h \rangle \rangle = b.\text{repr}(x)(i)$

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$. For any $x \in M$, any basis vector $b_i \in M$, and any index $i \in \iota$ such that $b(i) = b_i$, the coordinate of $x$ with respect to the basis vector $\langle b_i, \langle i, h \rangle \rangle$ in the reindexed basis $b.\text{reindexRange}$ equals the coordinate of $x$ with respect to $i$ in the original basis $b$. That is, $$ b.\text{reindexRange}.\text{repr}(x) \langle b_i, \langle i, h \rangle \rangle = b.\text{repr}(x)(i). $$

Basis.reindexFinsetRange definition

: Basis (Finset.univ.image b) R M

Full source

/-- `b.reindexFinsetRange` is a basis indexed by `Finset.univ.image b`,
the finite set of basis vectors themselves. -/
def reindexFinsetRange : Basis (Finset.univ.image b) R M :=
  b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv (by simp))

Basis reindexed by the finite set of basis vectors

Informal description

Given a basis `b` indexed by a finite type `ι` for a module `M` over a ring `R`, the basis `b.reindexFinsetRange` is a basis indexed by the finite set of all basis vectors `Finset.univ.image b`. For each basis vector `b i` in this set, the corresponding basis vector in `b.reindexFinsetRange` is `b i` itself. The representation isomorphism of `b.reindexFinsetRange` maps any element `x ∈ M` to its coordinates with respect to this new indexing set.

Basis.reindexFinsetRange_apply theorem

(x : Finset.univ.image b) : b.reindexFinsetRange x = x

Full source

@[simp]
theorem reindexFinsetRange_apply (x : Finset.univ.image b) : b.reindexFinsetRange x = x := by
  rcases x with ⟨bi, hbi⟩
  rcases Finset.mem_image.mp hbi with ⟨i, -, rfl⟩
  exact b.reindexFinsetRange_self i

Reindexed Basis Maps Basis Vectors to Themselves

Informal description

For any element $x$ in the finite set of basis vectors $\text{Finset.univ.image } b$, the basis vector $b.\text{reindexFinsetRange}(x)$ is equal to $x$ itself. In other words, the reindexed basis $b.\text{reindexFinsetRange}$ maps each basis vector in the finite set $\text{Finset.univ.image } b$ to itself.

Basis.reindexFinsetRange_repr_self theorem

(i : ι) : b.reindexFinsetRange.repr (b i) = Finsupp.single ⟨b i, Finset.mem_image_of_mem b (Finset.mem_univ i)⟩ 1

Full source

theorem reindexFinsetRange_repr_self (i : ι) :
    b.reindexFinsetRange.repr (b i) =
      Finsupp.single ⟨b i, Finset.mem_image_of_mem b (Finset.mem_univ i)⟩ 1 := by
  ext ⟨bi, hbi⟩
  rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self]
  simp [Finsupp.single_apply]

Coordinate Representation of Basis Vectors under Finite Range Reindexing

Informal description

For any basis $b$ of a module $M$ over a ring $R$ indexed by a finite type $\iota$, and for any index $i \in \iota$, the coordinate representation of the basis vector $b(i)$ with respect to the reindexed basis $b.\text{reindexFinsetRange}$ is the finitely supported function that takes the value $1$ at the index $\langle b(i), \text{Finset.mem\_image\_of\_mem } b (\text{Finset.mem\_univ } i) \rangle$ (which represents $b(i)$ in the finite set of all basis vectors) and $0$ elsewhere. In mathematical notation: $$b.\text{reindexFinsetRange}.\text{repr}(b(i)) = \text{single}_{\langle b(i), \text{Finset.mem\_image\_of\_mem } b (\text{Finset.mem\_univ } i) \rangle}(1).$$

Basis.constr definition

: (ι → M') ≃ₗ[S] M →ₗ[R] M'

Full source

/-- Construct a linear map given the value at the basis, called `Basis.constr b S f` where `b` is
a basis, `f` is the value of the linear map over the elements of the basis, and `S` is an
extra semiring (typically `S = R` or `S = ℕ`).

This definition is parameterized over an extra `Semiring S`,
such that `SMulCommClass R S M'` holds.
If `R` is commutative, you can set `S := R`; if `R` is not commutative,
you can recover an `AddEquiv` by setting `S := ℕ`.
See library note [bundled maps over different rings].
-/
def constr : (ι → M') ≃ₗ[S] M →ₗ[R] M' where
  toFun f := (Finsupp.linearCombination R id).comp <| Finsupp.lmapDomainFinsupp.lmapDomain R R f ∘ₗ ↑b.repr
  invFun f i := f (b i)
  left_inv f := by
    ext
    simp
  right_inv f := by
    refine b.ext fun i => ?_
    simp
  map_add' f g := by
    refine b.ext fun i => ?_
    simp
  map_smul' c f := by
    refine b.ext fun i => ?_
    simp

Linear map construction from basis vectors

Informal description

Given a basis $b$ of a module $M$ over a ring $R$ indexed by a type $\iota$, and an extra semiring $S$ such that scalar multiplication by $R$ and $S$ commutes on a module $M'$, the function `Basis.constr b S` constructs a linear equivalence between the space of functions $\iota \to M'$ and the space of linear maps $M \to M'$. Specifically, for any function $f : \iota \to M'$, the linear map `Basis.constr b S f` sends each basis vector $b(i)$ to $f(i)$, and extends linearly to all of $M$.

Basis.constr_def theorem

(f : ι → M') : constr (M' := M') b S f = linearCombination R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr

Full source

theorem constr_def (f : ι → M') :
    constr (M' := M') b S f = linearCombinationlinearCombination R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr :=
  rfl

Decomposition of Linear Map Construction via Basis Representation

Informal description

Given a basis $b$ of a module $M$ over a ring $R$ indexed by a type $\iota$, an extra semiring $S$ such that scalar multiplication by $R$ and $S$ commutes on a module $M'$, and a function $f : \iota \to M'$, the linear map constructed from $f$ via the basis $b$ satisfies: \[ \text{constr}_b^S f = \text{linearCombination}_R \text{id} \circ \text{Finsupp.lmapDomain}_R^R f \circ b.\text{repr} \] where: - $\text{linearCombination}_R \text{id}$ is the linear combination map with coefficients given by the identity function, - $\text{Finsupp.lmapDomain}_R^R f$ is the linear map induced by $f$ on finitely supported functions, and - $b.\text{repr}$ is the representation isomorphism of the basis $b$.

Basis.constr_apply theorem

(f : ι → M') (x : M) : constr (M' := M') b S f x = (b.repr x).sum fun b a => a • f b

Full source

theorem constr_apply (f : ι → M') (x : M) :
    constr (M' := M') b S f x = (b.repr x).sum fun b a => a • f b := by
  simp only [constr_def, LinearMap.comp_apply, lmapDomain_apply, linearCombination_apply]
  rw [Finsupp.sum_mapDomain_index] <;> simp [add_smul]

Evaluation of Linear Map Constructed from Basis Vectors

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$, indexed by a type $\iota$, and let $S$ be a semiring such that scalar multiplication by $R$ and $S$ commutes on a module $M'$. For any function $f : \iota \to M'$ and any element $x \in M$, the linear map $\text{constr}_b^S f$ evaluated at $x$ is equal to the sum $\sum_{i \in \iota} a_i \cdot f(i)$, where $(a_i)_{i \in \iota}$ are the coordinates of $x$ with respect to the basis $b$.

Basis.constr_basis theorem

(f : ι → M') (i : ι) : (constr (M' := M') b S f : M → M') (b i) = f i

Full source

@[simp]
theorem constr_basis (f : ι → M') (i : ι) : (constr (M' := M') b S f : M → M') (b i) = f i := by
  simp [Basis.constr_apply, b.repr_self]

Linear Map Construction on Basis Vectors: $(\text{constr}_b^S f)(b(i)) = f(i)$

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$, indexed by a type $\iota$, and let $S$ be a semiring such that scalar multiplication by $R$ and $S$ commutes on a module $M'$. For any function $f : \iota \to M'$ and any index $i \in \iota$, the linear map $\text{constr}_b^S f$ evaluated at the basis vector $b(i)$ equals $f(i)$, i.e., \[ (\text{constr}_b^S f)(b(i)) = f(i). \]

Basis.constr_eq theorem

{g : ι → M'} {f : M →ₗ[R] M'} (h : ∀ i, g i = f (b i)) : constr (M' := M') b S g = f

Full source

theorem constr_eq {g : ι → M'} {f : M →ₗ[R] M'} (h : ∀ i, g i = f (b i)) :
    constr (M' := M') b S g = f :=
  b.ext fun i => (b.constr_basis S g i).trans (h i)

Equality of Linear Maps Constructed from Basis Vectors: $\text{constr}_b^S g = f$ if $g(i) = f(b(i))$ for all $i$

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by a type $\iota$, and let $M'$ be another module over $R$ where scalar multiplication by $R$ and a semiring $S$ commutes. Given functions $g : \iota \to M'$ and $f : M \to M'$ such that $g(i) = f(b(i))$ for all $i \in \iota$, the linear map constructed from $g$ via the basis $b$ is equal to $f$, i.e., \[ \text{constr}_b^S g = f. \]

Basis.constr_self theorem

(f : M →ₗ[R] M') : (constr (M' := M') b S fun i => f (b i)) = f

Full source

theorem constr_self (f : M →ₗ[R] M') : (constr (M' := M') b S fun i => f (b i)) = f :=
  b.constr_eq S fun _ => rfl

Linear Map Construction from Basis Vectors Recovers Original Map

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by a type $\iota$, and let $M'$ be another module over $R$ where scalar multiplication by $R$ and a semiring $S$ commutes. For any linear map $f : M \to M'$, the linear map constructed from the function $i \mapsto f(b(i))$ via the basis $b$ is equal to $f$ itself, i.e., \[ \text{constr}_b^S (i \mapsto f(b(i))) = f. \]

Basis.constr_range theorem

{f : ι → M'} : LinearMap.range (constr (M' := M') b S f) = span R (range f)

Full source

theorem constr_range {f : ι → M'} :
    LinearMap.range (constr (M' := M') b S f) = span R (range f) := by
  rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]

Range of Linear Map Constructed from Basis Vectors Equals Span of Their Images

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by a type $\iota$, and let $M'$ be another module over $R$ where scalar multiplication by $R$ and a semiring $S$ commutes. For any function $f : \iota \to M'$, the range of the linear map constructed from $f$ via the basis $b$ is equal to the $R$-linear span of the range of $f$. In other words: \[ \text{range}(\text{constr}_b^S f) = \text{span}_R (\text{range } f) \]

Basis.constr_comp theorem

(f : M' →ₗ[R] M') (v : ι → M') : constr (M' := M') b S (f ∘ v) = f.comp (constr (M' := M') b S v)

Full source

@[simp]
theorem constr_comp (f : M' →ₗ[R] M') (v : ι → M') :
    constr (M' := M') b S (f ∘ v) = f.comp (constr (M' := M') b S v) :=
  b.ext fun i => by simp only [Basis.constr_basis, LinearMap.comp_apply, Function.comp]

Composition of Linear Maps Preserves Basis Construction: $\text{constr}_b^S (f \circ v) = f \circ \text{constr}_b^S v$

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$, and let $M'$ be another module over $R$ where scalar multiplication by $R$ and a semiring $S$ commutes. For any linear map $f : M' \to M'$ and any function $v : \iota \to M'$, the linear map constructed from the composition $f \circ v$ via the basis $b$ equals the composition of $f$ with the linear map constructed from $v$ via $b$. That is, \[ \text{constr}_b^S (f \circ v) = f \circ \text{constr}_b^S v. \]

Basis.constr_apply_fintype theorem

 [Fintype ι] (b : Basis ι R M) (f : ι → M') (x : M) : (constr (M' := M') b S f : M → M') x = ∑ i, b.equivFun x i • f i

Full source

@[simp]
theorem constr_apply_fintype [Fintype ι] (b : Basis ι R M) (f : ι → M') (x : M) :
    (constr (M' := M') b S f : M → M') x = ∑ i, b.equivFun x i • f i := by
  simp [b.constr_apply, b.equivFun_apply, Finsupp.sum_fintype]

Finite Basis Construction Formula: $\text{constr}_b^S f(x) = \sum_i (b.\text{equivFun } x)(i) \cdot f(i)$

Informal description

Let $\iota$ be a finite type, $R$ a ring, $M$ an $R$-module with basis $b : \text{Basis } \iota R M$, and $M'$ another $R$-module where scalar multiplication by $R$ and $S$ commutes. For any function $f : \iota \to M'$ and any $x \in M$, the linear map $\text{constr}_b^S f$ evaluated at $x$ is given by $\sum_{i \in \iota} (b.\text{equivFun } x)(i) \cdot f(i)$, where $b.\text{equivFun } x$ represents the coordinates of $x$ in the basis $b$.

Basis.equiv definition

: M ≃ₗ[R] M'

Full source

/-- If `b` is a basis for `M` and `b'` a basis for `M'`, and the index types are equivalent,
`b.equiv b' e` is a linear equivalence `M ≃ₗ[R] M'`, mapping `b i` to `b' (e i)`. -/
protected def equiv : M ≃ₗ[R] M' :=
  b.repr.trans (b'.reindex e.symm).repr.symm

Linear equivalence induced by basis equivalence

Informal description

Given a basis $b$ for a module $M$ over a ring $R$ indexed by $\iota$, a basis $b'$ for a module $M'$ over $R$ indexed by $\iota'$, and an equivalence $e : \iota \simeq \iota'$ between the index types, the linear equivalence $\text{Basis.equiv } b \ b' \ e : M \simeq_{R} M'$ maps each basis vector $b i$ to $b' (e i)$. This is implemented as the composition of the coordinate representation isomorphism of $b$ with the inverse of the coordinate representation isomorphism of the reindexed basis $b' \circ e^{-1}$.

Basis.equiv_apply theorem

: b.equiv b' e (b i) = b' (e i)

Full source

@[simp]
theorem equiv_apply : b.equiv b' e (b i) = b' (e i) := by simp [Basis.equiv]

Action of Basis Equivalence on Basis Vectors: $b.\text{equiv}\, b'\, e(b(i)) = b'(e(i))$

Informal description

Given a basis $b$ for an $R$-module $M$ indexed by $\iota$, a basis $b'$ for an $R$-module $M'$ indexed by $\iota'$, and an equivalence $e : \iota \simeq \iota'$ between the index types, the linear equivalence $b.\text{equiv}\, b'\, e$ maps each basis vector $b(i)$ to the corresponding basis vector $b'(e(i))$ in $M'$.

Basis.equiv_refl theorem

: b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M

Full source

@[simp]
theorem equiv_refl : b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M :=
  b.ext' fun i => by simp

Identity Basis Equivalence Yields Identity Linear Map

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$. The linear equivalence induced by the basis $b$ and the identity equivalence on $\iota$ is equal to the identity linear equivalence on $M$, i.e., $b.\text{equiv}\, b\, \text{id} = \text{id}_M$.

Basis.equiv_symm theorem

: (b.equiv b' e).symm = b'.equiv b e.symm

Full source

@[simp]
theorem equiv_symm : (b.equiv b' e).symm = b'.equiv b e.symm :=
  b'.ext' fun i => (b.equiv b' e).injective (by simp)

Inverse of Basis Equivalence Equals Equivalence with Inverse Index Map

Informal description

Given a basis $b$ for an $R$-module $M$ indexed by $\iota$, a basis $b'$ for an $R$-module $M'$ indexed by $\iota'$, and an equivalence $e : \iota \simeq \iota'$ between the index types, the inverse of the linear equivalence $\text{Basis.equiv } b \ b' \ e$ is equal to the linear equivalence $\text{Basis.equiv } b' \ b \ e^{-1}$.

Basis.equiv_trans theorem

 {ι'' : Type*} (b'' : Basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι'') :
  (b.equiv b' e).trans (b'.equiv b'' e') = b.equiv b'' (e.trans e')

Full source

@[simp]
theorem equiv_trans {ι'' : Type*} (b'' : Basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι'') :
    (b.equiv b' e).trans (b'.equiv b'' e') = b.equiv b'' (e.trans e') :=
  b.ext' fun i => by simp

Transitivity of Basis Equivalence: $(b.\text{equiv}\, b'\, e) \circ (b'.\text{equiv}\, b''\, e') = b.\text{equiv}\, b''\, (e \circ e')$

Informal description

Let $b$, $b'$, and $b''$ be bases for $R$-modules $M$, $M'$, and $M''$ indexed by $\iota$, $\iota'$, and $\iota''$ respectively. Given equivalences $e : \iota \simeq \iota'$ and $e' : \iota' \simeq \iota''$, the composition of the linear equivalences $b.\text{equiv}\, b'\, e$ and $b'.\text{equiv}\, b''\, e'$ is equal to the linear equivalence $b.\text{equiv}\, b''\, (e \circ e')$. In other words, the following diagram commutes: $$M \xrightarrow{b.\text{equiv}\, b'\, e} M' \xrightarrow{b'.\text{equiv}\, b''\, e'} M''$$ is equal to: $$M \xrightarrow{b.\text{equiv}\, b''\, (e \circ e')} M''$$

Basis.map_equiv theorem

(b : Basis ι R M) (b' : Basis ι' R M') (e : ι ≃ ι') : b.map (b.equiv b' e) = b'.reindex e.symm

Full source

@[simp]
theorem map_equiv (b : Basis ι R M) (b' : Basis ι' R M') (e : ι ≃ ι') :
    b.map (b.equiv b' e) = b'.reindex e.symm := by
  ext i
  simp

Compatibility of Basis Mapping and Reindexing via Equivalence

Informal description

Let $b$ be a basis for an $R$-module $M$ indexed by $\iota$, and $b'$ a basis for an $R$-module $M'$ indexed by $\iota'$. Given an equivalence $e : \iota \simeq \iota'$ between the index types, the basis obtained by first applying the linear equivalence $\text{Basis.equiv } b \ b' \ e$ to $b$ and then mapping via $\text{Basis.map}$ is equal to the basis obtained by reindexing $b'$ using the inverse equivalence $e^{-1}$. In other words, the following diagram commutes: $$b \xrightarrow{\text{map (equiv } b \ b' \ e)} b'.reindex e^{-1}$$

Basis.equiv' definition

 (f : M → M') (g : M' → M) (hf : ∀ i, f (b i) ∈ range b') (hg : ∀ i, g (b' i) ∈ range b) (hgf : ∀ i, g (f (b i)) = b i)
  (hfg : ∀ i, f (g (b' i)) = b' i) : M ≃ₗ[R] M'

Full source

/-- If `b` is a basis for `M` and `b'` a basis for `M'`,
and `f`, `g` form a bijection between the basis vectors,
`b.equiv' b' f g hf hg hgf hfg` is a linear equivalence `M ≃ₗ[R] M'`, mapping `b i` to `f (b i)`.
-/
def equiv' (f : M → M') (g : M' → M) (hf : ∀ i, f (b i) ∈ range b') (hg : ∀ i, g (b' i) ∈ range b)
    (hgf : ∀ i, g (f (b i)) = b i) (hfg : ∀ i, f (g (b' i)) = b' i) : M ≃ₗ[R] M' :=
  { constr (M' := M') b R (f ∘ b) with
    invFun := constr (M' := M) b' R (g ∘ b')
    left_inv :=
      have : (constr (M' := M) b' R (g ∘ b')).comp (constr (M' := M') b R (f ∘ b)) = LinearMap.id :=
        b.ext fun i =>
          Exists.elim (hf i) fun i' hi' => by
            rw [LinearMap.comp_apply, b.constr_basis, Function.comp_apply, ← hi', b'.constr_basis,
              Function.comp_apply, hi', hgf, LinearMap.id_apply]
      fun x => congr_arg (fun h : M →ₗ[R] M => h x) this
    right_inv :=
      have : (constr (M' := M') b R (f ∘ b)).comp (constr (M' := M) b' R (g ∘ b')) = LinearMap.id :=
        b'.ext fun i =>
          Exists.elim (hg i) fun i' hi' => by
            rw [LinearMap.comp_apply, b'.constr_basis, Function.comp_apply, ← hi', b.constr_basis,
              Function.comp_apply, hi', hfg, LinearMap.id_apply]
      fun x => congr_arg (fun h : M' →ₗ[R] M' => h x) this }

Linear equivalence between modules induced by a bijection of basis vectors

Informal description

Given two bases $b$ and $b'$ for modules $M$ and $M'$ respectively over a ring $R$, and functions $f : M \to M'$ and $g : M' \to M$ that form a bijection between the basis vectors (i.e., $f$ maps each basis vector $b(i)$ to some basis vector in $b'$, $g$ maps each basis vector $b'(i)$ to some basis vector in $b$, and they satisfy $g(f(b(i))) = b(i)$ and $f(g(b'(i))) = b'(i)$ for all $i$), then `Basis.equiv' b b' f g hf hg hgf hfg` constructs a linear equivalence between $M$ and $M'$ that maps each basis vector $b(i)$ to $f(b(i))$.

Basis.equiv'_apply theorem

(f : M → M') (g : M' → M) (hf hg hgf hfg) (i : ι) : b.equiv' b' f g hf hg hgf hfg (b i) = f (b i)

Full source

@[simp]
theorem equiv'_apply (f : M → M') (g : M' → M) (hf hg hgf hfg) (i : ι) :
    b.equiv' b' f g hf hg hgf hfg (b i) = f (b i) :=
  b.constr_basis R _ _

Action of Induced Linear Equivalence on Basis Vectors: $\text{equiv'}_b^{b'} f g (b(i)) = f(b(i))$

Informal description

Let $b$ and $b'$ be bases for modules $M$ and $M'$ respectively over a ring $R$, indexed by types $\iota$ and $\iota'$. Given functions $f : M \to M'$ and $g : M' \to M$ that satisfy: 1. For each $i \in \iota$, $f(b(i))$ is in the range of $b'$, 2. For each $j \in \iota'$, $g(b'(j))$ is in the range of $b$, 3. For each $i \in \iota$, $g(f(b(i))) = b(i)$, 4. For each $j \in \iota'$, $f(g(b'(j))) = b'(j)$, then the linear equivalence $\text{equiv'}_b^{b'} f g$ constructed from these data satisfies $\text{equiv'}_b^{b'} f g (b(i)) = f(b(i))$ for all $i \in \iota$.

Basis.equiv'_symm_apply theorem

(f : M → M') (g : M' → M) (hf hg hgf hfg) (i : ι') : (b.equiv' b' f g hf hg hgf hfg).symm (b' i) = g (b' i)

Full source

@[simp]
theorem equiv'_symm_apply (f : M → M') (g : M' → M) (hf hg hgf hfg) (i : ι') :
    (b.equiv' b' f g hf hg hgf hfg).symm (b' i) = g (b' i) :=
  b'.constr_basis R _ _

Inverse of Basis-Induced Linear Equivalence on Basis Vectors: $(\text{equiv'}\ b\ b'\ f\ g)^{-1}(b'(j)) = g(b'(j))$

Informal description

Let $b$ and $b'$ be bases for $R$-modules $M$ and $M'$ respectively, indexed by types $\iota$ and $\iota'$. Given functions $f : M \to M'$ and $g : M' \to M$ that satisfy: 1. $f(b(i))$ is in the range of $b'$ for all $i \in \iota$ 2. $g(b'(j))$ is in the range of $b$ for all $j \in \iota'$ 3. $g(f(b(i))) = b(i)$ for all $i \in \iota$ 4. $f(g(b'(j))) = b'(j)$ for all $j \in \iota'$ then for any $j \in \iota'$, the inverse of the linear equivalence $\text{equiv'}\ b\ b'\ f\ g\ hf\ hg\ hgf\ hfg$ applied to $b'(j)$ equals $g(b'(j))$.

Basis.sum_repr_mul_repr theorem

{ι'} [Fintype ι'] (b' : Basis ι' R M) (x : M) (i : ι) : (∑ j : ι', b.repr (b' j) i * b'.repr x j) = b.repr x i

Full source

theorem sum_repr_mul_repr {ι'} [Fintype ι'] (b' : Basis ι' R M) (x : M) (i : ι) :
    (∑ j : ι', b.repr (b' j) i * b'.repr x j) = b.repr x i := by
  conv_rhs => rw [← b'.sum_repr x]
  simp_rw [map_sum, map_smul, Finset.sum_apply']
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]

Coordinate Transformation Formula for Finite Bases: $\sum_j (b(b'(j)))_i \cdot (b'(x))_j = (b(x))_i$

Informal description

Let $M$ be a module over a ring $R$ with two finite bases $b$ indexed by $\iota$ and $b'$ indexed by $\iota'$. For any vector $x \in M$ and any index $i \in \iota$, the sum over $j \in \iota'$ of the product of the $i$-th coordinate of $b'(j)$ in basis $b$ and the $j$-th coordinate of $x$ in basis $b'$ equals the $i$-th coordinate of $x$ in basis $b$. That is: \[ \sum_{j \in \iota'} (b.\text{repr}(b'(j)))(i) \cdot (b'.\text{repr}(x))(j) = (b.\text{repr}(x))(i) \]

Basis.coord definition

: M →ₗ[R] R

Full source

/-- `b.coord i` is the linear function giving the `i`'th coordinate of a vector
with respect to the basis `b`.

`b.coord i` is an element of the dual space. In particular, for
finite-dimensional spaces it is the `ι`th basis vector of the dual space.
-/
@[simps!]
def coord : M →ₗ[R] R :=
  Finsupp.lapplyFinsupp.lapply i ∘ₗ ↑b.repr

Coordinate function with respect to a basis

Informal description

For a basis $ b $ of a module $ M $ over a ring $ R $ indexed by $ \iota $, the linear function $ b.\text{coord}\, i $ maps a vector $ x \in M $ to its $ i $-th coordinate with respect to the basis $ b $. This function is an element of the dual space of $ M $, and for finite-dimensional spaces, it corresponds to the $ i $-th basis vector of the dual space.

Basis.forall_coord_eq_zero_iff theorem

{x : M} : (∀ i, b.coord i x = 0) ↔ x = 0

Full source

theorem forall_coord_eq_zero_iff {x : M} : (∀ i, b.coord i x = 0) ↔ x = 0 :=
  Iff.trans (by simp only [b.coord_apply, DFunLike.ext_iff, Finsupp.zero_apply])
    b.repr.map_eq_zero_iff

Vanishing of All Coordinates Implies Zero Vector

Informal description

For any vector $x$ in a module $M$ with basis $b$ over a ring $R$, all coordinate functions $b.\text{coord}\, i$ evaluated at $x$ are zero if and only if $x$ is the zero vector. That is, $(\forall i, b.\text{coord}\, i\, x = 0) \leftrightarrow x = 0$.

Basis.sumCoords definition

: M →ₗ[R] R

Full source

/-- The sum of the coordinates of an element `m : M` with respect to a basis. -/
noncomputable def sumCoords : M →ₗ[R] R :=
  (Finsupp.lsum ℕ fun _ => LinearMap.id) ∘ₗ (b.repr : M →ₗ[R] ι →₀ R)

Sum of coordinates with respect to a basis

Informal description

The linear map that sends an element $m \in M$ to the sum of its coordinates with respect to the basis $b$. This is constructed by composing the representation isomorphism $b.\text{repr} : M \to \iota \to_{\text{f}} R$ (which gives the coordinates of $m$) with the linear map that sums the coordinates (using the identity map on $R$ for each coordinate).

Basis.coe_sumCoords theorem

: (b.sumCoords : M → R) = fun m => (b.repr m).sum fun _ => id

Full source

@[simp]
theorem coe_sumCoords : (b.sumCoords : M → R) = fun m => (b.repr m).sum fun _ => id :=
  rfl

Sum of Coordinates via Basis Representation

Informal description

For any element $m$ in the module $M$ over the ring $R$, the sum of its coordinates with respect to the basis $b$ is equal to the sum of the values of the finitely supported function obtained by applying the representation isomorphism $b.\text{repr}$ to $m$, where each coordinate is mapped via the identity function.

Basis.coe_sumCoords_of_fintype theorem

[Fintype ι] : (b.sumCoords : M → R) = ∑ i, b.coord i

Full source

@[simp high]
theorem coe_sumCoords_of_fintype [Fintype ι] : (b.sumCoords : M → R) = ∑ i, b.coord i := by
  ext m
  simp only [sumCoords, Finsupp.sum_fintype, LinearMap.id_coe, LinearEquiv.coe_coe, coord_apply,
    id, Fintype.sum_apply, imp_true_iff, Finsupp.coe_lsum, LinearMap.coe_comp, comp_apply,
    LinearMap.coeFn_sum]

Sum of Coordinates Equals Sum of Coordinate Functions for Finite Basis

Informal description

For a finite index set $\iota$, the sum of coordinates function with respect to a basis $b$ of a module $M$ over a ring $R$ is equal to the sum of the coordinate functions, i.e., for any $m \in M$, we have $b.\text{sumCoords}(m) = \sum_{i \in \iota} b.\text{coord}_i(m)$.

Basis.sumCoords_self_apply theorem

: b.sumCoords (b i) = 1

Full source

@[simp]
theorem sumCoords_self_apply : b.sumCoords (b i) = 1 := by
  simp only [Basis.sumCoords, LinearMap.id_coe, LinearEquiv.coe_coe, id, Basis.repr_self,
    Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp, Finsupp.sum_single_index]

Sum of Coordinates of Basis Vector Equals One

Informal description

For any basis $b$ of a module $M$ over a ring $R$ and any index $i \in \iota$, the sum of the coordinates of the basis vector $b(i)$ with respect to $b$ is equal to $1$.

Basis.dvd_coord_smul theorem

(i : ι) (m : M) (r : R) : r ∣ b.coord i (r • m)

Full source

theorem dvd_coord_smul (i : ι) (m : M) (r : R) : r ∣ b.coord i (r • m) :=
  ⟨b.coord i m, by simp⟩

Divisibility of Scaled Coordinate by Scalar in Basis

Informal description

For any basis $b$ of a module $M$ over a ring $R$, any index $i \in \iota$, any vector $m \in M$, and any scalar $r \in R$, the coordinate of $r \cdot m$ with respect to the basis vector $b_i$ is divisible by $r$, i.e., $r$ divides $b_i^*(r \cdot m)$ where $b_i^*$ is the $i$-th coordinate function.

Basis.coord_repr_symm theorem

(b : Basis ι R M) (i : ι) (f : ι →₀ R) : b.coord i (b.repr.symm f) = f i

Full source

theorem coord_repr_symm (b : Basis ι R M) (i : ι) (f : ι →₀ R) :
    b.coord i (b.repr.symm f) = f i := by
  simp only [repr_symm_apply, coord_apply, repr_linearCombination]

Coordinate Extraction from Inverse Basis Representation

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$ indexed by $\iota$. For any index $i \in \iota$ and any finitely supported function $f : \iota \to_{\text{f}} R$, the $i$-th coordinate of the vector $b.\text{repr}^{-1}(f)$ (the preimage of $f$ under the coordinate representation isomorphism) equals $f(i)$. In other words: $$ b_i^*(b^{-1}(f)) = f(i) $$ where $b_i^*$ denotes the $i$-th coordinate function and $b^{-1}$ is the inverse of the coordinate representation isomorphism.

Basis.coe_sumCoords_eq_finsum theorem

: (b.sumCoords : M → R) = fun m => ∑ᶠ i, b.coord i m

Full source

theorem coe_sumCoords_eq_finsum : (b.sumCoords : M → R) = fun m => ∑ᶠ i, b.coord i m := by
  ext m
  simp only [Basis.sumCoords, Basis.coord, Finsupp.lapply_apply, LinearMap.id_coe,
    LinearEquiv.coe_coe, Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp,
    finsum_eq_sum _ (b.repr m).finite_support, Finsupp.sum, Finset.finite_toSet_toFinset, id,
    Finsupp.fun_support_eq]

Sum of Coordinates as Finite Sum of Basis Coordinates

Informal description

For a basis $b$ of a module $M$ over a ring $R$, the linear map $b.\text{sumCoords} \colon M \to R$ is given by the function that sends each $m \in M$ to the sum of its coordinates with respect to $b$, i.e., $\sum_{i} (b.\text{coord}\, i) m$.

Basis.sumCoords_reindex theorem

: (b.reindex e).sumCoords = b.sumCoords

Full source

@[simp]
theorem sumCoords_reindex : (b.reindex e).sumCoords = b.sumCoords := by
  ext x
  simp only [coe_sumCoords, repr_reindex]
  exact Finsupp.sum_mapDomain_index (fun _ => rfl) fun _ _ _ => rfl

Invariance of Sum of Coordinates under Basis Reindexing

Informal description

Let $b$ be a basis for a module $M$ over a ring $R$ indexed by $\iota$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. Then the sum of coordinates linear map for the reindexed basis $b.\text{reindex}\, e$ is equal to the sum of coordinates linear map for the original basis $b$, i.e., $$(b.\text{reindex}\, e).\text{sumCoords} = b.\text{sumCoords}.$$

Basis.coord_equivFun_symm theorem

[Finite ι] (b : Basis ι R M) (i : ι) (f : ι → R) : b.coord i (b.equivFun.symm f) = f i

Full source

theorem coord_equivFun_symm [Finite ι] (b : Basis ι R M) (i : ι) (f : ι → R) :
    b.coord i (b.equivFun.symm f) = f i :=
  b.coord_repr_symm i (Finsupp.equivFunOnFinite.symm f)

Coordinate Extraction via Basis Inverse for Finite-Dimensional Modules

Informal description

Let $M$ be a module over a ring $R$ with a finite basis $b$ indexed by $\iota$. For any index $i \in \iota$ and any function $f : \iota \to R$, the $i$-th coordinate of the vector $b^{-1}(f)$ (the preimage of $f$ under the coordinate equivalence) is equal to $f(i)$. In other words: $$ b_i^*(b^{-1}(f)) = f(i) $$ where $b_i^*$ denotes the $i$-th coordinate function and $b^{-1}$ is the inverse of the coordinate equivalence.

Mathlib.LinearAlgebra.Basis.Defs

Main definitions

Main results

Implementation notes

Tags