Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Basis.ofRankEqZero definition

[Module.Free K V] {ι : Type*} [IsEmpty ι] (hV : Module.rank K V = 0) : Basis ι K V

Full source

/-- The `ι` indexed basis on `V`, where `ι` is an empty type and `V` is zero-dimensional.

See also `Module.finBasis`.
-/
noncomputable def Basis.ofRankEqZero [Module.Free K V] {ι : Type*} [IsEmpty ι]
    (hV : Module.rank K V = 0) : Basis ι K V :=
  haveI : Subsingleton V := by
    obtain ⟨_, b⟩ := Module.Free.exists_basis (R := K) (M := V)
    haveI := mk_eq_zero_iff.1 (hV ▸ b.mk_eq_rank'')
    exact b.repr.toEquiv.subsingleton
  Basis.empty _

Basis for zero-rank free module

Informal description

Given a free module $V$ over a ring $K$ with rank $0$ and an empty index type $\iota$, this defines a basis of $V$ indexed by $\iota$. Since $V$ has rank $0$, it is the zero module, and the basis is the empty basis (as $\iota$ is empty).

Basis.ofRankEqZero_apply theorem

[Module.Free K V] {ι : Type*} [IsEmpty ι] (hV : Module.rank K V = 0) (i : ι) : Basis.ofRankEqZero hV i = 0

Full source

@[simp]
theorem Basis.ofRankEqZero_apply [Module.Free K V] {ι : Type*} [IsEmpty ι]
    (hV : Module.rank K V = 0) (i : ι) : Basis.ofRankEqZero hV i = 0 := rfl

Zero Vector Property of Empty Basis in Zero-Rank Free Module

Informal description

Let $V$ be a free module over a ring $K$ with rank $0$, and let $\iota$ be an empty index type. For any $i \in \iota$, the basis vector $\text{Basis.ofRankEqZero}\, hV\, i$ is equal to $0$.

le_rank_iff_exists_linearIndependent theorem

[Module.Free K V] {c : Cardinal} : c ≤ Module.rank K V ↔ ∃ s : Set V, #s = c ∧ LinearIndepOn K id s

Full source

theorem le_rank_iff_exists_linearIndependent [Module.Free K V] {c : Cardinal} :
    c ≤ Module.rank K V ↔ ∃ s : Set V, #s = c ∧ LinearIndepOn K id s := by
  haveI := nontrivial_of_invariantBasisNumber K
  constructor
  · intro h
    obtain ⟨κ, t'⟩ := Module.Free.exists_basis (R := K) (M := V)
    let t := t'.reindexRange
    have : LinearIndepOn K id (Set.range t') := by
      convert t.linearIndependent.linearIndepOn_id
      ext
      simp [t]
    rw [← t.mk_eq_rank'', le_mk_iff_exists_subset] at h
    rcases h with ⟨s, hst, hsc⟩
    exact ⟨s, hsc, this.mono hst⟩
  · rintro ⟨s, rfl, si⟩
    exact si.cardinal_le_rank

Linear Independence Criterion for Subsets in Free Modules over Strong Rank Condition Rings

Informal description

Let $V$ be a free module over a ring $K$ satisfying the strong rank condition, and let $c$ be a cardinal number. Then $c \leq \dim_K V$ if and only if there exists a subset $S \subseteq V$ with cardinality $c$ that is linearly independent over $K$.

le_rank_iff_exists_linearIndependent_finset theorem

 [Module.Free K V] {n : ℕ} :
  ↑n ≤ Module.rank K V ↔ ∃ s : Finset V, s.card = n ∧ LinearIndependent K ((↑) : ↥(s : Set V) → V)

Full source

theorem le_rank_iff_exists_linearIndependent_finset
    [Module.Free K V] {n : ℕ} : ↑n ≤ Module.rank K V ↔
    ∃ s : Finset V, s.card = n ∧ LinearIndependent K ((↑) : ↥(s : Set V) → V) := by
  simp only [le_rank_iff_exists_linearIndependent, mk_set_eq_nat_iff_finset]
  constructor
  · rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩
    exact ⟨t, rfl, si⟩
  · rintro ⟨s, rfl, si⟩
    exact ⟨s, ⟨s, rfl, rfl⟩, si⟩

Linear Independence Criterion for Finite Subsets in Free Modules over Strong Rank Condition Rings

Informal description

Let $V$ be a free module over a ring $K$ satisfying the strong rank condition. For any natural number $n$, the inequality $n \leq \dim_K V$ holds if and only if there exists a finite subset $s \subseteq V$ with $|s| = n$ such that the set $s$ is linearly independent over $K$.

rank_le_one_iff theorem

[Module.Free K V] : Module.rank K V ≤ 1 ↔ ∃ v₀ : V, ∀ v, ∃ r : K, r • v₀ = v

Full source

/-- A vector space has dimension at most `1` if and only if there is a
single vector of which all vectors are multiples. -/
theorem rank_le_one_iff [Module.Free K V] :
    Module.rankModule.rank K V ≤ 1 ↔ ∃ v₀ : V, ∀ v, ∃ r : K, r • v₀ = v := by
  obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := V)
  constructor
  · intro hd
    rw [← b.mk_eq_rank'', le_one_iff_subsingleton] at hd
    rcases isEmpty_or_nonempty κ with hb | ⟨⟨i⟩⟩
    · use 0
      have h' : ∀ v : V, v = 0 := by
        simpa [range_eq_empty, Submodule.eq_bot_iff] using b.span_eq.symm
      intro v
      simp [h' v]
    · use b i
      have h' : (K ∙ b i) = ⊤ :=
        (subsingleton_range b).eq_singleton_of_mem (mem_range_self i) ▸ b.span_eq
      intro v
      have hv : v ∈ (⊤ : Submodule K V) := mem_top
      rwa [← h', mem_span_singleton] at hv
  · rintro ⟨v₀, hv₀⟩
    have h : (K ∙ v₀) = ⊤ := by
      ext
      simp [mem_span_singleton, hv₀]
    rw [← rank_top, ← h]
    refine (rank_span_le _).trans_eq ?_
    simp

Rank At Most One iff Module is Generated by a Single Vector

Informal description

Let $K$ be a ring satisfying the strong rank condition and $V$ a free $K$-module. The rank of $V$ is at most $1$ if and only if there exists a vector $v_0 \in V$ such that every vector $v \in V$ is a scalar multiple of $v_0$ (i.e., there exists $r \in K$ such that $v = r \cdot v_0$).

rank_eq_one_iff theorem

[Module.Free K V] : Module.rank K V = 1 ↔ ∃ v₀ : V, v₀ ≠ 0 ∧ ∀ v, ∃ r : K, r • v₀ = v

Full source

/-- A vector space has dimension `1` if and only if there is a
single non-zero vector of which all vectors are multiples. -/
theorem rank_eq_one_iff [Module.Free K V] :
    Module.rankModule.rank K V = 1 ↔ ∃ v₀ : V, v₀ ≠ 0 ∧ ∀ v, ∃ r : K, r • v₀ = v := by
  haveI := nontrivial_of_invariantBasisNumber K
  refine ⟨fun h ↦ ?_, fun ⟨v₀, h, hv⟩ ↦ (rank_le_one_iff.2 ⟨v₀, hv⟩).antisymm ?_⟩
  · obtain ⟨v₀, hv⟩ := rank_le_one_iff.1 h.le
    refine ⟨v₀, fun hzero ↦ ?_, hv⟩
    simp_rw [hzero, smul_zero, exists_const] at hv
    haveI : Subsingleton V := .intro fun _ _ ↦ by simp_rw [← hv]
    exact one_ne_zero (h ▸ rank_subsingleton' K V)
  · by_contra H
    rw [not_le, lt_one_iff_zero] at H
    obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := V)
    haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
    haveI := b.repr.toEquiv.subsingleton
    exact h (Subsingleton.elim _ _)

Characterization of rank-one free modules via spanning vectors

Informal description

Let $K$ be a ring satisfying the strong rank condition and $V$ a free $K$-module. The rank of $V$ is equal to $1$ if and only if there exists a nonzero vector $v_0 \in V$ such that every vector $v \in V$ is a scalar multiple of $v_0$ (i.e., there exists $r \in K$ such that $v = r \cdot v_0$).

rank_submodule_le_one_iff theorem

(s : Submodule K V) [Module.Free K s] : Module.rank K s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀

Full source

/-- A submodule has dimension at most `1` if and only if there is a
single vector in the submodule such that the submodule is contained in
its span. -/
theorem rank_submodule_le_one_iff (s : Submodule K V) [Module.Free K s] :
    Module.rankModule.rank K s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀ := by
  simp_rw [rank_le_one_iff, le_span_singleton_iff]
  constructor
  · rintro ⟨⟨v₀, hv₀⟩, h⟩
    use v₀, hv₀
    intro v hv
    obtain ⟨r, hr⟩ := h ⟨v, hv⟩
    use r
    rwa [Subtype.ext_iff, coe_smul] at hr
  · rintro ⟨v₀, hv₀, h⟩
    use ⟨v₀, hv₀⟩
    rintro ⟨v, hv⟩
    obtain ⟨r, hr⟩ := h v hv
    use r
    rwa [Subtype.ext_iff, coe_smul]

Submodule Rank At Most One iff Contained in a Single Vector's Span

Informal description

Let $K$ be a ring satisfying the strong rank condition, $V$ a free $K$-module, and $s$ a submodule of $V$. Then the rank of $s$ is at most 1 if and only if there exists a vector $v_0 \in s$ such that $s$ is contained in the span of $v_0$ (i.e., $s \subseteq K \cdot v_0$).

rank_submodule_eq_one_iff theorem

(s : Submodule K V) [Module.Free K s] : Module.rank K s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀

Full source

/-- A submodule has dimension `1` if and only if there is a
single non-zero vector in the submodule such that the submodule is contained in
its span. -/
theorem rank_submodule_eq_one_iff (s : Submodule K V) [Module.Free K s] :
    Module.rankModule.rank K s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀ := by
  simp_rw [rank_eq_one_iff, le_span_singleton_iff]
  refine ⟨fun ⟨⟨v₀, hv₀⟩, H, h⟩ ↦ ⟨v₀, hv₀, fun h' ↦ by
    simp only [h', ne_eq] at H; exact H rfl, fun v hv ↦ ?_⟩,
    fun ⟨v₀, hv₀, H, h⟩ ↦ ⟨⟨v₀, hv₀⟩,
      fun h' ↦ H (by rwa [AddSubmonoid.mk_eq_zero] at h'), fun ⟨v, hv⟩ ↦ ?_⟩⟩
  · obtain ⟨r, hr⟩ := h ⟨v, hv⟩
    exact ⟨r, by rwa [Subtype.ext_iff, coe_smul] at hr⟩
  · obtain ⟨r, hr⟩ := h v hv
    exact ⟨r, by rwa [Subtype.ext_iff, coe_smul]⟩

Characterization of rank-one submodules via spanning vectors

Informal description

Let $K$ be a ring satisfying the strong rank condition, $V$ a free $K$-module, and $s$ a free submodule of $V$. Then the rank of $s$ is equal to 1 if and only if there exists a nonzero vector $v_0 \in s$ such that $s$ is contained in the span of $v_0$ (i.e., $s \subseteq K \cdot v_0$).

rank_submodule_le_one_iff' theorem

(s : Submodule K V) [Module.Free K s] : Module.rank K s ≤ 1 ↔ ∃ v₀, s ≤ K ∙ v₀

Full source

/-- A submodule has dimension at most `1` if and only if there is a
single vector, not necessarily in the submodule, such that the
submodule is contained in its span. -/
theorem rank_submodule_le_one_iff' (s : Submodule K V) [Module.Free K s] :
    Module.rankModule.rank K s ≤ 1 ↔ ∃ v₀, s ≤ K ∙ v₀ := by
  haveI := nontrivial_of_invariantBasisNumber K
  constructor
  · rw [rank_submodule_le_one_iff]
    rintro ⟨v₀, _, h⟩
    exact ⟨v₀, h⟩
  · rintro ⟨v₀, h⟩
    obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := s)
    simpa [b.mk_eq_rank''] using b.linearIndependent.map' _ (ker_inclusion _ _ h)
      |>.cardinal_le_rank.trans (rank_span_le {v₀})

Submodule Rank At Most One iff Contained in Span of a Single Vector

Informal description

Let $K$ be a ring satisfying the strong rank condition, $V$ a free $K$-module, and $s$ a submodule of $V$. Then the rank of $s$ is at most 1 if and only if there exists a vector $v_0 \in V$ (not necessarily in $s$) such that $s$ is contained in the span of $v_0$ (i.e., $s \subseteq K \cdot v_0$).

Submodule.rank_le_one_iff_isPrincipal theorem

(W : Submodule K V) [Module.Free K W] : Module.rank K W ≤ 1 ↔ W.IsPrincipal

Full source

theorem Submodule.rank_le_one_iff_isPrincipal (W : Submodule K V) [Module.Free K W] :
    Module.rankModule.rank K W ≤ 1 ↔ W.IsPrincipal := by
  simp only [rank_le_one_iff, Submodule.isPrincipal_iff, le_antisymm_iff, le_span_singleton_iff,
    span_singleton_le_iff_mem]
  constructor
  · rintro ⟨⟨m, hm⟩, hm'⟩
    choose f hf using hm'
    exact ⟨m, ⟨fun v hv => ⟨f ⟨v, hv⟩, congr_arg ((↑) : W → V) (hf ⟨v, hv⟩)⟩, hm⟩⟩
  · rintro ⟨a, ⟨h, ha⟩⟩
    choose f hf using h
    exact ⟨⟨a, ha⟩, fun v => ⟨f v.1 v.2, Subtype.ext (hf v.1 v.2)⟩⟩

Rank of Submodule is at Most One if and only if Principal

Informal description

Let $K$ be a ring satisfying the strong rank condition, $V$ a free module over $K$, and $W$ a submodule of $V$. Then the rank of $W$ is at most 1 if and only if $W$ is a principal submodule (i.e., generated by a single element).

Module.rank_le_one_iff_top_isPrincipal theorem

[Module.Free K V] : Module.rank K V ≤ 1 ↔ (⊤ : Submodule K V).IsPrincipal

Full source

theorem Module.rank_le_one_iff_top_isPrincipal [Module.Free K V] :
    Module.rankModule.rank K V ≤ 1 ↔ (⊤ : Submodule K V).IsPrincipal := by
  haveI := Module.Free.of_equiv (topEquiv (R := K) (M := V)).symm
  rw [← Submodule.rank_le_one_iff_isPrincipal, rank_top]

Rank at Most One iff Module is Principal

Informal description

Let $K$ be a ring satisfying the strong rank condition and $V$ a free module over $K$. Then the rank of $V$ is at most 1 if and only if the top submodule of $V$ (i.e., $V$ itself) is principal (i.e., generated by a single element).

finrank_eq_one_iff theorem

[Module.Free K V] (ι : Type*) [Unique ι] : finrank K V = 1 ↔ Nonempty (Basis ι K V)

Full source

/-- A module has dimension 1 iff there is some `v : V` so `{v}` is a basis.
-/
theorem finrank_eq_one_iff [Module.Free K V] (ι : Type*) [Unique ι] :
    finrankfinrank K V = 1 ↔ Nonempty (Basis ι K V) := by
  constructor
  · intro h
    exact ⟨Module.basisUnique ι h⟩
  · rintro ⟨b⟩
    simpa using finrank_eq_card_basis b

Finite Dimension One iff Basis Exists for Singleton Index Type

Informal description

Let $V$ be a free module over a field $K$. The finite dimension of $V$ over $K$ is equal to 1 if and only if there exists a basis for $V$ indexed by a type $\iota$ with exactly one element.

finrank_eq_one_iff' theorem

[Module.Free K V] : finrank K V = 1 ↔ ∃ v ≠ 0, ∀ w : V, ∃ c : K, c • v = w

Full source

/-- A module has dimension 1 iff there is some nonzero `v : V` so every vector is a multiple of `v`.
-/
theorem finrank_eq_one_iff' [Module.Free K V] :
    finrankfinrank K V = 1 ↔ ∃ v ≠ 0, ∀ w : V, ∃ c : K, c • v = w := by
  rw [← rank_eq_one_iff]
  exact toNat_eq_iff one_ne_zero

Finite Dimension One Characterization via Spanning Vector

Informal description

Let $K$ be a ring satisfying the strong rank condition and $V$ a free $K$-module. The finite dimension of $V$ over $K$ is equal to $1$ if and only if there exists a nonzero vector $v \in V$ such that every vector $w \in V$ is a scalar multiple of $v$ (i.e., there exists $c \in K$ such that $w = c \cdot v$).

finrank_le_one_iff theorem

[Module.Free K V] [Module.Finite K V] : finrank K V ≤ 1 ↔ ∃ v : V, ∀ w : V, ∃ c : K, c • v = w

Full source

/-- A finite dimensional module has dimension at most 1 iff
there is some `v : V` so every vector is a multiple of `v`.
-/
theorem finrank_le_one_iff [Module.Free K V] [Module.Finite K V] :
    finrankfinrank K V ≤ 1 ↔ ∃ v : V, ∀ w : V, ∃ c : K, c • v = w := by
  rw [← rank_le_one_iff, ← finrank_eq_rank, Nat.cast_le_one]

Finite Dimension At Most One iff Module is Generated by a Single Vector

Informal description

Let $K$ be a ring satisfying the strong rank condition and $V$ a finite-dimensional free $K$-module. The finite dimension of $V$ over $K$ is at most 1 if and only if there exists a vector $v \in V$ such that every vector $w \in V$ is a scalar multiple of $v$ (i.e., there exists $c \in K$ such that $w = c \cdot v$).

Submodule.finrank_le_one_iff_isPrincipal theorem

(W : Submodule K V) [Module.Free K W] [Module.Finite K W] : finrank K W ≤ 1 ↔ W.IsPrincipal

Full source

theorem Submodule.finrank_le_one_iff_isPrincipal
    (W : Submodule K V) [Module.Free K W] [Module.Finite K W] :
    finrankfinrank K W ≤ 1 ↔ W.IsPrincipal := by
  rw [← W.rank_le_one_iff_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

Finite Rank of Submodule is at Most One if and only if Principal

Informal description

Let $K$ be a ring satisfying the strong rank condition, $V$ a free and finite module over $K$, and $W$ a submodule of $V$. Then the finite rank of $W$ is at most 1 if and only if $W$ is a principal submodule (i.e., generated by a single element).

Module.finrank_le_one_iff_top_isPrincipal theorem

[Module.Free K V] [Module.Finite K V] : finrank K V ≤ 1 ↔ (⊤ : Submodule K V).IsPrincipal

Full source

theorem Module.finrank_le_one_iff_top_isPrincipal [Module.Free K V] [Module.Finite K V] :
    finrankfinrank K V ≤ 1 ↔ (⊤ : Submodule K V).IsPrincipal := by
  rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

Finite-dimensional free module has dimension ≤1 iff principal

Informal description

Let $K$ be a ring satisfying the strong rank condition and $V$ a finite-dimensional free $K$-module. The finite dimension of $V$ over $K$ is at most 1 if and only if $V$ is a principal module (i.e., generated by a single element).

lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank theorem

[Module.Free K V] [Module.Finite K V] : lift.{u} #V = lift.{v} #K ^ lift.{u} (Module.rank K V)

Full source

theorem lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank [Module.Free K V]
    [Module.Finite K V] : lift.{u} #V = lift.{v} #K ^ lift.{u} (Module.rank K V) := by
  haveI := nontrivial_of_invariantBasisNumber K
  obtain ⟨s, hs⟩ := Module.Free.exists_basis (R := K) (M := V)
  -- `Module.Finite.finite_basis` is in a much later file, so we copy its proof to here
  haveI : Finite s := by
    obtain ⟨t, ht⟩ := ‹Module.Finite K V›
    exact basis_finite_of_finite_spans t.finite_toSet ht hs
  have := lift_mk_eq'.2 ⟨hs.repr.toEquiv⟩
  rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this

Cardinality of Finite-Dimensional Free Module as Power of Base Ring's Cardinality (Lifted Universe Version)

Informal description

Let $K$ be a ring satisfying the strong rank condition and $V$ a finite-dimensional free $K$-module. Then the cardinality of $V$ (lifted to a higher universe) equals the cardinality of $K$ (lifted to a higher universe) raised to the power of the rank of $V$ (also lifted to the same higher universe). In symbols: $$\text{lift}_{\{u\}} |V| = \text{lift}_{\{v\}} |K|^{\text{lift}_{\{u\}} (\text{rank}_K V)}$$

cardinalMk_eq_cardinalMk_field_pow_rank theorem

 (K V : Type u) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
  #V = #K ^ Module.rank K V

Full source

theorem cardinalMk_eq_cardinalMk_field_pow_rank (K V : Type u) [Ring K] [StrongRankCondition K]
    [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
    #V = #K ^ Module.rank K V := by
  simpa using lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V

Cardinality of Finite-Dimensional Free Module as Power of Base Ring's Cardinality

Informal description

Let $K$ be a ring satisfying the strong rank condition and $V$ a finite-dimensional free $K$-module. Then the cardinality of $V$ equals the cardinality of $K$ raised to the power of the rank of $V$ over $K$. In symbols: $$|V| = |K|^{\text{rank}_K V}$$

cardinal_lt_aleph0_of_finiteDimensional theorem

[Finite K] [Module.Free K V] [Module.Finite K V] : #V < ℵ₀

Full source

theorem cardinal_lt_aleph0_of_finiteDimensional [Finite K] [Module.Free K V] [Module.Finite K V] :
    #V < ℵ₀ := by
  rw [← lift_lt_aleph0.{v, u}, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V]
  exact power_lt_aleph0 (lift_lt_aleph0.2 (lt_aleph0_of_finite K))
    (lift_lt_aleph0.2 (rank_lt_aleph0 K V))

Finite-Dimensional Free Modules over Finite Rings Have Finite Cardinality

Informal description

Let $K$ be a finite ring and $V$ a finite-dimensional free $K$-module. Then the cardinality of $V$ is strictly less than $\aleph_0$ (the cardinality of countably infinite sets).

Subalgebra.rank_eq_one_iff theorem

[Nontrivial E] [Module.Free F S] : Module.rank F S = 1 ↔ S = ⊥

Full source

@[simp]
theorem rank_eq_one_iff [Nontrivial E] [Module.Free F S] : Module.rankModule.rank F S = 1 ↔ S = ⊥ := by
  refine ⟨fun h ↦ Subalgebra.eq_bot_of_rank_le_one h.le, ?_⟩
  rintro rfl
  obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := (⊥ : Subalgebra F E))
  refine le_antisymm ?_ ?_
  · have := lift_rank_range_le (Algebra.linearMap F E)
    rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this
  · by_contra H
    rw [not_le, lt_one_iff_zero] at H
    haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
    haveI := b.repr.toEquiv.subsingleton
    exact one_ne_zero congr((⊥ : Subalgebra F E).val $(Subsingleton.elim 1 0))

Rank-One Subalgebra Characterization in Nontrivial Algebras

Informal description

Let $F$ be a field and $E$ a nontrivial $F$-algebra. For any $F$-subalgebra $S$ of $E$ that is free as an $F$-module, the rank of $S$ over $F$ equals 1 if and only if $S$ is the trivial subalgebra (i.e., $S = \bot$).

Subalgebra.finrank_eq_one_iff theorem

[Nontrivial E] [Module.Free F S] : finrank F S = 1 ↔ S = ⊥

Full source

@[simp]
theorem finrank_eq_one_iff [Nontrivial E] [Module.Free F S] : finrankfinrank F S = 1 ↔ S = ⊥ := by
  rw [← Subalgebra.rank_eq_one_iff]
  exact toNat_eq_iff one_ne_zero

Finite Rank-One Subalgebra Characterization in Nontrivial Algebras

Informal description

Let $F$ be a field and $E$ a nontrivial $F$-algebra. For any $F$-subalgebra $S$ of $E$ that is free as an $F$-module, the finite rank of $S$ over $F$ equals 1 if and only if $S$ is the trivial subalgebra (i.e., $S = \bot$).

Subalgebra.bot_eq_top_iff_rank_eq_one theorem

[Nontrivial E] [Module.Free F E] : (⊥ : Subalgebra F E) = ⊤ ↔ Module.rank F E = 1

Full source

theorem bot_eq_top_iff_rank_eq_one [Nontrivial E] [Module.Free F E] :
    (⊥ : Subalgebra F E) = ⊤ ↔ Module.rank F E = 1 := by
  haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
  -- Porting note: removed `subalgebra_top_rank_eq_submodule_top_rank`
  rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]

Triviality of Subalgebra Equivalence to Rank One: $\bot = \top \leftrightarrow \text{rank}_F E = 1$

Informal description

Let $F$ be a field and $E$ a nontrivial $F$-algebra that is free as an $F$-module. The trivial subalgebra $\bot$ of $E$ equals the entire algebra $\top$ if and only if the rank of $E$ as an $F$-module is $1$.

Subalgebra.bot_eq_top_iff_finrank_eq_one theorem

[Nontrivial E] [Module.Free F E] : (⊥ : Subalgebra F E) = ⊤ ↔ finrank F E = 1

Full source

theorem bot_eq_top_iff_finrank_eq_one [Nontrivial E] [Module.Free F E] :
    (⊥ : Subalgebra F E) = ⊤ ↔ finrank F E = 1 := by
  haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
  rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
    Subalgebra.finrank_eq_one_iff, eq_comm]

Trivial Subalgebra Equals Entire Algebra iff Finite Rank is One

Informal description

Let $F$ be a field and $E$ a nontrivial $F$-algebra that is free as an $F$-module. The trivial subalgebra $\bot$ of $E$ equals the entire algebra $\top$ if and only if the finite rank of $E$ as an $F$-module is $1$.