refactor(algebra/*): add new mul_one_class and add_zero_class for…

… non-associative monoids (#6865)

This extracts a base class from `monoid M`, `mul_one_class M`, that drops the associativity assumption.

It goes on to weaken `monoid_hom` and `submonoid` to require `mul_one_class M` instead of `monoid M`, along with weakening the typeclass requirements for other primitive constructions like `monoid_hom.fst`.

Instances of the new classes are provided on `pi`, `prod`, `finsupp`, `(add_)submonoid`, and `(add_)monoid_algebra`.

This is by no means an exhaustive relaxation across mathlib, but it aims to broadly cover the foundations.

src/algebra/big_operators/basic.lean

@@ -136,13 +136,13 @@ lemma ring_hom.map_sum [semiring β] [semiring γ]
 g.to_add_monoid_hom.map_sum f s
 
 @[to_additive]
-lemma monoid_hom.coe_prod [monoid β] [comm_monoid γ] (f : α → β →* γ) (s : finset α) :
+lemma monoid_hom.coe_prod [mul_one_class β] [comm_monoid γ] (f : α → β →* γ) (s : finset α) :
   ⇑(∏ x in s, f x) = ∏ x in s, f x :=
 (monoid_hom.coe_fn β γ).map_prod _ _
 
 @[simp, to_additive]
-lemma monoid_hom.finset_prod_apply [monoid β] [comm_monoid γ] (f : α → β →* γ) (s : finset α)
-  (b : β) : (∏ x in s, f x) b = ∏ x in s, f x b :=
+lemma monoid_hom.finset_prod_apply [mul_one_class β] [comm_monoid γ] (f : α → β →* γ)
+  (s : finset α) (b : β) : (∏ x in s, f x) b = ∏ x in s, f x b :=
 (monoid_hom.eval b).map_prod _ _
 
 variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}

src/algebra/category/Mon/adjunctions.lean

@@ -23,6 +23,10 @@ universe u
 
 open category_theory
 
+-- typeclass inference cannot equate `with_one.monoid.to_mul_one_class` with
+-- `with_one.mul_one_class` without this.
+local attribute [semireducible] with_one with_zero
+
 /-- The functor of adjoining a neutral element `one` to a semigroup.
  -/
 @[to_additive "The functor of adjoining a neutral element `zero` to a semigroup", simps]

src/algebra/category/Mon/basic.lean

@@ -31,9 +31,18 @@ add_decl_doc AddMon
 
 namespace Mon
 
+/-- `monoid_hom` doesn't actually assume associativity. This alias is needed to make the category
+theory machinery work. -/
+@[to_additive "`add_monoid_hom` doesn't actually assume associativity. This alias is needed to make
+the category theory machinery work."]
+abbreviation assoc_monoid_hom (M N : Type*) [monoid M] [monoid N] := monoid_hom M N
+
 @[to_additive]
-instance bundled_hom : bundled_hom @monoid_hom :=
-⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩
+instance bundled_hom : bundled_hom assoc_monoid_hom :=
+⟨λ M N [monoid M] [monoid N], by exactI @monoid_hom.to_fun M N _ _,
+ λ M [monoid M], by exactI @monoid_hom.id M _,
+ λ M N P [monoid M] [monoid N] [monoid P], by exactI @monoid_hom.comp M N P _ _ _,
+ λ M N [monoid M] [monoid N], by exactI @monoid_hom.coe_inj M N _ _⟩
 
 attribute [derive [has_coe_to_sort, large_category, concrete_category]] Mon AddMon
 

src/algebra/group/defs.lean

@@ -182,36 +182,57 @@ theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c :=
 
 end right_cancel_semigroup
 
-/-- A `monoid` is a `semigroup` with an element `1` such that `1 * a = a * 1 = a`. -/
-@[ancestor semigroup has_one]
-class monoid (M : Type u) extends semigroup M, has_one M :=
-(one_mul : ∀ a : M, 1 * a = a) (mul_one : ∀ a : M, a * 1 = a)
-/-- An `add_monoid` is an `add_semigroup` with an element `0` such that `0 + a = a + 0 = a`. -/
-@[ancestor add_semigroup has_zero]
-class add_monoid (M : Type u) extends add_semigroup M, has_zero M :=
-(zero_add : ∀ a : M, 0 + a = a) (add_zero : ∀ a : M, a + 0 = a)
-attribute [to_additive] monoid
+/-- Typeclass for expressing that a type `M` with multiplication and a one satisfies
+`1 * a = a` and `a * 1 = a` for all `a : M`. -/
+@[ancestor has_one has_mul]
+class mul_one_class (M : Type u) extends has_one M, has_mul M :=
+(one_mul : ∀ (a : M), 1 * a = a)
+(mul_one : ∀ (a : M), a * 1 = a)
 
-section monoid
-variables {M : Type u} [monoid M]
+/-- Typeclass for expressing that a type `M` with addition and a zero satisfies
+`0 + a = a` and `a + 0 = a` for all `a : M`. -/
+@[ancestor has_zero has_add]
+class add_zero_class (M : Type u) extends has_zero M, has_add M :=
+(zero_add : ∀ (a : M), 0 + a = a)
+(add_zero : ∀ (a : M), a + 0 = a)
+
+attribute [to_additive] mul_one_class
+
+section mul_one_class
+variables {M : Type u} [mul_one_class M]
 
 @[ematch, simp, to_additive]
 lemma one_mul : ∀ a : M, 1 * a = a :=
-monoid.one_mul
+mul_one_class.one_mul
 
 @[ematch, simp, to_additive]
 lemma mul_one : ∀ a : M, a * 1 = a :=
-monoid.mul_one
+mul_one_class.mul_one
 
 attribute [ematch] add_zero zero_add -- TODO(Mario): Make to_additive transfer this
 
 @[to_additive]
-instance monoid_to_is_left_id : is_left_id M (*) 1 :=
-⟨ monoid.one_mul ⟩
+instance mul_one_class.to_is_left_id : is_left_id M (*) 1 :=
+⟨ mul_one_class.one_mul ⟩
 
 @[to_additive]
-instance monoid_to_is_right_id : is_right_id M (*) 1 :=
-⟨ monoid.mul_one ⟩
+instance mul_one_class.to_is_right_id : is_right_id M (*) 1 :=
+⟨ mul_one_class.mul_one ⟩
+
+end mul_one_class
+
+/-- A `monoid` is a `semigroup` with an element `1` such that `1 * a = a * 1 = a`. -/
+@[ancestor semigroup mul_one_class]
+class monoid (M : Type u) extends semigroup M, mul_one_class M
+
+/-- An `add_monoid` is an `add_semigroup` with an element `0` such that `0 + a = a + 0 = a`. -/
+@[ancestor add_semigroup add_zero_class]
+class add_monoid (M : Type u) extends add_semigroup M, add_zero_class M
+
+attribute [to_additive] monoid
+
+section monoid
+variables {M : Type u} [monoid M]
 
 @[to_additive]
 lemma left_inv_eq_right_inv {a b c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c :=