Mathlib.LinearAlgebra.Basis.Fin

Basis.mkFinCons definition

 {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R N) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0)
  (hsp : ∀ z : M, ∃ c : R, z + c • y ∈ N) : Basis (Fin (n + 1)) R M

Full source

/-- Let `b` be a basis for a submodule `N` of `M`. If `y : M` is linear independent of `N`
and `y` and `N` together span the whole of `M`, then there is a basis for `M`
whose basis vectors are given by `Fin.cons y b`. -/
noncomputable def mkFinCons {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R N)
    (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z : M, ∃ c : R, z + c • y ∈ N) :
    Basis (Fin (n + 1)) R M :=
  have span_b : Submodule.span R (Set.range (N.subtype ∘ b)) = N := by
    rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
  Basis.mk (v := Fin.cons y (N.subtype ∘ b))
    ((b.linearIndependent.map' N.subtype (Submodule.ker_subtype _)).fin_cons' _ _
      (by
        rintro c ⟨x, hx⟩ hc
        rw [span_b] at hx
        exact hli c x hx hc))
    fun x _ => by
      rw [Fin.range_cons, Submodule.mem_span_insert', span_b]
      exact hsp x

Basis extension by a linearly independent vector

Informal description

Given a submodule $N$ of $M$ with a basis $b$ indexed by $\text{Fin } n$, a vector $y \in M$ that is linearly independent of $N$ (i.e., for any scalar $c$ and any $x \in N$, $c y + x = 0$ implies $c = 0$), and such that $y$ and $N$ together span $M$ (i.e., for any $z \in M$, there exists a scalar $c$ such that $z + c y \in N$), then there exists a basis for $M$ indexed by $\text{Fin } (n+1)$ whose vectors are given by $\text{Fin.cons } y b$.

Basis.coe_mkFinCons theorem

 {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R N) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0)
  (hsp : ∀ z : M, ∃ c : R, z + c • y ∈ N) : (mkFinCons y b hli hsp : Fin (n + 1) → M) = Fin.cons y ((↑) ∘ b)

Full source

@[simp]
theorem coe_mkFinCons {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R N)
    (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z : M, ∃ c : R, z + c • y ∈ N) :
    (mkFinCons y b hli hsp : Fin (n + 1) → M) = Fin.cons y ((↑) ∘ b) := by
  unfold mkFinCons
  exact coe_mk (v := Fin.cons y (N.subtype ∘ b)) _ _

Basis Construction via Linear Extension Preserves Vectors

Informal description

Let $M$ be a module over a ring $R$, $N$ a submodule of $M$ with a basis $b$ indexed by $\text{Fin } n$, and $y \in M$ a vector such that: 1. $y$ is linearly independent of $N$ (i.e., for any scalar $c \in R$ and any $x \in N$, $c y + x = 0$ implies $c = 0$), 2. $y$ and $N$ together span $M$ (i.e., for any $z \in M$, there exists $c \in R$ such that $z + c y \in N$). Then the basis constructed by `mkFinCons` satisfies $(\text{mkFinCons}\ y\ b\ hli\ hsp)_i = \text{Fin.cons}\ y\ (b \circ \uparrow)_i$ for all $i \in \text{Fin } (n+1)$.

Basis.mkFinConsOfLE definition

 {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R N) (hNO : N ≤ O)
  (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ c : R, z + c • y ∈ N) : Basis (Fin (n + 1)) R O

Full source

/-- Let `b` be a basis for a submodule `N ≤ O`. If `y ∈ O` is linear independent of `N`
and `y` and `N` together span the whole of `O`, then there is a basis for `O`
whose basis vectors are given by `Fin.cons y b`. -/
noncomputable def mkFinConsOfLE {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O)
    (b : Basis (Fin n) R N) (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0)
    (hsp : ∀ z ∈ O, ∃ c : R, z + c • y ∈ N) : Basis (Fin (n + 1)) R O :=
  mkFinCons ⟨y, yO⟩ (b.map (Submodule.comapSubtypeEquivOfLe hNO).symm)
    (fun c x hc hx => hli c x (Submodule.mem_comap.mp hc) (congr_arg ((↑) : O → M) hx))
    fun z => hsp z z.2

Basis extension by a linearly independent vector in a submodule

Informal description

Given a submodule $N$ of $M$ with a basis $b$ indexed by $\text{Fin } n$, a vector $y \in O \subseteq M$ that is linearly independent of $N$ (i.e., for any scalar $c$ and any $x \in N$, $c y + x = 0$ implies $c = 0$), and such that $y$ and $N$ together span $O$ (i.e., for any $z \in O$, there exists a scalar $c$ such that $z + c y \in N$), then there exists a basis for $O$ indexed by $\text{Fin } (n+1)$ whose vectors are given by $\text{Fin.cons } y b$.

Basis.coe_mkFinConsOfLE theorem

 {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R N) (hNO : N ≤ O)
  (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ c : R, z + c • y ∈ N) :
  (mkFinConsOfLE y yO b hNO hli hsp : Fin (n + 1) → O) = Fin.cons ⟨y, yO⟩ (Submodule.inclusion hNO ∘ b)

Full source

@[simp]
theorem coe_mkFinConsOfLE {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R N)
    (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0)
    (hsp : ∀ z ∈ O, ∃ c : R, z + c • y ∈ N) :
    (mkFinConsOfLE y yO b hNO hli hsp : Fin (n + 1) → O) =
      Fin.cons ⟨y, yO⟩ (Submodule.inclusionSubmodule.inclusion hNO ∘ b) :=
  coe_mkFinCons _ _ _ _

Basis Extension Formula via Linear Independence and Spanning Condition

Informal description

Let $M$ be a module over a ring $R$, $N$ and $O$ submodules of $M$ with $N \subseteq O$, and $y \in O$ a vector. Suppose: 1. $y$ is linearly independent of $N$ (i.e., for any scalar $c \in R$ and any $x \in N$, $c y + x = 0$ implies $c = 0$), 2. $y$ and $N$ together span $O$ (i.e., for any $z \in O$, there exists $c \in R$ such that $z + c y \in N$). Given a basis $b$ of $N$ indexed by $\text{Fin } n$, the basis vectors of the extended basis $\text{mkFinConsOfLE}\ y\ yO\ b\ hNO\ hli\ hsp$ for $O$ (indexed by $\text{Fin } (n+1)$) are given by: - The first vector is $y$ (considered as an element of $O$ via $yO$), - The remaining vectors are the images of $b$ under the inclusion map $N \hookrightarrow O$.

Basis.finTwoProd definition

(R : Type*) [Semiring R] : Basis (Fin 2) R (R × R)

Full source

/-- The basis of `R × R` given by the two vectors `(1, 0)` and `(0, 1)`. -/
protected def finTwoProd (R : Type*) [Semiring R] : Basis (Fin 2) R (R × R) :=
  Basis.ofEquivFun (LinearEquiv.finTwoArrow R R).symm

Standard basis of $R \times R$ indexed by $\text{Fin } 2$

Informal description

The basis of the module $R \times R$ over a semiring $R$ indexed by the two-element type $\text{Fin } 2$, consisting of the vectors $(1, 0)$ and $(0, 1)$. This basis is constructed using the linear equivalence between functions from $\text{Fin } 2$ to $R$ and the product module $R \times R$.

Basis.finTwoProd_zero theorem

(R : Type*) [Semiring R] : Basis.finTwoProd R 0 = (1, 0)

Full source

@[simp]
theorem finTwoProd_zero (R : Type*) [Semiring R] : Basis.finTwoProd R 0 = (1, 0) := by
  simp [Basis.finTwoProd, LinearEquiv.finTwoArrow]

First Basis Vector of $R \times R$ is $(1, 0)$

Informal description

For any semiring $R$, the first basis vector of the standard basis of $R \times R$ indexed by $\text{Fin } 2$ is $(1, 0)$. That is, if $b$ is the basis constructed by `Basis.finTwoProd R`, then $b(0) = (1, 0)$.

Basis.finTwoProd_one theorem

(R : Type*) [Semiring R] : Basis.finTwoProd R 1 = (0, 1)

Full source

@[simp]
theorem finTwoProd_one (R : Type*) [Semiring R] : Basis.finTwoProd R 1 = (0, 1) := by
  simp [Basis.finTwoProd, LinearEquiv.finTwoArrow]

Second Basis Vector in Standard Basis of $R \times R$

Informal description

For any semiring $R$, the basis vector indexed by $1$ in the standard basis of $R \times R$ is equal to $(0, 1)$.

Basis.coe_finTwoProd_repr theorem

{R : Type*} [Semiring R] (x : R × R) : ⇑((Basis.finTwoProd R).repr x) = ![x.fst, x.snd]

Full source

@[simp]
theorem coe_finTwoProd_repr {R : Type*} [Semiring R] (x : R × R) :
    ⇑((Basis.finTwoProd R).repr x) = ![x.fst, x.snd] :=
  rfl

Representation of Elements in Standard Basis of $R \times R$ via Components

Informal description

For any semiring $R$ and any element $x = (x_1, x_2) \in R \times R$, the function representation of $x$ in the standard basis of $R \times R$ indexed by $\text{Fin } 2$ is equal to the function mapping $0$ to $x_1$ and $1$ to $x_2$, i.e., $\text{repr}(x)(i) = x_i$ for $i \in \{0,1\}$.