Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Submodule.finrank_lt theorem

[FiniteDimensional K V] {s : Submodule K V} (h : s ≠ ⊤) : finrank K s < finrank K V

Full source

/-- The dimension of a strict submodule is strictly bounded by the dimension of the ambient
space.

See also `Submodule.length_lt`. -/
theorem finrank_lt [FiniteDimensional K V] {s : Submodule K V} (h : s ≠ ⊤) :
    finrank K s < finrank K V := by
  rw [← s.finrank_quotient_add_finrank, add_comm]
  exact Nat.lt_add_of_pos_right (finrank_pos_iff.mpr (Quotient.nontrivial_of_lt_top _ h.lt_top))

Proper Submodule Has Strictly Smaller Dimension

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $s$ be a proper submodule of $V$ (i.e., $s \neq V$). Then the dimension of $s$ is strictly less than the dimension of $V$, i.e., $\dim_K s < \dim_K V$.

Submodule.finrank_sup_add_finrank_inf_eq theorem

 (s t : Submodule K V) [FiniteDimensional K s] [FiniteDimensional K t] :
  finrank K ↑(s ⊔ t) + finrank K ↑(s ⊓ t) = finrank K ↑s + finrank K ↑t

Full source

/-- The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t -/
theorem finrank_sup_add_finrank_inf_eq (s t : Submodule K V) [FiniteDimensional K s]
    [FiniteDimensional K t] :
    finrank K ↑(s ⊔ t) + finrank K ↑(s ⊓ t) = finrank K ↑s + finrank K ↑t := by
  have key : Module.rank K ↑(s ⊔ t) + Module.rank K ↑(s ⊓ t) = Module.rank K s + Module.rank K t :=
    rank_sup_add_rank_inf_eq s t
  repeat rw [← finrank_eq_rank] at key
  norm_cast at key

Dimension Formula for Submodule Sum and Intersection

Informal description

For any finite-dimensional submodules $s$ and $t$ of a vector space $V$ over a division ring $K$, the sum of the dimensions of $s + t$ and $s \cap t$ equals the sum of the dimensions of $s$ and $t$, i.e., \[ \dim_K(s + t) + \dim_K(s \cap t) = \dim_K s + \dim_K t. \]

Submodule.finrank_add_le_finrank_add_finrank theorem

 (s t : Submodule K V) [FiniteDimensional K s] [FiniteDimensional K t] :
  finrank K (s ⊔ t : Submodule K V) ≤ finrank K s + finrank K t

Full source

theorem finrank_add_le_finrank_add_finrank (s t : Submodule K V) [FiniteDimensional K s]
    [FiniteDimensional K t] : finrank K (s ⊔ t : Submodule K V) ≤ finrank K s + finrank K t := by
  rw [← finrank_sup_add_finrank_inf_eq]
  exact self_le_add_right _ _

Subadditivity of Dimension for Submodule Sum

Informal description

For any finite-dimensional submodules $s$ and $t$ of a vector space $V$ over a division ring $K$, the dimension of the sum $s + t$ is less than or equal to the sum of the dimensions of $s$ and $t$, i.e., \[ \dim_K(s + t) \leq \dim_K s + \dim_K t. \]

Submodule.finrank_add_finrank_le_of_disjoint theorem

[FiniteDimensional K V] {s t : Submodule K V} (hdisjoint : Disjoint s t) : finrank K s + finrank K t ≤ finrank K V

Full source

theorem finrank_add_finrank_le_of_disjoint [FiniteDimensional K V]
    {s t : Submodule K V} (hdisjoint : Disjoint s t) :
    finrank K s + finrank K t ≤ finrank K V := by
  rw [← Submodule.finrank_sup_add_finrank_inf_eq s t, hdisjoint.eq_bot, finrank_bot, add_zero]
  exact Submodule.finrank_le _

Dimension Bound for Disjoint Subspaces in Finite-Dimensional Vector Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $s$ and $t$ be two subspaces of $V$ such that $s \cap t = \{0\}$. Then the sum of the dimensions of $s$ and $t$ is less than or equal to the dimension of $V$, i.e., \[ \dim_K s + \dim_K t \leq \dim_K V. \]

Submodule.isCompl_iff_disjoint theorem

 [FiniteDimensional K V] (s t : Submodule K V) (hdim : finrank K V ≤ finrank K s + finrank K t) :
  IsCompl s t ↔ Disjoint s t

Full source

theorem isCompl_iff_disjoint [FiniteDimensional K V] (s t : Submodule K V)
    (hdim : finrank K V ≤ finrank K s + finrank K t) :
    IsComplIsCompl s t ↔ Disjoint s t :=
  ⟨fun h ↦ h.1, fun h ↦ ⟨h, codisjoint_iff.mpr <| eq_top_of_disjoint s t hdim h⟩⟩

Complementary Subspaces Characterization via Disjointness and Dimension Constraint

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $s$ and $t$ be two subspaces of $V$ such that $\operatorname{finrank}_K V \leq \operatorname{finrank}_K s + \operatorname{finrank}_K t$. Then $s$ and $t$ are complementary subspaces (i.e., $V = s \oplus t$) if and only if they are disjoint (i.e., $s \cap t = \{0\}$).

FiniteDimensional.LinearEquiv.quotEquivOfEquiv definition

 {p : Subspace K V} {q : Subspace K V₂} (f₁ : p ≃ₗ[K] q) (f₂ : V ≃ₗ[K] V₂) : (V ⧸ p) ≃ₗ[K] V₂ ⧸ q

Full source

/-- Given isomorphic subspaces `p q` of vector spaces `V` and `V₁` respectively,
  `p.quotient` is isomorphic to `q.quotient`. -/
noncomputable def LinearEquiv.quotEquivOfEquiv {p : Subspace K V} {q : Subspace K V₂}
    (f₁ : p ≃ₗ[K] q) (f₂ : V ≃ₗ[K] V₂) : (V ⧸ p) ≃ₗ[K] V₂ ⧸ q :=
  LinearEquiv.ofFinrankEq _ _
    (by
      rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₂])

Linear isomorphism between quotient spaces of isomorphic subspaces

Informal description

Given isomorphic subspaces $ p $ of $ V $ and $ q $ of $ V₂ $ via a linear equivalence $ f₁ : p ≃ₗ[K] q $, and a linear equivalence $ f₂ : V ≃ₗ[K] V₂ $, the quotient spaces $ V/p $ and $ V₂/q $ are linearly isomorphic.

FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv definition

{p q : Subspace K V} (f : (V ⧸ p) ≃ₗ[K] q) : (V ⧸ q) ≃ₗ[K] p

Full source

/-- Given the subspaces `p q`, if `p.quotient ≃ₗ[K] q`, then `q.quotient ≃ₗ[K] p` -/
noncomputable def LinearEquiv.quotEquivOfQuotEquiv {p q : Subspace K V} (f : (V ⧸ p) ≃ₗ[K] q) :
    (V ⧸ q) ≃ₗ[K] p :=
  LinearEquiv.ofFinrankEq _ _ <| by
    rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]

Linear equivalence between quotient and subspace induced by a quotient equivalence

Informal description

Given two subspaces $ p $ and $ q $ of a finite-dimensional vector space $ V $ over a division ring $ K $, if there exists a linear equivalence $ f $ between the quotient space $ V/p $ and the subspace $ q $, then there exists a linear equivalence between the quotient space $ V/q $ and the subspace $ p $.

LinearMap.finrank_range_add_finrank_ker theorem

 [FiniteDimensional K V] (f : V →ₗ[K] V₂) : finrank K (LinearMap.range f) + finrank K (LinearMap.ker f) = finrank K V

Full source

/-- rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to
the dimension of the source space. -/
theorem finrank_range_add_finrank_ker [FiniteDimensional K V] (f : V →ₗ[K] V₂) :
    finrank K (LinearMap.range f) + finrank K (LinearMap.ker f) = finrank K V := by
  rw [← f.quotKerEquivRange.finrank_eq]
  exact Submodule.finrank_quotient_add_finrank _

Rank-Nullity Theorem for Finite-Dimensional Vector Spaces

Informal description

Let $V$ and $V₂$ be finite-dimensional vector spaces over a division ring $K$, and let $f : V \to V₂$ be a linear map. Then the dimension of the range of $f$ plus the dimension of the kernel of $f$ equals the dimension of $V$, i.e., \[ \dim_K (\text{range } f) + \dim_K (\ker f) = \dim_K V. \]

LinearMap.ker_ne_bot_of_finrank_lt theorem

 [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (h : finrank K V₂ < finrank K V) :
  LinearMap.ker f ≠ ⊥

Full source

lemma ker_ne_bot_of_finrank_lt [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂}
    (h : finrank K V₂ < finrank K V) :
    LinearMap.kerLinearMap.ker f ≠ ⊥ := by
  have h₁ := f.finrank_range_add_finrank_ker
  have h₂ : finrank K (LinearMap.range f) ≤ finrank K V₂ := (LinearMap.range f).finrank_le
  suffices 0 < finrank K (LinearMap.ker f) from Submodule.one_le_finrank_iff.mp this
  omega

Nontrivial Kernel for Linear Maps Between Finite-Dimensional Spaces with $\dim V₂ < \dim V$

Informal description

Let $V$ and $V₂$ be finite-dimensional vector spaces over a division ring $K$, and let $f : V \to V₂$ be a linear map. If the dimension of $V₂$ is strictly less than the dimension of $V$, then the kernel of $f$ is nontrivial, i.e., $\ker f \neq \{0\}$.

LinearMap.injective_iff_surjective_of_finrank_eq_finrank theorem

 [FiniteDimensional K V] [FiniteDimensional K V₂] (H : finrank K V = finrank K V₂) {f : V →ₗ[K] V₂} :
  Function.Injective f ↔ Function.Surjective f

Full source

theorem injective_iff_surjective_of_finrank_eq_finrank [FiniteDimensional K V]
    [FiniteDimensional K V₂] (H : finrank K V = finrank K V₂) {f : V →ₗ[K] V₂} :
    Function.InjectiveFunction.Injective f ↔ Function.Surjective f := by
  have := finrank_range_add_finrank_ker f
  rw [← ker_eq_bot, ← range_eq_top]; refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [h, finrank_bot, add_zero, H] at this
    exact eq_top_of_finrank_eq this
  · rw [h, finrank_top, H] at this
    exact Submodule.finrank_eq_zero.1 (add_right_injective _ this)

Injective-Surjective Equivalence for Linear Maps on Equal-Dimensional Spaces

Informal description

Let $V$ and $V_2$ be finite-dimensional vector spaces over a division ring $K$ with $\dim_K V = \dim_K V_2$. For a linear map $f \colon V \to V_2$, the following are equivalent: 1. $f$ is injective. 2. $f$ is surjective.

LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank theorem

 [FiniteDimensional K V] [FiniteDimensional K V₂] (H : finrank K V = finrank K V₂) {f : V →ₗ[K] V₂} :
  LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤

Full source

theorem ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank [FiniteDimensional K V]
    [FiniteDimensional K V₂] (H : finrank K V = finrank K V₂) {f : V →ₗ[K] V₂} :
    LinearMap.kerLinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤ := by
  rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]

Kernel-Range Equivalence for Linear Maps on Equal-Dimensional Spaces

Informal description

Let $V$ and $V_2$ be finite-dimensional vector spaces over a division ring $K$ with $\dim_K V = \dim_K V_2$. For a linear map $f \colon V \to V_2$, the following are equivalent: 1. The kernel of $f$ is trivial ($\ker f = \{0\}$). 2. The range of $f$ is the entire space $V_2$ ($\text{range } f = V_2$).

LinearMap.linearEquivOfInjective definition

 [FiniteDimensional K V] [FiniteDimensional K V₂] (f : V →ₗ[K] V₂) (hf : Injective f)
  (hdim : finrank K V = finrank K V₂) : V ≃ₗ[K] V₂

Full source

/-- Given a linear map `f` between two vector spaces with the same dimension, if
`ker f = ⊥` then `linearEquivOfInjective` is the induced isomorphism
between the two vector spaces. -/
noncomputable def linearEquivOfInjective [FiniteDimensional K V] [FiniteDimensional K V₂]
    (f : V →ₗ[K] V₂) (hf : Injective f) (hdim : finrank K V = finrank K V₂) : V ≃ₗ[K] V₂ :=
  LinearEquiv.ofBijective f
    ⟨hf, (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hdim).mp hf⟩

Linear isomorphism induced by an injective linear map between equal-dimensional spaces

Informal description

Given a linear map $f \colon V \to V_2$ between finite-dimensional vector spaces over a field $K$ with $\dim_K V = \dim_K V_2$, if $f$ is injective (i.e., $\ker f = 0$), then `linearEquivOfInjective` constructs a linear isomorphism $V \simeq V_2$ induced by $f$.

LinearMap.linearEquivOfInjective_apply theorem

 [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (hf : Injective f)
  (hdim : finrank K V = finrank K V₂) (x : V) : f.linearEquivOfInjective hf hdim x = f x

Full source

@[simp]
theorem linearEquivOfInjective_apply [FiniteDimensional K V] [FiniteDimensional K V₂]
    {f : V →ₗ[K] V₂} (hf : Injective f) (hdim : finrank K V = finrank K V₂) (x : V) :
    f.linearEquivOfInjective hf hdim x = f x :=
  rfl

Application of Linear Isomorphism Induced by Injective Linear Map

Informal description

Let $V$ and $V_2$ be finite-dimensional vector spaces over a field $K$ with $\dim_K V = \dim_K V_2$. Given an injective linear map $f \colon V \to V_2$ and any vector $x \in V$, the linear isomorphism $\text{linearEquivOfInjective}\, f\, hf\, hdim$ constructed from $f$ satisfies $(\text{linearEquivOfInjective}\, f\, hf\, hdim)(x) = f(x)$.

Submodule.finrank_lt_finrank_of_lt theorem

{s t : Submodule K V} [FiniteDimensional K t] (hst : s < t) : finrank K s < finrank K t

Full source

theorem finrank_lt_finrank_of_lt {s t : Submodule K V} [FiniteDimensional K t] (hst : s < t) :
    finrank K s < finrank K t :=
  (comapSubtypeEquivOfLe hst.le).finrank_eq.symm.trans_lt <|
    finrank_lt <| by simp [not_le_of_lt hst]

Strict Monotonicity of Dimension for Submodules

Informal description

Let $V$ be a vector space over a division ring $K$, and let $s$ and $t$ be submodules of $V$ with $s$ strictly contained in $t$ (i.e., $s < t$). If $t$ is finite-dimensional, then the dimension of $s$ is strictly less than the dimension of $t$, i.e., $\dim_K s < \dim_K t$.

Submodule.finrank_strictMono theorem

[FiniteDimensional K V] : StrictMono fun s : Submodule K V => finrank K s

Full source

theorem finrank_strictMono [FiniteDimensional K V] :
    StrictMono fun s : Submodule K V => finrank K s := fun _ _ => finrank_lt_finrank_of_lt

Strict Monotonicity of Dimension for Submodules of Finite-Dimensional Vector Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$. The function that maps each submodule $s$ of $V$ to its dimension $\dim_K s$ is strictly monotone with respect to the inclusion relation on submodules. That is, for any two submodules $s$ and $t$ of $V$, if $s$ is strictly contained in $t$ ($s \subset t$), then $\dim_K s < \dim_K t$.

Submodule.finrank_add_eq_of_isCompl theorem

[FiniteDimensional K V] {U W : Submodule K V} (h : IsCompl U W) : finrank K U + finrank K W = finrank K V

Full source

theorem finrank_add_eq_of_isCompl [FiniteDimensional K V] {U W : Submodule K V} (h : IsCompl U W) :
    finrank K U + finrank K W = finrank K V := by
  rw [← finrank_sup_add_finrank_inf_eq, h.codisjoint.eq_top, h.disjoint.eq_bot, finrank_bot,
    add_zero]
  exact finrank_top _ _

Dimension Formula for Complementary Subspaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $U$ and $W$ be submodules of $V$ that are complements (i.e., $U \cap W = 0$ and $U + W = V$). Then the sum of the dimensions of $U$ and $W$ equals the dimension of $V$, i.e., \[ \dim_K U + \dim_K W = \dim_K V. \]

LinearIndependent.span_eq_top_of_card_eq_finrank' theorem

 {ι : Type*} [Fintype ι] [FiniteDimensional K V] {b : ι → V} (lin_ind : LinearIndependent K b)
  (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤

Full source

theorem LinearIndependent.span_eq_top_of_card_eq_finrank' {ι : Type*}
    [Fintype ι] [FiniteDimensional K V] {b : ι → V} (lin_ind : LinearIndependent K b)
    (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤ := by
  by_contra ne_top
  rw [← finrank_span_eq_card lin_ind] at card_eq
  exact ne_of_lt (Submodule.finrank_lt ne_top) card_eq

Linear Independence and Cardinality Imply Spanning in Finite-Dimensional Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $\{b_i\}_{i \in \iota}$ be a linearly independent family of vectors in $V$ indexed by a finite set $\iota$. If the cardinality of $\iota$ equals the dimension of $V$ (i.e., $|\iota| = \dim_K V$), then the linear span of $\{b_i\}_{i \in \iota}$ is the entire space $V$.

LinearIndependent.span_eq_top_of_card_eq_finrank theorem

 {ι : Type*} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b)
  (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤

Full source

theorem LinearIndependent.span_eq_top_of_card_eq_finrank {ι : Type*} [Nonempty ι]
    [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b)
    (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤ :=
  have : FiniteDimensional K V := .of_finrank_pos <| card_eq ▸ Fintype.card_pos
  lin_ind.span_eq_top_of_card_eq_finrank' card_eq

Linear Independence and Dimension Imply Spanning in Finite-Dimensional Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $\{b_i\}_{i \in \iota}$ be a linearly independent family of vectors in $V$ indexed by a nonempty finite set $\iota$. If the cardinality of $\iota$ equals the dimension of $V$ (i.e., $|\iota| = \dim_K V$), then the linear span of $\{b_i\}_{i \in \iota}$ is the entire space $V$.

basisOfLinearIndependentOfCardEqFinrank definition

 {ι : Type*} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b)
  (card_eq : Fintype.card ι = finrank K V) : Basis ι K V

Full source

/-- A linear independent family of `finrank K V` vectors forms a basis. -/
@[simps! repr_apply]
noncomputable def basisOfLinearIndependentOfCardEqFinrank {ι : Type*} [Nonempty ι] [Fintype ι]
    {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) :
    Basis ι K V :=
  Basis.mk lin_ind <| (lin_ind.span_eq_top_of_card_eq_finrank card_eq).ge

Basis from linear independence and dimension condition

Informal description

Given a finite-dimensional vector space $V$ over a field $K$, a nonempty finite index set $\iota$, and a linearly independent family of vectors $b : \iota \to V$ such that the cardinality of $\iota$ equals the dimension of $V$, the function constructs a basis for $V$ using the vectors $b$.

coe_basisOfLinearIndependentOfCardEqFinrank theorem

 {ι : Type*} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b)
  (card_eq : Fintype.card ι = finrank K V) : ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = b

Full source

@[simp]
theorem coe_basisOfLinearIndependentOfCardEqFinrank {ι : Type*} [Nonempty ι] [Fintype ι]
    {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) :
    ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = b :=
  Basis.coe_mk _ _

Basis Construction Preserves Given Vectors

Informal description

Given a finite-dimensional vector space $V$ over a field $K$, a nonempty finite index set $\iota$, and a linearly independent family of vectors $b : \iota \to V$ such that the cardinality of $\iota$ equals the dimension of $V$, the basis constructed from $b$ via `basisOfLinearIndependentOfCardEqFinrank` coincides with $b$ as a function. That is, the basis vectors are exactly the vectors in the family $b$.

basisOfPiSpaceOfLinearIndependent definition

 {ι : Type*} [Fintype ι] [Decidable (Nonempty ι)] {b : ι → (ι → K)} (hb : LinearIndependent K b) : Basis ι K (ι → K)

Full source

/-- In a vector space `ι → K`, a linear independent family indexed by `ι` is a basis. -/
noncomputable def basisOfPiSpaceOfLinearIndependent {ι : Type*} [Fintype ι]
    [Decidable (Nonempty ι)] {b : ι → (ι → K)} (hb : LinearIndependent K b) : Basis ι K (ι → K) :=
  if hι : Nonempty ι then
    basisOfLinearIndependentOfCardEqFinrank hb (Module.finrank_fintype_fun_eq_card K).symm
  else
    have : IsEmpty ι := not_nonempty_iff.mp hι
    Basis.empty _

Basis of function space from linear independence

Informal description

Given a finite index set $\iota$ and a linearly independent family of vectors $b : \iota \to (\iota \to K)$ in the vector space $\iota \to K$, the function constructs a basis for $\iota \to K$ using the vectors $b$. If $\iota$ is nonempty, it uses the dimension condition that the dimension of $\iota \to K$ equals the cardinality of $\iota$; otherwise, it constructs the empty basis.

coe_basisOfPiSpaceOfLinearIndependent theorem

 {ι : Type*} [Fintype ι] {b : ι → (ι → K)} (hb : LinearIndependent K b) : ⇑(basisOfPiSpaceOfLinearIndependent hb) = b

Full source

@[simp]
theorem coe_basisOfPiSpaceOfLinearIndependent {ι : Type*} [Fintype ι]
    {b : ι → (ι → K)} (hb : LinearIndependent K b) :
    ⇑(basisOfPiSpaceOfLinearIndependent hb) = b := by
  by_cases hι : Nonempty ι
  · simp [hι, basisOfPiSpaceOfLinearIndependent]
  · rw [basisOfPiSpaceOfLinearIndependent, dif_neg hι]
    ext i
    exact ((not_nonempty_iff.mp hι).false i).elim

Basis Construction in Function Space Preserves Given Vectors

Informal description

Given a finite index set $\iota$ and a linearly independent family of vectors $b : \iota \to (\iota \to K)$ in the function space $\iota \to K$, the basis constructed from $b$ via `basisOfPiSpaceOfLinearIndependent` coincides with $b$ as a function. That is, the basis vectors are exactly the vectors in the family $b$.

finsetBasisOfLinearIndependentOfCardEqFinrank definition

 {s : Finset V} (hs : s.Nonempty) (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) :
  Basis s K V

Full source

/-- A linear independent finset of `finrank K V` vectors forms a basis. -/
@[simps! repr_apply]
noncomputable def finsetBasisOfLinearIndependentOfCardEqFinrank {s : Finset V} (hs : s.Nonempty)
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) : Basis s K V :=
  @basisOfLinearIndependentOfCardEqFinrank _ _ _ _ _ _
    ⟨(⟨hs.choose, hs.choose_spec⟩ : s)⟩ _ _ lin_ind (_root_.trans (Fintype.card_coe _) card_eq)

Basis from linearly independent set matching dimension

Informal description

Given a nonempty finite set $s$ of vectors in a finite-dimensional vector space $V$ over a field $K$, if the vectors in $s$ are linearly independent and the cardinality of $s$ equals the dimension of $V$, then the inclusion map from $s$ to $V$ forms a basis for $V$.

coe_finsetBasisOfLinearIndependentOfCardEqFinrank theorem

 {s : Finset V} (hs : s.Nonempty) (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) :
  ⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = ((↑) : s → V)

Full source

@[simp]
theorem coe_finsetBasisOfLinearIndependentOfCardEqFinrank {s : Finset V} (hs : s.Nonempty)
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) :
    ⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = ((↑) : s → V) := by
  simp [finsetBasisOfLinearIndependentOfCardEqFinrank]

Basis Construction from Finite Set Preserves Inclusion Map

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $s$ be a nonempty finite subset of $V$. If the inclusion map from $s$ to $V$ is linearly independent and the cardinality of $s$ equals the dimension of $V$, then the basis constructed from $s$ via `finsetBasisOfLinearIndependentOfCardEqFinrank` coincides with the inclusion map. That is, the basis vectors are exactly the vectors in $s$.

setBasisOfLinearIndependentOfCardEqFinrank definition

 {s : Set V} [Nonempty s] [Fintype s] (lin_ind : LinearIndependent K ((↑) : s → V))
  (card_eq : s.toFinset.card = finrank K V) : Basis s K V

Full source

/-- A linear independent set of `finrank K V` vectors forms a basis. -/
@[simps! repr_apply]
noncomputable def setBasisOfLinearIndependentOfCardEqFinrank {s : Set V} [Nonempty s] [Fintype s]
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.toFinset.card = finrank K V) :
    Basis s K V :=
  basisOfLinearIndependentOfCardEqFinrank lin_ind (_root_.trans s.toFinset_card.symm card_eq)

Basis from linearly independent set matching dimension

Informal description

Given a finite-dimensional vector space $V$ over a field $K$, a nonempty finite subset $s$ of $V$, and a linearly independent family of vectors obtained by the inclusion map from $s$ to $V$ such that the cardinality of $s$ equals the dimension of $V$, the function constructs a basis for $V$ using the vectors in $s$.

coe_setBasisOfLinearIndependentOfCardEqFinrank theorem

 {s : Set V} [Nonempty s] [Fintype s] (lin_ind : LinearIndependent K ((↑) : s → V))
  (card_eq : s.toFinset.card = finrank K V) :
  ⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = ((↑) : s → V)

Full source

@[simp]
theorem coe_setBasisOfLinearIndependentOfCardEqFinrank {s : Set V} [Nonempty s] [Fintype s]
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.toFinset.card = finrank K V) :
    ⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = ((↑) : s → V) := by
  simp [setBasisOfLinearIndependentOfCardEqFinrank]

Basis Construction from Subset Preserves Inclusion Map

Informal description

Given a finite-dimensional vector space $V$ over a field $K$, a nonempty finite subset $s$ of $V$, and a linearly independent family of vectors obtained by the inclusion map from $s$ to $V$ such that the cardinality of $s$ equals the dimension of $V$, the basis constructed from $s$ via `setBasisOfLinearIndependentOfCardEqFinrank` coincides with the inclusion map from $s$ to $V$. That is, the basis vectors are exactly the vectors in the subset $s$.

is_simple_module_of_finrank_eq_one theorem

{A} [Semiring A] [Module A V] [SMul K A] [IsScalarTower K A V] (h : finrank K V = 1) : IsSimpleOrder (Submodule A V)

Full source

/-- Any `K`-algebra module that is 1-dimensional over `K` is simple. -/
theorem is_simple_module_of_finrank_eq_one {A} [Semiring A] [Module A V] [SMul K A]
    [IsScalarTower K A V] (h : finrank K V = 1) : IsSimpleOrder (Submodule A V) := by
  haveI := nontrivial_of_finrank_eq_succ h
  refine ⟨fun S => or_iff_not_imp_left.2 fun hn => ?_⟩
  rw [← restrictScalars_inj K] at hn ⊢
  haveI : FiniteDimensional _ _ := .of_finrank_eq_succ h
  refine eq_top_of_finrank_eq ((Submodule.finrank_le _).antisymm ?_)
  simpa only [h, finrank_bot] using Submodule.finrank_strictMono (Ne.bot_lt hn)

One-Dimensional Modules are Simple

Informal description

Let $V$ be a vector space over a division ring $K$ with $\dim_K V = 1$, and let $A$ be a semiring with a module structure on $V$ and a scalar multiplication action of $K$ on $A$ such that $K$'s action factors through $A$ (i.e., $[IsScalarTower K A V]$). Then the lattice of $A$-submodules of $V$ is simple, meaning it has no nontrivial proper submodules.

Subalgebra.isSimpleOrder_of_finrank theorem

(hr : finrank F E = 2) : IsSimpleOrder (Subalgebra F E)

Full source

theorem Subalgebra.isSimpleOrder_of_finrank (hr : finrank F E = 2) :
    IsSimpleOrder (Subalgebra F E) :=
  let i := nontrivial_of_finrank_pos (zero_lt_two.trans_eq hr.symm)
  { toNontrivial :=
      ⟨⟨⊥, ⊤, fun h => by cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)⟩⟩
    eq_bot_or_eq_top := by
      intro S
      haveI : FiniteDimensional F E := .of_finrank_eq_succ hr
      haveI : FiniteDimensional F S :=
        FiniteDimensional.finiteDimensional_submodule (Subalgebra.toSubmodule S)
      have : finrank F S ≤ 2 := hr ▸ S.toSubmodule.finrank_le
      have : 0 < finrank F S := finrank_pos_iff.mpr inferInstance
      interval_cases h : finrank F { x // x ∈ S }
      · left
        exact Subalgebra.eq_bot_of_finrank_one h
      · right
        rw [← hr] at h
        rw [← Algebra.toSubmodule_eq_top]
        exact eq_top_of_finrank_eq h }

Simplicity of Subalgebra Lattice for Field Extensions of Dimension 2

Informal description

For a field extension $E$ over $F$, if the dimension of $E$ as a vector space over $F$ is equal to 2, then the lattice of subalgebras of $E$ over $F$ is simple (i.e., it has no nontrivial proper subalgebras).

Module.End.exists_ker_pow_eq_ker_pow_succ theorem

 [FiniteDimensional K V] (f : End K V) : ∃ k : ℕ, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)

Full source

theorem exists_ker_pow_eq_ker_pow_succ [FiniteDimensional K V] (f : End K V) :
    ∃ k : ℕ, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ) := by
  classical
    by_contra h_contra
    simp_rw [not_exists, not_and] at h_contra
    have h_le_ker_pow : ∀ n : ℕ, n ≤ (finrank K V).succ →
        n ≤ finrank K (LinearMap.ker (f ^ n)) := by
      intro n hn
      induction n with
      | zero => exact zero_le (finrank _ _)
      | succ n ih =>
        have h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ) := by
          refine lt_of_le_of_ne ?_ (h_contra n (Nat.le_of_succ_le_succ hn))
          rw [pow_succ']
          apply LinearMap.ker_le_ker_comp
        have h_finrank_lt_finrank :
            finrank K (LinearMap.ker (f ^ n)) < finrank K (LinearMap.ker (f ^ n.succ)) := by
          apply Submodule.finrank_lt_finrank_of_lt h_ker_lt_ker
        calc
          n.succ ≤ (finrank K ↑(LinearMap.ker (f ^ n))).succ :=
            Nat.succ_le_succ (ih (Nat.le_of_succ_le hn))
          _ ≤ finrank K ↑(LinearMap.ker (f ^ n.succ)) := Nat.succ_le_of_lt h_finrank_lt_finrank
    have h_any_n_lt : ∀ n, n ≤ (finrank K V).succ → n ≤ finrank K V := fun n hn =>
      (h_le_ker_pow n hn).trans (Submodule.finrank_le _)
    show False
    exact Nat.not_succ_le_self _ (h_any_n_lt (finrank K V).succ (finrank K V).succ.le_refl)

Stabilization of Kernel Powers for Finite-Dimensional Endomorphisms

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f$ be an endomorphism of $V$. Then there exists a natural number $k \leq \dim_K V$ such that the kernel of $f^k$ equals the kernel of $f^{k+1}$.

Module.End.ker_pow_eq_ker_pow_finrank_of_le theorem

 [FiniteDimensional K V] {f : End K V} {m : ℕ} (hm : finrank K V ≤ m) :
  LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)

Full source

theorem ker_pow_eq_ker_pow_finrank_of_le [FiniteDimensional K V] {f : End K V} {m : ℕ}
    (hm : finrank K V ≤ m) : LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V) := by
  obtain ⟨k, h_k_le, hk⟩ :
    ∃ k, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ) :=
    exists_ker_pow_eq_ker_pow_succ f
  calc
    LinearMap.ker (f ^ m) = LinearMap.ker (f ^ (k + (m - k))) := by
      rw [add_tsub_cancel_of_le (h_k_le.trans hm)]
    _ = LinearMap.ker (f ^ k) := by rw [ker_pow_constant hk _]
    _ = LinearMap.ker (f ^ (k + (finrank K V - k))) := ker_pow_constant hk (finrank K V - k)
    _ = LinearMap.ker (f ^ finrank K V) := by rw [add_tsub_cancel_of_le h_k_le]

Kernel Stabilization for Powers of an Endomorphism at Dimension

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f \colon V \to V$ be a linear endomorphism. For any natural number $m$ such that $\dim_K V \leq m$, the kernel of $f^m$ equals the kernel of $f^{\dim_K V}$.

Module.End.ker_pow_le_ker_pow_finrank theorem

[FiniteDimensional K V] (f : End K V) (m : ℕ) : LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Full source

theorem ker_pow_le_ker_pow_finrank [FiniteDimensional K V] (f : End K V) (m : ℕ) :
    LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V) := by
  by_cases h_cases : m < finrank K V
  · rw [← add_tsub_cancel_of_le (Nat.le_of_lt h_cases), add_comm, pow_add]
    apply LinearMap.ker_le_ker_comp
  · rw [ker_pow_eq_ker_pow_finrank_of_le (le_of_not_lt h_cases)]

Kernel Containment for Powers of an Endomorphism up to Dimension

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f \colon V \to V$ be a linear endomorphism. For any natural number $m$, the kernel of $f^m$ is contained in the kernel of $f^{\dim_K V}$.