[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V ↔ Module.rank K V < ℵ₀
[PROOFSTEP]
let b := Basis.ofVectorSpace K V
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V ↔ Module.rank K V < ℵ₀
[PROOFSTEP]
rw [← b.mk_eq_rank'', lt_aleph0_iff_set_finite]
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V ↔ Set.Finite (Basis.ofVectorSpaceIndex K V)
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V → Set.Finite (Basis.ofVectorSpaceIndex K V)
[PROOFSTEP]
intro
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
a✝ : IsNoetherian K V
⊢ Set.Finite (Basis.ofVectorSpaceIndex K V)
[PROOFSTEP]
exact finite_of_linearIndependent (Basis.ofVectorSpaceIndex.linearIndependent K V)
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ Set.Finite (Basis.ofVectorSpaceIndex K V) → IsNoetherian K V
[PROOFSTEP]
intro hbfinite
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : Set.Finite (Basis.ofVectorSpaceIndex K V)
⊢ IsNoetherian K V
[PROOFSTEP]
refine' @isNoetherian_of_linearEquiv K (⊤ : Submodule K V) V _ _ _ _ _ (LinearEquiv.ofTop _ rfl) (id _)
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : Set.Finite (Basis.ofVectorSpaceIndex K V)
⊢ IsNoetherian K { x // x ∈ ⊤ }
[PROOFSTEP]
refine' isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, _⟩
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : Set.Finite (Basis.ofVectorSpaceIndex K V)
⊢ span K ↑(Set.Finite.toFinset hbfinite) = ⊤
[PROOFSTEP]
rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsNoetherian K V
⊢ ↑(Basis.ofVectorSpaceIndex K V) ≃ { x // x ∈ finsetBasisIndex K V }
[PROOFSTEP]
rw [coeSort_finsetBasisIndex]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsNoetherian K V
⊢ Set.range ↑(finsetBasis K V) = Basis.ofVectorSpaceIndex K V
[PROOFSTEP]
rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V ↔ Module.Finite K V
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V → Module.Finite K V
[PROOFSTEP]
intro h
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ Module.Finite K V
[PROOFSTEP]
exact
  ⟨⟨finsetBasisIndex K V, by
      convert (finsetBasis K V).span_eq
      simp⟩⟩
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ span K ↑(finsetBasisIndex K V) = ⊤
[PROOFSTEP]
convert (finsetBasis K V).span_eq
[GOAL]
case h.e'_2.h.e'_6
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ ↑(finsetBasisIndex K V) = Set.range ↑(finsetBasis K V)
[PROOFSTEP]
simp
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.Finite K V → IsNoetherian K V
[PROOFSTEP]
rintro ⟨s, hs⟩
[GOAL]
case mpr.mk.intro
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : span K ↑s = ⊤
⊢ IsNoetherian K V
[PROOFSTEP]
rw [IsNoetherian.iff_rank_lt_aleph0, ← rank_top, ← hs]
[GOAL]
case mpr.mk.intro
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : span K ↑s = ⊤
⊢ Module.rank K { x // x ∈ span K ↑s } < ℵ₀
[PROOFSTEP]
exact lt_of_le_of_lt (rank_span_le _) s.finite_toSet.lt_aleph0
