refactor(algebra/graded_monoid): provide better names for lemmas abou…

…t internal graduations (#15488)

This provides `set_like.one_mem_graded` as the preferred spelling of the projection `set_like.has_graded_one.one_mem`.

This follows the usual pattern of not including the typeclass name in the lemma that it provides; we don't usually write `add_semigroup.add_assoc`. The new lemmas are now listed in the docstring as the preferred API for working with these typeclasses.

src/algebra/direct_sum/internal.lean

@@ -47,38 +47,38 @@ instance add_comm_monoid.of_submonoid_on_semiring [semiring R] [set_like σ R]
   [add_submonoid_class σ R] (A : ι → σ) : ∀ i, add_comm_monoid (A i) :=
 λ i, by apply_instance
 
-instance add_comm_group.of_subgroup_on_semiring [ring R] [set_like σ R]
+instance add_comm_group.of_subgroup_on_ring [ring R] [set_like σ R]
   [add_subgroup_class σ R] (A : ι → σ) : ∀ i, add_comm_group (A i) :=
 λ i, by apply_instance
 
-lemma set_like.has_graded_one.algebra_map_mem [has_zero ι]
+lemma set_like.algebra_map_mem_graded [has_zero ι]
   [comm_semiring S] [semiring R] [algebra S R]
   (A : ι → submodule S R) [set_like.has_graded_one A] (s : S) : algebra_map S R s ∈ A 0 :=
 begin
   rw algebra.algebra_map_eq_smul_one,
-  exact ((A 0).smul_mem s set_like.has_graded_one.one_mem),
+  exact ((A 0).smul_mem s $ set_like.one_mem_graded _),
 end
 
-lemma set_like.has_graded_one.nat_cast_mem [has_zero ι] [add_monoid_with_one R]
+lemma set_like.nat_cast_mem_graded [has_zero ι] [add_monoid_with_one R]
   [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [set_like.has_graded_one A] (n : ℕ) :
-  (n : R) ∈ A 0:=
+  (n : R) ∈ A 0 :=
 begin
   induction n,
   { rw nat.cast_zero,
     exact zero_mem (A 0), },
   { rw nat.cast_succ,
-    exact add_mem n_ih set_like.has_graded_one.one_mem, },
+    exact add_mem n_ih (set_like.one_mem_graded _), },
 end
 
-lemma set_like.has_graded_one.int_cast_mem [has_zero ι] [add_group_with_one R]
+lemma set_like.int_cast_mem_graded [has_zero ι] [add_group_with_one R]
   [set_like σ R] [add_subgroup_class σ R] (A : ι → σ) [set_like.has_graded_one A] (z : ℤ) :
   (z : R) ∈ A 0:=
 begin
   induction z,
   { rw int.cast_of_nat,
-    exact set_like.has_graded_one.nat_cast_mem _ _, },
+    exact set_like.nat_cast_mem_graded _ _, },
   { rw int.cast_neg_succ_of_nat,
-    exact neg_mem (set_like.has_graded_one.nat_cast_mem _ _), },
+    exact neg_mem (set_like.nat_cast_mem_graded _ _), },
 end
 
 section direct_sum
@@ -107,7 +107,7 @@ instance gsemiring [add_monoid ι] [semiring R] [set_like σ R] [add_submonoid_c
   zero_mul := λ i j _, subtype.ext (zero_mul _),
   mul_add := λ i j _ _ _, subtype.ext (mul_add _ _ _),
   add_mul := λ i j _ _ _, subtype.ext (add_mul _ _ _),
-  nat_cast := λ n, ⟨n, set_like.has_graded_one.nat_cast_mem _ _⟩,
+  nat_cast := λ n, ⟨n, set_like.nat_cast_mem_graded _ _⟩,
   nat_cast_zero := subtype.ext nat.cast_zero,
   nat_cast_succ := λ n, subtype.ext (nat.cast_succ n),
   ..set_like.gmonoid A }
@@ -123,7 +123,7 @@ instance gcomm_semiring [add_comm_monoid ι] [comm_semiring R] [set_like σ R]
 instance gring [add_monoid ι] [ring R] [set_like σ R] [add_subgroup_class σ R]
   (A : ι → σ) [set_like.graded_monoid A] :
   direct_sum.gring (λ i, A i) :=
-{ int_cast := λ z, ⟨z, set_like.has_graded_one.int_cast_mem _ _⟩,
+{ int_cast := λ z, ⟨z, set_like.int_cast_mem_graded _ _⟩,
   int_cast_of_nat := λ n, subtype.ext $ int.cast_of_nat _,
   int_cast_neg_succ_of_nat := λ n, subtype.ext $ int.cast_neg_succ_of_nat n,
   ..set_like.gsemiring A }
@@ -170,7 +170,7 @@ instance galgebra [add_monoid ι]
   (A : ι → submodule S R) [set_like.graded_monoid A] :
   direct_sum.galgebra S (λ i, A i) :=
 { to_fun := ((algebra.linear_map S R).cod_restrict (A 0) $
-    set_like.has_graded_one.algebra_map_mem A).to_add_monoid_hom,
+    set_like.algebra_map_mem_graded A).to_add_monoid_hom,
   map_one := subtype.ext $ by exact (algebra_map S R).map_one,
   map_mul := λ x y, sigma.subtype_ext (add_zero 0).symm $ (algebra_map S R).map_mul _ _,
   commutes := λ r ⟨i, xi⟩,

src/algebra/graded_monoid.lean

@@ -64,16 +64,24 @@ provides the `Prop` typeclasses:
 * `set_like.has_graded_mul A` (which provides the obvious `graded_monoid.ghas_mul A` instance)
 * `set_like.graded_monoid A` (which provides the obvious `graded_monoid.gmonoid A` and
   `graded_monoid.gcomm_monoid A` instances)
-* `set_like.is_homogeneous A` (which says that `a` is homogeneous iff `a ∈ A i` for some `i : ι`)
+
+which respectively provide the API lemmas
+
+* `set_like.one_mem_graded`
+* `set_like.mul_mem_graded`
+* `set_like.pow_mem_graded`, `set_like.list_prod_map_mem_graded`
 
 Strictly this last class is unecessary as it has no fields not present in its parents, but it is
-included for convenience. Note that there is no need for `graded_ring` or similar, as all the
-information it would contain is already supplied by `graded_monoid` when `A` is a collection
-of additively-closed set_like objects such as `submodule`s. These constructions are explored in
-`algebra.direct_sum.internal`.
+included for convenience. Note that there is no need for `set_like.graded_ring` or similar, as all
+the information it would contain is already supplied by `graded_monoid` when `A` is a collection
+of objects satisfying `add_submonoid_class` such as `submodule`s. These constructions are explored
+in `algebra.direct_sum.internal`.
 
-This file also contains the definition of `set_like.homogeneous_submonoid A`, which is, as the name
-suggests, the submonoid consisting of all the homogeneous elements.
+This file also defines:
+
+* `set_like.is_homogeneous A` (which says that `a` is homogeneous iff `a ∈ A i` for some `i : ι`)
+* `set_like.homogeneous_submonoid A`, which is, as the name suggests, the submonoid consisting of
+  all the homogeneous elements.
 
 ## tags
 
@@ -411,9 +419,12 @@ class set_like.has_graded_one {S : Type*} [set_like S R] [has_one R] [has_zero 
   (A : ι → S) : Prop :=
 (one_mem : (1 : R) ∈ A 0)
 
+lemma set_like.one_mem_graded {S : Type*} [set_like S R] [has_one R] [has_zero ι] (A : ι → S)
+  [set_like.has_graded_one A] : (1 : R) ∈ A 0 := set_like.has_graded_one.one_mem
+
 instance set_like.ghas_one {S : Type*} [set_like S R] [has_one R] [has_zero ι] (A : ι → S)
   [set_like.has_graded_one A] : graded_monoid.ghas_one (λ i, A i) :=
-{ one := ⟨1, set_like.has_graded_one.one_mem⟩ }
+{ one := ⟨1, set_like.one_mem_graded _⟩ }
 
 @[simp] lemma set_like.coe_ghas_one {S : Type*} [set_like S R] [has_one R] [has_zero ι] (A : ι → S)
   [set_like.has_graded_one A] : ↑(@graded_monoid.ghas_one.one _ (λ i, A i) _ _) = (1 : R) := rfl
@@ -423,10 +434,15 @@ class set_like.has_graded_mul {S : Type*} [set_like S R] [has_mul R] [has_add ι
   (A : ι → S) : Prop :=
 (mul_mem : ∀ ⦃i j⦄ {gi gj}, gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j))
 
+lemma set_like.mul_mem_graded {S : Type*} [set_like S R] [has_mul R] [has_add ι] {A : ι → S}
+  [set_like.has_graded_mul A] ⦃i j⦄ {gi gj} (hi : gi ∈ A i) (hj : gj ∈ A j) :
+  gi * gj ∈ A (i + j) :=
+set_like.has_graded_mul.mul_mem hi hj
+
 instance set_like.ghas_mul {S : Type*} [set_like S R] [has_mul R] [has_add ι] (A : ι → S)
   [set_like.has_graded_mul A] :
   graded_monoid.ghas_mul (λ i, A i) :=
-{ mul := λ i j a b, ⟨(a * b : R), set_like.has_graded_mul.mul_mem a.prop b.prop⟩ }
+{ mul := λ i j a b, ⟨(a * b : R), set_like.mul_mem_graded a.prop b.prop⟩ }
 
 @[simp] lemma set_like.coe_ghas_mul {S : Type*} [set_like S R] [has_mul R] [has_add ι] (A : ι → S)
   [set_like.has_graded_mul A] {i j : ι} (x : A i) (y : A j) :
@@ -436,35 +452,37 @@ instance set_like.ghas_mul {S : Type*} [set_like S R] [has_mul R] [has_add ι] (
 class set_like.graded_monoid {S : Type*} [set_like S R] [monoid R] [add_monoid ι]
   (A : ι → S) extends set_like.has_graded_one A, set_like.has_graded_mul A : Prop
 
-namespace set_like.graded_monoid
+namespace set_like
 variables {S : Type*} [set_like S R] [monoid R] [add_monoid ι]
 variables {A : ι → S} [set_like.graded_monoid A]
 
-lemma pow_mem (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) : r ^ n ∈ A (n • i) :=
+lemma pow_mem_graded (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) : r ^ n ∈ A (n • i) :=
 begin
   induction n,
-  { rw [pow_zero, zero_nsmul], exact one_mem },
-  { rw [pow_succ', succ_nsmul'], exact mul_mem n_ih h },
+  { rw [pow_zero, zero_nsmul], exact one_mem_graded _ },
+  { rw [pow_succ', succ_nsmul'], exact mul_mem_graded n_ih h },
 end
 
-lemma list_prod_map_mem {ι'} (l : list ι') (i : ι' → ι) (r : ι' → R) (h : ∀ j ∈ l, r j ∈ A (i j)) :
+lemma list_prod_map_mem_graded {ι'} (l : list ι') (i : ι' → ι) (r : ι' → R)
+  (h : ∀ j ∈ l, r j ∈ A (i j)) :
   (l.map r).prod ∈ A (l.map i).sum :=
 begin
   induction l,
   { rw [list.map_nil, list.map_nil, list.prod_nil, list.sum_nil],
-    exact one_mem },
+    exact one_mem_graded _ },
   { rw [list.map_cons, list.map_cons, list.prod_cons, list.sum_cons],
-    exact mul_mem (h _ $ list.mem_cons_self _ _) (l_ih $ λ j hj, h _ $ list.mem_cons_of_mem _ hj) },
+    exact mul_mem_graded
+      (h _ $ list.mem_cons_self _ _) (l_ih $ λ j hj, h _ $ list.mem_cons_of_mem _ hj) },
 end
 
-lemma list_prod_of_fn_mem {n} (i : fin n → ι) (r : fin n → R) (h : ∀ j, r j ∈ A (i j)) :
+lemma list_prod_of_fn_mem_graded {n} (i : fin n → ι) (r : fin n → R) (h : ∀ j, r j ∈ A (i j)) :
   (list.of_fn r).prod ∈ A (list.of_fn i).sum :=
 begin
   rw [list.of_fn_eq_map, list.of_fn_eq_map],
-  exact list_prod_map_mem _ _ _ (λ _ _, h _),
+  exact list_prod_map_mem_graded _ _ _ (λ _ _, h _),
 end
 
-end set_like.graded_monoid
+end set_like
 
 /-- Build a `gmonoid` instance for a collection of subobjects. -/
 instance set_like.gmonoid {S : Type*} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S)
@@ -474,7 +492,7 @@ instance set_like.gmonoid {S : Type*} [set_like S R] [monoid R] [add_monoid ι]
   mul_one := λ ⟨i, a, h⟩, sigma.subtype_ext (add_zero _) (mul_one _),
   mul_assoc := λ ⟨i, a, ha⟩ ⟨j, b, hb⟩ ⟨k, c, hc⟩,
     sigma.subtype_ext (add_assoc _ _ _) (mul_assoc _ _ _),
-  gnpow := λ n i a, ⟨a ^ n, set_like.graded_monoid.pow_mem n a.prop⟩,
+  gnpow := λ n i a, ⟨a ^ n, set_like.pow_mem_graded n a.prop⟩,
   gnpow_zero' := λ n, sigma.subtype_ext (zero_nsmul _) (pow_zero _),
   gnpow_succ' := λ n a, sigma.subtype_ext (succ_nsmul _ _) (pow_succ _ _),
   ..set_like.ghas_one A,
@@ -513,7 +531,7 @@ lemma set_like.list_dprod_eq (A : ι → S) [set_like.graded_monoid A]
   (fι : α → ι) (fA : Π a, A (fι a)) (l : list α) :
   (l.dprod fι fA : (λ i, ↥(A i)) _) =
     ⟨list.prod (l.map (λ a, fA a)), (l.dprod_index_eq_map_sum fι).symm ▸
-      list_prod_map_mem l _ _ (λ i hi, (fA i).prop)⟩ :=
+      list_prod_map_mem_graded l _ _ (λ i hi, (fA i).prop)⟩ :=
 subtype.ext $ set_like.coe_list_dprod _ _ _ _
 
 end dprod
@@ -533,12 +551,12 @@ def set_like.is_homogeneous (A : ι → S) (a : R) : Prop := ∃ i, a ∈ A i
 
 lemma set_like.is_homogeneous_one [has_zero ι] [has_one R]
   (A : ι → S) [set_like.has_graded_one A] : set_like.is_homogeneous A (1 : R) :=
-⟨0, set_like.has_graded_one.one_mem⟩
+⟨0, set_like.one_mem_graded _⟩
 
 lemma set_like.is_homogeneous.mul [has_add ι] [has_mul R] {A : ι → S}
   [set_like.has_graded_mul A] {a b : R} :
   set_like.is_homogeneous A a → set_like.is_homogeneous A b → set_like.is_homogeneous A (a * b)
-| ⟨i, hi⟩ ⟨j, hj⟩ := ⟨i + j, set_like.has_graded_mul.mul_mem hi hj⟩
+| ⟨i, hi⟩ ⟨j, hj⟩ := ⟨i + j, set_like.mul_mem_graded hi hj⟩
 
 /-- When `A` is a `set_like.graded_monoid A`, then the homogeneous elements forms a submonoid. -/
 def set_like.homogeneous_submonoid [add_monoid ι] [monoid R]

src/algebraic_geometry/projective_spectrum/scheme.lean

@@ -97,20 +97,20 @@ The degree zero part of the localized ring `Aₓ` is the subring of elements of
 that `a` and `x^n` have the same degree.
 -/
 def degree_zero_part {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) : subring (away f) :=
-{ carrier := { y | ∃ (n : ℕ) (a : 𝒜 (m * n)), y = mk a.1 ⟨f^n, ⟨n, rfl⟩⟩ },
+{ carrier := { y | ∃ (n : ℕ) (a : 𝒜 (m * n)), y = mk a ⟨f^n, ⟨n, rfl⟩⟩ },
   mul_mem' := λ _ _ ⟨n, ⟨a, h⟩⟩ ⟨n', ⟨b, h'⟩⟩, h.symm ▸ h'.symm ▸
     ⟨n+n', ⟨⟨a.1 * b.1, (mul_add m n n').symm ▸ mul_mem a.2 b.2⟩,
     by {rw mk_mul, congr' 1, simp only [pow_add], refl }⟩⟩,
   one_mem' := ⟨0, ⟨1, (mul_zero m).symm ▸ one_mem⟩,
-    by { symmetry, convert ← mk_self 1, simp only [pow_zero], refl, }⟩,
+    by { symmetry, rw subtype.coe_mk, convert ← mk_self 1, simp only [pow_zero], refl, }⟩,
   add_mem' := λ _ _ ⟨n, ⟨a, h⟩⟩ ⟨n', ⟨b, h'⟩⟩, h.symm ▸ h'.symm ▸
     ⟨n+n', ⟨⟨f ^ n * b.1 + f ^ n' * a.1, (mul_add m n n').symm ▸
-      add_mem (mul_mem (by { rw mul_comm, exact set_like.graded_monoid.pow_mem n f_deg }) b.2)
+      add_mem (mul_mem (by { rw mul_comm, exact set_like.pow_mem_graded n f_deg }) b.2)
         begin
           rw add_comm,
           refine mul_mem _ a.2,
           rw mul_comm,
-          exact set_like.graded_monoid.pow_mem _ f_deg
+          exact set_like.pow_mem_graded _ f_deg
         end⟩, begin
           rw add_mk,
           congr' 1,

src/algebraic_geometry/projective_spectrum/structure_sheaf.lean

@@ -143,8 +143,8 @@ begin
   rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, wa⟩,
   rcases hb x with ⟨Vb, mb, ib, jb, ⟨rb, rb_mem⟩, ⟨sb, sb_mem⟩, wb⟩,
   refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, opens.inf_le_left _ _ ≫ ia, ja + jb,
-    ⟨ra * rb, set_like.graded_monoid.mul_mem ra_mem rb_mem⟩,
-    ⟨sa * sb, set_like.graded_monoid.mul_mem sa_mem sb_mem⟩, λ y, ⟨λ h, _, _⟩⟩,
+    ⟨ra * rb, set_like.mul_mem_graded ra_mem rb_mem⟩,
+    ⟨sa * sb, set_like.mul_mem_graded sa_mem sb_mem⟩, λ y, ⟨λ h, _, _⟩⟩,
   { cases (y : projective_spectrum.Top 𝒜).is_prime.mem_or_mem h with h h,
     { choose nin hy using wa ⟨y, (opens.inf_le_left Va Vb y).2⟩, exact nin h },
     { choose nin hy using wb ⟨y, (opens.inf_le_right Va Vb y).2⟩, exact nin h }, },

src/linear_algebra/clifford_algebra/grading.lean

@@ -146,7 +146,7 @@ lemma even_odd_induction (n : zmod 2) {P : Π x, x ∈ even_odd Q n → Prop}
     P v (submodule.mem_supr_of_mem ⟨n.val, n.nat_cast_zmod_val⟩ h))
   (hadd : ∀ {x y hx hy}, P x hx → P y hy → P (x + y) (submodule.add_mem _ hx hy))
   (hιι_mul : ∀ m₁ m₂ {x hx}, P x hx → P (ι Q m₁ * ι Q m₂ * x)
-    (zero_add n ▸ set_like.graded_monoid.mul_mem (ι_mul_ι_mem_even_odd_zero Q m₁ m₂) hx))
+    (zero_add n ▸ set_like.mul_mem_graded (ι_mul_ι_mem_even_odd_zero Q m₁ m₂) hx))
   (x : clifford_algebra Q) (hx : x ∈ even_odd Q n) : P x hx :=
 begin
   apply submodule.supr_induction' _ _ (hr 0 (submodule.zero_mem _)) @hadd,
@@ -182,10 +182,10 @@ end
 scalars, closed under addition, and under left-multiplication by a pair of vectors. -/
 @[elab_as_eliminator]
 lemma even_induction  {P : Π x, x ∈ even_odd Q 0 → Prop}
-  (hr : ∀ r : R, P (algebra_map _ _ r) (set_like.has_graded_one.algebra_map_mem _ _))
+  (hr : ∀ r : R, P (algebra_map _ _ r) (set_like.algebra_map_mem_graded _ _))
   (hadd : ∀ {x y hx hy}, P x hx → P y hy → P (x + y) (submodule.add_mem _ hx hy))
   (hιι_mul : ∀ m₁ m₂ {x hx}, P x hx → P (ι Q m₁ * ι Q m₂ * x)
-    (zero_add 0 ▸ set_like.graded_monoid.mul_mem (ι_mul_ι_mem_even_odd_zero Q m₁ m₂) hx))
+    (zero_add 0 ▸ set_like.mul_mem_graded (ι_mul_ι_mem_even_odd_zero Q m₁ m₂) hx))
   (x : clifford_algebra Q) (hx : x ∈ even_odd Q 0) : P x hx :=
 begin
   refine even_odd_induction Q 0 (λ rx, _) @hadd hιι_mul x hx,
@@ -201,7 +201,7 @@ lemma odd_induction {P : Π x, x ∈ even_odd Q 1 → Prop}
   (hι : ∀ v, P (ι Q v) (ι_mem_even_odd_one _ _))
   (hadd : ∀ {x y hx hy}, P x hx → P y hy → P (x + y) (submodule.add_mem _ hx hy))
   (hιι_mul : ∀ m₁ m₂ {x hx}, P x hx → P (ι Q m₁ * ι Q m₂ * x)
-    (zero_add (1 : zmod 2) ▸ set_like.graded_monoid.mul_mem (ι_mul_ι_mem_even_odd_zero Q m₁ m₂) hx))
+    (zero_add (1 : zmod 2) ▸ set_like.mul_mem_graded (ι_mul_ι_mem_even_odd_zero Q m₁ m₂) hx))
   (x : clifford_algebra Q) (hx : x ∈ even_odd Q 1) : P x hx :=
 begin
   refine even_odd_induction Q 1 (λ ιv, _) @hadd hιι_mul x hx,

src/ring_theory/graded_algebra/homogeneous_localization.lean

@@ -167,10 +167,12 @@ instance : comm_monoid (num_denom_same_deg 𝒜 x) :=
   mul_comm := λ c1 c2, ext _ (add_comm _ _) (mul_comm _ _) (mul_comm _ _) }
 
 instance : has_pow (num_denom_same_deg 𝒜 x) ℕ :=
-{ pow := λ c n, ⟨n • c.deg, ⟨c.num ^ n, pow_mem n c.num.2⟩, ⟨c.denom ^ n, pow_mem n c.denom.2⟩,
+{ pow := λ c n, ⟨n • c.deg,
+    @graded_monoid.gmonoid.gnpow _ (λ i, ↥(𝒜 i)) _ _ n _ c.num,
+    @graded_monoid.gmonoid.gnpow _ (λ i, ↥(𝒜 i)) _ _ n _ c.denom,
     begin
       cases n,
-      { simp only [pow_zero],
+      { simp only [graded_monoid.gmonoid.gnpow, subtype.coe_mk, pow_zero],
         exact λ r, (infer_instance : x.is_prime).ne_top $ (ideal.eq_top_iff_one _).mpr r, },
       { exact λ r, c.denom_not_mem $
           ((infer_instance : x.is_prime).pow_mem_iff_mem n.succ (nat.zero_lt_succ _)).mp r }