feat(linear_algebra/finite_dimensional): generalize from field to div…

…ision_ring and more (#17401)

+ Replace K by ℕ in two proofs in *linear_algebra/basis*, which immediately allows generalization from `division_ring` to `field` in *submodule/basic*, *field_theory/tower*, *linear_algebra/dimension*, *projective_space/basic*, *linear_algebra/finite_dimensional*, and *affine_space/finite_dimensional*. (~~@riccardobrasca authored many of these;~~ @semorrison made some `division_ring` generalizations a while ago; @adamtopaz's TODO in *projective_space/basic* is now resolved. Let me know if you can think of more stuff to generalize.)

+ Add `subalgebra.is_simple_order_of_finrank_prime` in *field_theory/tower*. Inspired by [#17237](#17237 (comment)) (@xroblot).

+ Make `subalgebra.to_submodule` an `order_embedding` in *subalgebra/basic*, remove lemmas rendered redundant, and fix things in *intermediate_field*, *field_theory/normal*, and *adjoin/fg*.

+ Changes in *linear_algebra/finite_dimensional* and *linear_algebra/finrank*:

    + Add `finite_dimensional_of_dim_eq_nat`: used to golf `finite_dimensional_of_dim_eq_zero/one`.

    + Add `submodule.finrank_le_finrank_of_le` and `finrank_lt_finrank_of_lt` which only assumes the larger submodule is finite rather than the whole module. Rename the original `finrank_lt_finrank_of_lt` to `finrank_strict_mono`, matching the existing `finrank_mono`.

    + Remove `subalgebra.dim/finrank_eq_one_of_eq_bot` which has a substitutable equality among its assumptions (use `dim/finrank_bot` instead).
   
    + Add `subalgebra.dim/finrank/finite_dimensional_to_submodule` and an instance `finite_dimensional_subalgebra` similar to [finite_dimensional_submodule](https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html#finite_dimensional.finite_dimensional_submodule).

    + Generalize `section subalgebra_dim` from `[field E]` to `[ring E]`, adding `[nontrivial E]` hypothesis whenever necessary.

    + Generalize `subalgebra.eq_bot_of_dim_one` to `of_dim_le_one` and golf the proof (together with `eq_bot_of_finrank_one`).

    + Move `finite_dimensional.of_subalgebra_to_submodule` from *splitting_field* to *finite_dimensional*.

+ Add `exists_nat_eq_of_le_nat` in *cardinal/basic*.

+ Fix a slow proof in *polynomial/bernstein*.



Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

src/algebra/algebra/subalgebra/basic.lean

@@ -219,25 +219,24 @@ instance to_linear_ordered_comm_ring {R A}
 
 end
 
-/-- Convert a `subalgebra` to `submodule` -/
-def to_submodule : submodule R A :=
-{ carrier := S,
-  zero_mem' := (0:S).2,
-  add_mem' := λ x y hx hy, (⟨x, hx⟩ + ⟨y, hy⟩ : S).2,
-  smul_mem' := λ c x hx, (algebra.smul_def c x).symm ▸
-    (⟨algebra_map R A c, S.range_le ⟨c, rfl⟩⟩ * ⟨x, hx⟩:S).2 }
+/-- The forgetful map from `subalgebra` to `submodule` as an `order_embedding` -/
+def to_submodule : subalgebra R A ↪o submodule R A :=
+{ to_embedding :=
+  { to_fun := λ S,
+    { carrier := S,
+      zero_mem' := (0:S).2,
+      add_mem' := λ x y hx hy, (⟨x, hx⟩ + ⟨y, hy⟩ : S).2,
+      smul_mem' := λ c x hx, (algebra.smul_def c x).symm ▸
+        (⟨algebra_map R A c, S.range_le ⟨c, rfl⟩⟩ * ⟨x, hx⟩:S).2 },
+    inj' := λ S T h, ext $ by apply set_like.ext_iff.1 h },
+  map_rel_iff' := λ S T, set_like.coe_subset_coe.symm.trans set_like.coe_subset_coe }
+/- TODO: bundle other forgetful maps between algebraic substructures, e.g.
+  `to_subsemiring` and `to_subring` in this file. -/
 
 @[simp] lemma mem_to_submodule {x} : x ∈ S.to_submodule ↔ x ∈ S := iff.rfl
 
 @[simp] lemma coe_to_submodule (S : subalgebra R A) : (↑S.to_submodule : set A) = S := rfl
 
-theorem to_submodule_injective :
-  function.injective (to_submodule : subalgebra R A → submodule R A) :=
-λ S T h, ext $ λ x, by rw [← mem_to_submodule, ← mem_to_submodule, h]
-
-theorem to_submodule_inj {S U : subalgebra R A} : S.to_submodule = U.to_submodule ↔ S = U :=
-to_submodule_injective.eq_iff
-
 section
 
 /-! `subalgebra`s inherit structure from their `submodule` coercions. -/
@@ -573,7 +572,7 @@ set.mem_univ x
   (⊤ : subalgebra R A).to_subring = ⊤ := rfl
 
 @[simp] lemma to_submodule_eq_top {S : subalgebra R A} : S.to_submodule = ⊤ ↔ S = ⊤ :=
-subalgebra.to_submodule_injective.eq_iff' top_to_submodule
+subalgebra.to_submodule.injective.eq_iff' top_to_submodule
 
 @[simp] lemma to_subsemiring_eq_top {S : subalgebra R A} : S.to_subsemiring = ⊤ ↔ S = ⊤ :=
 subalgebra.to_subsemiring_injective.eq_iff' top_to_subsemiring

src/algebra/module/submodule/basic.lean

@@ -462,5 +462,5 @@ end submodule
 
 /-- Subspace of a vector space. Defined to equal `submodule`. -/
 abbreviation subspace (R : Type u) (M : Type v)
-  [field R] [add_comm_group M] [module R M] :=
+  [division_ring R] [add_comm_group M] [module R M] :=
 submodule R M

src/analysis/inner_product_space/two_dim.lean

@@ -350,7 +350,7 @@ linear_isometry_equiv.ext $ o.linear_isometry_equiv_comp_right_angle_rotation φ
 /-- For a nonzero vector `x` in an oriented two-dimensional real inner product space `E`,
 `![x, J x]` forms an (orthogonal) basis for `E`. -/
 def basis_right_angle_rotation (x : E) (hx : x ≠ 0) : basis (fin 2) ℝ E :=
-@basis_of_linear_independent_of_card_eq_finrank _ _ _ _ _ _ _ _ ![x, J x]
+@basis_of_linear_independent_of_card_eq_finrank ℝ _ _ _ _ _ _ _ ![x, J x]
 (linear_independent_of_ne_zero_of_inner_eq_zero (λ i, by { fin_cases i; simp [hx] })
   begin
     intros i j hij,

src/field_theory/intermediate_field.lean

@@ -485,7 +485,7 @@ by { rw [set_like.ext_iff, set_like.ext'_iff, set.ext_iff], refl }
 
 lemma eq_of_le_of_finrank_le [finite_dimensional K L] (h_le : F ≤ E)
   (h_finrank : finrank K E ≤ finrank K F) : F = E :=
-to_subalgebra_injective $ subalgebra.to_submodule_injective $ eq_of_le_of_finrank_le h_le h_finrank
+to_subalgebra_injective $ subalgebra.to_submodule.injective $ eq_of_le_of_finrank_le h_le h_finrank
 
 lemma eq_of_le_of_finrank_eq [finite_dimensional K L] (h_le : F ≤ E)
   (h_finrank : finrank K F = finrank K E) : F = E :=

src/field_theory/normal.lean

@@ -68,7 +68,7 @@ begin
   let s := basis.of_vector_space F K,
   refine ⟨∏ x, minpoly F (s x),
     splits_prod _ $ λ x hx, h.splits (s x),
-    subalgebra.to_submodule_injective _⟩,
+    subalgebra.to_submodule.injective _⟩,
   rw [algebra.top_to_submodule, eq_top_iff, ← s.span_eq, submodule.span_le, set.range_subset_iff],
   refine λ x, algebra.subset_adjoin (multiset.mem_to_finset.mpr $
     (mem_roots $ mt (polynomial.map_eq_zero $ algebra_map F K).1 $

src/field_theory/tower.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
+import data.nat.prime
 import ring_theory.algebra_tower
 import linear_algebra.matrix.finite_dimensional
 import linear_algebra.matrix.to_lin
@@ -38,7 +39,7 @@ section field
 open cardinal
 
 variables (F : Type u) (K : Type v) (A : Type w)
-variables [field F] [field K] [add_comm_group A]
+variables [field F] [division_ring K] [add_comm_group A]
 variables [algebra F K] [module K A] [module F A] [is_scalar_tower F K A]
 
 /-- Tower law: if `A` is a `K`-vector space and `K` is a field extension of `F` then
@@ -73,7 +74,7 @@ of_fintype_basis $ b.smul c
 
 Note this cannot be an instance as Lean cannot infer `L`.
 -/
-theorem left (L : Type*) [ring L] [nontrivial L]
+theorem left (K L : Type*) [field K] [algebra F K] [ring L] [nontrivial L]
   [algebra F L] [algebra K L] [is_scalar_tower F K L]
   [finite_dimensional F L] : finite_dimensional F K :=
 finite_dimensional.of_injective
@@ -100,6 +101,19 @@ begin
     exact mt (@right F K A _ _ _ _ _ _ _) hA }
 end
 
+theorem subalgebra.is_simple_order_of_finrank_prime (A) [ring A] [is_domain A] [algebra F A]
+  (hp : (finrank F A).prime) : is_simple_order (subalgebra F A) :=
+{ to_nontrivial :=
+    ⟨⟨⊥, ⊤, λ he, nat.not_prime_one ((subalgebra.bot_eq_top_iff_finrank_eq_one.1 he).subst hp)⟩⟩,
+  eq_bot_or_eq_top := λ K, begin
+    haveI := finite_dimensional_of_finrank hp.pos,
+    letI := division_ring_of_finite_dimensional F K,
+    refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp _ (λ h, _),
+    { exact subalgebra.eq_bot_of_finrank_one },
+    { exact algebra.to_submodule_eq_top.1 (eq_top_of_finrank_eq $ K.finrank_to_submodule.trans h) },
+  end }
+/- TODO: `intermediate_field` version -/
+
 instance linear_map (F : Type u) (V : Type v) (W : Type w)
   [field F] [add_comm_group V] [module F V] [add_comm_group W] [module F W]
   [finite_dimensional F V] [finite_dimensional F W] :

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -565,14 +565,14 @@ by rw [coplanar, coplanar, vector_span_insert_eq_vector_span h]
 
 end affine_space'
 
-section field
+section division_ring
 
 variables {k : Type*} {V : Type*} {P : Type*}
 include V
 
 open affine_subspace finite_dimensional module
 
-variables [field k] [add_comm_group V] [module k V] [affine_space V P]
+variables [division_ring k] [add_comm_group V] [module k V] [affine_space V P]
 
 /-- Adding a point to a finite-dimensional subspace increases the dimension by at most one. -/
 lemma finrank_vector_span_insert_le (s : affine_subspace k P) (p : P) :
@@ -649,4 +649,4 @@ variables (k)
 lemma coplanar_triple (p₁ p₂ p₃ : P) : coplanar k ({p₁, p₂, p₃} : set P) :=
 (collinear_pair k p₂ p₃).coplanar_insert p₁
 
-end field
+end division_ring

src/linear_algebra/basis.lean

@@ -1320,12 +1320,7 @@ instance : is_atomistic (submodule K V) :=
 
 end atoms_of_submodule_lattice
 
-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}
+variables {K V}
 
 lemma linear_map.exists_left_inverse_of_injective (f : V →ₗ[K] V')
   (hf_inj : f.ker = ⊥) : ∃g:V' →ₗ[K] V, g.comp f = linear_map.id :=
@@ -1342,7 +1337,7 @@ begin
   have BC := this.subset_extend (subset_univ _),
   let hC := basis.extend this,
   haveI : inhabited V := ⟨0⟩,
-  refine ⟨hC.constr K (C.restrict (inv_fun f)), hB.ext (λ b, _)⟩,
+  refine ⟨hC.constr ℕ (C.restrict (inv_fun f)), hB.ext (λ b, _)⟩,
   rw image_subset_iff at BC,
   have fb_eq : f b = hC ⟨f b, BC b.2⟩,
   { change f b = basis.extend this _,
@@ -1365,7 +1360,7 @@ begin
   let C := basis.of_vector_space_index K V',
   let hC := basis.of_vector_space K V',
   haveI : inhabited V := ⟨0⟩,
-  use hC.constr K (C.restrict (inv_fun f)),
+  use hC.constr ℕ (C.restrict (inv_fun f)),
   refine hC.ext (λ c, _),
   rw [linear_map.comp_apply, hC.constr_basis],
   simp [right_inverse_inv_fun (linear_map.range_eq_top.1 hf_surj) c]
@@ -1402,4 +1397,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)
 
-end field
+end division_ring

src/linear_algebra/dimension.lean

@@ -1020,12 +1020,6 @@ by simp [dim_fun']
 
 end fintype
 
-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']
-
 theorem dim_quotient_add_dim (p : submodule K V) :
   module.rank K (V ⧸ p) + 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
@@ -1108,7 +1102,7 @@ lemma exists_mem_ne_zero_of_dim_pos {s : submodule K V} (h : 0 < module.rank K s
   ∃ b : V, b ∈ s ∧ b ≠ 0 :=
 exists_mem_ne_zero_of_ne_bot $ assume eq, by rw [eq, dim_bot] at h; exact lt_irrefl _ h
 
-end field
+end division_ring
 
 section rank
 
@@ -1141,8 +1135,10 @@ by rw [rank, rank, linear_map.range_comp]; exact dim_map_le _ _
 
 end
 
-section field
-variables [field K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
+end rank
+
+section division_ring
+variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
 variables [add_comm_group V'] [module K V']
 
 lemma rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V :=
@@ -1163,13 +1159,6 @@ lemma rank_finset_sum_le {η} (s : finset η) (f : η → V →ₗ[K] V') :
 @finset.sum_hom_rel _ _ _ _ _ (λa b, rank a ≤ b) f (λ d, rank (f d)) s (le_of_eq rank_zero)
       (λ i g c h, le_trans (rank_add_le _ _) (add_le_add_left h _))
 
-end field
-
-end rank
-
-section division_ring
-variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V']
-
 /-- The `ι` indexed basis on `V`, where `ι` is an empty type and `V` is zero-dimensional.
 
 See also `finite_dimensional.fin_basis`.
@@ -1301,11 +1290,6 @@ lemma module.rank_le_one_iff_top_is_principal :
   module.rank K V ≤ 1 ↔ (⊤ : submodule K V).is_principal :=
 by rw [← submodule.rank_le_one_iff_is_principal, dim_top]
 
-end division_ring
-
-section field
-variables [field K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V']
-
 lemma le_rank_iff_exists_linear_independent {c : cardinal} {f : V →ₗ[K] V'} :
   c ≤ rank f ↔
   ∃ s : set V, cardinal.lift.{v'} (#s) = cardinal.lift.{v} c ∧
@@ -1340,6 +1324,6 @@ begin
     exact ⟨s, ⟨s, rfl, rfl⟩, si⟩ }
 end
 
-end field
+end division_ring
 
 end module