Mathlib.LinearAlgebra.FiniteDimensional.Basic

LinearIndependent.lt_aleph0_of_finiteDimensional theorem

{ι : Type w} [FiniteDimensional K V] {v : ι → V} (h : LinearIndependent K v) : #ι < ℵ₀

Full source

theorem _root_.LinearIndependent.lt_aleph0_of_finiteDimensional {ι : Type w} [FiniteDimensional K V]
    {v : ι → V} (h : LinearIndependent K v) : #ι < ℵ₀ :=
  h.lt_aleph0_of_finite

Linear Independence Implies Finite Index Set in Finite-Dimensional Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $\{v_i\}_{i \in \iota}$ be a linearly independent family of vectors in $V$. Then the cardinality of the index set $\iota$ is strictly less than $\aleph_0$ (i.e., $\iota$ is finite).

FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card theorem

 [FiniteDimensional L W] {t : Finset W} (h : finrank L W + 1 < t.card) :
  ∃ f : W → L, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x

Full source

/-- A slight strengthening of `exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card`
available when working over an ordered field:
we can ensure a positive coefficient, not just a nonzero coefficient.
-/
theorem exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card [FiniteDimensional L W]
    {t : Finset W} (h : finrank L W + 1 < t.card) :
    ∃ f : W → L, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x := by
  obtain ⟨f, sum, total, nonzero⟩ :=
    Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card h
  exact ⟨f, sum, total, exists_pos_of_sum_zero_of_exists_nonzero f total nonzero⟩

Existence of Positive-Coefficient Linear Relation in Overdetermined System

Informal description

Let $W$ be a finite-dimensional vector space over a field $L$, and let $t$ be a finite set of vectors in $W$ such that $\text{finrank}_L W + 1 < |t|$. Then there exists a function $f : W \to L$ such that: 1. $\sum_{e \in t} f(e) \cdot e = 0$, 2. $\sum_{e \in t} f(e) = 0$, 3. There exists $x \in t$ with $f(x) > 0$.

FiniteDimensional.basisSingleton definition

(ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0) : Basis ι K V

Full source

/-- In a vector space with dimension 1, each set {v} is a basis for `v ≠ 0`. -/
@[simps repr_apply]
noncomputable def basisSingleton (ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V)
    (hv : v ≠ 0) : Basis ι K V :=
  let b := Module.basisUnique ι h
  let h : b.repr v default ≠ 0 := mt Module.basisUnique_repr_eq_zero_iff.mp hv
  Basis.ofRepr
    { toFun := fun w => Finsupp.single default (b.repr w default / b.repr v default)
      invFun := fun f => f default • v
      map_add' := by simp [add_div]
      map_smul' := by simp [mul_div]
      left_inv := fun w => by
        apply_fun b.repr using b.repr.toEquiv.injective
        apply_fun Equiv.finsuppUnique
        simp only [LinearEquiv.map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
          smul_eq_mul, Pi.smul_apply, Equiv.finsuppUnique_apply]
        exact div_mul_cancel₀ _ h
      right_inv := fun f => by
        ext
        simp only [LinearEquiv.map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
          RingHom.id_apply, smul_eq_mul, Pi.smul_apply]
        exact mul_div_cancel_right₀ _ h }

Basis consisting of a single nonzero vector in a 1-dimensional space

Informal description

Given a vector space $V$ over a field $K$ with $\text{finrank}_K V = 1$, a type $\iota$ with a unique element, and a nonzero vector $v \in V$, the function constructs a basis for $V$ consisting of the single vector $v$. More precisely, the basis $\text{basisSingleton}$ is defined such that for the unique index $i \in \iota$, $\text{basisSingleton}(\iota, h, v, hv)(i) = v$, and the range of this basis is exactly the singleton set $\{v\}$.

FiniteDimensional.basisSingleton_apply theorem

(ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0) (i : ι) : basisSingleton ι h v hv i = v

Full source

@[simp]
theorem basisSingleton_apply (ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0)
    (i : ι) : basisSingleton ι h v hv i = v := by
  cases Unique.uniq ‹Unique ι› i
  simp [basisSingleton]

Evaluation of Singleton Basis in 1-Dimensional Space

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$ with $\text{finrank}_K V = 1$. Given a type $\iota$ with a unique element and a nonzero vector $v \in V$, the basis $\text{basisSingleton}$ constructed from $v$ satisfies $\text{basisSingleton}(\iota, h, v, hv)(i) = v$ for the unique index $i \in \iota$.

FiniteDimensional.range_basisSingleton theorem

(ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0) : Set.range (basisSingleton ι h v hv) = { v }

Full source

@[simp]
theorem range_basisSingleton (ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0) :
    Set.range (basisSingleton ι h v hv) = {v} := by rw [Set.range_unique, basisSingleton_apply]

Range of Singleton Basis in 1-Dimensional Space is $\{v\}$

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$ with $\text{finrank}_K V = 1$. Given a type $\iota$ with a unique element and a nonzero vector $v \in V$, the range of the basis $\text{basisSingleton}(\iota, h, v, hv)$ is the singleton set $\{v\}$.

FiniteDimensional.of_rank_eq_nat theorem

{n : ℕ} (h : Module.rank K V = n) : FiniteDimensional K V

Full source

theorem FiniteDimensional.of_rank_eq_nat {n : ℕ} (h : Module.rank K V = n) :
    FiniteDimensional K V :=
  Module.finite_of_rank_eq_nat h

Finite-Dimensionality from Rank Equality to Natural Number

Informal description

For any natural number $n$, if the rank of a vector space $V$ over a division ring $K$ is equal to $n$, then $V$ is finite-dimensional.

FiniteDimensional.of_rank_eq_zero theorem

(h : Module.rank K V = 0) : FiniteDimensional K V

Full source

theorem FiniteDimensional.of_rank_eq_zero (h : Module.rank K V = 0) : FiniteDimensional K V :=
  Module.finite_of_rank_eq_zero h

Finite-dimensionality from zero rank

Informal description

Let $V$ be a vector space over a division ring $K$. If the rank of $V$ over $K$ is zero, then $V$ is finite-dimensional.

FiniteDimensional.of_rank_eq_one theorem

(h : Module.rank K V = 1) : FiniteDimensional K V

Full source

theorem FiniteDimensional.of_rank_eq_one (h : Module.rank K V = 1) : FiniteDimensional K V :=
  Module.finite_of_rank_eq_one h

Finite-Dimensionality from Rank One

Informal description

If the rank of a vector space $V$ over a division ring $K$ is equal to $1$, then $V$ is finite-dimensional.

finiteDimensional_bot instance

: FiniteDimensional K (⊥ : Submodule K V)

Full source

instance finiteDimensional_bot : FiniteDimensional K (⊥ : Submodule K V) :=
  .of_rank_eq_zero <| by simp

Finite-Dimensionality of the Zero Submodule

Informal description

The zero submodule $\{0\}$ of any vector space $V$ over a division ring $K$ is finite-dimensional.

Submodule.finiteDimensional_of_le theorem

{S₁ S₂ : Submodule K V} [FiniteDimensional K S₂] (h : S₁ ≤ S₂) : FiniteDimensional K S₁

Full source

/-- A submodule contained in a finite-dimensional submodule is
finite-dimensional. -/
theorem finiteDimensional_of_le {S₁ S₂ : Submodule K V} [FiniteDimensional K S₂] (h : S₁ ≤ S₂) :
    FiniteDimensional K S₁ :=
  (isNoetherian_of_le h).finite

Finite-dimensionality of submodules contained in finite-dimensional submodules

Informal description

Let $K$ be a division ring and $V$ a vector space over $K$. For any submodules $S₁$ and $S₂$ of $V$, if $S₂$ is finite-dimensional and $S₁$ is contained in $S₂$ (i.e., $S₁ \leq S₂$), then $S₁$ is also finite-dimensional.

Submodule.finiteDimensional_inf_left instance

(S₁ S₂ : Submodule K V) [FiniteDimensional K S₁] : FiniteDimensional K (S₁ ⊓ S₂ : Submodule K V)

Full source

/-- The inf of two submodules, the first finite-dimensional, is
finite-dimensional. -/
instance finiteDimensional_inf_left (S₁ S₂ : Submodule K V) [FiniteDimensional K S₁] :
    FiniteDimensional K (S₁ ⊓ S₂ : Submodule K V) :=
  finiteDimensional_of_le inf_le_left

Finite-Dimensionality of Intersection with Finite-Dimensional Submodule

Informal description

For any two submodules $S₁$ and $S₂$ of a vector space $V$ over a division ring $K$, if $S₁$ is finite-dimensional, then the intersection $S₁ \cap S₂$ is also finite-dimensional.

Submodule.finiteDimensional_inf_right instance

(S₁ S₂ : Submodule K V) [FiniteDimensional K S₂] : FiniteDimensional K (S₁ ⊓ S₂ : Submodule K V)

Full source

/-- The inf of two submodules, the second finite-dimensional, is
finite-dimensional. -/
instance finiteDimensional_inf_right (S₁ S₂ : Submodule K V) [FiniteDimensional K S₂] :
    FiniteDimensional K (S₁ ⊓ S₂ : Submodule K V) :=
  finiteDimensional_of_le inf_le_right

Finite-dimensionality of Submodule Intersection with Finite-dimensional Submodule

Informal description

For any two submodules $S₁$ and $S₂$ of a vector space $V$ over a division ring $K$, if $S₂$ is finite-dimensional, then the infimum (intersection) $S₁ \cap S₂$ is also finite-dimensional.

Submodule.finiteDimensional_sup instance

 (S₁ S₂ : Submodule K V) [h₁ : FiniteDimensional K S₁] [h₂ : FiniteDimensional K S₂] :
  FiniteDimensional K (S₁ ⊔ S₂ : Submodule K V)

Full source

/-- The sup of two finite-dimensional submodules is
finite-dimensional. -/
instance finiteDimensional_sup (S₁ S₂ : Submodule K V) [h₁ : FiniteDimensional K S₁]
    [h₂ : FiniteDimensional K S₂] : FiniteDimensional K (S₁ ⊔ S₂ : Submodule K V) := by
  unfold FiniteDimensional at *
  rw [finite_def] at *
  exact (fg_top _).2 (((fg_top S₁).1 h₁).sup ((fg_top S₂).1 h₂))

Finite-dimensionality of the Sum of Finite-dimensional Submodules

Informal description

For any two finite-dimensional submodules $S₁$ and $S₂$ of a vector space $V$ over a division ring $K$, the supremum (sum) $S₁ + S₂$ is also finite-dimensional.

Submodule.finiteDimensional_finset_sup instance

 {ι : Type*} (s : Finset ι) (S : ι → Submodule K V) [∀ i, FiniteDimensional K (S i)] :
  FiniteDimensional K (s.sup S : Submodule K V)

Full source

/-- The submodule generated by a finite supremum of finite dimensional submodules is
finite-dimensional.

Note that strictly this only needs `∀ i ∈ s, FiniteDimensional K (S i)`, but that doesn't
work well with typeclass search. -/
instance finiteDimensional_finset_sup {ι : Type*} (s : Finset ι) (S : ι → Submodule K V)
    [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K (s.sup S : Submodule K V) := by
  refine
    @Finset.sup_induction _ _ _ _ s S (fun i => FiniteDimensional K ↑i) (finiteDimensional_bot K V)
      ?_ fun i _ => by infer_instance
  intro S₁ hS₁ S₂ hS₂
  exact Submodule.finiteDimensional_sup S₁ S₂

Finite-Dimensionality of the Supremum of Finite-Dimensional Submodules over a Finite Index Set

Informal description

For any finite set $s$ of indices and family of submodules $(S_i)_{i \in s}$ of a vector space $V$ over a division ring $K$, if each $S_i$ is finite-dimensional, then the supremum $\bigsqcup_{i \in s} S_i$ (the submodule generated by the union of all $S_i$) is also finite-dimensional.

Submodule.finiteDimensional_iSup instance

 {ι : Sort*} [Finite ι] (S : ι → Submodule K V) [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K ↑(⨆ i, S i)

Full source

/-- The submodule generated by a supremum of finite dimensional submodules, indexed by a finite
sort is finite-dimensional. -/
instance finiteDimensional_iSup {ι : Sort*} [Finite ι] (S : ι → Submodule K V)
    [∀ i, FiniteDimensional K (S i)] : FiniteDimensional K ↑(⨆ i, S i) := by
  cases nonempty_fintype (PLift ι)
  rw [← iSup_plift_down, ← Finset.sup_univ_eq_iSup]
  exact Submodule.finiteDimensional_finset_sup _ _

Finite-Dimensionality of the Supremum of Finite-Dimensional Submodules over a Finite Index Set

Informal description

For any finite index set $\iota$ and family of submodules $(S_i)_{i \in \iota}$ of a vector space $V$ over a division ring $K$, if each $S_i$ is finite-dimensional, then the supremum $\bigsqcup_{i \in \iota} S_i$ (the submodule generated by the union of all $S_i$) is also finite-dimensional.

finiteDimensional_finsupp instance

{ι : Type*} [Finite ι] [FiniteDimensional K V] : FiniteDimensional K (ι →₀ V)

Full source

instance finiteDimensional_finsupp {ι : Type*} [Finite ι] [FiniteDimensional K V] :
    FiniteDimensional K (ι →₀ V) :=
  Module.Finite.finsupp

Finite-Dimensionality of Finitely Supported Functions over a Finite Index Set

Informal description

For any finite index set $\iota$ and finite-dimensional vector space $V$ over a division ring $K$, the space of finitely supported functions $\iota \to_{\text{f}} V$ is also finite-dimensional.

LinearMap.surjective_of_injective theorem

[FiniteDimensional K V] {f : V →ₗ[K] V} (hinj : Injective f) : Surjective f

Full source

/-- On a finite-dimensional space, an injective linear map is surjective. -/
theorem surjective_of_injective [FiniteDimensional K V] {f : V →ₗ[K] V} (hinj : Injective f) :
    Surjective f := by
  have h := rank_range_of_injective _ hinj
  rw [← finrank_eq_rank, ← finrank_eq_rank, Nat.cast_inj] at h
  exact range_eq_top.1 (eq_top_of_finrank_eq h)

Injective Linear Maps on Finite-Dimensional Spaces are Surjective

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f : V \to V$ be an injective linear map. Then $f$ is surjective.

LinearMap.finiteDimensional_of_surjective theorem

[FiniteDimensional K V] (f : V →ₗ[K] V₂) (hf : LinearMap.range f = ⊤) : FiniteDimensional K V₂

Full source

/-- The image under an onto linear map of a finite-dimensional space is also finite-dimensional. -/
theorem finiteDimensional_of_surjective [FiniteDimensional K V] (f : V →ₗ[K] V₂)
    (hf : LinearMap.range f = ⊤) : FiniteDimensional K V₂ :=
  Module.Finite.of_surjective f <| range_eq_top.1 hf

Surjective Linear Maps Preserve Finite-Dimensionality

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f : V \to V_2$ be a linear map. If $f$ is surjective (i.e., $\text{range}(f) = V_2$), then $V_2$ is also finite-dimensional over $K$.

LinearMap.finiteDimensional_range instance

[FiniteDimensional K V] (f : V →ₗ[K] V₂) : FiniteDimensional K (LinearMap.range f)

Full source

/-- The range of a linear map defined on a finite-dimensional space is also finite-dimensional. -/
instance finiteDimensional_range [FiniteDimensional K V] (f : V →ₗ[K] V₂) :
    FiniteDimensional K (LinearMap.range f) :=
  Module.Finite.range f

Finite-Dimensionality of the Range of a Linear Map

Informal description

For any finite-dimensional vector space $V$ over a division ring $K$ and any linear map $f : V \to V_2$, the range of $f$ is also a finite-dimensional vector space over $K$.

LinearMap.injective_iff_surjective theorem

[FiniteDimensional K V] {f : V →ₗ[K] V} : Injective f ↔ Surjective f

Full source

/-- On a finite-dimensional space, a linear map is injective if and only if it is surjective. -/
theorem injective_iff_surjective [FiniteDimensional K V] {f : V →ₗ[K] V} :
    InjectiveInjective f ↔ Surjective f :=
  ⟨surjective_of_injective, fun hsurj =>
    let ⟨g, hg⟩ := f.exists_rightInverse_of_surjective (range_eq_top.2 hsurj)
    have : Function.RightInverse g f := LinearMap.ext_iff.1 hg
    (leftInverse_of_surjective_of_rightInverse (surjective_of_injective this.injective)
        this).injective⟩

Equivalence of Injectivity and Surjectivity for Linear Maps on Finite-Dimensional Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$. For a linear map $f: V \to V$, the following are equivalent: 1. $f$ is injective. 2. $f$ is surjective.

LinearMap.injOn_iff_surjOn theorem

 {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) : Set.InjOn f p ↔ Set.SurjOn f p p

Full source

lemma injOn_iff_surjOn {p : Submodule K V} [FiniteDimensional K p]
    {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) :
    Set.InjOnSet.InjOn f p ↔ Set.SurjOn f p p := by
  rw [Set.injOn_iff_injective, ← Set.MapsTo.restrict_surjective_iff h]
  change InjectiveInjective (f.domRestrict p) ↔ Surjective (f.restrict h)
  simp [disjoint_iff, ← injective_iff_surjective]

Equivalence of Injectivity and Surjectivity for Linear Maps on Finite-Dimensional Submodules

Informal description

Let $V$ be a vector space over a division ring $K$, and let $p$ be a finite-dimensional submodule of $V$. For a linear map $f : V \to V$ such that $f(x) \in p$ for all $x \in p$, the following are equivalent: 1. $f$ is injective when restricted to $p$. 2. $f$ is surjective when restricted to $p$ (i.e., $f$ maps $p$ onto $p$).

LinearMap.ker_eq_bot_iff_range_eq_top theorem

[FiniteDimensional K V] {f : V →ₗ[K] V} : LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤

Full source

theorem ker_eq_bot_iff_range_eq_top [FiniteDimensional K V] {f : V →ₗ[K] V} :
    LinearMap.kerLinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤ := by
  rw [range_eq_top, ker_eq_bot, injective_iff_surjective]

Equivalence of Trivial Kernel and Full Range for Linear Maps on Finite-Dimensional Spaces

Informal description

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

LinearMap.mul_eq_one_of_mul_eq_one theorem

[FiniteDimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) : g * f = 1

Full source

/-- In a finite-dimensional space, if linear maps are inverse to each other on one side then they
are also inverse to each other on the other side. -/
theorem mul_eq_one_of_mul_eq_one [FiniteDimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) :
    g * f = 1 := by
  have ginj : Injective g :=
    HasLeftInverse.injective ⟨f, fun x => show (f * g) x = (1 : V →ₗ[K] V) x by rw [hfg]⟩
  let ⟨i, hi⟩ := g.exists_rightInverse_of_surjective
    (range_eq_top.2 (injective_iff_surjective.1 ginj))
  have : f * (g * i) = f * 1 := congr_arg _ hi
  rw [← mul_assoc, hfg, one_mul, mul_one] at this; rwa [← this]

One-Sided Inverse Implies Two-Sided Inverse for Linear Maps on Finite-Dimensional Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f, g : V \to V$ be linear maps. If $f \circ g = \text{id}_V$, then $g \circ f = \text{id}_V$.

LinearMap.mul_eq_one_comm theorem

[FiniteDimensional K V] {f g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1

Full source

/-- In a finite-dimensional space, linear maps are inverse to each other on one side if and only if
they are inverse to each other on the other side. -/
theorem mul_eq_one_comm [FiniteDimensional K V] {f g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1 :=
  ⟨mul_eq_one_of_mul_eq_one, mul_eq_one_of_mul_eq_one⟩

Equivalence of Left and Right Inverses for Linear Maps on Finite-Dimensional Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f, g \colon V \to V$ be linear maps. Then $f \circ g = \text{id}_V$ if and only if $g \circ f = \text{id}_V$.

LinearMap.comp_eq_id_comm theorem

[FiniteDimensional K V] {f g : V →ₗ[K] V} : f.comp g = id ↔ g.comp f = id

Full source

/-- In a finite-dimensional space, linear maps are inverse to each other on one side if and only if
they are inverse to each other on the other side. -/
theorem comp_eq_id_comm [FiniteDimensional K V] {f g : V →ₗ[K] V} : f.comp g = id ↔ g.comp f = id :=
  mul_eq_one_comm

Equivalence of Left and Right Inverses for Linear Maps on Finite-Dimensional Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f, g \colon V \to V$ be linear maps. Then $f \circ g = \text{id}_V$ if and only if $g \circ f = \text{id}_V$.

LinearMap.comap_eq_sup_ker_of_disjoint theorem

 {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) (h' : Disjoint p (ker f)) :
  p.comap f = p ⊔ ker f

Full source

theorem comap_eq_sup_ker_of_disjoint {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V}
    (h : ∀ x ∈ p, f x ∈ p) (h' : Disjoint p (ker f)) :
    p.comap f = p ⊔ ker f := by
  refine le_antisymm (fun x hx ↦ ?_) (sup_le_iff.mpr ⟨h, ker_le_comap _⟩)
  obtain ⟨⟨y, hy⟩, hxy⟩ :=
    surjective_of_injective ((injective_restrict_iff_disjoint h).mpr h') ⟨f x, hx⟩
  replace hxy : f y = f x := by simpa [Subtype.ext_iff] using hxy
  exact Submodule.mem_sup.mpr ⟨y, hy, x - y, by simp [hxy], add_sub_cancel y x⟩

Preimage of Submodule under Linear Map as Supremum with Kernel

Informal description

Let $V$ be a vector space over a division ring $K$, and let $p$ be a finite-dimensional submodule of $V$. Given a linear map $f : V \to V$ that preserves $p$ (i.e., $f(x) \in p$ for all $x \in p$) and such that $p$ is disjoint from the kernel of $f$, then the preimage of $p$ under $f$ equals the supremum of $p$ and the kernel of $f$, i.e., \[ f^{-1}(p) = p \sqcup \ker f. \]

LinearMap.ker_comp_eq_of_commute_of_disjoint_ker theorem

 [FiniteDimensional K V] {f g : V →ₗ[K] V} (h : Commute f g) (h' : Disjoint (ker f) (ker g)) :
  ker (f ∘ₗ g) = ker f ⊔ ker g

Full source

theorem ker_comp_eq_of_commute_of_disjoint_ker [FiniteDimensional K V] {f g : V →ₗ[K] V}
    (h : Commute f g) (h' : Disjoint (ker f) (ker g)) :
    ker (f ∘ₗ g) = kerker f ⊔ ker g := by
  suffices ∀ x, f x = 0 → f (g x) = 0 by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa
  intro x hx
  rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]

Kernel of Composition of Commuting Linear Maps with Disjoint Kernels

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f, g : V \to V$ be commuting linear maps (i.e., $f \circ g = g \circ f$) with disjoint kernels. Then the kernel of their composition $f \circ g$ is equal to the supremum of their individual kernels: \[ \ker(f \circ g) = \ker f \sqcup \ker g. \]

LinearMap.ker_noncommProd_eq_of_supIndep_ker theorem

 [FiniteDimensional K V] {ι : Type*} {f : ι → V →ₗ[K] V} (s : Finset ι) (comm) (h : s.SupIndep fun i ↦ ker (f i)) :
  ker (s.noncommProd f comm) = ⨆ i ∈ s, ker (f i)

Full source

theorem ker_noncommProd_eq_of_supIndep_ker [FiniteDimensional K V] {ι : Type*} {f : ι → V →ₗ[K] V}
    (s : Finset ι) (comm) (h : s.SupIndep fun i ↦ ker (f i)) :
    ker (s.noncommProd f comm) = ⨆ i ∈ s, ker (f i) := by
  classical
  induction s using Finset.induction_on with
  | empty => simp [Module.End.one_eq_id]
  | insert i s hi ih =>
    replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
        ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))
    rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
    · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
    · exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by aesop)
    · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
      simpa [ih, hi, Finset.sup_eq_iSup] using h

Kernel of Noncommutative Product of Linear Maps with Independent Kernels

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $\{f_i : V \to V\}_{i \in \iota}$ be a family of linear maps indexed by a type $\iota$. For any finite subset $s \subseteq \iota$ such that the kernels $\{\ker(f_i)\}_{i \in s}$ are independent in the lattice of submodules (i.e., $s$ is `SupIndep` with respect to the kernels), and for any proof `comm` that the $f_i$ commute pairwise, the kernel of their noncommutative product equals the supremum of their individual kernels: \[ \ker\left(\prod_{i \in s} f_i\right) = \bigsqcup_{i \in s} \ker(f_i). \]

LinearEquiv.ofInjectiveEndo definition

(f : V →ₗ[K] V) (h_inj : Injective f) : V ≃ₗ[K] V

Full source

/-- The linear equivalence corresponding to an injective endomorphism. -/
noncomputable def ofInjectiveEndo (f : V →ₗ[K] V) (h_inj : Injective f) : V ≃ₗ[K] V :=
  LinearEquiv.ofBijective f ⟨h_inj, LinearMap.injective_iff_surjective.mp h_inj⟩

Linear equivalence induced by an injective endomorphism

Informal description

Given a finite-dimensional vector space $V$ over a division ring $K$ and an injective linear endomorphism $f : V \to V$, the linear equivalence $\text{ofInjectiveEndo}\, f$ is defined as the bijective linear map from $V$ to itself, which exists because injectivity implies surjectivity in this context.

LinearEquiv.coe_ofInjectiveEndo theorem

(f : V →ₗ[K] V) (h_inj : Injective f) : ⇑(ofInjectiveEndo f h_inj) = f

Full source

@[simp]
theorem coe_ofInjectiveEndo (f : V →ₗ[K] V) (h_inj : Injective f) :
    ⇑(ofInjectiveEndo f h_inj) = f :=
  rfl

Underlying Function of Linear Equivalence for Injective Endomorphism

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f : V \to V$ be an injective linear map. Then the underlying function of the linear equivalence $\text{ofInjectiveEndo}\, f$ is equal to $f$ itself.

LinearEquiv.ofInjectiveEndo_right_inv theorem

(f : V →ₗ[K] V) (h_inj : Injective f) : f * (ofInjectiveEndo f h_inj).symm = 1

Full source

@[simp]
theorem ofInjectiveEndo_right_inv (f : V →ₗ[K] V) (h_inj : Injective f) :
    f * (ofInjectiveEndo f h_inj).symm = 1 :=
  LinearMap.ext <| (ofInjectiveEndo f h_inj).apply_symm_apply

Right Inverse Property of Linear Equivalence for Injective Endomorphisms

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f : V \to V$ be an injective linear map. Then the composition of $f$ with the inverse of the linear equivalence $\text{ofInjectiveEndo}\, f$ is the identity map on $V$, i.e., $f \circ f^{-1} = \text{id}_V$.

LinearEquiv.ofInjectiveEndo_left_inv theorem

(f : V →ₗ[K] V) (h_inj : Injective f) : ((ofInjectiveEndo f h_inj).symm : V →ₗ[K] V) * f = 1

Full source

@[simp]
theorem ofInjectiveEndo_left_inv (f : V →ₗ[K] V) (h_inj : Injective f) :
    ((ofInjectiveEndo f h_inj).symm : V →ₗ[K] V) * f = 1 :=
  LinearMap.ext <| (ofInjectiveEndo f h_inj).symm_apply_apply

Left Inverse Property of Linear Equivalence for Injective Endomorphisms

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f : V \to V$ be an injective linear map. Then the composition of the inverse of the linear equivalence $\text{ofInjectiveEndo}\, f$ with $f$ is the identity map on $V$, i.e., $f^{-1} \circ f = \text{id}_V$.

LinearMap.isUnit_iff_ker_eq_bot theorem

[FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ (LinearMap.ker f) = ⊥

Full source

theorem isUnit_iff_ker_eq_bot [FiniteDimensional K V] (f : V →ₗ[K] V) :
    IsUnitIsUnit f ↔ (LinearMap.ker f) = ⊥ := by
  constructor
  · rintro ⟨u, rfl⟩
    exact LinearMap.ker_eq_bot_of_inverse u.inv_mul
  · intro h_inj
    rw [ker_eq_bot] at h_inj
    exact ⟨⟨f, (LinearEquiv.ofInjectiveEndo f h_inj).symm.toLinearMap,
      LinearEquiv.ofInjectiveEndo_right_inv f h_inj, LinearEquiv.ofInjectiveEndo_left_inv f h_inj⟩,
      rfl⟩

Invertibility of Linear Endomorphism is Equivalent to Trivial Kernel in Finite Dimensions

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$. For a linear endomorphism $f : V \to V$, the following are equivalent: 1. $f$ is invertible (i.e., $f$ is a unit in the ring of linear endomorphisms). 2. The kernel of $f$ is trivial (i.e., $\ker f = \{0\}$).

LinearMap.isUnit_iff_range_eq_top theorem

[FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ (LinearMap.range f) = ⊤

Full source

theorem isUnit_iff_range_eq_top [FiniteDimensional K V] (f : V →ₗ[K] V) :
    IsUnitIsUnit f ↔ (LinearMap.range f) = ⊤ := by
  rw [isUnit_iff_ker_eq_bot, ker_eq_bot_iff_range_eq_top]

Invertibility of Linear Endomorphism is Equivalent to Full Range in Finite Dimensions

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$. For a linear endomorphism $f : V \to V$, the following are equivalent: 1. $f$ is invertible (i.e., $f$ is a unit in the ring of linear endomorphisms). 2. The range of $f$ is the entire space $V$ (i.e., $\operatorname{range} f = V$).

finrank_zero_iff_forall_zero theorem

[FiniteDimensional K V] : finrank K V = 0 ↔ ∀ x : V, x = 0

Full source

theorem finrank_zero_iff_forall_zero [FiniteDimensional K V] : finrankfinrank K V = 0 ↔ ∀ x : V, x = 0 :=
  Module.finrank_zero_iff.trans (subsingleton_iff_forall_eq 0)

Zero-Dimensional Vector Space Characterization: $\text{finrank}_K V = 0 \leftrightarrow V = \{0\}$

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$. The dimension of $V$ is zero if and only if every vector in $V$ is the zero vector, i.e., $\text{finrank}_K V = 0 \leftrightarrow \forall x \in V, x = 0$.

basisOfFinrankZero definition

[FiniteDimensional K V] {ι : Type*} [IsEmpty ι] (hV : finrank K V = 0) : Basis ι K V

Full source

/-- If `ι` is an empty type and `V` is zero-dimensional, there is a unique `ι`-indexed basis. -/
noncomputable def basisOfFinrankZero [FiniteDimensional K V] {ι : Type*} [IsEmpty ι]
    (hV : finrank K V = 0) : Basis ι K V :=
  haveI : Subsingleton V := finrank_zero_iff.1 hV
  Basis.empty _

Basis of a zero-dimensional vector space over an empty index set

Informal description

Given a finite-dimensional vector space $V$ over a field $K$ with $\text{finrank}_K V = 0$ and an empty index type $\iota$, there exists a unique basis of $V$ indexed by $\iota$. This basis is constructed using the fact that $V$ is a zero-dimensional space (and hence a singleton set).

FiniteDimensional.exists_mul_eq_one theorem

 (F : Type*) {K : Type*} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) :
  ∃ y, x * y = 1

Full source

lemma FiniteDimensional.exists_mul_eq_one (F : Type*) {K : Type*} [Field F] [Ring K] [IsDomain K]
    [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : ∃ y, x * y = 1 := by
  have : Function.Surjective (LinearMap.mulLeft F x) :=
    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
  exact this 1

Existence of Multiplicative Inverse in Finite-Dimensional Algebras over Fields

Informal description

Let $F$ be a field and $K$ be a domain with an $F$-algebra structure. If $K$ is finite-dimensional as a vector space over $F$, then for any nonzero element $x \in K$, there exists an element $y \in K$ such that $x \cdot y = 1$.

divisionRingOfFiniteDimensional definition

(F K : Type*) [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] : DivisionRing K

Full source

/-- A domain that is module-finite as an algebra over a field is a division ring. -/
noncomputable def divisionRingOfFiniteDimensional (F K : Type*) [Field F] [Ring K] [IsDomain K]
    [Algebra F K] [FiniteDimensional F K] : DivisionRing K where
  __ := ‹IsDomain K›
  inv x :=
    letI := Classical.decEq K
    if H : x = 0 then 0 else Classical.choose <| FiniteDimensional.exists_mul_eq_one F H
  mul_inv_cancel x hx := show x * dite _ (h := _) _ _ = _ by
    rw [dif_neg hx]
    exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)
  inv_zero := dif_pos rfl
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl

Finite-dimensional algebra over a field is a division ring

Informal description

Given a field $F$ and a domain $K$ with an $F$-algebra structure, if $K$ is finite-dimensional as a vector space over $F$, then $K$ is a division ring. This means every nonzero element $x \in K$ has a multiplicative inverse $x^{-1} \in K$ such that $x \cdot x^{-1} = 1$.

FiniteDimensional.isUnit theorem

 (F : Type*) {K : Type*} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) :
  IsUnit x

Full source

lemma FiniteDimensional.isUnit (F : Type*) {K : Type*} [Field F] [Ring K] [IsDomain K]
    [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : IsUnit x :=
  let _ := divisionRingOfFiniteDimensional F K; H.isUnit

Nonzero Elements in Finite-Dimensional Algebras over Fields are Units

Informal description

Let $F$ be a field and $K$ be a domain with an $F$-algebra structure. If $K$ is finite-dimensional as a vector space over $F$, then every nonzero element $x \in K$ is a unit (i.e., has a multiplicative inverse in $K$).

fieldOfFiniteDimensional definition

(F K : Type*) [Field F] [h : CommRing K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] : Field K

Full source

/-- An integral domain that is module-finite as an algebra over a field is a field. -/
noncomputable def fieldOfFiniteDimensional (F K : Type*) [Field F] [h : CommRing K] [IsDomain K]
    [Algebra F K] [FiniteDimensional F K] : Field K :=
  { divisionRingOfFiniteDimensional F K with
    toCommRing := h }

Finite-dimensional algebra over a field is a field

Informal description

Given a field $F$ and a commutative domain $K$ with an $F$-algebra structure, if $K$ is finite-dimensional as a vector space over $F$, then $K$ is a field. This means every nonzero element $x \in K$ has a multiplicative inverse $x^{-1} \in K$ such that $x \cdot x^{-1} = 1$, and multiplication is commutative.

finrank_span_singleton theorem

{v : V} (hv : v ≠ 0) : finrank K (K ∙ v) = 1

Full source

theorem finrank_span_singleton {v : V} (hv : v ≠ 0) : finrank K (K ∙ v) = 1 := by
  apply le_antisymm
  · exact finrank_span_le_card ({v} : Set V)
  · rw [Nat.succ_le_iff, finrank_pos_iff]
    use ⟨v, mem_span_singleton_self v⟩, 0
    apply Subtype.coe_ne_coe.mp
    simp [hv]

Dimension of Span of a Nonzero Vector is One

Informal description

For any nonzero vector $v$ in a vector space $V$ over a field $K$, the dimension of the span of $\{v\}$ is equal to $1$, i.e., $\dim_K (K \cdot v) = 1$.

exists_smul_eq_of_finrank_eq_one theorem

(h : finrank K V = 1) {x : V} (hx : x ≠ 0) (y : V) : ∃ (c : K), c • x = y

Full source

/-- In a one-dimensional space, any vector is a multiple of any nonzero vector -/
lemma exists_smul_eq_of_finrank_eq_one
    (h : finrank K V = 1) {x : V} (hx : x ≠ 0) (y : V) :
    ∃ (c : K), c • x = y := by
  have : Submodule.span K {x} = ⊤ := by
    have : FiniteDimensional K V := .of_finrank_eq_succ h
    apply eq_top_of_finrank_eq
    rw [h]
    exact finrank_span_singleton hx
  have : y ∈ Submodule.span K {x} := by rw [this]; exact mem_top
  exact mem_span_singleton.1 this

Characterization of One-Dimensional Vector Spaces: Every Vector is a Scalar Multiple of a Nonzero Vector

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$ with $\dim_K V = 1$. For any nonzero vector $x \in V$ and any vector $y \in V$, there exists a scalar $c \in K$ such that $y = c \cdot x$.

Set.finrank_mono theorem

[FiniteDimensional K V] {s t : Set V} (h : s ⊆ t) : s.finrank K ≤ t.finrank K

Full source

theorem Set.finrank_mono [FiniteDimensional K V] {s t : Set V} (h : s ⊆ t) :
    s.finrank K ≤ t.finrank K :=
  Submodule.finrank_mono (span_mono h)

Monotonicity of Dimension under Subset Inclusion 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 subsets of $V$ such that $s \subseteq t$. Then the dimension of the subspace spanned by $s$ is less than or equal to the dimension of the subspace spanned by $t$, i.e., $\dim_K \text{span}(s) \leq \dim_K \text{span}(t)$.

finrank_eq_one_iff_of_nonzero theorem

(v : V) (nz : v ≠ 0) : finrank K V = 1 ↔ span K ({ v } : Set V) = ⊤

Full source

/-- A vector space with a nonzero vector `v` has dimension 1 iff `v` spans.
-/
theorem finrank_eq_one_iff_of_nonzero (v : V) (nz : v ≠ 0) :
    finrankfinrank K V = 1 ↔ span K ({v} : Set V) = ⊤ :=
  ⟨fun h => by simpa using (basisSingleton Unit h v nz).span_eq, fun s =>
    finrank_eq_card_basis
      (Basis.mk (LinearIndepOn.id_singleton _ nz)
        (by simp [← s]))⟩

Dimension One Characterization via Span of a Nonzero Vector

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $v \in V$ be a nonzero vector. Then the dimension of $V$ over $K$ is 1 if and only if the span of $\{v\}$ is the entire space $V$, i.e., $\text{span}_K(\{v\}) = V$.

finrank_eq_one_iff_of_nonzero' theorem

(v : V) (nz : v ≠ 0) : finrank K V = 1 ↔ ∀ w : V, ∃ c : K, c • v = w

Full source

/-- A module with a nonzero vector `v` has dimension 1 iff every vector is a multiple of `v`.
-/
theorem finrank_eq_one_iff_of_nonzero' (v : V) (nz : v ≠ 0) :
    finrankfinrank K V = 1 ↔ ∀ w : V, ∃ c : K, c • v = w := by
  rw [finrank_eq_one_iff_of_nonzero v nz]
  apply span_singleton_eq_top_iff

Dimension One Characterization via Scalar Multiples of a Nonzero Vector

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $v \in V$ be a nonzero vector. Then the dimension of $V$ over $K$ is 1 if and only if every vector $w \in V$ can be written as a scalar multiple of $v$, i.e., there exists $c \in K$ such that $w = c \cdot v$.

surjective_of_nonzero_of_finrank_eq_one theorem

 {W A : Type*} [Semiring A] [Module A V] [AddCommGroup W] [Module K W] [Module A W] [LinearMap.CompatibleSMul V W K A]
  (h : finrank K W = 1) {f : V →ₗ[A] W} (w : f ≠ 0) : Surjective f

Full source

theorem surjective_of_nonzero_of_finrank_eq_one {W A : Type*} [Semiring A] [Module A V]
    [AddCommGroup W] [Module K W] [Module A W] [LinearMap.CompatibleSMul V W K A]
    (h : finrank K W = 1) {f : V →ₗ[A] W} (w : f ≠ 0) : Surjective f := by
  change Surjective (f.restrictScalars K)
  obtain ⟨v, n⟩ := DFunLike.ne_iff.mp w
  intro z
  obtain ⟨c, rfl⟩ := (finrank_eq_one_iff_of_nonzero' (f v) n).mp h z
  exact ⟨c • v, by simp⟩

Surjectivity of Nonzero Linear Maps to One-Dimensional Spaces

Informal description

Let $V$ and $W$ be vector spaces over a field $K$, with $W$ having dimension 1. Let $A$ be a semiring and suppose $V$ is an $A$-module while $W$ is both a $K$-module and an $A$-module with compatible scalar actions. For any nonzero $A$-linear map $f: V \to W$, the map $f$ is surjective.

Subalgebra.finiteDimensional_toSubmodule theorem

{S : Subalgebra F E} : FiniteDimensional F (Subalgebra.toSubmodule S) ↔ FiniteDimensional F S

Full source

/-- A `Subalgebra` is `FiniteDimensional` iff it is `FiniteDimensional` as a submodule. -/
theorem Subalgebra.finiteDimensional_toSubmodule {S : Subalgebra F E} :
    FiniteDimensionalFiniteDimensional F (Subalgebra.toSubmodule S) ↔ FiniteDimensional F S :=
  Iff.rfl

Finite-Dimensionality of Subalgebra and its Underlying Submodule

Informal description

For any subalgebra $S$ of an algebra $E$ over a field $F$, the subalgebra $S$ is finite-dimensional over $F$ if and only if the underlying submodule of $S$ is finite-dimensional over $F$.

FiniteDimensional.finiteDimensional_subalgebra instance

[FiniteDimensional F E] (S : Subalgebra F E) : FiniteDimensional F S

Full source

instance FiniteDimensional.finiteDimensional_subalgebra [FiniteDimensional F E]
    (S : Subalgebra F E) : FiniteDimensional F S :=
  FiniteDimensional.of_subalgebra_toSubmodule inferInstance

Finite-Dimensionality of Subalgebras in Finite-Dimensional Algebras

Informal description

Every subalgebra $S$ of a finite-dimensional algebra $E$ over a field $F$ is itself finite-dimensional over $F$.

Module.End.ker_pow_constant theorem

 {f : End K V} {k : ℕ} (h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)) :
  ∀ m, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))

Full source

theorem ker_pow_constant {f : End K V} {k : ℕ}
    (h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)) :
    ∀ m, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))
  | 0 => by simp
  | m + 1 => by
    apply le_antisymm
    · rw [add_comm, pow_add]
      apply LinearMap.ker_le_ker_comp
    · rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]

Stabilization of Kernel Powers for Linear Endomorphisms

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $f \colon V \to V$ be a linear endomorphism. For any natural number $k$, if the kernel of $f^k$ equals the kernel of $f^{k+1}$, then for all natural numbers $m$, the kernel of $f^k$ equals the kernel of $f^{k+m}$.

Mathlib.LinearAlgebra.FiniteDimensional.Basic

Main definitions

Implementation notes