Mathlib.LinearAlgebra.Basis.VectorSpace

Basis.extend definition

(hs : LinearIndepOn K id s) : Basis (hs.extend (subset_univ s)) K V

Full source

/-- If `s` is a linear independent set of vectors, we can extend it to a basis. -/
noncomputable def extend (hs : LinearIndepOn K id s) :
    Basis (hs.extend (subset_univ s)) K V :=
  Basis.mk
    (hs.linearIndepOn_extend _).linearIndependent_restrict
    (SetLike.coe_subset_coe.mp <| by simpa using hs.subset_span_extend (subset_univ s))

Extension of a linearly independent set to a basis

Informal description

Given a field $K$ and a vector space $V$ over $K$, if $s$ is a linearly independent subset of $V$, then `Basis.extend hs` constructs a basis for $V$ by extending $s$ to a maximal linearly independent set (using the axiom of choice). The resulting basis is indexed by the extended set and satisfies that each vector in $s$ is mapped to itself under the basis map.

Basis.extend_apply_self theorem

(hs : LinearIndepOn K id s) (x : hs.extend _) : Basis.extend hs x = x

Full source

theorem extend_apply_self (hs : LinearIndepOn K id s) (x : hs.extend _) : Basis.extend hs x = x :=
  Basis.mk_apply _ _ _

Extended Basis Preserves Original Vectors: $b(x) = x$ for $x$ in Extended Basis

Informal description

Let $K$ be a field and $V$ a vector space over $K$. Given a linearly independent subset $s \subseteq V$ and an element $x$ in the extended basis set obtained from $s$, the basis vector corresponding to $x$ in the extended basis equals $x$ itself. That is, if $b$ is the basis obtained by extending $s$, then $b(x) = x$.

Basis.coe_extend theorem

(hs : LinearIndepOn K id s) : ⇑(Basis.extend hs) = ((↑) : _ → _)

Full source

@[simp]
theorem coe_extend (hs : LinearIndepOn K id s) : ⇑(Basis.extend hs) = ((↑) : _ → _) :=
  funext (extend_apply_self hs)

Inclusion Representation of Extended Basis

Informal description

Let $K$ be a field and $V$ a vector space over $K$. Given a linearly independent subset $s \subseteq V$, the basis obtained by extending $s$ to a basis of $V$ (via `Basis.extend`) is represented by the inclusion map from the extended index set to $V$.

Basis.range_extend theorem

(hs : LinearIndepOn K id s) : range (Basis.extend hs) = hs.extend (subset_univ _)

Full source

theorem range_extend (hs : LinearIndepOn K id s) :
    range (Basis.extend hs) = hs.extend (subset_univ _) := by
  rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]

Range of Extended Basis Equals Maximal Linearly Independent Extension

Informal description

Let $K$ be a field and $V$ a vector space over $K$. Given a linearly independent subset $s \subseteq V$, the range of the basis obtained by extending $s$ (via `Basis.extend hs`) is equal to the maximal linearly independent extension of $s$ within $V$.

Basis.sumExtendIndex definition

(hs : LinearIndependent K v) : Set V

Full source

/-- Auxiliary definition: the index for the new basis vectors in `Basis.sumExtend`.

The specific value of this definition should be considered an implementation detail. -/
def sumExtendIndex (hs : LinearIndependent K v) : Set V :=
  LinearIndepOn.extendLinearIndepOn.extend hs.linearIndepOn_id (subset_univ _) \ range v

Index set for basis extension of a linearly independent family

Informal description

Given a linearly independent family of vectors $ v $ in a vector space $ V $ over a field $ K $, the set `Basis.sumExtendIndex hs` is defined as the extension of the linear independence set $ \text{range } v $ to a basis of $ V $, minus the original vectors in $ \text{range } v $. This serves as an auxiliary index set for constructing a basis that extends the given linearly independent family.

Basis.sumExtend definition

(hs : LinearIndependent K v) : Basis (ι ⊕ sumExtendIndex hs) K V

Full source

/-- If `v` is a linear independent family of vectors, extend it to a basis indexed by a sum type. -/
noncomputable def sumExtend (hs : LinearIndependent K v) : Basis (ι ⊕ sumExtendIndex hs) K V :=
  let s := Set.range v
  let e : ι ≃ s := Equiv.ofInjective v hs.injective
  let b := hs.linearIndepOn_id.extend (subset_univ (Set.range v))
  (Basis.extend hs.linearIndepOn_id).reindex <|
    Equiv.symm <|
      calc
        ι ⊕ (b \ s : Set V) ≃ s ⊕ (b \ s : Set V) := Equiv.sumCongr e (Equiv.refl _)
        _ ≃ b :=
          haveI := Classical.decPred (· ∈ s)
          Equiv.Set.sumDiffSubset (hs.linearIndepOn_id.subset_extend _)

Basis extension of a linearly independent family via sum indexing

Informal description

Given a field $K$, a vector space $V$ over $K$, and a linearly independent family of vectors $v : \iota \to V$, the basis `Basis.sumExtend hs` is constructed by extending the family $v$ to a basis of $V$. The resulting basis is indexed by the disjoint union of the original index type $\iota$ and an auxiliary index set (the complement of $\text{range } v$ in the extended basis). The construction first establishes a bijection between $\iota$ and $\text{range } v$, then extends the linearly independent set $\text{range } v$ to a basis $b$ of $V$, and finally reindexes this basis using an equivalence that combines the original indexing with the new basis vectors.

Basis.subset_extend theorem

{s : Set V} (hs : LinearIndepOn K id s) : s ⊆ hs.extend (Set.subset_univ _)

Full source

theorem subset_extend {s : Set V} (hs : LinearIndepOn K id s) : s ⊆ hs.extend (Set.subset_univ _) :=
  hs.subset_extend _

Inclusion of Linearly Independent Set in its Basis Extension

Informal description

For any set $s$ of vectors in a vector space $V$ over a field $K$, if $s$ is linearly independent, then $s$ is contained in its extension to a basis of $V$.

Basis.extendLe definition

(hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) : Basis (hs.extend hst) K V

Full source

/-- If `s` is a family of linearly independent vectors contained in a set `t` spanning `V`,
then one can get a basis of `V` containing `s` and contained in `t`. -/
noncomputable def extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
    Basis (hs.extend hst) K V :=
  Basis.mk
    ((hs.linearIndepOn_extend _).linearIndependent ..)
    (le_trans ht <| Submodule.span_le.2 <| by simpa using hs.subset_span_extend hst)

Extension of a linearly independent set to a basis within a spanning set

Informal description

Given a field $K$, a vector space $V$ over $K$, a linearly independent subset $s \subseteq V$, a subset $t \subseteq V$ containing $s$, and the assumption that $t$ spans $V$, the function `Basis.extendLe` constructs a basis for $V$ indexed by the extension of $s$ within $t$. This basis contains $s$ and is contained in $t$.

Basis.extendLe_apply_self theorem

 (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) (x : hs.extend hst) : Basis.extendLe hs hst ht x = x

Full source

theorem extendLe_apply_self (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t)
    (x : hs.extend hst) : Basis.extendLe hs hst ht x = x :=
  Basis.mk_apply _ _ _

Basis Extension Preserves Vectors: $\text{extendLe}(hs, hst, ht)(x) = x$

Informal description

Let $K$ be a field, $V$ a vector space over $K$, $s \subseteq V$ a linearly independent subset, and $t \subseteq V$ a subset containing $s$ that spans $V$. For any vector $x$ in the extended basis $\text{extend}(s, t)$, the basis vector $\text{extendLe}(hs, hst, ht)(x)$ equals $x$ itself.

Basis.coe_extendLe theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) : ⇑(Basis.extendLe hs hst ht) = ((↑) : _ → _)

Full source

@[simp]
theorem coe_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
    ⇑(Basis.extendLe hs hst ht) = ((↑) : _ → _) :=
  funext (extendLe_apply_self hs hst ht)

Basis Extension Coincides with Inclusion: $\text{extendLe}(hs, hst, ht) = \iota$

Informal description

Let $K$ be a field, $V$ a vector space over $K$, $s \subseteq V$ a linearly independent subset, and $t \subseteq V$ a subset containing $s$ that spans $V$. Then the basis vectors of the extended basis $\text{extendLe}(hs, hst, ht)$ are exactly the elements of the extended set $\text{extend}(s, t)$, i.e., the basis map $\text{extendLe}(hs, hst, ht)$ coincides with the inclusion map from $\text{extend}(s, t)$ to $V$.

Basis.range_extendLe theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) : range (Basis.extendLe hs hst ht) = hs.extend hst

Full source

theorem range_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
    range (Basis.extendLe hs hst ht) = hs.extend hst := by
  rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]

Range of Extended Basis Equals Extended Set

Informal description

Let $K$ be a field, $V$ a vector space over $K$, $s \subseteq V$ a linearly independent subset, and $t \subseteq V$ a subset containing $s$ that spans $V$. Then the range of the basis vectors obtained from the extension $\text{extendLe}(hs, hst, ht)$ is exactly the extended set $\text{extend}(s, t)$.

Basis.subset_extendLe theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) : s ⊆ range (Basis.extendLe hs hst ht)

Full source

theorem subset_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
    s ⊆ range (Basis.extendLe hs hst ht) :=
  (range_extendLe hs hst ht).symm ▸ hs.subset_extend hst

Inclusion of Original Set in Extended Basis

Informal description

Let $K$ be a field, $V$ a vector space over $K$, $s \subseteq V$ a linearly independent subset, and $t \subseteq V$ a subset containing $s$ such that $t$ spans $V$. Then the original set $s$ is contained in the range of the basis vectors obtained from the extension $\text{extendLe}(hs, hst, ht)$.

Basis.extendLe_subset theorem

(hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) : range (Basis.extendLe hs hst ht) ⊆ t

Full source

theorem extendLe_subset (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
    rangerange (Basis.extendLe hs hst ht) ⊆ t :=
  (range_extendLe hs hst ht).symm ▸ hs.extend_subset hst

Extended Basis Vectors are Contained in Spanning Set

Informal description

Let $K$ be a field, $V$ a vector space over $K$, $s \subseteq V$ a linearly independent subset, and $t \subseteq V$ a subset containing $s$ that spans $V$. Then the range of the basis vectors obtained by extending $s$ within $t$ is a subset of $t$.

Basis.ofSpan definition

(hs : ⊤ ≤ span K s) : Basis ((linearIndepOn_empty K id).extend (empty_subset s)) K V

Full source

/-- If a set `s` spans the space, this is a basis contained in `s`. -/
noncomputable def ofSpan (hs : ⊤ ≤ span K s) :
    Basis ((linearIndepOn_empty K id).extend (empty_subset s)) K V :=
  extendLe (linearIndependent_empty K V) (empty_subset s) hs

Basis constructed from a spanning set

Informal description

Given a field $K$ and a vector space $V$ over $K$, if a subset $s \subseteq V$ spans the entire space (i.e., $\text{span}_K s = V$), then `Basis.ofSpan` constructs a basis for $V$ by extending the empty set (which is trivially linearly independent) within $s$. The resulting basis is indexed by the extension of the empty set in $s$.

Basis.ofSpan_apply_self theorem

(hs : ⊤ ≤ span K s) (x : (linearIndepOn_empty K id).extend (empty_subset s)) : Basis.ofSpan hs x = x

Full source

theorem ofSpan_apply_self (hs : ⊤ ≤ span K s)
    (x : (linearIndepOn_empty K id).extend (empty_subset s)) :
    Basis.ofSpan hs x = x :=
  extendLe_apply_self (linearIndependent_empty K V) (empty_subset s) hs x

Basis Vector Preservation in Span Construction: $\text{Basis.ofSpan}(hs)(x) = x$

Informal description

Let $K$ be a field and $V$ a vector space over $K$. If a subset $s \subseteq V$ spans $V$ (i.e., $\text{span}_K s = V$), then for any vector $x$ in the extended basis obtained from the empty set within $s$, the basis vector $\text{Basis.ofSpan}(hs)(x)$ equals $x$ itself.

Basis.coe_ofSpan theorem

(hs : ⊤ ≤ span K s) : ⇑(ofSpan hs) = ((↑) : _ → _)

Full source

@[simp]
theorem coe_ofSpan (hs : ⊤ ≤ span K s) : ⇑(ofSpan hs) = ((↑) : _ → _) :=
  funext (ofSpan_apply_self hs)

Basis Vector Representation in Span Construction

Informal description

Given a field $K$ and a vector space $V$ over $K$, if a subset $s \subseteq V$ spans $V$ (i.e., $\text{span}_K s = V$), then the basis vectors of the basis constructed by `Basis.ofSpan hs` are exactly the elements of the extended basis set obtained from the empty set within $s$. In other words, the function representing the basis vectors coincides with the inclusion map from the extended basis set to $V$.

Basis.range_ofSpan theorem

(hs : ⊤ ≤ span K s) : range (ofSpan hs) = (linearIndepOn_empty K id).extend (empty_subset s)

Full source

theorem range_ofSpan (hs : ⊤ ≤ span K s) :
    range (ofSpan hs) = (linearIndepOn_empty K id).extend (empty_subset s) := by
  rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]

Range of Basis Vectors from Spanning Set Equals Extended Empty Set

Informal description

Let $K$ be a field and $V$ a vector space over $K$. Given a subset $s \subseteq V$ that spans $V$ (i.e., $\text{span}_K s = V$), the range of the basis vectors constructed by `Basis.ofSpan hs` is equal to the extension of the empty set (which is trivially linearly independent) within $s$.

Basis.ofSpan_subset theorem

(hs : ⊤ ≤ span K s) : range (ofSpan hs) ⊆ s

Full source

theorem ofSpan_subset (hs : ⊤ ≤ span K s) : rangerange (ofSpan hs) ⊆ s :=
  extendLe_subset (linearIndependent_empty K V) (empty_subset s) hs

Basis vectors from spanning set are contained in the set

Informal description

Let $K$ be a field and $V$ a vector space over $K$. If a subset $s \subseteq V$ spans $V$ (i.e., $\text{span}_K s = V$), then the range of the basis vectors constructed by `Basis.ofSpan` is contained in $s$.

Basis.ofVectorSpaceIndex definition

: Set V

Full source

/-- A set used to index `Basis.ofVectorSpace`. -/
noncomputable def ofVectorSpaceIndex : Set V :=
  (linearIndepOn_empty K id).extend (subset_univ _)

Indexing set for vector space basis

Informal description

The indexing set used to construct a basis for a vector space $V$ over a field $K$ via `Basis.ofVectorSpace`. It is obtained by extending the empty set, which is trivially linearly independent, to a maximal linearly independent subset of $V$.

Basis.ofVectorSpace definition

: Basis (ofVectorSpaceIndex K V) K V

Full source

/-- Each vector space has a basis. -/
noncomputable def ofVectorSpace : Basis (ofVectorSpaceIndex K V) K V :=
  Basis.extend (linearIndependent_empty K V)

Basis of a vector space via extension of the empty set

Informal description

Given a vector space $V$ over a field $K$, the function constructs a basis for $V$ by extending the empty set (which is trivially linearly independent) to a maximal linearly independent subset of $V$. The resulting basis is indexed by this extended set.

Module.Free.of_divisionRing instance

: Module.Free K V

Full source

@[stacks 09FN "Generalized from fields to division rings."]
instance (priority := 100) _root_.Module.Free.of_divisionRing : Module.Free K V :=
  Module.Free.of_basis (ofVectorSpace K V)

Vector Spaces are Free Modules over Division Rings

Informal description

Every vector space $V$ over a division ring $K$ is a free module.

Basis.ofVectorSpace_apply_self theorem

(x : ofVectorSpaceIndex K V) : ofVectorSpace K V x = x

Full source

theorem ofVectorSpace_apply_self (x : ofVectorSpaceIndex K V) : ofVectorSpace K V x = x := by
  unfold ofVectorSpace
  exact Basis.mk_apply _ _ _

Basis Vector Identity: $b(x) = x$ for Basis of Vector Space

Informal description

For any element $x$ in the indexing set of the basis constructed by `Basis.ofVectorSpace` for a vector space $V$ over a field $K$, the basis vector corresponding to $x$ is equal to $x$ itself.

Basis.coe_ofVectorSpace theorem

: ⇑(ofVectorSpace K V) = ((↑) : _ → _)

Full source

@[simp]
theorem coe_ofVectorSpace : ⇑(ofVectorSpace K V) = ((↑) : _ → _ ) :=
  funext fun x => ofVectorSpace_apply_self K V x

Basis Vectors as Canonical Inclusion in Vector Space Basis

Informal description

The basis vectors of the basis constructed by `Basis.ofVectorSpace` for a vector space $V$ over a field $K$ are exactly the elements of the indexing set `ofVectorSpaceIndex K V`, viewed as elements of $V$ via the canonical inclusion map.

Basis.ofVectorSpaceIndex.linearIndependent theorem

: LinearIndependent K ((↑) : ofVectorSpaceIndex K V → V)

Full source

theorem ofVectorSpaceIndex.linearIndependent :
    LinearIndependent K ((↑) : ofVectorSpaceIndex K V → V) := by
  convert (ofVectorSpace K V).linearIndependent
  ext x
  rw [ofVectorSpace_apply_self]

Linear Independence of Vector Space Basis Indexing Set

Informal description

For any vector space $V$ over a field $K$, the canonical inclusion map from the indexing set $\text{ofVectorSpaceIndex}\,K\,V$ to $V$ is linearly independent over $K$.

Basis.range_ofVectorSpace theorem

: range (ofVectorSpace K V) = ofVectorSpaceIndex K V

Full source

theorem range_ofVectorSpace : range (ofVectorSpace K V) = ofVectorSpaceIndex K V :=
  range_extend _

Range of Basis Vectors Equals Indexing Set in Vector Space Basis

Informal description

For a vector space $V$ over a field $K$, the range of the basis vectors obtained from the basis constructed by `Basis.ofVectorSpace` is equal to the indexing set `ofVectorSpaceIndex K V$.

Basis.exists_basis theorem

: ∃ s : Set V, Nonempty (Basis s K V)

Full source

theorem exists_basis : ∃ s : Set V, Nonempty (Basis s K V) :=
  ⟨ofVectorSpaceIndex K V, ⟨ofVectorSpace K V⟩⟩

Existence of a Basis for a Vector Space

Informal description

For any vector space $V$ over a field $K$, there exists a subset $s \subseteq V$ such that $s$ forms a basis for $V$ over $K$.

VectorSpace.card_fintype theorem

[Fintype K] [Fintype V] : ∃ n : ℕ, card V = card K ^ n

Full source

theorem VectorSpace.card_fintype [Fintype K] [Fintype V] : ∃ n : ℕ, card V = card K ^ n := by
  classical
  exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩

Cardinality of Finite Vector Space over Finite Field: $|V| = |K|^n$

Informal description

For a finite field $K$ and a finite-dimensional vector space $V$ over $K$, there exists a natural number $n$ such that the cardinality of $V$ is equal to the cardinality of $K$ raised to the power $n$, i.e., $|V| = |K|^n$.

nonzero_span_atom theorem

(v : V) (hv : v ≠ 0) : IsAtom (span K { v } : Submodule K V)

Full source

/-- For a module over a division ring, the span of a nonzero element is an atom of the
lattice of submodules. -/
theorem nonzero_span_atom (v : V) (hv : v ≠ 0) : IsAtom (span K {v} : Submodule K V) := by
  constructor
  · rw [Submodule.ne_bot_iff]
    exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩
  · intro T hT
    by_contra h
    apply hT.2
    change span K {v} ≤ T
    simp_rw [span_singleton_le_iff_mem, ← Ne.eq_def, Submodule.ne_bot_iff] at *
    rcases h with ⟨s, ⟨hs, hz⟩⟩
    rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
    rcases eq_or_ne a 0 with rfl | h
    · simp only [zero_smul, ne_eq, not_true] at hz
    · rwa [T.smul_mem_iff h] at hs

Span of Nonzero Vector is an Atom in Submodule Lattice

Informal description

For any nonzero vector $v$ in a vector space $V$ over a division ring $K$, the span of $\{v\}$ is an atom in the lattice of submodules of $V$.

atom_iff_nonzero_span theorem

(W : Submodule K V) : IsAtom W ↔ ∃ v ≠ 0, W = span K { v }

Full source

/-- The atoms of the lattice of submodules of a module over a division ring are the
submodules equal to the span of a nonzero element of the module. -/
theorem atom_iff_nonzero_span (W : Submodule K V) :
    IsAtomIsAtom W ↔ ∃ v ≠ 0, W = span K {v} := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · obtain ⟨hbot, h⟩ := h
    rcases (Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩
    refine ⟨v, ⟨hv, ?_⟩⟩
    by_contra heq
    specialize h (span K {v})
    rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h
    exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)
  · rcases h with ⟨v, ⟨hv, rfl⟩⟩
    exact nonzero_span_atom v hv

Characterization of Atomic Submodules via Nonzero Spans

Informal description

A submodule $W$ of a vector space $V$ over a division ring $K$ is an atom in the lattice of submodules if and only if there exists a nonzero vector $v \in V$ such that $W$ is the span of $\{v\}$.

instIsAtomisticSubmodule instance

: IsAtomistic (Submodule K V)

Full source

/-- The lattice of submodules of a module over a division ring is atomistic. -/
instance : IsAtomistic (Submodule K V) :=
  CompleteLattice.isAtomistic_iff.2 fun W => by
    refine ⟨_, submodule_eq_sSup_le_nonzero_spans W, ?_⟩
    rintro _ ⟨w, ⟨_, ⟨hw, rfl⟩⟩⟩
    exact nonzero_span_atom w hw

Atomistic Lattice of Submodules in a Vector Space

Informal description

The lattice of submodules of a vector space $V$ over a division ring $K$ is atomistic, meaning every element is the supremum of the atoms (minimal nonzero submodules) beneath it.

LinearMap.exists_leftInverse_of_injective theorem

(f : V →ₗ[K] V') (hf_inj : LinearMap.ker f = ⊥) : ∃ g : V' →ₗ[K] V, g.comp f = LinearMap.id

Full source

theorem LinearMap.exists_leftInverse_of_injective (f : V →ₗ[K] V') (hf_inj : LinearMap.ker f = ⊥) :
    ∃ g : V' →ₗ[K] V, g.comp f = LinearMap.id := by
  let B := Basis.ofVectorSpaceIndex K V
  let hB := Basis.ofVectorSpace K V
  have hB₀ : _ := hB.linearIndependent.linearIndepOn_id
  have : LinearIndepOn K _root_.id (f '' B) := by
    have h₁ : LinearIndepOn K _root_.id (f '' Set.range (Basis.ofVectorSpace K V)) :=
      LinearIndepOn.image (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])
    rwa [Basis.range_ofVectorSpace K V] at h₁
  let C := this.extend (subset_univ _)
  have BC := this.subset_extend (subset_univ _)
  let hC := Basis.extend this
  haveI Vinh : Inhabited V := ⟨0⟩
  refine ⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hB.ext fun b => ?_⟩
  rw [image_subset_iff] at BC
  have fb_eq : f b = hC ⟨f b, BC b.2⟩ := by
    change f b = Basis.extend this _
    simp_rw [Basis.extend_apply_self]
  dsimp []
  rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]
  exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _

Existence of Left Inverse for Injective Linear Maps

Informal description

For any injective linear map $f \colon V \to V'$ between vector spaces over a field $K$ (i.e., $\ker f = 0$), there exists a left inverse linear map $g \colon V' \to V$ such that $g \circ f = \text{id}_V$.

Submodule.exists_isCompl theorem

(p : Submodule K V) : ∃ q : Submodule K V, IsCompl p q

Full source

theorem Submodule.exists_isCompl (p : Submodule K V) : ∃ q : Submodule K V, IsCompl p q :=
  let ⟨f, hf⟩ := p.subtype.exists_leftInverse_of_injective p.ker_subtype
  ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| LinearMap.ext_iff.1 hf⟩

Existence of Complementary Submodule in Vector Spaces

Informal description

For any submodule $p$ of a vector space $V$ over a field $K$, there exists a complementary submodule $q$ such that $p$ and $q$ form a direct sum decomposition of $V$ (i.e., $p \cap q = 0$ and $p + q = V$).

Submodule.complementedLattice instance

: ComplementedLattice (Submodule K V)

Full source

instance Submodule.complementedLattice : ComplementedLattice (Submodule K V) :=
  ⟨Submodule.exists_isCompl⟩

Complemented Lattice of Submodules in a Vector Space

Informal description

The lattice of submodules of a vector space $V$ over a field $K$ is complemented, meaning that for every submodule $p$ of $V$, there exists a complementary submodule $q$ such that $p \cap q = 0$ and $p + q = V$.

LinearMap.exists_extend theorem

{p : Submodule K V} (f : p →ₗ[K] V') : ∃ g : V →ₗ[K] V', g.comp p.subtype = f

Full source

/-- Any linear map `f : p →ₗ[K] V'` defined on a subspace `p` can be extended to the whole
space. -/
theorem LinearMap.exists_extend {p : Submodule K V} (f : p →ₗ[K] V') :
    ∃ g : V →ₗ[K] V', g.comp p.subtype = f :=
  let ⟨g, hg⟩ := p.subtype.exists_leftInverse_of_injective p.ker_subtype
  ⟨f.comp g, by rw [LinearMap.comp_assoc, hg, f.comp_id]⟩

Extension of Linear Maps from Subspaces to the Whole Space

Informal description

For any subspace $p$ of a vector space $V$ over a field $K$ and any linear map $f \colon p \to V'$, there exists a linear map $g \colon V \to V'$ extending $f$, i.e., such that $g$ restricted to $p$ equals $f$.

Submodule.exists_le_ker_of_lt_top theorem

(p : Submodule K V) (hp : p < ⊤) : ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ ker f

Full source

/-- If `p < ⊤` is a subspace of a vector space `V`, then there exists a nonzero linear map
`f : V →ₗ[K] K` such that `p ≤ ker f`. -/
theorem Submodule.exists_le_ker_of_lt_top (p : Submodule K V) (hp : p < ⊤) :
    ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ ker f := by
  rcases SetLike.exists_of_lt hp with ⟨v, -, hpv⟩; clear hp
  rcases (LinearPMap.supSpanSingleton ⟨p, 0⟩ v (1 : K) hpv).toFun.exists_extend with ⟨f, hf⟩
  refine ⟨f, ?_, ?_⟩
  · rintro rfl
    rw [LinearMap.zero_comp] at hf
    have := LinearPMap.supSpanSingleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv 0 p.zero_mem 1
    simpa using (LinearMap.congr_fun hf _).trans this
  · refine fun x hx => mem_ker.2 ?_
    have := LinearPMap.supSpanSingleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv x hx 0
    simpa using (LinearMap.congr_fun hf _).trans this

Existence of Nonzero Linear Functional Vanishing on a Proper Subspace

Informal description

For any proper subspace $p$ of a vector space $V$ over a field $K$ (i.e., $p$ is strictly contained in $V$), there exists a nonzero linear functional $f \colon V \to K$ such that $p$ is contained in the kernel of $f$.

quotient_prod_linearEquiv theorem

(p : Submodule K V) : Nonempty (((V ⧸ p) × p) ≃ₗ[K] V)

Full source

theorem quotient_prod_linearEquiv (p : Submodule K V) : Nonempty (((V ⧸ p) × p) ≃ₗ[K] V) :=
  let ⟨q, hq⟩ := p.exists_isCompl
  Nonempty.intro <|
    ((quotientEquivOfIsCompl p q hq).prodCongr (LinearEquiv.refl _ _)).trans
      (prodEquivOfIsCompl q p hq.symm)

Linear Equivalence Between Quotient-Product Space and Original Vector Space

Informal description

For any submodule $p$ of a vector space $V$ over a field $K$, there exists a linear equivalence between the product space $(V / p) \times p$ and $V$ itself, where $V / p$ denotes the quotient space of $V$ by $p$.

Mathlib.LinearAlgebra.Basis.VectorSpace

Main statements

Tags