feat(finite_dimensional/subalgebra) : add subalgebra.is_simple_order_…

…of_finrank (#17237)

This PR adds some lemma that will be used in the proof (#17285) that two complex embeddings of a field define the same place iff they are equal or complex conjugate, mainly:
- `subalgebra.is_simple_order_of_finrank` shows that the only two subalgebras in an algebra of dimension 2 are exactly `⊥` and  `⊤`

src/field_theory/subfield.lean

@@ -313,6 +313,10 @@ instance : inhabited (subfield K) := ⟨⊤⟩
 
 @[simp] lemma coe_top : ((⊤ : subfield K) : set K) = set.univ := rfl
 
+/-- The ring equiv between the top element of `subfield K` and `K`. -/
+@[simps]
+def top_equiv : (⊤ : subfield K) ≃+* K := subsemiring.top_equiv
+
 /-! # comap -/
 
 variables (f : K →+* L)

src/linear_algebra/finite_dimensional.lean

@@ -1235,6 +1235,10 @@ begin
   exact lt_of_le_of_finrank_lt_finrank le_top lt
 end
 
+lemma eq_top_of_finrank_eq [finite_dimensional K V] {S : submodule K V}
+  (h : finrank K S = finrank K V) :
+  S = ⊤ := finite_dimensional.eq_of_le_of_finrank_eq le_top (by simp [h, finrank_top])
+
 lemma finrank_mono [finite_dimensional K V] :
   monotone (λ (s : submodule K V), finrank K s) :=
 λ s t hst,
@@ -1737,20 +1741,6 @@ begin
   exact subalgebra.eq_bot_of_finrank_one h,
 end
 
-@[simp]
-lemma subalgebra.bot_eq_top_of_dim_eq_one (h : module.rank F E = 1) : (⊥ : subalgebra F E) = ⊤ :=
-begin
-  rw [← dim_top, ← subalgebra_top_dim_eq_submodule_top_dim] at h,
-  exact eq.symm (subalgebra.eq_bot_of_dim_one h),
-end
-
-@[simp]
-lemma subalgebra.bot_eq_top_of_finrank_eq_one (h : finrank F E = 1) : (⊥ : subalgebra F E) = ⊤ :=
-begin
-  rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank] at h,
-  exact eq.symm (subalgebra.eq_bot_of_finrank_one h),
-end
-
 @[simp]
 theorem subalgebra.dim_eq_one_iff {S : subalgebra F E} : module.rank F S = 1 ↔ S = ⊥ :=
 ⟨subalgebra.eq_bot_of_dim_one, subalgebra.dim_eq_one_of_eq_bot⟩
@@ -1759,6 +1749,42 @@ theorem subalgebra.dim_eq_one_iff {S : subalgebra F E} : module.rank F S = 1 ↔
 theorem subalgebra.finrank_eq_one_iff {S : subalgebra F E} : finrank F S = 1 ↔ S = ⊥ :=
 ⟨subalgebra.eq_bot_of_finrank_one, subalgebra.finrank_eq_one_of_eq_bot⟩
 
+lemma subalgebra.bot_eq_top_iff_dim_eq_one :
+  (⊥ : subalgebra F E) = ⊤ ↔ module.rank F E = 1 :=
+by rw [← dim_top, ← subalgebra_top_dim_eq_submodule_top_dim, subalgebra.dim_eq_one_iff, eq_comm]
+
+lemma subalgebra.bot_eq_top_iff_finrank_eq_one :
+  (⊥ : subalgebra F E) = ⊤ ↔ finrank F E = 1 :=
+by rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
+       subalgebra.finrank_eq_one_iff, eq_comm]
+
+@[simp]
+lemma subalgebra.bot_eq_top_of_finrank_eq_one (h : finrank F E = 1) : (⊥ : subalgebra F E) = ⊤ :=
+subalgebra.bot_eq_top_iff_finrank_eq_one.2 h
+
+@[simp]
+lemma subalgebra.bot_eq_top_of_dim_eq_one (h : module.rank F E = 1) : (⊥ : subalgebra F E) = ⊤ :=
+subalgebra.bot_eq_top_iff_dim_eq_one.2 h
+
+lemma subalgebra.is_simple_order_of_finrank (hr : finrank F E = 2) :
+  is_simple_order (subalgebra F E) :=
+{ to_nontrivial :=
+    ⟨⟨⊥, ⊤, λ h, by cases hr.symm.trans (subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)⟩⟩,
+  eq_bot_or_eq_top :=
+  begin
+    intro S,
+    haveI : finite_dimensional F E := finite_dimensional_of_finrank_eq_succ hr,
+    haveI : finite_dimensional F S :=
+      finite_dimensional.finite_dimensional_submodule S.to_submodule,
+    have : finrank F S ≤ 2 := hr ▸ S.to_submodule.finrank_le,
+    have : 0 < finrank F S := finrank_pos_iff.mpr infer_instance,
+    interval_cases (finrank F S),
+    { left, exact subalgebra.eq_bot_of_finrank_one h, },
+    { right, rw ← hr at h,
+      rw ← algebra.to_submodule_eq_top,
+      exact submodule.eq_top_of_finrank_eq h, },
+  end }
+
 end subalgebra_dim
 
 namespace module

src/ring_theory/subring/basic.lean

@@ -434,6 +434,10 @@ instance : has_top (subring R) :=
 
 @[simp] lemma coe_top : ((⊤ : subring R) : set R) = set.univ := rfl
 
+/-- The ring equiv between the top element of `subring R` and `R`. -/
+@[simps]
+def top_equiv : (⊤ : subring R) ≃+* R := subsemiring.top_equiv
+
 /-! ## comap -/
 
 /-- The preimage of a subring along a ring homomorphism is a subring. -/

src/ring_theory/subsemiring/basic.lean

@@ -404,6 +404,16 @@ instance : has_top (subsemiring R) :=
 
 @[simp] lemma coe_top : ((⊤ : subsemiring R) : set R) = set.univ := rfl
 
+/-- The ring equiv between the top element of `subsemiring R` and `R`. -/
+@[simps]
+def top_equiv : (⊤ : subsemiring R) ≃+* R :=
+{ to_fun := λ r, r,
+  inv_fun := λ r, ⟨r, subsemiring.mem_top r⟩,
+  left_inv := λ r, set_like.eta r _,
+  right_inv := λ r, set_like.coe_mk r _,
+  map_mul' := (⊤ : subsemiring R).coe_mul,
+  map_add' := (⊤ : subsemiring R).coe_add, }
+
 /-- The preimage of a subsemiring along a ring homomorphism is a subsemiring. -/
 def comap (f : R →+* S) (s : subsemiring S) : subsemiring R :=
 { carrier := f ⁻¹' s,