feat(group_theory/submonoid): center of a submonoid (#8921)

This adds `set.center`, `submonoid.center`, `subsemiring.center`, and `subring.center`, to complement the existing `subgroup.center`.

This ran into a timeout, so had to squeeze some `simp`s in an unrelated file.

src/analysis/analytic/basic.lean

@@ -505,7 +505,8 @@ lemma has_fpower_series_on_ball.is_O_image_sub_image_sub_deriv_principal
     (λ y, ∥y - (x, x)∥ * ∥y.1 - y.2∥) (𝓟 $ emetric.ball (x, x) r') :=
 begin
   lift r' to ℝ≥0 using ne_top_of_lt hr,
-  rcases (zero_le r').eq_or_lt with rfl|hr'0, { simp },
+  rcases (zero_le r').eq_or_lt with rfl|hr'0,
+  { simp only [is_O_bot, emetric.ball_zero, principal_empty, ennreal.coe_zero] },
   obtain ⟨a, ha, C, hC : 0 < C, hp⟩ :
     ∃ (a ∈ Ioo (0 : ℝ) 1) (C > 0), ∀ (n : ℕ), ∥p n∥ * ↑r' ^ n ≤ C * a ^ n,
     from p.norm_mul_pow_le_mul_pow_of_lt_radius (hr.trans_le hf.r_le),
@@ -519,7 +520,7 @@ begin
     { rw [emetric.ball_prod_same], exact emetric.ball_subset_ball hr.le hy' },
     set A : ℕ → F := λ n, p n (λ _, y.1 - x) - p n (λ _, y.2 - x),
     have hA : has_sum (λ n, A (n + 2)) (f y.1 - f y.2 - (p 1 (λ _, y.1 - y.2))),
-    { convert (has_sum_nat_add_iff' 2).2 ((hf.has_sum_sub hy.1).sub (hf.has_sum_sub hy.2)),
+    { convert (has_sum_nat_add_iff' 2).2 ((hf.has_sum_sub hy.1).sub (hf.has_sum_sub hy.2)) using 1,
       rw [finset.sum_range_succ, finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self,
         zero_add, ← subsingleton.pi_single_eq (0 : fin 1) (y.1 - x), pi.single,
         ← subsingleton.pi_single_eq (0 : fin 1) (y.2 - x), pi.single, ← (p 1).map_sub, ← pi.single,
@@ -529,7 +530,7 @@ begin
       (C * (a / r') ^ 2) * (∥y - (x, x)∥ * ∥y.1 - y.2∥) * ((n + 2) * a ^ n),
     have hAB : ∀ n, ∥A (n + 2)∥ ≤ B n := λ n,
     calc ∥A (n + 2)∥ ≤ ∥p (n + 2)∥ * ↑(n + 2) * ∥y - (x, x)∥ ^ (n + 1) * ∥y.1 - y.2∥ :
-      by simpa [fintype.card_fin, pi_norm_const, prod.norm_def, pi.sub_def, prod.fst_sub,
+      by simpa only [fintype.card_fin, pi_norm_const, prod.norm_def, pi.sub_def, prod.fst_sub,
         prod.snd_sub, sub_sub_sub_cancel_right]
         using (p $ n + 2).norm_image_sub_le (λ _, y.1 - x) (λ _, y.2 - x)
     ... = ∥p (n + 2)∥ * ∥y - (x, x)∥ ^ n * (↑(n + 2) * ∥y - (x, x)∥ * ∥y.1 - y.2∥) :
@@ -539,7 +540,7 @@ begin
         hy'.le, norm_nonneg, pow_nonneg, div_nonneg, mul_nonneg, nat.cast_nonneg,
         hC.le, r'.coe_nonneg, ha.1.le]
     ... = B n :
-      by { field_simp [B, pow_succ, hr'0.ne'], simp [mul_assoc, mul_comm, mul_left_comm] },
+      by { field_simp [B, pow_succ, hr'0.ne'], simp only [mul_assoc, mul_comm, mul_left_comm] },
     have hBL : has_sum B (L y),
     { apply has_sum.mul_left,
       simp only [add_mul],

src/group_theory/subgroup.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 -/
 import group_theory.submonoid
+import group_theory.submonoid.center
 import algebra.group.conj
 import algebra.pointwise
 import order.atoms
@@ -1006,15 +1007,18 @@ instance top_normal : normal (⊤ : subgroup G) := ⟨λ _ _, mem_top⟩
 
 variable (G)
 /-- The center of a group `G` is the set of elements that commute with everything in `G` -/
-@[to_additive "The center of a group `G` is the set of elements that commute with everything in
-`G`"]
+@[to_additive "The center of an additive group `G` is the set of elements that commute with
+everything in `G`"]
 def center : subgroup G :=
-{ carrier := {z | ∀ g, g * z = z * g},
-  one_mem' := by simp,
-  mul_mem' := λ a b (ha : ∀ g, g * a = a * g) (hb : ∀ g, g * b = b * g) g,
-    by assoc_rw [ha, hb g],
-  inv_mem' := λ a (ha : ∀ g, g * a = a * g) g,
-    by rw [← inv_inj, mul_inv_rev, inv_inv, ← ha, mul_inv_rev, inv_inv] }
+{ carrier := set.center G,
+  inv_mem' := λ a, set.inv_mem_center,
+  .. submonoid.center G }
+
+@[to_additive]
+lemma coe_center : ↑(center G) = set.center G := rfl
+
+@[simp, to_additive]
+lemma center_to_submonoid : (center G).to_submonoid = submonoid.center G := rfl
 
 variable {G}
 

src/group_theory/submonoid/center.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import group_theory.submonoid.operations
+
+/-!
+# Centers of magmas and monoids
+
+## Main definitions
+
+* `set.center`: the center of a magma
+* `submonoid.center`: the center of a monoid
+* `set.add_center`: the center of an additive magma
+* `add_submonoid.center`: the center of an additive monoid
+
+We show `subgrup.center` and `subsemiring.center` and `subring.center` in other files.
+-/
+
+variables {M : Type*}
+
+namespace set
+
+variables (M)
+
+/-- The center of a magma. -/
+@[to_additive add_center /-" The center of an additive magma. "-/]
+def center [has_mul M] : set M := {z | ∀ m, m * z = z * m}
+
+@[to_additive mem_add_center]
+lemma mem_center_iff [has_mul M] {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g := iff.rfl
+
+@[simp, to_additive zero_mem_add_center]
+lemma one_mem_center [mul_one_class M] : (1 : M) ∈ set.center M := by simp [mem_center_iff]
+
+@[simp]
+lemma zero_mem_center [mul_zero_class M] : (0 : M) ∈ set.center M := by simp [mem_center_iff]
+
+variables {M}
+
+@[simp, to_additive add_mem_add_center]
+lemma mul_mem_center [semigroup M] {a b : M}
+  (ha : a ∈ set.center M) (hb : b ∈ set.center M) : a * b ∈ set.center M :=
+λ g, by rw [mul_assoc, ←hb g, ← mul_assoc, ha g, mul_assoc]
+
+@[simp, to_additive neg_mem_add_center]
+lemma inv_mem_center [group M] {a : M} (ha : a ∈ set.center M) : a⁻¹ ∈ set.center M :=
+λ g, by rw [← inv_inj, mul_inv_rev, inv_inv, ← ha, mul_inv_rev, inv_inv]
+
+@[simp]
+lemma add_mem_center [distrib M] {a b : M}
+  (ha : a ∈ set.center M) (hb : b ∈ set.center M) : a + b ∈ set.center M :=
+λ c, by rw [add_mul, mul_add, ha c, hb c]
+
+@[simp]
+lemma neg_mem_center [ring M] {a : M} (ha : a ∈ set.center M) : -a ∈ set.center M :=
+λ c, by rw [←neg_mul_comm, ha (-c), neg_mul_comm]
+
+@[to_additive subset_add_center_add_units]
+lemma subset_center_units [monoid M] :
+  (coe : units M → M) ⁻¹' center M ⊆ set.center (units M) :=
+λ a ha b, units.ext $ ha _
+
+lemma center_units_subset [group_with_zero M] :
+  set.center (units M) ⊆ (coe : units M → M) ⁻¹' center M :=
+λ a ha b, begin
+  obtain rfl | hb := eq_or_ne b 0,
+  { rw [zero_mul, mul_zero], },
+  { exact units.ext_iff.mp (ha (units.mk0 _ hb)) }
+end
+
+/-- In a group with zero, the center of the units is the preimage of the center. -/
+lemma center_units_eq [group_with_zero M] :
+  set.center (units M) = (coe : units M → M) ⁻¹' center M :=
+subset.antisymm center_units_subset subset_center_units
+
+@[simp]
+lemma inv_mem_center' [group_with_zero M] {a : M} (ha : a ∈ set.center M) : a⁻¹ ∈ set.center M :=
+begin
+  obtain rfl | ha0 := eq_or_ne a 0,
+  { rw inv_zero, exact zero_mem_center M },
+  lift a to units M using ha0,
+  rw ←units.coe_inv',
+  exact center_units_subset (inv_mem_center (subset_center_units ha)),
+end
+
+variables (M)
+
+@[simp, to_additive add_center_eq_univ]
+lemma center_eq_univ [comm_semigroup M] : center M = set.univ :=
+subset.antisymm (subset_univ _) $ λ x _ y, mul_comm y x
+
+end set
+
+namespace submonoid
+section
+variables (M) [monoid M]
+
+/-- The center of a monoid `M` is the set of elements that commute with everything in `M` -/
+@[to_additive "The center of a monoid `M` is the set of elements that commute with everything in
+`M`"]
+def center : submonoid M :=
+{ carrier := set.center M,
+  one_mem' := set.one_mem_center M,
+  mul_mem' := λ a b, set.mul_mem_center }
+
+@[to_additive] lemma coe_center : ↑(center M) = set.center M := rfl
+
+variables {M}
+
+@[to_additive] lemma mem_center_iff {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g := iff.rfl
+
+/-- The center of a monoid is commutative. -/
+instance : comm_monoid (center M) :=
+{ mul_comm := λ a b, subtype.ext $ b.prop _,
+  .. (center M).to_monoid }
+
+end
+
+section
+variables (M) [comm_monoid M]
+
+@[simp] lemma center_eq_top : center M = ⊤ :=
+set_like.coe_injective (set.center_eq_univ M)
+
+end
+
+end submonoid

src/ring_theory/subring.lean

@@ -32,6 +32,8 @@ Notation used here:
 
 * `instance : complete_lattice (subring R)` : the complete lattice structure on the subrings.
 
+* `subring.center` : the center of a ring `R`.
+
 * `subring.closure` : subring closure of a set, i.e., the smallest subring that includes the set.
 
 * `subring.gi` : `closure : set M → subring M` and coercion `coe : subring M → set M`
@@ -476,6 +478,35 @@ 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⟩
 
+section
+
+variables (R)
+
+/-- The center of a semiring `R` is the set of elements that commute with everything in `R` -/
+def center : subring R :=
+{ carrier := set.center R,
+  neg_mem' := λ a, set.neg_mem_center,
+  .. subsemiring.center R }
+
+lemma coe_center : ↑(center R) = set.center R := rfl
+
+@[simp] lemma center_to_subsemiring : (center R).to_subsemiring = subsemiring.center R := rfl
+
+variables {R}
+
+lemma mem_center_iff {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g :=
+iff.rfl
+
+@[simp] lemma center_eq_top (R) [comm_ring R] : center R = ⊤ :=
+set_like.coe_injective (set.center_eq_univ R)
+
+/-- The center is commutative. -/
+instance : comm_ring (center R) :=
+{ ..subsemiring.center.comm_semiring,
+  ..(center R).to_ring}
+
+end
+
 /-! # subring closure of a subset -/
 
 /-- The `subring` generated by a set. -/

src/ring_theory/subsemiring.lean

@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 
 import algebra.ring.prod
 import group_theory.submonoid
+import group_theory.submonoid.center
 import data.equiv.ring
 
 /-!
@@ -374,6 +375,33 @@ instance : complete_lattice (subsemiring R) :=
 lemma eq_top_iff' (A : subsemiring R) : A = ⊤ ↔ ∀ x : R, x ∈ A :=
 eq_top_iff.trans ⟨λ h m, h $ mem_top m, λ h m _, h m⟩
 
+section
+
+/-- The center of a semiring `R` is the set of elements that commute with everything in `R` -/
+def center (R) [semiring R] : subsemiring R :=
+{ carrier := set.center R,
+  zero_mem' := set.zero_mem_center R,
+  add_mem' := λ a b, set.add_mem_center,
+  .. submonoid.center R }
+
+lemma coe_center (R) [semiring R] : ↑(center R) = set.center R := rfl
+
+@[simp]
+lemma center_to_submonoid (R) [semiring R] : (center R).to_submonoid = submonoid.center R := rfl
+
+lemma mem_center_iff {R} [semiring R] {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g :=
+iff.rfl
+
+@[simp] lemma center_eq_top (R) [comm_semiring R] : center R = ⊤ :=
+set_like.coe_injective (set.center_eq_univ R)
+
+/-- The center is commutative. -/
+instance {R} [semiring R] : comm_semiring (center R) :=
+{ ..submonoid.center.comm_monoid,
+  ..(center R).to_semiring}
+
+end
+
 /-- The `subsemiring` generated by a set. -/
 def closure (s : set R) : subsemiring R := Inf {S | s ⊆ S}