refactor(linear_algebra/dimension): generalize definition of `module.…

…rank` (#7634)

The main change is to generalize the definition of `module.rank`. It used to be the infimum over cardinalities of bases, and is now the supremum over cardinalities of linearly independent sets.

I have not attempted to systematically generalize  theorems about the rank; there is lots more work to be done. For now I've just made a few easy generalizations (either replacing `field` with `division_ring`, or `division_ring` with `ring`+`nontrivial`).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/linear_algebra/basis.lean

@@ -282,9 +282,8 @@ calc b.reindex_range.repr (b i) = b.reindex_range.repr (b.reindex_range ⟨b i,
   congr_arg _ (b.reindex_range_self _ _).symm
 ... = finsupp.single ⟨b i, mem_range_self i⟩ 1 : b.reindex_range.repr_self _
 
-@[simp] lemma reindex_range_apply [nontrivial R] {bi : M} {i : ι} (h : b i = bi) :
-  b.reindex_range ⟨bi, ⟨i, h⟩⟩ = b i :=
-by { convert b.reindex_range_self i, rw h }
+@[simp] lemma reindex_range_apply [nontrivial R] (x : range b) : b.reindex_range x = x :=
+by { rcases x with ⟨bi, ⟨i, rfl⟩⟩, exact b.reindex_range_self i, }
 
 lemma reindex_range_repr' [nontrivial R] (x : M) {bi : M} {i : ι} (h : b i = bi) :
   b.reindex_range.repr x ⟨bi, ⟨i, h⟩⟩ = b.repr x i :=
@@ -743,9 +742,9 @@ end basis
 
 end module
 
-section vector_space
+section division_ring
 
-variables [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V']
+variables [division_ring K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V']
 variables {v : ι → V} {s t : set V} {x y z : V}
 
 include K
@@ -828,6 +827,20 @@ end exists_basis
 
 end basis
 
+open fintype
+variables (K V)
+
+theorem vector_space.card_fintype [fintype K] [fintype V] :
+  ∃ n : ℕ, card V = (card K) ^ n :=
+⟨card (basis.of_vector_space_index K V), module.card_fintype (basis.of_vector_space K V)⟩
+
+end division_ring
+
+section field
+
+variables [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V']
+variables {v : ι → V} {s t : set V} {x y z : V}
+
 lemma linear_map.exists_left_inverse_of_injective (f : V →ₗ[K] V')
   (hf_inj : f.ker = ⊥) : ∃g:V' →ₗ V, g.comp f = linear_map.id :=
 begin
@@ -903,11 +916,4 @@ let ⟨q, hq⟩ := p.exists_is_compl in nonempty.intro $
 ((quotient_equiv_of_is_compl p q hq).prod (linear_equiv.refl _ _)).trans
   (prod_equiv_of_is_compl q p hq.symm)
 
-open fintype
-variables (K) (V)
-
-theorem vector_space.card_fintype [fintype K] [fintype V] :
-  ∃ n : ℕ, card V = (card K) ^ n :=
-⟨card (basis.of_vector_space_index K V), module.card_fintype (basis.of_vector_space K V)⟩
-
-end vector_space
+end field

src/linear_algebra/dimension.lean

@@ -13,7 +13,11 @@ import set_theory.cardinal_ordinal
 ## Main definitions
 
 * The rank of a module is defined as `module.rank : cardinal`.
-  This is currently only defined for vector spaces, i.e., when the base semiring is a field.
+  This is defined as the supremum of the cardinalities of linearly independent subsets.
+
+Although this definition works for any module over a (semi)ring,
+for now we quickly specialize to division rings and then to fields.
+There's lots of generalization still to be done.
 
 ## Main statements
 
@@ -40,34 +44,36 @@ variables {ι : Type w} {ι' : Type w'} {η : Type u₁'} {φ : η → Type*}
 
 open_locale classical big_operators
 
-open basis
+open basis submodule function set
 
 section module
-variables [field K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
+
+section
+variables [semiring K] [add_comm_monoid V] [module K V]
 include K
-open submodule function set
 
 variables (K V)
 
 /-- The rank of a module, defined as a term of type `cardinal`.
 
-In a vector space, this is the same as the dimension of the space.
+We define this as the supremum of the cardinalities of linearly independent subsets.
 
-TODO: this is currently only defined for vector spaces, as the cardinality of
-the basis set. It should be generalized to modules in general.
+In a vector space, this is the same as the dimension of the space
+(i.e. the cardinality of any basis).
 
 The definition is marked as protected to avoid conflicts with `_root_.rank`,
 the rank of a linear map.
 -/
 protected def module.rank : cardinal :=
-cardinal.min
-  (nonempty_subtype.2 (exists_basis K V))
-  (λ ι, cardinal.mk ι.1)
-variables {K V}
+cardinal.sup.{v v}
+  (λ ι : {s : set V // linear_independent K (coe : s → V)}, cardinal.mk ι.1)
 
+end
+
+section division_ring
+variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
 variables {K V}
 
-section
 theorem basis.le_span {J : set V} (v : basis ι K V)
    (hJ : span K J = ⊤) : cardinal.mk (range v) ≤ cardinal.mk J :=
 begin
@@ -101,7 +107,6 @@ begin
         cardinal.finset_card, set.finite.coe_to_finset] at hi, },
     { rw hJ, apply set.subset_univ } },
 end
-end
 
 /-- The dimension theorem: if `v` and `v'` are two bases, their index types
 have the same cardinalities. -/
@@ -130,12 +135,19 @@ cardinal.lift_inj.1 $ mk_eq_mk_of_basis v v'
 theorem basis.mk_eq_dim'' {ι : Type v} (v : basis ι K V) :
   cardinal.mk ι = module.rank K V :=
 begin
-  obtain ⟨⟨ι, ⟨v'⟩⟩, e : module.rank K V = _⟩ :=
-    cardinal.min_eq (nonempty_subtype.2 (exists_basis K V)) _,
-  rw [e, ← cardinal.mk_range_eq _ v.injective],
-  exact mk_eq_mk_of_basis' v.reindex_range v'
+  apply le_antisymm,
+  { transitivity,
+    swap,
+    apply cardinal.le_sup,
+    exact ⟨set.range v, by { convert v.reindex_range.linear_independent, ext, simp }⟩,
+    exact (cardinal.eq_congr (equiv.of_injective v v.injective)).le, },
+  { exact cardinal.sup_le.mpr (λ i,
+      (cardinal.mk_le_mk_of_subset (basis.subset_extend i.2)).trans
+        (mk_eq_mk_of_basis' (basis.extend i.2) v).le), },
 end
 
+attribute [irreducible] module.rank
+
 theorem basis.mk_range_eq_dim (v : basis ι K V) :
   cardinal.mk (range v) = module.rank K V :=
 v.reindex_range.mk_eq_dim''
@@ -289,6 +301,13 @@ begin
       ⟨equiv.ulift.trans (equiv.sum_congr equiv.ulift equiv.ulift).symm ⟩),
 end
 
+end division_ring
+
+section field
+variables [field K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
+variables [add_comm_group V'] [module K V']
+variables {K V}
+
 theorem dim_quotient_add_dim (p : submodule K V) :
   module.rank K p.quotient + module.rank K p = module.rank K V :=
 by classical; exact let ⟨f⟩ := quotient_prod_linear_equiv p in dim_prod.symm.trans f.dim_eq
@@ -724,12 +743,14 @@ begin
       simp [hw] } }
 end
 
+end field
+
 end module
 
 section unconstrained_universes
 
 variables {E : Type v'}
-variables [field K] [add_comm_group V] [module K V]
+variables [division_ring K] [add_comm_group V] [module K V]
           [add_comm_group E] [module K E]
 open module
 

src/linear_algebra/linear_independent.lean

@@ -862,6 +862,30 @@ lemma span_le_span_iff [nontrivial R] {s t u: set M}
 
 end module
 
+section nontrivial
+
+variables [ring R] [nontrivial R] [add_comm_group M] [add_comm_group M']
+variables [module R M] [no_zero_smul_divisors R M] [module R M']
+variables {v : ι → M} {s t : set M} {x y z : M}
+
+lemma linear_independent_unique_iff
+  (v : ι → M) [unique ι] :
+  linear_independent R v ↔ v (default ι) ≠ 0 :=
+begin
+  simp only [linear_independent_iff, finsupp.total_unique, smul_eq_zero],
+  refine ⟨λ h hv, _, λ hv l hl, finsupp.unique_ext $ hl.resolve_right hv⟩,
+  have := h (finsupp.single (default ι) 1) (or.inr hv),
+  exact one_ne_zero (finsupp.single_eq_zero.1 this)
+end
+
+alias linear_independent_unique_iff ↔ _ linear_independent_unique
+
+lemma linear_independent_singleton {x : M} (hx : x ≠ 0) :
+  linear_independent R (λ x, x : ({x} : set M) → M) :=
+linear_independent_unique coe hx
+
+end nontrivial
+
 /-!
 ### Properties which require `division_ring K`
 
@@ -900,23 +924,15 @@ begin
     exact false.elim (h _ ((smul_mem_iff _ ha').1 ha)) }
 end
 
-lemma linear_independent_unique_iff [ring R] [nontrivial R] [add_comm_monoid M] [module R M]
-  [no_zero_smul_divisors R M]
-  (v : ι → M) [unique ι] :
-  linear_independent R v ↔ v (default ι) ≠ 0 :=
+lemma linear_independent.insert (hs : linear_independent K (λ b, b : s → V)) (hx : x ∉ span K s) :
+  linear_independent K (λ b, b : insert x s → V) :=
 begin
-  simp only [linear_independent_iff, finsupp.total_unique, smul_eq_zero],
-  refine ⟨λ h hv, _, λ hv l hl, finsupp.unique_ext $ hl.resolve_right hv⟩,
-  have := h (finsupp.single (default ι) 1) (or.inr hv),
-  exact one_ne_zero (finsupp.single_eq_zero.1 this)
+  rw ← union_singleton,
+  have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem _) hx,
+  apply hs.union (linear_independent_singleton x0),
+  rwa [disjoint_span_singleton' x0]
 end
 
-alias linear_independent_unique_iff ↔ _ linear_independent_unique
-
-lemma linear_independent_singleton {x : V} (hx : x ≠ 0) :
-  linear_independent K (λ x, x : ({x} : set V) → V) :=
-linear_independent_unique coe hx
-
 lemma linear_independent_option' :
   linear_independent K (λ o, option.cases_on' o x v : option ι → V) ↔
     linear_independent K v ∧ (x ∉ submodule.span K (range v)) :=
@@ -939,15 +955,6 @@ lemma linear_independent_option {v : option ι → V} :
     linear_independent K (v ∘ coe : ι → V) ∧ v none ∉ submodule.span K (range (v ∘ coe : ι → V)) :=
 by simp only [← linear_independent_option', option.cases_on'_none_coe]
 
-lemma linear_independent.insert (hs : linear_independent K (λ b, b : s → V)) (hx : x ∉ span K s) :
-  linear_independent K (λ b, b : insert x s → V) :=
-begin
-  rw ← union_singleton,
-  have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem _) hx,
-  apply hs.union (linear_independent_singleton x0),
-  rwa [disjoint_span_singleton' x0]
-end
-
 theorem linear_independent_insert' {ι} {s : set ι} {a : ι} {f : ι → V} (has : a ∉ s) :
   linear_independent K (λ x : insert a s, f x) ↔
   linear_independent K (λ x : s, f x) ∧ f a ∉ submodule.span K (f '' s) :=

src/ring_theory/principal_ideal_domain.lean

@@ -14,7 +14,7 @@ principal ideal domain (PID) is an integral domain which is a principal ideal ri
 # Main definitions
 
 Note that for principal ideal domains, one should use
-`[integral domain R] [is_principal_ideal_ring R]`. There is no explicit definition of a PID.
+`[integral_domain R] [is_principal_ideal_ring R]`. There is no explicit definition of a PID.
 Theorems about PID's are in the `principal_ideal_ring` namespace.
 
 - `is_principal_ideal_ring`: a predicate on commutative rings, saying that every