feat(ring_theory): define subsemirings (#2837)

~~Depends on #2836,~~ needs a better module docstring.

Some lemmas are missing, most notably `(subsemiring.closure s : set R) = add_submonoid.closure (submonoid.closure s)`.

Author: urkud

src/group_theory/congruence.lean

@@ -804,7 +804,7 @@ noncomputable def quotient_ker_equiv_range (f : M →* P) : (ker f).quotient ≃
 { map_mul' := monoid_hom.map_mul _,
   ..@equiv.of_bijective _ _
       ((@mul_equiv.to_monoid_hom (ker_lift f).mrange _ _ _
-        $ mul_equiv.submonoid_congr ker_lift_range_eq).comp (ker_lift f).range_restrict) $
+        $ mul_equiv.submonoid_congr ker_lift_range_eq).comp (ker_lift f).mrange_restrict) $
       (equiv.bijective _).comp
         ⟨λ x y h, injective_ker_lift f $ by rcases x; rcases y; injections,
          λ ⟨w, z, hzm, hz⟩, ⟨z, by rcases hz; rcases _x; refl⟩⟩ }

src/group_theory/monoid_localization.lean

@@ -230,16 +230,16 @@ by rw [mul_comm, sec_spec]
 @[to_additive "Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that
 `f(S) ⊆ add_units N`, for all `w : M, z : N` and `y ∈ S`, we have `w - f y = z ↔ w = f y + z`."]
 lemma mul_inv_left {f : M →* N} (h : ∀ y : S, is_unit (f y))
-  (y : S) (w z) : w * ↑(is_unit.lift_right (f.restrict S) h y)⁻¹ = z ↔ w = f y * z :=
+  (y : S) (w z) : w * ↑(is_unit.lift_right (f.mrestrict S) h y)⁻¹ = z ↔ w = f y * z :=
 by rw mul_comm; convert units.inv_mul_eq_iff_eq_mul _;
-  exact (is_unit.coe_lift_right (f.restrict S) h _).symm
+  exact (is_unit.coe_lift_right (f.mrestrict S) h _).symm
 
 /-- Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that `f(S) ⊆ units N`, for all
     `w : M, z : N` and `y ∈ S`, we have `z = w * (f y)⁻¹ ↔ z * f y = w`. -/
 @[to_additive "Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that
 `f(S) ⊆ add_units N`, for all `w : M, z : N` and `y ∈ S`, we have `z = w - f y ↔ z + f y = w`."]
 lemma mul_inv_right {f : M →* N} (h : ∀ y : S, is_unit (f y))
-  (y : S) (w z) : z = w * ↑(is_unit.lift_right (f.restrict S) h y)⁻¹ ↔ z * f y = w :=
+  (y : S) (w z) : z = w * ↑(is_unit.lift_right (f.mrestrict S) h y)⁻¹ ↔ z * f y = w :=
 by rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
 
 /-- Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that
@@ -249,8 +249,8 @@ by rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
 `f(S) ⊆ add_units N`, for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`, we have
 `f x₁ - f y₁ = f x₂ - f y₂ ↔ f (x₁ + y₂) = f (x₂ + y₁)`."]
 lemma mul_inv {f : M →* N} (h : ∀ y : S, is_unit (f y)) {x₁ x₂} {y₁ y₂ : S} :
-  f x₁ * ↑(is_unit.lift_right (f.restrict S) h y₁)⁻¹ =
-    f x₂ * ↑(is_unit.lift_right (f.restrict S) h y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁) :=
+  f x₁ * ↑(is_unit.lift_right (f.mrestrict S) h y₁)⁻¹ =
+    f x₂ * ↑(is_unit.lift_right (f.mrestrict S) h y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁) :=
 by rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ←mul_assoc, mul_inv_left h, mul_comm x₂,
   f.map_mul, f.map_mul]
 
@@ -259,17 +259,17 @@ by rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ←mul_assoc, mul_inv_le
 @[to_additive "Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that
 `f(S) ⊆ add_units N`, for all `y, z ∈ S`, we have `- (f y) = - (f z) → f y = f z`."]
 lemma inv_inj {f : M →* N} (hf : ∀ y : S, is_unit (f y)) {y z}
-  (h : (is_unit.lift_right (f.restrict S) hf y)⁻¹ = (is_unit.lift_right (f.restrict S) hf z)⁻¹) :
+  (h : (is_unit.lift_right (f.mrestrict S) hf y)⁻¹ = (is_unit.lift_right (f.mrestrict S) hf z)⁻¹) :
   f y = f z :=
 by rw [←mul_one (f y), eq_comm, ←mul_inv_left hf y (f z) 1, h];
-  convert units.inv_mul _; exact (is_unit.coe_lift_right (f.restrict S) hf _).symm
+  convert units.inv_mul _; exact (is_unit.coe_lift_right (f.mrestrict S) hf _).symm
 
 /-- Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that `f(S) ⊆ units N`, for all
     `y ∈ S`, `(f y)⁻¹` is unique. -/
 @[to_additive "Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that
 `f(S) ⊆ add_units N`, for all `y ∈ S`, `- (f y)` is unique."]
 lemma inv_unique {f : M →* N} (h : ∀ y : S, is_unit (f y)) {y : S}
-  {z} (H : f y * z = 1) : ↑(is_unit.lift_right (f.restrict S) h y)⁻¹ = z :=
+  {z} (H : f y * z = 1) : ↑(is_unit.lift_right (f.mrestrict S) h y)⁻¹ = z :=
 by rw [←one_mul ↑(_)⁻¹, mul_inv_left, ←H]
 
 variables (f : localization_map S N)
@@ -292,7 +292,7 @@ f.map_right_cancel $ by rw [mul_comm _ x, mul_comm _ y, h]
 @[to_additive "Given a localization map `f : M →+ N`, the surjection sending `(x, y) : M × S`
 to `f x - f y`."]
 noncomputable def mk' (f : localization_map S N) (x : M) (y : S) : N :=
-f.to_map x * ↑(is_unit.lift_right (f.to_map.restrict S) f.map_units y)⁻¹
+f.to_map x * ↑(is_unit.lift_right (f.to_map.mrestrict S) f.map_units y)⁻¹
 
 @[to_additive] lemma mk'_mul (x₁ x₂ : M) (y₁ y₂ : S) :
   f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂ :=
@@ -399,9 +399,9 @@ by rw [mul_comm, mk'_mul_cancel_right]
 
 @[to_additive] lemma is_unit_comp (j : N →* P) (y : S) :
   is_unit (j.comp f.to_map y) :=
-⟨units.map j $ is_unit.lift_right (f.to_map.restrict S) f.map_units y,
+⟨units.map j $ is_unit.lift_right (f.to_map.mrestrict S) f.map_units y,
   show j _ = j _, from congr_arg j $
-    (is_unit.coe_lift_right (f.to_map.restrict S) f.map_units _)⟩
+    (is_unit.coe_lift_right (f.to_map.mrestrict S) f.map_units _)⟩
 
 variables {g : M →* P}
 
@@ -414,7 +414,7 @@ lemma eq_of_eq (hg : ∀ y : S, is_unit (g y)) {x y} (h : f.to_map x = f.to_map
   g x = g y :=
 begin
   obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h,
-  rw [←mul_one (g x), ←is_unit.mul_lift_right_inv (g.restrict S) hg c],
+  rw [←mul_one (g x), ←is_unit.mul_lift_right_inv (g.mrestrict S) hg c],
   show _ * (g c * _) = _,
   rw [←mul_assoc, ←g.map_mul, hc, mul_inv_left hg, g.map_mul, mul_comm],
 end
@@ -441,7 +441,7 @@ of `add_comm_monoid`s `g : M →+ P` such that `g y` is invertible for all `y :
 induced from `N` to `P` sending `z : N` to `g x - g y`, where `(x, y) : M × S` are such that
 `z = f x - f y`."]
 noncomputable def lift : N →* P :=
-{ to_fun := λ z, g (f.sec z).1 * ↑(is_unit.lift_right (g.restrict S) hg (f.sec z).2)⁻¹,
+{ to_fun := λ z, g (f.sec z).1 * ↑(is_unit.lift_right (g.mrestrict S) hg (f.sec z).2)⁻¹,
   map_one' := by rw [mul_inv_left, mul_one]; exact f.eq_of_eq hg
     (by rw [←sec_spec, one_mul]),
   map_mul' := λ x y,
@@ -461,7 +461,7 @@ variables {S g}
 of `add_comm_monoid`s `g : M →+ P` such that `g y` is invertible for all `y : S`, the homomorphism
 induced from `N` to `P` maps `f x - f y` to `g x - g y` for all `x : M, y ∈ S`."]
 lemma lift_mk' (x y) :
-  f.lift hg (f.mk' x y) = g x * ↑(is_unit.lift_right (g.restrict S) hg y)⁻¹ :=
+  f.lift hg (f.mk' x y) = g x * ↑(is_unit.lift_right (g.mrestrict S) hg y)⁻¹ :=
 (mul_inv hg).2 $ f.eq_of_eq hg $ by
   rw [f.to_map.map_mul, f.to_map.map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]
 
@@ -585,7 +585,7 @@ begin
       obtain ⟨x, hx⟩ := f.surj z,
       use x,
       rw [←hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2)],
-      erw [is_unit.mul_lift_right_inv (g.restrict S) hg, mul_one] },
+      erw [is_unit.mul_lift_right_inv (g.mrestrict S) hg, mul_one] },
   { intros H v,
     obtain ⟨x, hx⟩ := H v,
     use f.mk' x.1 x.2,

src/group_theory/submonoid.lean

@@ -791,7 +791,7 @@ lemma closure_Union {ι} (s : ι → set M) : closure (⋃ i, s i) = ⨆ i, clos
 @[to_additive]
 lemma mem_supr_of_directed {ι} [hι : nonempty ι] {S : ι → submonoid M} (hS : directed (≤) S)
   {x : M} :
-  x ∈ (supr S : submonoid M) ↔ ∃ i, x ∈ S i :=
+  x ∈ (⨆ i, S i) ↔ ∃ i, x ∈ S i :=
 begin
   refine ⟨_, λ ⟨i, hi⟩, (le_def.1 $ le_supr S i) hi⟩,
   suffices : x ∈ closure (⋃ i, (S i : set M)) → ∃ i, x ∈ S i,
@@ -803,6 +803,11 @@ begin
     exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩ }
 end
 
+@[to_additive]
+lemma coe_supr_of_directed {ι} [nonempty ι] {S : ι → submonoid M} (hS : directed (≤) S) :
+  ((⨆ i, S i : submonoid M) : set M) = ⋃ i, ↑(S i) :=
+set.ext $ λ x, by simp [mem_supr_of_directed hS]
+
 @[to_additive]
 lemma mem_Sup_of_directed_on {S : set (submonoid M)} (Sne : S.nonempty)
   (hS : directed_on (≤) S) {x : M} :
@@ -813,6 +818,11 @@ begin
   exact (directed_on_iff_directed _).1 hS
 end
 
+@[to_additive]
+lemma coe_Sup_of_directed_on {S : set (submonoid M)} (Sne : S.nonempty) (hS : directed_on (≤) S) :
+  (↑(Sup S) : set M) = ⋃ s ∈ S, ↑s :=
+set.ext $ λ x, by simp [mem_Sup_of_directed_on Sne hS]
+
 variables {N : Type*} [monoid N] {P : Type*} [monoid P]
 
 /-- The preimage of a submonoid along a monoid homomorphism is a submonoid. -/
@@ -969,29 +979,26 @@ lemma map_mrange (g : N →* P) (f : M →* N) : f.mrange.map g = (g.comp f).mra
 
 /-- Restriction of a monoid hom to a submonoid of the domain. -/
 @[to_additive "Restriction of an add_monoid hom to an `add_submonoid` of the domain."]
-def restrict {N : Type*} [monoid N] (f : M →* N) (S : submonoid M) : S →* N := f.comp S.subtype
+def mrestrict {N : Type*} [monoid N] (f : M →* N) (S : submonoid M) : S →* N := f.comp S.subtype
 
-@[to_additive]
-lemma restrict_apply {N : Type*} [monoid N] (f : M →* N) (x : S) : f.restrict S x = f x := rfl
-
-@[simp, to_additive] lemma restrict_eq {N : Type} [monoid N] (f : M →* N) (x) :
-  f.restrict S x = f x := rfl
+@[simp, to_additive]
+lemma mrestrict_apply {N : Type*} [monoid N] (f : M →* N) (x : S) : f.mrestrict S x = f x := rfl
 
 /-- Restriction of a monoid hom to a submonoid of the codomain. -/
 @[to_additive "Restriction of an `add_monoid` hom to an `add_submonoid` of the codomain."]
-def cod_restrict (f : M →* N) (S : submonoid N) (h : ∀ x, f x ∈ S) : M →* S :=
+def cod_mrestrict (f : M →* N) (S : submonoid N) (h : ∀ x, f x ∈ S) : M →* S :=
 { to_fun := λ n, ⟨f n, h n⟩,
   map_one' := subtype.eq f.map_one,
   map_mul' := λ x y, subtype.eq (f.map_mul x y) }
 
 /-- Restriction of a monoid hom to its range iterpreted as a submonoid. -/
 @[to_additive "Restriction of an `add_monoid` hom to its range interpreted as a submonoid."]
-def range_restrict {N} [monoid N] (f : M →* N) : M →* f.mrange :=
-f.cod_restrict f.mrange $ λ x, ⟨x, submonoid.mem_top x, rfl⟩
+def mrange_restrict {N} [monoid N] (f : M →* N) : M →* f.mrange :=
+f.cod_mrestrict f.mrange $ λ x, ⟨x, submonoid.mem_top x, rfl⟩
 
 @[simp, to_additive]
-lemma coe_range_restrict {N} [monoid N] (f : M →* N) (x : M) :
-  (f.range_restrict x : N) = f x :=
+lemma coe_mrange_restrict {N} [monoid N] (f : M →* N) (x : M) :
+  (f.mrange_restrict x : N) = f x :=
 rfl
 
 @[to_additive]
@@ -1029,7 +1036,7 @@ lemma eq_of_eq_on_mdense {s : set M} (hs : closure s = ⊤) {f g : M →* N} (h
 eq_of_eq_on_mtop $ hs ▸ eq_on_mclosure h
 
 @[to_additive]
-lemma closure_preimage_le (f : M →* N) (s : set N) :
+lemma mclosure_preimage_le (f : M →* N) (s : set N) :
   closure (f ⁻¹' s) ≤ (closure s).comap f :=
 closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx
 
@@ -1041,7 +1048,7 @@ lemma map_mclosure (f : M →* N) (s : set M) :
   (closure s).map f = closure (f '' s) :=
 le_antisymm
   (map_le_iff_le_comap.2 $ le_trans (closure_mono $ set.subset_preimage_image _ _)
-    (closure_preimage_le _ _))
+    (mclosure_preimage_le _ _))
   (closure_le.2 $ set.image_subset _ subset_closure)
 
 end monoid_hom
@@ -1063,12 +1070,12 @@ namespace submonoid
 
 variables {N : Type*} [monoid N]
 
-open monoid_hom lattice
+open monoid_hom
 
 /-- The monoid hom associated to an inclusion of submonoids. -/
 @[to_additive "The `add_monoid` hom associated to an inclusion of submonoids."]
 def inclusion {S T : submonoid M} (h : S ≤ T) : S →* T :=
-S.subtype.cod_restrict _ (λ x, h x.2)
+S.subtype.cod_mrestrict _ (λ x, h x.2)
 
 @[simp, to_additive]
 lemma range_subtype (s : submonoid M) : s.subtype.mrange = s :=

src/ring_theory/localization.lean

@@ -323,7 +323,7 @@ variables {g : R →+* P} (hg : ∀ y : M, is_unit (g y))
 `g : R →* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
 `S` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : R, y ∈ M`. -/
 lemma lift_mk' (x y) :
-  f.lift hg (f.mk' x y) = g x * ↑(is_unit.lift_right (g.to_monoid_hom.restrict M) hg y)⁻¹ :=
+  f.lift hg (f.mk' x y) = g x * ↑(is_unit.lift_right (g.to_monoid_hom.mrestrict M) hg y)⁻¹ :=
 f.to_localization_map.lift_mk' _ _ _
 
 lemma lift_mk'_spec (x v) (y : M) :