feat(algebra/group_with_zero): add semigroup_with_zero (#7346)

Split from #6786. By putting the new typeclass _before_ `mul_zero_one_class`, it doesn't need any annotations on `zero_ne_one` as the original PR did.

src/algebra/group/pi.lean

@@ -25,6 +25,10 @@ namespace pi
 instance semigroup [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
 by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
 
+instance semigroup_with_zero [∀ i, semigroup_with_zero $ f i] :
+  semigroup_with_zero (Π i : I, f i) :=
+by refine_struct { zero := (0 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field
+
 @[to_additive]
 instance comm_semigroup [∀ i, comm_semigroup $ f i] : comm_semigroup (Π i : I, f i) :=
 by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field

src/algebra/group/prod.lean

@@ -85,6 +85,9 @@ instance [semigroup M] [semigroup N] : semigroup (M × N) :=
 { mul_assoc := assume a b c, mk.inj_iff.mpr ⟨mul_assoc _ _ _, mul_assoc _ _ _⟩,
   .. prod.has_mul }
 
+instance [semigroup_with_zero M] [semigroup_with_zero N] : semigroup_with_zero (M × N) :=
+{ .. prod.mul_zero_class, .. prod.semigroup }
+
 @[to_additive]
 instance [mul_one_class M] [mul_one_class N] : mul_one_class (M × N) :=
 { one_mul := assume a, prod.rec_on a $ λa b, mk.inj_iff.mpr ⟨one_mul _, one_mul _⟩,

src/algebra/group/with_one.lean

@@ -189,7 +189,7 @@ instance [has_mul α] : mul_zero_class (with_zero α) :=
 @[simp] lemma mul_zero {α : Type u} [has_mul α]
   (a : with_zero α) : a * 0 = 0 := by cases a; refl
 
-instance [semigroup α] : semigroup (with_zero α) :=
+instance [semigroup α] : semigroup_with_zero (with_zero α) :=
 { mul_assoc := λ a b c, match a, b, c with
     | none,   _,      _      := rfl
     | some a, none,   _      := rfl
@@ -204,7 +204,7 @@ instance [comm_semigroup α] : comm_semigroup (with_zero α) :=
     | some a, none   := rfl
     | some a, some b := congr_arg some (mul_comm _ _)
     end,
-  ..with_zero.semigroup }
+  ..with_zero.semigroup_with_zero }
 
 instance [mul_one_class α] : mul_zero_one_class (with_zero α) :=
 { one_mul := λ a, match a with
@@ -220,8 +220,7 @@ instance [mul_one_class α] : mul_zero_one_class (with_zero α) :=
 
 instance [monoid α] : monoid_with_zero (with_zero α) :=
 { ..with_zero.mul_zero_one_class,
-  ..with_zero.has_one,
-  ..with_zero.semigroup }
+  ..with_zero.semigroup_with_zero }
 
 instance [comm_monoid α] : comm_monoid_with_zero (with_zero α) :=
 { ..with_zero.monoid_with_zero, ..with_zero.comm_semigroup }

src/algebra/group_with_zero/basic.lean

@@ -222,6 +222,28 @@ protected lemma pullback_nonzero [has_zero M₀'] [has_one M₀']
 
 end
 
+section semigroup_with_zero
+
+/-- Pullback a `semigroup_with_zero` class along an injective function. -/
+protected def function.injective.semigroup_with_zero
+  [has_zero M₀'] [has_mul M₀'] [semigroup_with_zero M₀] (f : M₀' → M₀) (hf : injective f)
+  (zero : f 0 = 0) (mul : ∀ x y, f (x * y) = f x * f y) :
+  semigroup_with_zero M₀' :=
+{ .. hf.mul_zero_class f zero mul,
+  .. ‹has_zero M₀'›,
+  .. hf.semigroup f mul }
+
+/-- Pushforward a `semigroup_with_zero` class along an surjective function. -/
+protected def function.surjective.semigroup_with_zero
+  [semigroup_with_zero M₀] [has_zero M₀'] [has_mul M₀'] (f : M₀ → M₀') (hf : surjective f)
+  (zero : f 0 = 0) (mul : ∀ x y, f (x * y) = f x * f y) :
+  semigroup_with_zero M₀' :=
+{ .. hf.mul_zero_class f zero mul,
+  .. ‹has_zero M₀'›,
+  .. hf.semigroup f mul }
+
+end semigroup_with_zero
+
 section monoid_with_zero
 
 /-- Pullback a `monoid_with_zero` class along an injective function. -/

src/algebra/group_with_zero/defs.lean

@@ -54,13 +54,24 @@ class no_zero_divisors (M₀ : Type*) [has_mul M₀] [has_zero M₀] : Prop :=
 
 export no_zero_divisors (eq_zero_or_eq_zero_of_mul_eq_zero)
 
+/-- A type `S₀` is a "semigroup with zero” if it is a semigroup with zero element, and `0` is left
+and right absorbing. -/
+@[protect_proj] class semigroup_with_zero (S₀ : Type*) extends semigroup S₀, mul_zero_class S₀.
+
+/- By defining this _after_ `semigroup_with_zero`, we ensure that searches for `mul_zero_class` find
+this class first. -/
 /-- A typeclass for non-associative monoids with zero elements. -/
 @[protect_proj] class mul_zero_one_class (M₀ : Type*) extends mul_one_class M₀, mul_zero_class M₀.
 
-/-- A type `M` is a “monoid with zero” if it is a monoid with zero element, and `0` is left
+/-- A type `M₀` is a “monoid with zero” if it is a monoid with zero element, and `0` is left
 and right absorbing. -/
 @[protect_proj] class monoid_with_zero (M₀ : Type*) extends monoid M₀, mul_zero_one_class M₀.
 
+@[priority 100] -- see Note [lower instance priority]
+instance monoid_with_zero.to_semigroup_with_zero (M₀ : Type*) [monoid_with_zero M₀] :
+  semigroup_with_zero M₀ :=
+{ ..‹monoid_with_zero M₀› }
+
 /-- A type `M` is a `cancel_monoid_with_zero` if it is a monoid with zero element, `0` is left
 and right absorbing, and left/right multiplication by a non-zero element is injective. -/
 @[protect_proj] class cancel_monoid_with_zero (M₀ : Type*) extends monoid_with_zero M₀ :=

src/algebra/monoid_algebra.lean

@@ -97,11 +97,12 @@ section semigroup
 
 variables [semiring k] [semigroup G]
 
-instance : semigroup (monoid_algebra k G) :=
+instance : semigroup_with_zero (monoid_algebra k G) :=
 { mul       := (*),
   mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index,
     sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
-    add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add],}
+    add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add],
+  .. monoid_algebra.mul_zero_class }
 
 end semigroup
 
@@ -174,7 +175,7 @@ instance : semiring (monoid_algebra k G) :=
   zero      := 0,
   add       := (+),
   .. monoid_algebra.mul_zero_one_class,
-  .. monoid_algebra.semigroup,
+  .. monoid_algebra.semigroup_with_zero,
   .. monoid_algebra.distrib,
   .. finsupp.add_comm_monoid }
 
@@ -682,11 +683,12 @@ section semigroup
 
 variables [semiring k] [add_semigroup G]
 
-instance : semigroup (add_monoid_algebra k G) :=
+instance : semigroup_with_zero (add_monoid_algebra k G) :=
 { mul       := (*),
   mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index,
     sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
-    add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add] }
+    add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add],
+  .. add_monoid_algebra.mul_zero_class }
 
 end semigroup
 
@@ -747,7 +749,7 @@ instance : semiring (add_monoid_algebra k G) :=
   nsmul_zero' := by { intros, ext, simp [-nsmul_eq_mul, add_smul] },
   nsmul_succ' := by { intros, ext, simp [-nsmul_eq_mul, nat.succ_eq_one_add, add_smul] },
   .. add_monoid_algebra.mul_zero_one_class,
-  .. add_monoid_algebra.semigroup,
+  .. add_monoid_algebra.semigroup_with_zero,
   .. add_monoid_algebra.distrib,
   .. finsupp.add_comm_monoid }
 

src/algebra/ordered_monoid.lean

@@ -554,7 +554,7 @@ local attribute [reducible] with_zero
 
 instance [add_semigroup α] : add_semigroup (with_top α) :=
 { add := (+),
-  ..@additive.add_semigroup _ $ @with_zero.semigroup (multiplicative α) _ }
+  ..(by apply_instance : add_semigroup (additive (with_zero (multiplicative α)))) }
 
 @[norm_cast] lemma coe_add [has_add α] {a b : α} : ((a + b : α) : with_top α) = a + b := rfl
 

src/algebra/pointwise.lean

@@ -336,6 +336,9 @@ instance set_semiring.distrib [has_mul α] : distrib (set_semiring α) :=
 instance set_semiring.mul_zero_one_class [mul_one_class α] : mul_zero_one_class (set_semiring α) :=
 { ..set_semiring.mul_zero_class, ..set.mul_one_class }
 
+instance set_semiring.semigroup_with_zero [semigroup α] : semigroup_with_zero (set_semiring α) :=
+{ ..set_semiring.mul_zero_class, ..set.semigroup }
+
 instance set_semiring.semiring [monoid α] : semiring (set_semiring α) :=
 { ..set_semiring.add_comm_monoid,
   ..set_semiring.distrib,

src/data/equiv/transfer_instance.lean

@@ -124,6 +124,11 @@ protected def semigroup [semigroup β] : semigroup α :=
 let mul := e.has_mul in
 by resetI; apply e.injective.semigroup _; intros; exact e.apply_symm_apply _
 
+/-- Transfer `semigroup_with_zero` across an `equiv` -/
+protected def semigroup_with_zero [semigroup_with_zero β] : semigroup_with_zero α :=
+let mul := e.has_mul, zero := e.has_zero in
+by resetI; apply e.injective.semigroup_with_zero _; intros; exact e.apply_symm_apply _
+
 /-- Transfer `comm_semigroup` across an `equiv` -/
 @[to_additive "Transfer `add_comm_semigroup` across an `equiv`"]
 protected def comm_semigroup [comm_semigroup β] : comm_semigroup α :=

src/data/finsupp/pointwise.lean

@@ -55,9 +55,10 @@ instance : mul_zero_class (α →₀ β) :=
 
 end
 
-instance [semiring β] : semigroup (α →₀ β) :=
+instance [semigroup_with_zero β] : semigroup_with_zero (α →₀ β) :=
 { mul       := (*),
-  mul_assoc := λ f g h, by { ext, simp only [mul_apply, mul_assoc], }, }
+  mul_assoc := λ f g h, by { ext, simp only [mul_apply, mul_assoc], },
+  ..(infer_instance : mul_zero_class (α →₀ β)) }
 
 instance [semiring β] : distrib (α →₀ β) :=
 { left_distrib := λ f g h, by { ext, simp only [mul_apply, add_apply, left_distrib] {proj := ff} },

src/topology/locally_constant/algebra.lean

@@ -59,6 +59,10 @@ instance [mul_zero_one_class Y] : mul_zero_one_class (locally_constant X Y) :=
 { mul_assoc := by { intros, ext, simp only [mul_apply, mul_assoc] },
   .. locally_constant.has_mul }
 
+instance [semigroup_with_zero Y] : semigroup_with_zero (locally_constant X Y) :=
+{ .. locally_constant.mul_zero_class,
+  .. locally_constant.semigroup }
+
 @[to_additive] instance [comm_semigroup Y] : comm_semigroup (locally_constant X Y) :=
 { mul_comm := by { intros, ext, simp only [mul_apply, mul_comm] },
   .. locally_constant.semigroup }