chore(*): add a div/sub field to (add_)group(_with_zero) (#…

…5303)

This PR is intended to fix the following kind of diamonds:
Let `foo X` be a type with a `∀ X, has_div (foo X)` instance but no `∀ X, has_inv (foo X)`, e.g. when `foo X` is a `euclidean_domain`. Suppose we also have an instance `∀ X [cromulent X], group_with_zero (foo X)`. Then the `(/)` coming from `group_with_zero_has_div` cannot be defeq to the `(/)` coming from `foo.has_div`.

As a consequence of making the `has_div` instances defeq, we can no longer assume that `(div_eq_mul_inv a b : a / b = a * b⁻¹) = rfl` for all groups. The previous preparation PR #5302 should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/algebra/field.lean

@@ -14,18 +14,13 @@ variables {α : Type u}
 
 /-- A `division_ring` is a `ring` with multiplicative inverses for nonzero elements -/
 @[protect_proj, ancestor ring has_inv]
-class division_ring (α : Type u) extends ring α, has_inv α, nontrivial α :=
+class division_ring (α : Type u) extends ring α, div_inv_monoid α, nontrivial α :=
 (mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
-(inv_mul_cancel : ∀ {a : α}, a ≠ 0 → a⁻¹ * a = 1)
 (inv_zero : (0 : α)⁻¹ = 0)
 
 section division_ring
 variables [division_ring α] {a b : α}
 
-@[priority 100] -- see Note [lower instance priority]
-instance division_ring_has_div : has_div α :=
-⟨λ a b, a * b⁻¹⟩
-
 /-- Every division ring is a `group_with_zero`. -/
 @[priority 100] -- see Note [lower instance priority]
 instance division_ring.to_group_with_zero :
@@ -41,10 +36,7 @@ begin
   { exact ring.inverse_unit (units.mk0 x hx) }
 end
 
-@[field_simps] lemma inv_eq_one_div (a : α) : a⁻¹ = 1 / a := by simp
-
-lemma mul_one_div (a b : α) : a * (1 / b) = a / b :=
-by rw [← inv_eq_one_div, div_eq_mul_inv]
+attribute [field_simps] inv_eq_one_div
 
 local attribute [simp]
   division_def mul_comm mul_assoc
@@ -133,8 +125,7 @@ variable [field α]
 
 @[priority 100] -- see Note [lower instance priority]
 instance field.to_division_ring : division_ring α :=
-{ inv_mul_cancel := λ _ h, by rw [mul_comm, field.mul_inv_cancel h]
-  ..show field α, by apply_instance }
+{ ..show field α, by apply_instance }
 
 /-- Every field is a `comm_group_with_zero`. -/
 @[priority 100] -- see Note [lower instance priority]

src/algebra/group/basic.lean

@@ -133,18 +133,17 @@ end right_cancel_monoid
 
 section div_inv_monoid
 
--- TODO: in a later PR, this `group G` instance will become `div_inv_monoid`
-variables {G : Type u} [group G]
+variables {G : Type u} [div_inv_monoid G]
 
 @[to_additive]
-lemma group.inv_eq_one_div (x : G) :
+lemma inv_eq_one_div (x : G) :
   x⁻¹ = 1 / x :=
-by rw [group.div_eq_mul_inv, one_mul]
+by rw [div_eq_mul_inv, one_mul]
 
 @[to_additive]
-lemma group.mul_one_div (x y : G) :
+lemma mul_one_div (x y : G) :
   x * (1 / y) = x / y :=
-by rw [group.div_eq_mul_inv, one_mul, group.div_eq_mul_inv]
+by rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]
 
 end div_inv_monoid
 
@@ -304,11 +303,11 @@ lemma mul_right_eq_self : a * b = a ↔ b = 1 :=
 
 @[to_additive]
 lemma div_left_injective : function.injective (λ a, a / b) :=
-by simpa only [group.div_eq_mul_inv] using λ a a' h, mul_left_injective (b⁻¹) h
+by simpa only [div_eq_mul_inv] using λ a a' h, mul_left_injective (b⁻¹) h
 
 @[to_additive]
 lemma div_right_injective : function.injective (λ a, b / a) :=
-by simpa only [group.div_eq_mul_inv] using λ a a' h, inv_injective (mul_right_injective b h)
+by simpa only [div_eq_mul_inv] using λ a a' h, inv_injective (mul_right_injective b h)
 
 end group
 

src/algebra/group/defs.lean

@@ -290,16 +290,87 @@ class cancel_comm_monoid (M : Type u) extends left_cancel_comm_monoid M, right_c
 
 end cancel_monoid
 
-/-- A `group` is a `monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`. -/
-@[protect_proj, ancestor monoid has_inv]
-class group (α : Type u) extends monoid α, has_inv α :=
-(mul_left_inv : ∀ a : α, a⁻¹ * a = 1)
-/-- An `add_group` is an `add_monoid` with a unary `-` satisfying `-a + a = 0`. -/
-@[protect_proj, ancestor add_monoid has_neg]
-class add_group (α : Type u) extends add_monoid α, has_neg α :=
-(add_left_neg : ∀ a : α, -a + a = 0)
+/-- `try_refl_tac` solves goals of the form `∀ a b, f a b = g a b`,
+if they hold by definition. -/
+meta def try_refl_tac : tactic unit := `[intros; refl]
+
+/-- A `div_inv_monoid` is a `monoid` with operations `/` and `⁻¹` satisfying
+`div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹`.
+
+This is the immediate common ancestor of `group` and `group_with_zero`,
+in order to deduplicate the name `div_eq_mul_inv`.
+The default for `div` is such that `a / b = a * b⁻¹` holds by definition.
+
+Adding `div` as a field rather than defining `a / b := a * b⁻¹` allows us to
+avoid certain classes of unification failures, for example:
+Let `foo X` be a type with a `∀ X, has_div (foo X)` instance but no
+`∀ X, has_inv (foo X)`, e.g. when `foo X` is a `euclidean_domain`. Suppose we
+also have an instance `∀ X [cromulent X], group_with_zero (foo X)`. Then the
+`(/)` coming from `group_with_zero_has_div` cannot be definitionally equal to
+the `(/)` coming from `foo.has_div`.
+-/
+@[protect_proj, ancestor monoid has_inv has_div]
+class div_inv_monoid (G : Type u) extends monoid G, has_inv G, has_div G :=
+(div := λ a b, a * b⁻¹)
+(div_eq_mul_inv : ∀ a b : G, a / b = a * b⁻¹ . try_refl_tac)
+
+/-- A `sub_neg_monoid` is an `add_monoid` with unary `-` and binary `-` operations
+satisfying `sub_eq_add_neg : ∀ a b, a - b = a + -b`.
+
+The default for `sub` is such that `a - b = a + -b` holds by definition.
+
+Adding `sub` as a field rather than defining `a - b := a + -b` allows us to
+avoid certain classes of unification failures, for example:
+Let `foo X` be a type with a `∀ X, has_sub (foo X)` instance but no
+`∀ X, has_neg (foo X)`. Suppose we also have an instance
+`∀ X [cromulent X], add_group (foo X)`. Then the `(-)` coming from
+`add_group.has_sub` cannot be definitionally equal to the `(-)` coming from
+`foo.has_sub`.
+-/
+@[protect_proj, ancestor add_monoid has_neg has_sub]
+class sub_neg_monoid (G : Type u) extends add_monoid G, has_neg G, has_sub G :=
+(sub := λ a b, a + -b)
+(sub_eq_add_neg : ∀ a b : G, a - b = a + -b . try_refl_tac)
+
+attribute [to_additive sub_neg_monoid] div_inv_monoid
+
+@[to_additive]
+lemma div_eq_mul_inv {G : Type u} [div_inv_monoid G] :
+  ∀ a b : G, a / b = a * b⁻¹ :=
+div_inv_monoid.div_eq_mul_inv
+
+/-- A `group` is a `monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.
+
+There is also a division operation `/` such that `a / b = a * b⁻¹`,
+with a default so that `a / b = a * b⁻¹` holds by definition.
+-/
+@[protect_proj, ancestor div_inv_monoid]
+class group (G : Type u) extends div_inv_monoid G :=
+(mul_left_inv : ∀ a : G, a⁻¹ * a = 1)
+
+/-- An `add_group` is an `add_monoid` with a unary `-` satisfying `-a + a = 0`.
+
+There is also a binary operation `-` such that `a - b = a + -b`,
+with a default so that `a - b = a + -b` holds by definition.
+-/
+@[protect_proj, ancestor sub_neg_monoid]
+class add_group (A : Type u) extends sub_neg_monoid A :=
+(add_left_neg : ∀ a : A, -a + a = 0)
+
 attribute [to_additive] group
 
+/-- Abbreviation for `@div_inv_monoid.to_monoid _ (@group.to_div_inv_monoid _ _)`.
+
+Useful because it corresponds to the fact that `Grp` is a subcategory of `Mon`.
+Not an instance since it duplicates `@div_inv_monoid.to_monoid _ (@group.to_div_inv_monoid _ _)`.
+-/
+@[to_additive "Abbreviation for `@sub_neg_monoid.to_add_monoid _ (@add_group.to_sub_neg_monoid _ _)`.
+
+Useful because it corresponds to the fact that `AddGroup` is a subcategory of `AddMon`.
+Not an instance since it duplicates `@sub_neg_monoid.to_add_monoid _ (@add_group.to_sub_neg_monoid _ _)`."]
+def group.to_monoid (G : Type u) [group G] : monoid G :=
+@div_inv_monoid.to_monoid _ (@group.to_div_inv_monoid _ _)
+
 section group
 variables {G : Type u} [group G] {a b c : G}
 
@@ -340,25 +411,6 @@ instance group.to_cancel_monoid : cancel_monoid G :=
 
 end group
 
--- TODO: in a later PR, this section will be deleted because it is bundled as part of `group`
-section has_div
-
-variables {G : Type u} [group G]
-
-@[priority 100, to_additive]    -- see Note [lower instance priority]
-instance group_has_div : has_div G :=
-⟨λ a b, a * b⁻¹⟩
-
--- TODO: in a later PR, this will be part of the `group` structure
-@[to_additive]
-lemma group.div_eq_mul_inv (a b : G) : a / b = a * b⁻¹ :=
-rfl
-
-lemma sub_eq_add_neg {G : Type u} [add_group G] (a b : G) : a - b = a + -b :=
-add_group.sub_eq_add_neg a b
-
-end has_div
-
 /-- A commutative group is a group with commutative `(*)`. -/
 @[protect_proj, ancestor group comm_monoid]
 class comm_group (G : Type u) extends group G, comm_monoid G

src/algebra/group/hom.lean

@@ -749,10 +749,27 @@ add_decl_doc add_monoid_hom.has_neg
   (f : M →* G) (x : M) :
   f⁻¹ x = (f x)⁻¹ := rfl
 
+/-- If `f` and `g` are monoid homomorphisms to a commutative group, then `f / g` is the homomorphism
+sending `x` to `(f x) / (g x). -/
+@[to_additive]
+instance {M G} [monoid M] [comm_group G] : has_div (M →* G) :=
+⟨λ f g, mk' (λ x, f x / g x) $ λ a b,
+  by simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]⟩
+
+/-- If `f` and `g` are monoid homomorphisms to an additive commutative group, then `f - g`
+is the homomorphism sending `x` to `(f x) - (g x). -/
+add_decl_doc add_monoid_hom.has_sub
+
+@[simp, to_additive] lemma div_apply {M G} {mM : monoid M} {gG : comm_group G}
+  (f g : M →* G) (x : M) :
+  (f / g) x = f x / g x := rfl
+
 /-- If `G` is a commutative group, then `M →* G` a commutative group too. -/
 @[to_additive]
 instance {M G} [monoid M] [comm_group G] : comm_group (M →* G) :=
 { inv := has_inv.inv,
+  div := has_div.div,
+  div_eq_mul_inv := by { intros, ext, apply div_eq_mul_inv },
   mul_left_inv := by intros; ext; apply mul_left_inv,
   ..monoid_hom.comm_monoid }
 
@@ -777,10 +794,6 @@ of_map_add_neg f (by simpa only [sub_eq_add_neg] using hf)
   ⇑(of_map_sub f hf) = f :=
 rfl
 
-@[simp] lemma sub_apply (f g : A →+ B) (a : A) :
-  (f - g) a = f a - g a :=
-rfl
-
 end add_monoid_hom
 
 section commute

src/algebra/group/inj_surj.lean

@@ -126,6 +126,26 @@ protected def group [group M₂] (f : M₁ → M₂) (hf : injective f)
 { mul_left_inv := λ x, hf $ by erw [mul, inv, mul_left_inv, one],
   .. hf.monoid f one mul, ..‹has_inv M₁› }
 
+/-- A type endowed with `1`, `*`, `⁻¹` and `/` is a group,
+if it admits an injective map to a group that preserves these operations.
+
+This version of `injective.group` makes sure that the `/` operation is defeq
+to the specified division operator.
+-/
+@[to_additive
+"A type endowed with `0`, `+` and `-` is an additive group,
+if it admits an injective map to an additive group that preserves these operations.
+
+This version of `injective.add_group` makes sure that the `-` operation is defeq
+to the specified subtraction operator."]
+protected def group_div [has_div M₁] [group M₂] (f : M₁ → M₂) (hf : injective f)
+  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f (x⁻¹) = (f x)⁻¹)
+  (div : ∀ x y, f (x / y) = f x / f y) :
+  group M₁ :=
+{ div_eq_mul_inv := λ x y, hf $ by erw [div, mul, inv, div_eq_mul_inv],
+  mul_left_inv := λ x, hf $ by erw [mul, inv, mul_left_inv, one],
+  .. hf.monoid f one mul, ..‹has_inv M₁›, ..‹has_div M₁› }
+
 /-- A type endowed with `1`, `*` and `⁻¹` is a commutative group,
 if it admits an injective map that preserves `1`, `*` and `⁻¹` to a commutative group. -/
 @[to_additive
@@ -136,6 +156,25 @@ protected def comm_group [comm_group M₂] (f : M₁ → M₂) (hf : injective f
   comm_group M₁ :=
 { .. hf.comm_monoid f one mul, .. hf.group f one mul inv }
 
+/-- A type endowed with `1`, `*`, `⁻¹` and `/` is a commutative group,
+if it admits an injective map to a commutative group that preserves these operations.
+
+This version of `injective.comm_group` makes sure that the `/` operation is defeq
+to the specified division operator.
+-/
+@[to_additive
+"A type endowed with `0`, `+` and `-` is an additive commutative group,
+if it admits an injective map to an additive commutative group that preserves these operations.
+
+This version of `injective.add_comm_group` makes sure that the `-` operation is defeq
+to the specified subtraction operator."]
+protected def comm_group_div [has_div M₁] [comm_group M₂] (f : M₁ → M₂) (hf : injective f)
+  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f (x⁻¹) = (f x)⁻¹)
+  (div : ∀ x y, f (x / y) = f x / f y) :
+comm_group M₁ :=
+{ .. hf.comm_monoid f one mul, .. hf.group_div f one mul inv div }
+
+
 end injective
 
 /-!

src/algebra/group/pi.lean

@@ -41,11 +41,6 @@ instance group [∀ i, group $ f i] : group (Π i : I, f i) :=
 by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, .. };
   tactic.pi_instance_derive_field
 
--- TODO: derive this from `@[to_additive] pi.div_apply`,
--- when the `add_group -> has_sub` diamond is fixed
-@[simp] lemma sub_apply [∀ i, add_group $ f i] (x y : Π i : I, f i) (i : I) :
-  (x - y) i = x i - y i := rfl
-
 @[to_additive]
 instance comm_group [∀ i, comm_group $ f i] : comm_group (Π i : I, f i) :=
 by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, .. };
@@ -70,6 +65,12 @@ instance comm_monoid_with_zero [∀ i, comm_monoid_with_zero $ f i] :
 by refine_struct { zero := (0 : Π i, f i), one := (1 : Π i, f i), mul := (*), .. };
   tactic.pi_instance_derive_field
 
+@[to_additive]
+instance div_inv_monoid [∀ i, div_inv_monoid $ f i] :
+  div_inv_monoid (Π i : I, f i) :=
+{ div_eq_mul_inv := λ x y, funext (λ i, div_eq_mul_inv (x i) (y i)),
+  .. pi.monoid, .. pi.has_div, .. pi.has_inv }
+
 section instance_lemmas
 open function
 

src/algebra/group/prod.lean

@@ -66,6 +66,14 @@ lemma snd_inv [has_inv G] [has_inv H] (p : G × H) : (p⁻¹).2 = (p.2)⁻¹ :=
 @[simp, to_additive]
 lemma inv_mk [has_inv G] [has_inv H] (a : G) (b : H) : (a, b)⁻¹ = (a⁻¹, b⁻¹) := rfl
 
+@[to_additive]
+instance [has_div M] [has_div N] : has_div (M × N) := ⟨λ p q, ⟨p.1 / q.1, p.2 / q.2⟩⟩
+
+@[simp] lemma fst_sub [add_group A] [add_group B] (a b : A × B) : (a - b).1 = a.1 - b.1 := rfl
+@[simp] lemma snd_sub [add_group A] [add_group B] (a b : A × B) : (a - b).2 = a.2 - b.2 := rfl
+@[simp] lemma mk_sub_mk [add_group A] [add_group B] (x₁ x₂ : A) (y₁ y₂ : B) :
+(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂) := rfl
+
 @[to_additive]
 instance [semigroup M] [semigroup N] : semigroup (M × N) :=
 { mul_assoc := assume a b c, mk.inj_iff.mpr ⟨mul_assoc _ _ _, mul_assoc _ _ _⟩,
@@ -80,12 +88,8 @@ instance [monoid M] [monoid N] : monoid (M × N) :=
 @[to_additive]
 instance [group G] [group H] : group (G × H) :=
 { mul_left_inv := assume a, mk.inj_iff.mpr ⟨mul_left_inv _, mul_left_inv _⟩,
-  .. prod.monoid, .. prod.has_inv }
-
-@[simp] lemma fst_sub [add_group A] [add_group B] (a b : A × B) : (a - b).1 = a.1 - b.1 := rfl
-@[simp] lemma snd_sub [add_group A] [add_group B] (a b : A × B) : (a - b).2 = a.2 - b.2 := rfl
-@[simp] lemma mk_sub_mk [add_group A] [add_group B] (x₁ x₂ : A) (y₁ y₂ : B) :
-  (x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂) := rfl
+  div_eq_mul_inv := λ a b, mk.inj_iff.mpr ⟨div_eq_mul_inv _ _, div_eq_mul_inv _ _⟩,
+  .. prod.monoid, .. prod.has_inv, .. prod.has_div }
 
 @[to_additive]
 instance [comm_semigroup G] [comm_semigroup H] : comm_semigroup (G × H) :=

src/algebra/group/type_tags.lean

@@ -163,13 +163,43 @@ instance [has_neg α] : has_inv (multiplicative α) := ⟨λ x, additive.of_mul
 @[simp] lemma to_add_inv [has_neg α] (x : multiplicative α) :
   (x⁻¹).to_add = -x.to_add := rfl
 
+instance additive.has_sub [has_div α] : has_sub (additive α) :=
+{ sub := λ x y, additive.of_mul (x.to_mul / y.to_mul) }
+
+instance multiplicative.has_div [has_sub α] : has_div (multiplicative α) :=
+{ div := λ x y, multiplicative.of_add (x.to_add - y.to_add) }
+
+@[simp] lemma of_add_sub [has_sub α] (x y : α) :
+  multiplicative.of_add (x - y) = multiplicative.of_add x / multiplicative.of_add y :=
+rfl
+
+@[simp] lemma to_add_div [has_sub α] (x y : multiplicative α) :
+  (x / y).to_add = x.to_add - y.to_add :=
+rfl
+
+@[simp] lemma of_mul_div [has_div α] (x y : α) :
+  additive.of_mul (x / y) = additive.of_mul x - additive.of_mul y :=
+rfl
+
+@[simp] lemma to_mul_sub [has_div α] (x y : additive α) :
+  (x - y).to_mul = x.to_mul / y.to_mul :=
+rfl
+
+instance [div_inv_monoid α] : sub_neg_monoid (additive α) :=
+{ sub_eq_add_neg := @div_eq_mul_inv α _,
+  .. additive.has_neg, .. additive.has_sub, .. additive.add_monoid }
+
+instance [sub_neg_monoid α] : div_inv_monoid (multiplicative α) :=
+{ div_eq_mul_inv := @sub_eq_add_neg α _,
+  .. multiplicative.has_inv, .. multiplicative.has_div, .. multiplicative.monoid }
+
 instance [group α] : add_group (additive α) :=
 { add_left_neg := @mul_left_inv α _,
-  .. additive.has_neg, .. additive.add_monoid }
+  .. additive.sub_neg_monoid }
 
 instance [add_group α] : group (multiplicative α) :=
 { mul_left_inv := @add_left_neg α _,
-  .. multiplicative.has_inv, ..multiplicative.monoid }
+  .. multiplicative.div_inv_monoid }
 
 instance [comm_group α] : add_comm_group (additive α) :=
 { .. additive.add_group, .. additive.add_comm_monoid }