From 93a15d6b53e58995332e4ad516dc7dfd7e77aa76 Mon Sep 17 00:00:00 2001
From: Shing Tak Lam <shingtaklam1324@gmail.com>
Date: Fri, 3 Sep 2021 22:57:16 +0000
Subject: [PATCH] feat(ring_theory/subring): field structure on centers of a
 division_ring (#8472)

I've also tidied up the subtitles. Previously there was a mix of h1 and h3s, I've made them all h2s.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 src/group_theory/submonoid/center.lean | 16 ++++++++++
 src/ring_theory/subring.lean           | 41 ++++++++++++++++++++------
 2 files changed, 48 insertions(+), 9 deletions(-)

diff --git a/src/group_theory/submonoid/center.lean b/src/group_theory/submonoid/center.lean
index 9a646869c6f76..b14fc116cda81 100644
--- a/src/group_theory/submonoid/center.lean
+++ b/src/group_theory/submonoid/center.lean
@@ -86,6 +86,22 @@ begin
   exact center_units_subset (inv_mem_center (subset_center_units ha)),
 end
 
+@[simp, to_additive sub_mem_add_center]
+lemma div_mem_center [group M] {a b : M} (ha : a ∈ set.center M) (hb : b ∈ set.center M) :
+  a / b ∈ set.center M :=
+begin
+  rw [div_eq_mul_inv],
+  exact mul_mem_center ha (inv_mem_center hb),
+end
+
+@[simp]
+lemma div_mem_center' [group_with_zero M] {a b : M} (ha : a ∈ set.center M)
+  (hb : b ∈ set.center M) : a / b ∈ set.center M :=
+begin
+  rw div_eq_mul_inv,
+  exact mul_mem_center ha (inv_mem_center' hb),
+end
+
 variables (M)
 
 @[simp, to_additive add_center_eq_univ]
diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean
index b75a1f1ace6d1..984ab2cd5d691 100644
--- a/src/ring_theory/subring.lean
+++ b/src/ring_theory/subring.lean
@@ -304,7 +304,7 @@ s.subtype.map_nat_cast n
 @[simp, norm_cast] lemma coe_int_cast (n : ℤ) : ((n : s) : R) = n :=
 s.subtype.map_int_cast n
 
-/-! # Partial order -/
+/-! ## Partial order -/
 
 @[simp] lemma mem_to_submonoid {s : subring R} {x : R} : x ∈ s.to_submonoid ↔ x ∈ s := iff.rfl
 @[simp] lemma coe_to_submonoid (s : subring R) : (s.to_submonoid : set R) = s := rfl
@@ -312,7 +312,7 @@ s.subtype.map_int_cast n
   x ∈ s.to_add_subgroup ↔ x ∈ s := iff.rfl
 @[simp] lemma coe_to_add_subgroup (s : subring R) : (s.to_add_subgroup : set R) = s := rfl
 
-/-! # top -/
+/-! ## top -/
 
 /-- The subring `R` of the ring `R`. -/
 instance : has_top (subring R) :=
@@ -322,7 +322,7 @@ instance : has_top (subring R) :=
 
 @[simp] lemma coe_top : ((⊤ : subring R) : set R) = set.univ := rfl
 
-/-! # comap -/
+/-! ## comap -/
 
 /-- The preimage of a subring along a ring homomorphism is a subring. -/
 def comap {R : Type u} {S : Type v} [ring R] [ring S]
@@ -340,7 +340,7 @@ lemma comap_comap (s : subring T) (g : S →+* T) (f : R →+* S) :
   (s.comap g).comap f = s.comap (g.comp f) :=
 rfl
 
-/-! # map -/
+/-! ## map -/
 
 /-- The image of a subring along a ring homomorphism is a subring. -/
 def map {R : Type u} {S : Type v} [ring R] [ring S]
@@ -385,7 +385,7 @@ namespace ring_hom
 
 variables (g : S →+* T) (f : R →+* S)
 
-/-! # range -/
+/-! ## range -/
 
 /-- The range of a ring homomorphism, as a subring of the target. See Note [range copy pattern]. -/
 def range {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) : subring S :=
@@ -424,7 +424,7 @@ end ring_hom
 
 namespace subring
 
-/-! # bot -/
+/-! ## bot -/
 
 instance : has_bot (subring R) := ⟨(int.cast_ring_hom R).range⟩
 
@@ -436,7 +436,7 @@ ring_hom.coe_range (int.cast_ring_hom R)
 lemma mem_bot {x : R} : x ∈ (⊥ : subring R) ↔ ∃ (n : ℤ), ↑n = x :=
 ring_hom.mem_range
 
-/-! # inf -/
+/-! ## inf -/
 
 /-- The inf of two subrings is their intersection. -/
 instance : has_inf (subring R) :=
@@ -481,6 +481,8 @@ instance : complete_lattice (subring R) :=
 lemma eq_top_iff' (A : subring R) : A = ⊤ ↔ ∀ x : R, x ∈ A :=
 eq_top_iff.trans ⟨λ h m, h $ mem_top m, λ h m _, h m⟩
 
+/-! ## Center of a ring -/
+
 section
 
 variables (R)
@@ -510,7 +512,28 @@ instance : comm_ring (center R) :=
 
 end
 
-/-! # subring closure of a subset -/
+section division_ring
+
+variables {K : Type u} [division_ring K]
+
+instance : field (center K) :=
+{ inv := λ a, ⟨a⁻¹, set.inv_mem_center' a.prop⟩,
+  mul_inv_cancel := λ ⟨a, ha⟩ h, subtype.ext $ mul_inv_cancel $ subtype.coe_injective.ne h,
+  div := λ a b, ⟨a / b, set.div_mem_center' a.prop b.prop⟩,
+  div_eq_mul_inv := λ a b, subtype.ext $ div_eq_mul_inv _ _,
+  inv_zero := subtype.ext inv_zero,
+  ..(center K).nontrivial,
+  ..center.comm_ring }
+
+@[simp]
+lemma center.coe_inv (a : center K) : ((a⁻¹ : center K) : K) = (a : K)⁻¹ := rfl
+
+@[simp]
+lemma center.coe_div (a b : center K) : ((a / b : center K) : K) = (a : K) / (b : K) := rfl
+
+end division_ring
+
+/-! ## subring closure of a subset -/
 
 /-- The `subring` generated by a set. -/
 def closure (s : set R) : subring R := Inf {S | s ⊆ S}
@@ -893,7 +916,7 @@ lemma add_subgroup.int_mul_mem {G : add_subgroup R} (k : ℤ) {g : R} (h : g ∈
 by { convert add_subgroup.gsmul_mem G h k, simp }
 
 
-/-! ### Actions by `subring`s
+/-! ## Actions by `subring`s
 
 These are just copies of the definitions about `subsemiring` starting from
 `subsemiring.mul_action`.