chore(LinearAlgebra/Dimension): generalize and golf (leanprover-community#32339)

LinearAlgebra/Dimension/Finite.lean: generalize Ring/AddCommGroup to Semiring/AddCommMonoid whenever possible

LinearAlgebra/Dimension/DivisionRing.lean: generalize DivisionRing to OrzechProperty, move to new file OrzechProperty.lean

Author: alreadydone

Mathlib.lean

@@ -4502,6 +4502,7 @@ public import Mathlib.LinearAlgebra.Dimension.Free
 public import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 public import Mathlib.LinearAlgebra.Dimension.LinearMap
 public import Mathlib.LinearAlgebra.Dimension.Localization
+public import Mathlib.LinearAlgebra.Dimension.OrzechProperty
 public import Mathlib.LinearAlgebra.Dimension.RankNullity
 public import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 public import Mathlib.LinearAlgebra.Dimension.Subsingleton

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -6,6 +6,7 @@ Authors: Xavier Roblot
 module
 
 public import Mathlib.LinearAlgebra.Countable
+public import Mathlib.LinearAlgebra.Dimension.OrzechProperty
 public import Mathlib.LinearAlgebra.FreeModule.PID
 public import Mathlib.MeasureTheory.Group.FundamentalDomain
 public import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Mathlib/FieldTheory/PerfectClosure.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.CharP.Lemmas
 public import Mathlib.FieldTheory.Perfect
+public import Mathlib.LinearAlgebra.Dimension.OrzechProperty
 
 /-!
 

Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.CharP.Lemmas
 public import Mathlib.Algebra.CharP.IntermediateField
 public import Mathlib.FieldTheory.PurelyInseparable.Basic
+public import Mathlib.LinearAlgebra.Dimension.OrzechProperty
 
 /-!
 

Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

@@ -9,6 +9,7 @@ public import Mathlib.FieldTheory.Finiteness
 public import Mathlib.LinearAlgebra.AffineSpace.Basis
 public import Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
 public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+public import Mathlib.LinearAlgebra.Dimension.OrzechProperty
 
 /-!
 # Finite-dimensional subspaces of affine spaces.

Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

@@ -35,8 +35,8 @@ noncomputable section
 
 universe u₀ u v v' v'' u₁' w w'
 
-variable {K R : Type u} {V V₁ V₂ V₃ : Type v} {V' V'₁ : Type v'} {V'' : Type v''}
-variable {ι : Type w} {ι' : Type w'} {η : Type u₁'} {φ : η → Type*}
+variable {K : Type u} {V V₁ V₂ V₃ : Type v}
+variable {ι : Type w}
 
 open Cardinal Basis Submodule Function Set
 
@@ -46,7 +46,6 @@ section DivisionRing
 
 variable [DivisionRing K]
 variable [AddCommGroup V] [Module K V]
-variable [AddCommGroup V'] [Module K V']
 variable [AddCommGroup V₁] [Module K V₁]
 
 /-- If a vector space has a finite dimension, the index set of `Basis.ofVectorSpace` is finite. -/
@@ -106,110 +105,3 @@ end
 end DivisionRing
 
 end Module
-
-section Basis
-
-open Module
-
-variable [DivisionRing K] [AddCommGroup V] [Module K V]
-
-theorem linearIndependent_of_top_le_span_of_card_eq_finrank {ι : Type*} [Fintype ι] {b : ι → V}
-    (spans : ⊤ ≤ span K (Set.range b)) (card_eq : Fintype.card ι = finrank K V) :
-    LinearIndependent K b :=
-  linearIndependent_iff'.mpr fun s g dependent i i_mem_s => by
-    classical
-    by_contra gx_ne_zero
-    -- We'll derive a contradiction by showing `b '' (univ \ {i})` of cardinality `n - 1`
-    -- spans a vector space of dimension `n`.
-    refine not_le_of_gt (span_lt_top_of_card_lt_finrank
-      (show (b '' (Set.univ \ {i})).toFinset.card < finrank K V from ?_)) ?_
-    · calc
-        (b '' (Set.univ \ {i})).toFinset.card = ((Set.univ \ {i}).toFinset.image b).card := by
-          rw [Set.toFinset_card, Fintype.card_ofFinset]
-        _ ≤ (Set.univ \ {i}).toFinset.card := Finset.card_image_le
-        _ = (Finset.univ.erase i).card := (congr_arg Finset.card (Finset.ext (by simp [and_comm])))
-        _ < Finset.univ.card := Finset.card_erase_lt_of_mem (Finset.mem_univ i)
-        _ = finrank K V := card_eq
-    -- We already have that `b '' univ` spans the whole space,
-    -- so we only need to show that the span of `b '' (univ \ {i})` contains each `b j`.
-    refine spans.trans (span_le.mpr ?_)
-    rintro _ ⟨j, rfl, rfl⟩
-    -- The case that `j ≠ i` is easy because `b j ∈ b '' (univ \ {i})`.
-    by_cases j_eq : j = i
-    swap
-    · refine subset_span ⟨j, (Set.mem_diff _).mpr ⟨Set.mem_univ _, ?_⟩, rfl⟩
-      exact mt Set.mem_singleton_iff.mp j_eq
-    -- To show `b i ∈ span (b '' (univ \ {i}))`, we use that it's a weighted sum
-    -- of the other `b j`s.
-    rw [j_eq, SetLike.mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum fun j => g j • b j) from _]
-    · refine neg_mem (smul_mem _ _ (sum_mem fun k hk => ?_))
-      obtain ⟨k_ne_i, _⟩ := Finset.mem_erase.mp hk
-      refine smul_mem _ _ (subset_span ⟨k, ?_, rfl⟩)
-      simp_all only [Set.mem_univ, Set.mem_diff, Set.mem_singleton_iff, and_self, not_false_eq_true]
-    -- To show `b i` is a weighted sum of the other `b j`s, we'll rewrite this sum
-    -- to have the form of the assumption `dependent`.
-    apply eq_neg_of_add_eq_zero_left
-    calc
-      (b i + (g i)⁻¹ • (s.erase i).sum fun j => g j • b j) =
-          (g i)⁻¹ • (g i • b i + (s.erase i).sum fun j => g j • b j) := by
-        rw [smul_add, ← mul_smul, inv_mul_cancel₀ gx_ne_zero, one_smul]
-      _ = (g i)⁻¹ • (0 : V) := congr_arg _ ?_
-      _ = 0 := smul_zero _
-    -- And then it's just a bit of manipulation with finite sums.
-    rwa [← Finset.insert_erase i_mem_s, Finset.sum_insert (Finset.notMem_erase _ _)] at dependent
-
-/-- A finite family of vectors is linearly independent if and only if
-its cardinality equals the dimension of its span. -/
-theorem linearIndependent_iff_card_eq_finrank_span {ι : Type*} [Fintype ι] {b : ι → V} :
-    LinearIndependent K b ↔ Fintype.card ι = (Set.range b).finrank K := by
-  constructor
-  · intro h
-    exact (finrank_span_eq_card h).symm
-  · intro hc
-    let f := Submodule.subtype (span K (Set.range b))
-    let b' : ι → span K (Set.range b) := fun i =>
-      ⟨b i, mem_span.2 fun p hp => hp (Set.mem_range_self _)⟩
-    have hs : ⊤ ≤ span K (Set.range b') := by
-      intro x
-      have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
-      have hf : f '' Set.range b' = Set.range b := by
-        ext x
-        simp [f, b', Set.mem_image, Set.mem_range]
-      rw [hf] at h
-      have hx : (x : V) ∈ span K (Set.range b) := x.property
-      simp_rw [h] at hx
-      simpa [f, mem_map] using hx
-    have hi : LinearMap.ker f = ⊥ := ker_subtype _
-    convert (linearIndependent_of_top_le_span_of_card_eq_finrank hs hc).map' _ hi
-
-theorem linearIndependent_iff_card_le_finrank_span {ι : Type*} [Fintype ι] {b : ι → V} :
-    LinearIndependent K b ↔ Fintype.card ι ≤ (Set.range b).finrank K := by
-  rw [linearIndependent_iff_card_eq_finrank_span, (finrank_range_le_card _).ge_iff_eq']
-
-/-- A family of `finrank K V` vectors forms a basis if they span the whole space. -/
-noncomputable def basisOfTopLeSpanOfCardEqFinrank {ι : Type*} [Fintype ι] (b : ι → V)
-    (le_span : ⊤ ≤ span K (Set.range b)) (card_eq : Fintype.card ι = finrank K V) : Basis ι K V :=
-  Basis.mk (linearIndependent_of_top_le_span_of_card_eq_finrank le_span card_eq) le_span
-
-@[simp]
-theorem coe_basisOfTopLeSpanOfCardEqFinrank {ι : Type*} [Fintype ι] (b : ι → V)
-    (le_span : ⊤ ≤ span K (Set.range b)) (card_eq : Fintype.card ι = finrank K V) :
-    ⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b :=
-  Basis.coe_mk _ _
-
-/-- A finset of `finrank K V` vectors forms a basis if they span the whole space. -/
-@[simps! repr_apply]
-noncomputable def finsetBasisOfTopLeSpanOfCardEqFinrank {s : Finset V}
-    (le_span : ⊤ ≤ span K (s : Set V)) (card_eq : s.card = finrank K V) : Basis {x // x ∈ s} K V :=
-  basisOfTopLeSpanOfCardEqFinrank ((↑) : ↥(s : Set V) → V)
-    ((@Subtype.range_coe_subtype _ fun x => x ∈ s).symm ▸ le_span)
-    (_root_.trans (Fintype.card_coe _) card_eq)
-
-/-- A set of `finrank K V` vectors forms a basis if they span the whole space. -/
-@[simps! repr_apply]
-noncomputable def setBasisOfTopLeSpanOfCardEqFinrank {s : Set V} [Fintype s]
-    (le_span : ⊤ ≤ span K s) (card_eq : s.toFinset.card = finrank K V) : Basis s K V :=
-  basisOfTopLeSpanOfCardEqFinrank ((↑) : s → V) ((@Subtype.range_coe_subtype _ s).symm ▸ le_span)
-    (_root_.trans s.toFinset_card.symm card_eq)
-
-end Basis

Mathlib/LinearAlgebra/Dimension/Finite.lean

@@ -24,9 +24,9 @@ noncomputable section
 
 universe u v v' w
 
-variable {R : Type u} {M M₁ : Type v} {M' : Type v'} {ι : Type w}
-variable [Ring R] [AddCommGroup M] [AddCommGroup M'] [AddCommGroup M₁]
-variable [Module R M] [Module R M'] [Module R M₁]
+variable {R : Type u} {M : Type v} {ι : Type w}
+variable [Semiring R] [AddCommMonoid M]
+variable [Module R M]
 
 attribute [local instance] nontrivial_of_invariantBasisNumber
 
@@ -56,7 +56,7 @@ theorem rank_le {n : ℕ}
 section RankZero
 
 /-- See `rank_zero_iff` for a stronger version with `NoZeroSMulDivisor R M`. -/
-lemma rank_eq_zero_iff :
+lemma rank_eq_zero_iff {R M} [Ring R] [AddCommGroup M] [Module R M] :
     Module.rank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0 := by
   nontriviality R
   constructor
@@ -77,7 +77,7 @@ lemma rank_eq_zero_iff :
     apply ha
     simpa using DFunLike.congr_fun (linearIndependent_iff.mp hs (Finsupp.single i a) (by simpa)) i
 
-variable [Nontrivial R]
+variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R]
 
 section
 variable [NoZeroSMulDivisors R M]
@@ -101,6 +101,12 @@ theorem rank_pos_iff_nontrivial : 0 < Module.rank R M ↔ Nontrivial M :=
 theorem rank_pos [Nontrivial M] : 0 < Module.rank R M :=
   rank_pos_iff_nontrivial.mpr ‹_›
 
+omit [Nontrivial R] in
+theorem Module.finite_of_rank_eq_zero (h : Module.rank R M = 0) : Module.Finite R M := by
+  nontriviality R
+  rw [rank_zero_iff] at h
+  infer_instance
+
 end
 
 theorem exists_mem_ne_zero_of_rank_pos {s : Submodule R M} (h : 0 < Module.rank R s) :
@@ -119,13 +125,6 @@ theorem Module.finite_of_rank_eq_nat [Module.Free R M] {n : ℕ} (h : Module.ran
     b.linearIndependent.cardinal_le_rank |>.trans_eq h |>.trans_lt <| nat_lt_aleph0 n
   exact Module.Finite.of_basis b
 
-theorem Module.finite_of_rank_eq_zero [NoZeroSMulDivisors R M]
-    (h : Module.rank R M = 0) :
-    Module.Finite R M := by
-  nontriviality R
-  rw [rank_zero_iff] at h
-  infer_instance
-
 theorem Module.finite_of_rank_eq_one [Module.Free R M] (h : Module.rank R M = 1) :
     Module.Finite R M :=
   Module.finite_of_rank_eq_nat <| h.trans Nat.cast_one.symm
@@ -240,7 +239,7 @@ theorem Module.Finite.not_linearIndependent_of_infinite {ι : Type*} [Infinite 
     (v : ι → M) : ¬LinearIndependent R v := mt LinearIndependent.finite <| @not_finite _ _
 
 section
-variable [NoZeroSMulDivisors R M]
+variable {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
 
 theorem iSupIndep.subtype_ne_bot_le_rank [Nontrivial R]
     {V : ι → Submodule R M} (hV : iSupIndep V) :
@@ -289,6 +288,7 @@ theorem iSupIndep.subtype_ne_bot_le_finrank
 
 end
 
+variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
 variable [Module.Finite R M] [StrongRankCondition R]
 
 section
@@ -357,21 +357,16 @@ theorem Module.finrank_zero_of_subsingleton [Subsingleton M] :
 lemma LinearIndependent.finrank_eq_zero_of_infinite {ι} [Infinite ι] {v : ι → M}
     (hv : LinearIndependent R v) : finrank R M = 0 := toNat_eq_zero.mpr <| .inr hv.aleph0_le_rank
 
-section
-variable [NoZeroSMulDivisors R M]
-
 /-- A finite-dimensional space is nontrivial if it has positive `finrank`. -/
-theorem Module.nontrivial_of_finrank_pos (h : 0 < finrank R M) : Nontrivial M :=
-  rank_pos_iff_nontrivial.mp (lt_rank_of_lt_finrank h)
+theorem Module.nontrivial_of_finrank_pos (h : 0 < finrank R M) : Nontrivial M := by
+  contrapose! h; exact finrank_zero_of_subsingleton.le
 
 /-- A finite-dimensional space is nontrivial if it has `finrank` equal to the successor of a
 natural number. -/
 theorem Module.nontrivial_of_finrank_eq_succ {n : ℕ}
     (hn : finrank R M = n.succ) : Nontrivial M :=
   nontrivial_of_finrank_pos (R := R) (by rw [hn]; exact n.succ_pos)
 
-end
-
 variable (R M)
 
 @[simp]
@@ -382,6 +377,7 @@ end
 
 section StrongRankCondition
 
+variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
 variable [StrongRankCondition R] [Module.Finite R M]
 
 /-- A finite rank torsion-free module has positive `finrank` iff it has a nonzero element. -/
@@ -430,6 +426,10 @@ theorem Module.finrank_eq_zero_of_rank_eq_zero (h : Module.rank R M = 0) :
   delta finrank
   rw [h, zero_toNat]
 
+section
+
+variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
+
 theorem Submodule.bot_eq_top_of_rank_eq_zero [NoZeroSMulDivisors R M] (h : Module.rank R M = 0) :
     (⊥ : Submodule R M) = ⊤ := by
   nontriviality R
@@ -459,6 +459,8 @@ lemma Submodule.one_le_finrank_iff [StrongRankCondition R] [NoZeroSMulDivisors R
     1 ≤ finrank R S ↔ S ≠ ⊥ := by
   contrapose!; rw [Nat.lt_one_iff, finrank_eq_zero]
 
+end
+
 @[simp]
 theorem Set.finrank_empty [Nontrivial R] :
     Set.finrank R (∅ : Set M) = 0 := by
@@ -499,6 +501,7 @@ end FinrankZero
 
 section RankOne
 
+variable {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M]
 variable [NoZeroSMulDivisors R M] [StrongRankCondition R]
 
 /-- If there is a nonzero vector and every other vector is a multiple of it,
@@ -514,20 +517,22 @@ then the module has dimension one. -/
 theorem finrank_eq_one (v : M) (n : v ≠ 0) (h : ∀ w : M, ∃ c : R, c • v = w) : finrank R M = 1 :=
   finrank_eq_of_rank_eq (rank_eq_one v n h)
 
-/-- If every vector is a multiple of some `v : M`, then `M` has dimension at most one.
--/
+end RankOne
+
+section
+
+variable [StrongRankCondition R]
+
+theorem rank_le_one (v : M) (h : ∀ w : M, ∃ c : R, c • v = w) : Module.rank R M ≤ 1 := by
+  simpa using LinearMap.lift_rank_le_of_surjective _
+    (id h : Surjective (LinearMap.toSpanSingleton R M v))
+
+/-- If every vector is a multiple of some `v : M`, then `M` has dimension at most one. -/
 theorem finrank_le_one (v : M) (h : ∀ w : M, ∃ c : R, c • v = w) : finrank R M ≤ 1 := by
-  haveI := nontrivial_of_invariantBasisNumber R
-  rcases eq_or_ne v 0 with (rfl | hn)
-  · haveI :=
-      _root_.subsingleton_of_forall_eq (0 : M) fun w => by
-        obtain ⟨c, rfl⟩ := h w
-        simp
-    rw [finrank_zero_of_subsingleton]
-    exact zero_le_one
-  · exact (finrank_eq_one v hn h).le
+  rw [← map_one toNat, finrank]
+  exact toNat_le_toNat (rank_le_one v h) one_lt_aleph0
 
-end RankOne
+end
 
 namespace Module
 variable {ι : Type*}