feat(group_theory/submonoid/basic): weaken assumptions for has_one instance to one_mem_class for set_like subobjects (#16104)

j-loreaux · j-loreaux · commit 4e861f25ba5c · 2022-08-19T09:24:17.000Z
diff --git a/src/algebra/algebra/subalgebra/basic.lean b/src/algebra/algebra/subalgebra/basic.lean
@@ -278,8 +278,8 @@ protected lemma coe_sub {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebr
   ↑(algebra_map R' S r) = algebra_map R' A r := rfl
 
 protected lemma coe_pow (x : S) (n : ℕ) : (↑(x^n) : A) = (↑x)^n := submonoid_class.coe_pow x n
-protected lemma coe_eq_zero {x : S} : (x : A) = 0 ↔ x = 0 := add_submonoid_class.coe_eq_zero
-protected lemma coe_eq_one {x : S} : (x : A) = 1 ↔ x = 1 := submonoid_class.coe_eq_one
+protected lemma coe_eq_zero {x : S} : (x : A) = 0 ↔ x = 0 := zero_mem_class.coe_eq_zero
+protected lemma coe_eq_one {x : S} : (x : A) = 1 ↔ x = 1 := one_mem_class.coe_eq_one
 
 -- todo: standardize on the names these morphisms
 -- compare with submodule.subtype
diff --git a/src/algebra/direct_sum/basic.lean b/src/algebra/direct_sum/basic.lean
@@ -263,7 +263,7 @@ lemma coe_of_apply {M S : Type*} [decidable_eq ι] [add_comm_monoid M]
 begin
   obtain rfl | h := decidable.eq_or_ne i j,
   { rw [direct_sum.of_eq_same, if_pos rfl], },
-  { rw [direct_sum.of_eq_of_ne _ _ _ _ h, if_neg h, add_submonoid_class.coe_zero], },
+  { rw [direct_sum.of_eq_of_ne _ _ _ _ h, if_neg h, zero_mem_class.coe_zero], },
 end
 
 /-- The `direct_sum` formed by a collection of additive submonoids (or subgroups, or submodules) of
diff --git a/src/algebra/direct_sum/decomposition.lean b/src/algebra/direct_sum/decomposition.lean
@@ -109,7 +109,7 @@ by rw [decompose_of_mem _ hx, direct_sum.of_eq_same, subtype.coe_mk]
 lemma decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j):
   (decompose ℳ x j : M) = 0 :=
 by rw [decompose_of_mem _ hx, direct_sum.of_eq_of_ne _ _ _ _ hij,
-  add_submonoid_class.coe_zero]
+  zero_mem_class.coe_zero]
 
 /-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
 an additive monoid to a direct sum of components. -/
diff --git a/src/algebra/module/injective.lean b/src/algebra/module/injective.lean
@@ -261,7 +261,7 @@ begin
   rw extension_of_max_adjoin.extend_ideal_to_is_extension i f h y r
     (by rw eq1; exact submodule.zero_mem _ : r • y ∈ _),
   simp only [extension_of_max_adjoin.ideal_to, linear_map.coe_mk, eq1, subtype.coe_mk,
-    ← add_submonoid_class.zero_def, (extension_of_max i f).to_linear_pmap.map_zero]
+    ← zero_mem_class.zero_def, (extension_of_max i f).to_linear_pmap.map_zero]
 end
 
 lemma extension_of_max_adjoin.extend_ideal_to_wd (h : module.Baer R Q) {y : N} (r r' : R)
diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean
@@ -370,7 +370,7 @@ begin
       ← is_scalar_tower.algebra_map_eq, ← eval₂_eq_eval_map] },
   { obtain ⟨P, hPmo, hProot⟩ := h,
     refine ⟨P, hPmo, _⟩,
-    rw [← aeval_def, aeval_coe, aeval_def, hProot, add_submonoid_class.coe_zero] },
+    rw [← aeval_def, aeval_coe, aeval_def, hProot, zero_mem_class.coe_zero] },
 end
 
 /-- The map `E → F` when `E` is an intermediate field contained in the intermediate field `F`.
diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean
@@ -388,25 +388,29 @@ end galois_insertion
 
 end submonoid
 
-namespace submonoid_class
+namespace one_mem_class
 
-variables {A : Type*} [set_like A M] [hA : submonoid_class A M] (S' : A)
+variables {A M₁ : Type*} [set_like A M₁] [has_one M₁] [hA : one_mem_class A M₁] (S' : A)
 include hA
 
 /-- A submonoid of a monoid inherits a 1. -/
 @[to_additive "An `add_submonoid` of an `add_monoid` inherits a zero."]
-instance has_one : has_one S' := ⟨⟨_, one_mem S'⟩⟩
+instance has_one : has_one S' := ⟨⟨1, one_mem_class.one_mem S'⟩⟩
 
-@[simp, norm_cast, to_additive] lemma coe_one : ((1 : S') : M) = 1 := rfl
+@[simp, norm_cast, to_additive] lemma coe_one : ((1 : S') : M₁) = 1 := rfl
 
 variables {S'}
-@[simp, norm_cast, to_additive] lemma coe_eq_one {x : S'} : (↑x : M) = 1 ↔ x = 1 :=
-(subtype.ext_iff.symm : (x : M) = (1 : S') ↔ x = 1)
+@[simp, norm_cast, to_additive] lemma coe_eq_one {x : S'} : (↑x : M₁) = 1 ↔ x = 1 :=
+(subtype.ext_iff.symm : (x : M₁) = (1 : S') ↔ x = 1)
 variables (S')
 
-@[to_additive] lemma one_def : (1 : S') = ⟨1, one_mem S'⟩ := rfl
+@[to_additive] lemma one_def : (1 : S') = ⟨1, one_mem_class.one_mem S'⟩ := rfl
+
+end one_mem_class
 
-omit hA
+namespace submonoid_class
+
+variables {A : Type*} [set_like A M] [hA : submonoid_class A M] (S' : A)
 
 /-- An `add_submonoid` of an `add_monoid` inherits a scalar multiplication. -/
 instance _root_.add_submonoid_class.has_nsmul {M} [add_monoid M] {A : Type*} [set_like A M]
diff --git a/src/ring_theory/graded_algebra/basic.lean b/src/ring_theory/graded_algebra/basic.lean
@@ -99,7 +99,7 @@ by rw [graded_ring.proj_apply, decompose_symm_of, equiv.apply_symm_apply]
 
 lemma graded_ring.mem_support_iff [Π i (x : 𝒜 i), decidable (x ≠ 0)] (r : A) (i : ι) :
   i ∈ (decompose 𝒜 r).support ↔ graded_ring.proj 𝒜 i r ≠ 0 :=
-dfinsupp.mem_support_iff.trans add_submonoid_class.coe_eq_zero.not.symm
+dfinsupp.mem_support_iff.trans zero_mem_class.coe_eq_zero.not.symm
 
 end graded_ring
 
@@ -246,10 +246,10 @@ def graded_ring.proj_zero_ring_hom : A →+* A :=
   map_add' := λ _ _, by { rw decompose_add, refl },
   map_mul' := begin
     refine direct_sum.decomposition.induction_on 𝒜 (λ x, _) _ _,
-    { simp only [zero_mul, decompose_zero, zero_apply, add_submonoid_class.coe_zero] },
+    { simp only [zero_mul, decompose_zero, zero_apply, zero_mem_class.coe_zero] },
     { rintros i ⟨c, hc⟩,
       refine direct_sum.decomposition.induction_on 𝒜 _ _ _,
-      { simp only [mul_zero, decompose_zero, zero_apply, add_submonoid_class.coe_zero] },
+      { simp only [mul_zero, decompose_zero, zero_apply, zero_mem_class.coe_zero] },
       { rintros j ⟨c', hc'⟩,
         { simp only [subtype.coe_mk],
           by_cases h : i + j = 0,
diff --git a/src/ring_theory/graded_algebra/homogeneous_ideal.lean b/src/ring_theory/graded_algebra/homogeneous_ideal.lean
@@ -553,7 +553,7 @@ def homogeneous_ideal.irrelevant : homogeneous_ideal 𝒜 :=
 ⟨(graded_ring.proj_zero_ring_hom 𝒜).ker, λ i r (hr : (decompose 𝒜 r 0 : A) = 0), begin
   change (decompose 𝒜 (decompose 𝒜 r _ : A) 0 : A) = 0,
   by_cases h : i = 0,
-  { rw [h, hr, decompose_zero, zero_apply, add_submonoid_class.coe_zero] },
+  { rw [h, hr, decompose_zero, zero_apply, zero_mem_class.coe_zero] },
   { rw [decompose_of_mem_ne 𝒜 (set_like.coe_mem _) h] }
 end⟩
 
diff --git a/src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial/basic.lean
@@ -696,7 +696,7 @@ begin
   obtain ⟨x, hx'⟩ := x,
   obtain ⟨y, rfl⟩ := (ring_hom.mem_range).1 hx',
   refine subtype.eq _,
-  simp only [ring_hom.comp_apply, quotient.eq_zero_iff_mem, add_submonoid_class.coe_zero,
+  simp only [ring_hom.comp_apply, quotient.eq_zero_iff_mem, zero_mem_class.coe_zero,
     subtype.val_eq_coe],
   suffices : C (i y) ∈ (I.map (polynomial.map_ring_hom i)),
   { obtain ⟨f, hf⟩ := mem_image_of_mem_map_of_surjective (polynomial.map_ring_hom i)
