feat(ring_theory/subring): centralizer as a subring (#18861)

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/algebra/algebra/subalgebra/basic.lean

@@ -1049,10 +1049,15 @@ lemma mem_centralizer_iff {s : set A} {z : A} :
   z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g :=
 iff.rfl
 
+lemma center_le_centralizer (s) : center R A ≤ centralizer R s := s.center_subset_centralizer
+
 lemma centralizer_le (s t : set A) (h : s ⊆ t) :
   centralizer R t ≤ centralizer R s :=
 set.centralizer_subset h
 
+@[simp] lemma centralizer_eq_top_iff_subset {s : set A} : centralizer R s = ⊤ ↔ s ⊆ center R A :=
+set_like.ext'_iff.trans set.centralizer_eq_top_iff_subset
+
 @[simp]
 lemma centralizer_univ : centralizer R set.univ = center R A :=
 set_like.ext' (set.centralizer_univ A)

src/group_theory/subgroup/basic.lean

@@ -1604,9 +1604,14 @@ set_like.ext' (set.centralizer_univ G)
 @[to_additive] lemma le_centralizer_iff : H ≤ K.centralizer ↔ K ≤ H.centralizer :=
 ⟨λ h x hx y hy, (h hy x hx).symm, λ h x hx y hy, (h hy x hx).symm⟩
 
+lemma center_le_centralizer (s) : center G ≤ centralizer s := set.center_subset_centralizer s
+
 @[to_additive] lemma centralizer_le (h : H ≤ K) : centralizer K ≤ centralizer H :=
 submonoid.centralizer_le h
 
+@[simp] lemma centralizer_eq_top_iff_subset {s} : centralizer s = ⊤ ↔ s ≤ center G :=
+set_like.ext'_iff.trans set.centralizer_eq_top_iff_subset
+
 @[to_additive] instance subgroup.centralizer.characteristic [hH : H.characteristic] :
   H.centralizer.characteristic :=
 begin

src/group_theory/submonoid/centralizer.lean

@@ -50,6 +50,8 @@ variables {S}
 @[to_additive] lemma mem_centralizer_iff {z : M} : z ∈ centralizer S ↔ ∀ g ∈ S, g * z = z * g :=
 iff.rfl
 
+lemma center_le_centralizer (s) : center M ≤ centralizer s := s.center_subset_centralizer
+
 @[to_additive] instance decidable_mem_centralizer (a) [decidable $ ∀ b ∈ S, b * a = a * b] :
   decidable (a ∈ centralizer S) :=
 decidable_of_iff' _ mem_centralizer_iff
@@ -58,6 +60,9 @@ decidable_of_iff' _ mem_centralizer_iff
 lemma centralizer_le (h : S ⊆ T) : centralizer T ≤ centralizer S :=
 set.centralizer_subset h
 
+@[simp] lemma centralizer_eq_top_iff_subset {s : set M} : centralizer s = ⊤ ↔ s ⊆ center M :=
+set_like.ext'_iff.trans set.centralizer_eq_top_iff_subset
+
 variables (M)
 
 @[simp, to_additive]

src/group_theory/subsemigroup/centralizer.lean

@@ -100,6 +100,14 @@ end
 lemma centralizer_subset [has_mul M] (h : S ⊆ T) : centralizer T ⊆ centralizer S :=
 λ t ht s hs, ht s (h hs)
 
+lemma center_subset_centralizer [has_mul M] (S : set M) : set.center M ⊆ S.centralizer :=
+λ x hx m _, hx m
+
+@[simp] lemma centralizer_eq_top_iff_subset {s : set M} [has_mul M] :
+  centralizer s = set.univ ↔ s ⊆ center M :=
+eq_top_iff.trans $ ⟨λ h x hx g, (h trivial _ hx).symm,
+                    λ h x _ m hm, (h hm x).symm⟩
+
 variables (M)
 
 @[simp, to_additive add_centralizer_univ]
@@ -112,6 +120,7 @@ variables {M} (S)
 lemma centralizer_eq_univ [comm_semigroup M] : centralizer S = univ :=
 subset.antisymm (subset_univ _) $ λ x hx y hy, mul_comm y x
 
+
 end set
 
 namespace subsemigroup
@@ -135,10 +144,15 @@ iff.rfl
   decidable (a ∈ centralizer S) :=
 decidable_of_iff' _ mem_centralizer_iff
 
+lemma center_le_centralizer (S) : center M ≤ centralizer S := S.center_subset_centralizer
+
 @[to_additive]
 lemma centralizer_le (h : S ⊆ T) : centralizer T ≤ centralizer S :=
 set.centralizer_subset h
 
+@[simp] lemma centralizer_eq_top_iff_subset {s : set M} : centralizer s = ⊤ ↔ s ⊆ center M :=
+set_like.ext'_iff.trans set.centralizer_eq_top_iff_subset
+
 variables (M)
 
 @[simp, to_additive]

src/ring_theory/non_unital_subsemiring/basic.lean

@@ -417,10 +417,17 @@ lemma mem_centralizer_iff {R} [non_unital_semiring R] {s : set R} {z : R} :
   z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g :=
 iff.rfl
 
+lemma center_le_centralizer {R} [non_unital_semiring R] (s) : center R ≤ centralizer s :=
+  s.center_subset_centralizer
+
 lemma centralizer_le {R} [non_unital_semiring R] (s t : set R) (h : s ⊆ t) :
   centralizer t ≤ centralizer s :=
 set.centralizer_subset h
 
+@[simp] lemma centralizer_eq_top_iff_subset {R} [non_unital_semiring R] {s : set R} :
+  centralizer s = ⊤ ↔ s ⊆ center R :=
+set_like.ext'_iff.trans set.centralizer_eq_top_iff_subset
+
 @[simp]
 lemma centralizer_univ {R} [non_unital_semiring R] : centralizer set.univ = center R :=
 set_like.ext' (set.centralizer_univ R)

src/ring_theory/subring/basic.lean

@@ -651,6 +651,39 @@ lemma center.coe_div (a b : center K) : ((a / b : center K) : K) = (a : K) / (b
 
 end division_ring
 
+section centralizer
+
+/-- The centralizer of a set inside a ring as a `subring`. -/
+def centralizer (s : set R) : subring R :=
+{ neg_mem' := λ x, set.neg_mem_centralizer,
+  ..subsemiring.centralizer s }
+
+@[simp, norm_cast]
+lemma coe_centralizer (s : set R) : (centralizer s : set R) = s.centralizer := rfl
+
+lemma centralizer_to_submonoid (s : set R) :
+  (centralizer s).to_submonoid = submonoid.centralizer s := rfl
+
+lemma centralizer_to_subsemiring (s : set R) :
+  (centralizer s).to_subsemiring = subsemiring.centralizer s := rfl
+
+lemma mem_centralizer_iff {s : set R} {z : R} :
+  z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g :=
+iff.rfl
+
+lemma center_le_centralizer (s) : center R ≤ centralizer s := s.center_subset_centralizer
+
+lemma centralizer_le (s t : set R) (h : s ⊆ t) : centralizer t ≤ centralizer s :=
+set.centralizer_subset h
+
+@[simp] lemma centralizer_eq_top_iff_subset {s : set R} : centralizer s = ⊤ ↔ s ⊆ center R :=
+set_like.ext'_iff.trans set.centralizer_eq_top_iff_subset
+
+@[simp] lemma centralizer_univ : centralizer set.univ = center R :=
+set_like.ext' (set.centralizer_univ R)
+
+end centralizer
+
 /-! ## subring closure of a subset -/
 
 /-- The `subring` generated by a set. -/

src/ring_theory/subsemiring/basic.lean

@@ -604,10 +604,17 @@ lemma mem_centralizer_iff {R} [semiring R] {s : set R} {z : R} :
   z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g :=
 iff.rfl
 
+lemma center_le_centralizer {R} [semiring R] (s) : center R ≤ centralizer s :=
+  s.center_subset_centralizer
+
 lemma centralizer_le {R} [semiring R] (s t : set R) (h : s ⊆ t) :
   centralizer t ≤ centralizer s :=
 set.centralizer_subset h
 
+@[simp] lemma centralizer_eq_top_iff_subset {R} [semiring R] {s : set R} :
+  centralizer s = ⊤ ↔ s ⊆ center R :=
+set_like.ext'_iff.trans set.centralizer_eq_top_iff_subset
+
 @[simp]
 lemma centralizer_univ {R} [semiring R] : centralizer set.univ = center R :=
 set_like.ext' (set.centralizer_univ R)