chore(algebra/group,algebra/group_with_zero): a few more injective/su…

…rjective constructors (#5547)

src/algebra/group/inj_surj.lean

@@ -115,6 +115,19 @@ protected def comm_monoid [comm_monoid M₂] (f : M₁ → M₂) (hf : injective
 
 variables [has_inv M₁]
 
+/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `div_inv_monoid`
+if it admits an injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `div_inv_monoid`. -/
+@[to_additive
+"A type endowed with `0`, `+`, unary `-`, and binary `-` is a `sub_neg_monoid`
+if it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to
+a `sub_neg_monoid`."]
+protected def div_inv_monoid [has_div M₁] [div_inv_monoid 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) :
+  div_inv_monoid M₁ :=
+{ div_eq_mul_inv := λ x y, hf $ by erw [div, mul, inv, div_eq_mul_inv],
+  .. hf.monoid f one mul, .. ‹has_inv M₁›, .. ‹has_div M₁› }
+
 /-- A type endowed with `1`, `*` and `⁻¹` is a group,
 if it admits an injective map that preserves `1`, `*` and `⁻¹` to a group. -/
 @[to_additive
@@ -133,7 +146,7 @@ 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,
+"A type endowed with `0`, `+` and `-` (unary and binary) 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
@@ -142,9 +155,7 @@ protected def group_div [has_div M₁] [group M₂] (f : M₁ → M₂) (hf : in
   (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₁› }
+{ .. hf.div_inv_monoid f one mul inv div, .. hf.group f one mul inv }
 
 /-- A type endowed with `1`, `*` and `⁻¹` is a commutative group,
 if it admits an injective map that preserves `1`, `*` and `⁻¹` to a commutative group. -/
@@ -174,7 +185,6 @@ protected def comm_group_div [has_div M₁] [comm_group M₂] (f : M₁ → M₂
   comm_group M₁ :=
 { .. hf.comm_monoid f one mul, .. hf.group_div f one mul inv div }
 
-
 end injective
 
 /-!
@@ -235,14 +245,26 @@ variables [has_inv M₂]
 /-- A type endowed with `1`, `*` and `⁻¹` is a group,
 if it admits a surjective map that preserves `1`, `*` and `⁻¹` from a group. -/
 @[to_additive
-"A type endowed with `0` and `+` is an additive group,
-if it admits a surjective map that preserves `0` and `+` to an additive group."]
+"A type endowed with `0`, `+`, and unary `-` is an additive group,
+if it admits a surjective map that preserves `0`, `+`, and `-` from an additive group."]
 protected def group [group M₁] (f : M₁ → M₂) (hf : surjective f)
   (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) :
   group M₂ :=
 { mul_left_inv := hf.forall.2 $ λ x, by erw [← inv, ← mul, mul_left_inv, one]; refl,
   ..‹has_inv M₂›, .. hf.monoid f one mul }
 
+/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `div_inv_monoid`,
+if it admits a surjective map that preserves `1`, `*`, `⁻¹`, and `/` from a `div_inv_monoid` -/
+@[to_additive
+"A type endowed with `0`, `+`, and `-` (unary and binary) is an additive group,
+if it admits a surjective map that preserves `0`, `+`, and `-` from a `sub_neg_monoid`"]
+protected def div_inv_monoid [has_div M₂] [div_inv_monoid M₁] (f : M₁ → M₂) (hf : surjective 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) :
+  div_inv_monoid M₂ :=
+{ div_eq_mul_inv := hf.forall₂.2 $ λ x y, by erw [← inv, ← mul, ← div, div_eq_mul_inv],
+  .. hf.monoid f one mul, .. ‹has_div M₂›, .. ‹has_inv M₂› }
+
 /-- A type endowed with `1`, `*`, `⁻¹` and `/` is a group,
 if it admits an surjective map from a group that preserves these operations.
 
@@ -259,9 +281,7 @@ protected def group_div [has_div M₂] [group M₁] (f : M₁ → M₂) (hf : su
   (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 := hf.forall.2 $ λ x, hf.forall.2 $
-    λ y, by erw [← div, div_eq_mul_inv, mul, inv]; refl,
-  ..‹has_div M₂›, .. hf.group f one mul inv }
+{ .. hf.div_inv_monoid f one mul inv div, .. hf.group f one mul inv }
 
 /-- A type endowed with `1`, `*` and `⁻¹` is a commutative group,
 if it admits a surjective map that preserves `1`, `*` and `⁻¹` from a commutative group. -/

src/algebra/group_with_zero/basic.lean

@@ -340,6 +340,19 @@ protected def function.injective.group_with_zero [has_zero G₀'] [has_mul G₀'
   .. hf.monoid_with_zero f zero one mul,
   .. pullback_nonzero f zero one }
 
+/-- Pullback a `group_with_zero` class along an injective function. This is a version of
+`function.injective.group_with_zero` that uses a specified `/` instead of the default
+`a / b = a * b⁻¹`. -/
+protected def function.injective.group_with_zero_div [has_zero G₀'] [has_mul G₀'] [has_one G₀']
+  [has_inv G₀'] [has_div G₀'] (f : G₀' → G₀) (hf : injective f) (zero : f 0 = 0) (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_with_zero G₀' :=
+{ .. hf.monoid_with_zero f zero one mul,
+  .. hf.div_inv_monoid f one mul inv div,
+  .. pullback_nonzero f zero one,
+  .. hf.group_with_zero f zero one mul inv }
+
 /-- Pushforward a `group_with_zero` class along an surjective function. -/
 protected def function.surjective.group_with_zero [has_zero G₀'] [has_mul G₀'] [has_one G₀']
   [has_inv G₀'] (h01 : (0:G₀') ≠ 1)
@@ -354,6 +367,16 @@ protected def function.surjective.group_with_zero [has_zero G₀'] [has_mul G₀
   exists_pair_ne := ⟨0, 1, h01⟩,
   .. hf.monoid_with_zero f zero one mul }
 
+/-- Pushforward a `group_with_zero` class along a surjective function. This is a version of
+`function.surjective.group_with_zero` that uses a specified `/` instead of the default
+`a / b = a * b⁻¹`. -/
+protected def function.surjective.group_with_zero_div [has_zero G₀'] [has_mul G₀'] [has_one G₀']
+  [has_inv G₀'] [has_div G₀'] (h01 : (0:G₀') ≠ 1) (f : G₀ → G₀') (hf : surjective f)
+  (zero : f 0 = 0) (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_with_zero G₀' :=
+{ .. hf.div_inv_monoid f one mul inv div, .. hf.group_with_zero h01 f zero one mul inv }
+
 @[simp] lemma mul_inv_cancel_right' {b : G₀} (h : b ≠ 0) (a : G₀) :
   (a * b) * b⁻¹ = a :=
 calc (a * b) * b⁻¹ = a * (b * b⁻¹) : mul_assoc _ _ _
@@ -668,6 +691,14 @@ protected def function.injective.comm_group_with_zero [has_zero G₀'] [has_mul
   comm_group_with_zero G₀' :=
 { .. hf.group_with_zero f zero one mul inv, .. hf.comm_semigroup f mul }
 
+/-- Pullback a `comm_group_with_zero` class along an injective function. -/
+protected def function.injective.comm_group_with_zero_div [has_zero G₀'] [has_mul G₀'] [has_one G₀']
+  [has_inv G₀'] [has_div G₀'] (f : G₀' → G₀) (hf : injective f) (zero : f 0 = 0) (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_with_zero G₀' :=
+{ .. hf.group_with_zero_div f zero one mul inv div, .. hf.comm_semigroup f mul }
+
 /-- Pushforward a `comm_group_with_zero` class along an surjective function. -/
 protected def function.surjective.comm_group_with_zero [has_zero G₀'] [has_mul G₀'] [has_one G₀']
   [has_inv G₀'] (h01 : (0:G₀') ≠ 1)
@@ -676,6 +707,14 @@ protected def function.surjective.comm_group_with_zero [has_zero G₀'] [has_mul
   comm_group_with_zero G₀' :=
 { .. hf.group_with_zero h01 f zero one mul inv, .. hf.comm_semigroup f mul }
 
+/-- Pushforward a `comm_group_with_zero` class along a surjective function. -/
+protected def function.surjective.comm_group_with_zero_div [has_zero G₀'] [has_mul G₀']
+  [has_one G₀'] [has_inv G₀'] [has_div G₀'] (h01 : (0:G₀') ≠ 1) (f : G₀ → G₀') (hf : surjective f)
+  (zero : f 0 = 0) (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_with_zero G₀' :=
+{ .. hf.group_with_zero_div h01 f zero one mul inv div, .. hf.comm_semigroup f mul }
+
 lemma mul_inv' : (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
 by rw [mul_inv_rev', mul_comm]