From fa858ca44bd2776682d5d79c01d31558a748641a Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 22 Nov 2022 23:33:11 -0600 Subject: [PATCH 01/13] raw mathport: f69e8f317a18ab43f12cdcacaa1a3765eb512065 --- Mathlib/Algebra/Group/InjSurj.lean | 439 +++++++++++++++++++++++++++++ 1 file changed, 439 insertions(+) create mode 100644 Mathlib/Algebra/Group/InjSurj.lean diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean new file mode 100644 index 0000000000000..f506153e429aa --- /dev/null +++ b/Mathlib/Algebra/Group/InjSurj.lean @@ -0,0 +1,439 @@ +/- +Copyright (c) 2020 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin +-/ +import Mathbin.Algebra.Group.Defs +import Mathbin.Logic.Function.Basic +import Mathbin.Data.Int.Cast.Basic + +/-! +# Lifting algebraic data classes along injective/surjective maps + +This file provides definitions that are meant to deal with +situations such as the following: + +Suppose that `G` is a group, and `H` is a type endowed with +`has_one H`, `has_mul H`, and `has_inv H`. +Suppose furthermore, that `f : G → H` is a surjective map +that respects the multiplication, and the unit elements. +Then `H` satisfies the group axioms. + +The relevant definition in this case is `function.surjective.group`. +Dually, there is also `function.injective.group`. +And there are versions for (additive) (commutative) semigroups/monoids. +-/ + + +namespace Function + +/-! +### Injective +-/ + + +namespace Injective + +variable {M₁ : Type _} {M₂ : Type _} [Mul M₁] + +/-- A type endowed with `*` is a semigroup, +if it admits an injective map that preserves `*` to a semigroup. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `+` is an additive semigroup,\nif it admits an injective map that preserves `+` to an additive semigroup."] +protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : + Semigroup M₁ := + { ‹Mul M₁› with mul_assoc := fun x y z => hf <| by erw [mul, mul, mul, mul, mul_assoc] } +#align function.injective.semigroup Function.Injective.semigroup + +/-- A type endowed with `*` is a commutative semigroup, +if it admits an injective map that preserves `*` to a commutative semigroup. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `+` is an additive commutative semigroup,\nif it admits an injective map that preserves `+` to an additive commutative semigroup."] +protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : + CommSemigroup M₁ := + { hf.Semigroup f mul with mul_comm := fun x y => hf <| by erw [mul, mul, mul_comm] } +#align function.injective.comm_semigroup Function.Injective.commSemigroup + +/-- A type endowed with `*` is a left cancel semigroup, +if it admits an injective map that preserves `*` to a left cancel semigroup. +See note [reducible non-instances]. -/ +@[reducible, + to_additive AddLeftCancelSemigroup + "A type endowed with `+` is an additive left cancel semigroup,\nif it admits an injective map that preserves `+` to an additive left cancel semigroup."] +protected def leftCancelSemigroup [LeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) + (mul : ∀ x y, f (x * y) = f x * f y) : LeftCancelSemigroup M₁ := + { hf.Semigroup f mul with mul := (· * ·), + mul_left_cancel := fun x y z H => hf <| (mul_right_inj (f x)).1 <| by erw [← mul, ← mul, H] <;> rfl } +#align function.injective.left_cancel_semigroup Function.Injective.leftCancelSemigroup + +/-- A type endowed with `*` is a right cancel semigroup, +if it admits an injective map that preserves `*` to a right cancel semigroup. +See note [reducible non-instances]. -/ +@[reducible, + to_additive AddRightCancelSemigroup + "A type endowed with `+` is an additive right cancel semigroup,\nif it admits an injective map that preserves `+` to an additive right cancel semigroup."] +protected def rightCancelSemigroup [RightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) + (mul : ∀ x y, f (x * y) = f x * f y) : RightCancelSemigroup M₁ := + { hf.Semigroup f mul with mul := (· * ·), + mul_right_cancel := fun x y z H => hf <| (mul_left_inj (f y)).1 <| by erw [← mul, ← mul, H] <;> rfl } +#align function.injective.right_cancel_semigroup Function.Injective.rightCancelSemigroup + +variable [One M₁] + +/-- A type endowed with `1` and `*` is a mul_one_class, +if it admits an injective map that preserves `1` and `*` to a mul_one_class. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an add_zero_class,\nif it admits an injective map that preserves `0` and `+` to an add_zero_class."] +protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₁ := + { ‹One M₁›, ‹Mul M₁› with one_mul := fun x => hf <| by erw [mul, one, one_mul], + mul_one := fun x => hf <| by erw [mul, one, mul_one] } +#align function.injective.mul_one_class Function.Injective.mulOneClass + +variable [Pow M₁ ℕ] + +/-- A type endowed with `1` and `*` is a monoid, +if it admits an injective map that preserves `1` and `*` to a monoid. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an additive monoid,\nif it admits an injective map that preserves `0` and `+` to an additive monoid.\nThis version takes a custom `nsmul` as a `[has_smul ℕ M₁]` argument."] +protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₁ := + { hf.Semigroup f mul, hf.MulOneClass f one mul with npow := fun n x => x ^ n, + npow_zero' := fun x => hf <| by erw [npow, one, pow_zero], + npow_succ' := fun n x => hf <| by erw [npow, pow_succ, mul, npow] } +#align function.injective.monoid Function.Injective.monoid + +/-- A type endowed with `0`, `1` and `+` is an additive monoid with one, +if it admits an injective map that preserves `0`, `1` and `+` to an additive monoid with one. +See note [reducible non-instances]. -/ +@[reducible] +protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [HasSmul ℕ M₁] [NatCast M₁] [AddMonoidWithOne M₂] + (f : M₁ → M₂) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) + (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₁ := + { hf.AddMonoid f zero add nsmul with natCast := coe, nat_cast_zero := hf (by erw [nat_cast, Nat.cast_zero, zero]), + nat_cast_succ := fun n => hf (by erw [nat_cast, Nat.cast_succ, add, one, nat_cast]), one := 1 } +#align function.injective.add_monoid_with_one Function.Injective.addMonoidWithOne + +/-- A type endowed with `1` and `*` is a left cancel monoid, +if it admits an injective map that preserves `1` and `*` to a left cancel monoid. +See note [reducible non-instances]. -/ +@[reducible, + to_additive AddLeftCancelMonoid + "A type endowed with `0` and `+` is an additive left cancel monoid,\nif it admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] +protected def leftCancelMonoid [LeftCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : LeftCancelMonoid M₁ := + { hf.LeftCancelSemigroup f mul, hf.Monoid f one mul npow with } +#align function.injective.left_cancel_monoid Function.Injective.leftCancelMonoid + +/-- A type endowed with `1` and `*` is a right cancel monoid, +if it admits an injective map that preserves `1` and `*` to a right cancel monoid. +See note [reducible non-instances]. -/ +@[reducible, + to_additive AddRightCancelMonoid + "A type endowed with `0` and `+` is an additive left cancel monoid,\nif it admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] +protected def rightCancelMonoid [RightCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : RightCancelMonoid M₁ := + { hf.RightCancelSemigroup f mul, hf.Monoid f one mul npow with } +#align function.injective.right_cancel_monoid Function.Injective.rightCancelMonoid + +/-- A type endowed with `1` and `*` is a cancel monoid, +if it admits an injective map that preserves `1` and `*` to a cancel monoid. +See note [reducible non-instances]. -/ +@[reducible, + to_additive AddCancelMonoid + "A type endowed with `0` and `+` is an additive left cancel monoid,\nif it admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] +protected def cancelMonoid [CancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelMonoid M₁ := + { hf.LeftCancelMonoid f one mul npow, hf.RightCancelMonoid f one mul npow with } +#align function.injective.cancel_monoid Function.Injective.cancelMonoid + +/-- A type endowed with `1` and `*` is a commutative monoid, +if it admits an injective map that preserves `1` and `*` to a commutative monoid. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an additive commutative monoid,\nif it admits an injective map that preserves `0` and `+` to an additive commutative monoid."] +protected def commMonoid [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₁ := + { hf.CommSemigroup f mul, hf.Monoid f one mul npow with } +#align function.injective.comm_monoid Function.Injective.commMonoid + +/-- A type endowed with `1` and `*` is a cancel commutative monoid, +if it admits an injective map that preserves `1` and `*` to a cancel commutative monoid. +See note [reducible non-instances]. -/ +@[reducible, + to_additive AddCancelCommMonoid + "A type endowed with `0` and `+` is an additive cancel commutative monoid,\nif it admits an injective map that preserves `0` and `+` to an additive cancel commutative monoid."] +protected def cancelCommMonoid [CancelCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelCommMonoid M₁ := + { hf.LeftCancelSemigroup f mul, hf.CommMonoid f one mul npow with } +#align function.injective.cancel_comm_monoid Function.Injective.cancelCommMonoid + +--See note [reducible non-instances] +/-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type +which has an involutive inversion. -/ +@[reducible, + to_additive + "A type has an involutive negation if it admits a surjective map that\npreserves `⁻¹` to a type which has an involutive inversion."] +protected def hasInvolutiveInv {M₁ : Type _} [Inv M₁] [HasInvolutiveInv M₂] (f : M₁ → M₂) (hf : Injective f) + (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : HasInvolutiveInv M₁ where + inv := Inv.inv + inv_inv x := hf <| by rw [inv, inv, inv_inv] +#align function.injective.has_involutive_inv Function.Injective.hasInvolutiveInv + +variable [Inv M₁] [Div M₁] [Pow 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`. +See note [reducible non-instances]. -/ +@[reducible, + to_additive SubNegMonoid + "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `sub_neg_monoid`\nif it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to\na `sub_neg_monoid`.\nThis version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and\n`[has_smul ℤ M₁]` arguments."] +protected def divInvMonoid [DivInvMonoid 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) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₁ := + { hf.Monoid f one mul npow, ‹Inv M₁›, ‹Div M₁› with zpow := fun n x => x ^ n, + zpow_zero' := fun x => hf <| by erw [zpow, zpow_zero, one], + zpow_succ' := fun n x => hf <| by erw [zpow, mul, zpow_of_nat, pow_succ, zpow, zpow_of_nat], + zpow_neg' := fun n x => hf <| by erw [zpow, zpow_neg_succ_of_nat, inv, zpow, zpow_coe_nat], + div_eq_mul_inv := fun x y => hf <| by erw [div, mul, inv, div_eq_mul_inv] } +#align function.injective.div_inv_monoid Function.Injective.divInvMonoid + +-- See note [reducible non-instances] +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_monoid` +if it admits an injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `division_monoid`. -/ +@[reducible, + to_additive + "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `subtraction_monoid`\nif it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to\na `subtraction_monoid`.\nThis version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and\n`[has_smul ℤ M₁]` arguments."] +protected def divisionMonoid [DivisionMonoid 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) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionMonoid M₁ := + { hf.DivInvMonoid f one mul inv div npow zpow, hf.HasInvolutiveInv f inv with + mul_inv_rev := fun x y => hf <| by erw [inv, mul, mul_inv_rev, mul, inv, inv], + inv_eq_of_mul := fun x y h => hf <| by erw [inv, inv_eq_of_mul_eq_one_right (by erw [← mul, h, one])] } +#align function.injective.division_monoid Function.Injective.divisionMonoid + +-- See note [reducible non-instances] +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_comm_monoid` +if it admits an injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `division_comm_monoid`. +See note [reducible non-instances]. -/ +@[reducible, + to_additive SubtractionCommMonoid + "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `subtraction_comm_monoid`\nif it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to\na `subtraction_comm_monoid`.\nThis version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and\n`[has_smul ℤ M₁]` arguments."] +protected def divisionCommMonoid [DivisionCommMonoid 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) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionCommMonoid M₁ := + { hf.DivisionMonoid f one mul inv div npow zpow, hf.CommSemigroup f mul with } +#align function.injective.division_comm_monoid Function.Injective.divisionCommMonoid + +/-- A type endowed with `1`, `*` and `⁻¹` is a group, +if it admits an injective map that preserves `1`, `*` and `⁻¹` to a group. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an additive group,\nif it admits an injective map that preserves `0` and `+` to an additive group."] +protected def group [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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) + (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : Group M₁ := + { hf.DivInvMonoid f one mul inv div npow zpow with + mul_left_inv := fun x => hf <| by erw [mul, inv, mul_left_inv, one] } +#align function.injective.group Function.Injective.group + +/-- A type endowed with `0`, `1` and `+` is an additive group with one, +if it admits an injective map that preserves `0`, `1` and `+` to an additive group with one. +See note [reducible non-instances]. -/ +@[reducible] +protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [HasSmul ℕ M₁] [Neg M₁] [Sub M₁] [HasSmul ℤ M₁] + [NatCast M₁] [IntCast M₁] [AddGroupWithOne M₂] (f : M₁ → M₂) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) + (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) + (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) + (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₁ := + { hf.AddGroup f zero add neg sub nsmul zsmul, hf.AddMonoidWithOne f zero one add nsmul nat_cast with intCast := coe, + int_cast_of_nat := fun n => hf (by simp only [nat_cast, int_cast, Int.cast_ofNat]), + int_cast_neg_succ_of_nat := fun n => hf (by erw [int_cast, neg, nat_cast, Int.cast_neg, Int.cast_ofNat]) } +#align function.injective.add_group_with_one Function.Injective.addGroupWithOne + +/-- A type endowed with `1`, `*` and `⁻¹` is a commutative group, +if it admits an injective map that preserves `1`, `*` and `⁻¹` to a commutative group. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an additive commutative group,\nif it admits an injective map that preserves `0` and `+` to an additive commutative group."] +protected def commGroup [CommGroup 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) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₁ := + { hf.CommMonoid f one mul npow, hf.Group f one mul inv div npow zpow with } +#align function.injective.comm_group Function.Injective.commGroup + +end Injective + +/-! +### Surjective +-/ + + +namespace Surjective + +variable {M₁ : Type _} {M₂ : Type _} [Mul M₂] + +/-- A type endowed with `*` is a semigroup, +if it admits a surjective map that preserves `*` from a semigroup. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `+` is an additive semigroup,\nif it admits a surjective map that preserves `+` from an additive semigroup."] +protected def semigroup [Semigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) : + Semigroup M₂ := + { ‹Mul M₂› with mul_assoc := hf.forall₃.2 fun x y z => by simp only [← mul, mul_assoc] } +#align function.surjective.semigroup Function.Surjective.semigroup + +/-- A type endowed with `*` is a commutative semigroup, +if it admits a surjective map that preserves `*` from a commutative semigroup. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `+` is an additive commutative semigroup,\nif it admits a surjective map that preserves `+` from an additive commutative semigroup."] +protected def commSemigroup [CommSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) : + CommSemigroup M₂ := + { hf.Semigroup f mul with mul_comm := hf.Forall₂.2 fun x y => by erw [← mul, ← mul, mul_comm] } +#align function.surjective.comm_semigroup Function.Surjective.commSemigroup + +variable [One M₂] + +/-- A type endowed with `1` and `*` is a mul_one_class, +if it admits a surjective map that preserves `1` and `*` from a mul_one_class. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an add_zero_class,\nif it admits a surjective map that preserves `0` and `+` to an add_zero_class."] +protected def mulOneClass [MulOneClass M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₂ := + { ‹One M₂›, ‹Mul M₂› with one_mul := hf.forall.2 fun x => by erw [← one, ← mul, one_mul], + mul_one := hf.forall.2 fun x => by erw [← one, ← mul, mul_one] } +#align function.surjective.mul_one_class Function.Surjective.mulOneClass + +variable [Pow M₂ ℕ] + +/-- A type endowed with `1` and `*` is a monoid, +if it admits a surjective map that preserves `1` and `*` to a monoid. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an additive monoid,\nif it admits a surjective map that preserves `0` and `+` to an additive monoid.\nThis version takes a custom `nsmul` as a `[has_smul ℕ M₂]` argument."] +protected def monoid [Monoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₂ := + { hf.Semigroup f mul, hf.MulOneClass f one mul with npow := fun n x => x ^ n, + npow_zero' := hf.forall.2 fun x => by erw [← npow, pow_zero, ← one], + npow_succ' := fun n => hf.forall.2 fun x => by erw [← npow, pow_succ, ← npow, ← mul] } +#align function.surjective.monoid Function.Surjective.monoid + +/-- A type endowed with `0`, `1` and `+` is an additive monoid with one, +if it admits a surjective map that preserves `0`, `1` and `*` from an additive monoid with one. +See note [reducible non-instances]. -/ +@[reducible] +protected def addMonoidWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [HasSmul ℕ M₂] [NatCast M₂] [AddMonoidWithOne M₁] + (f : M₁ → M₂) (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) + (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₂ := + { hf.AddMonoid f zero add nsmul with natCast := coe, + nat_cast_zero := by + rw [← nat_cast, Nat.cast_zero, zero] + rfl, + nat_cast_succ := fun n => by + rw [← nat_cast, Nat.cast_succ, add, one, nat_cast] + rfl, + one := 1 } +#align function.surjective.add_monoid_with_one Function.Surjective.addMonoidWithOne + +/-- A type endowed with `1` and `*` is a commutative monoid, +if it admits a surjective map that preserves `1` and `*` from a commutative monoid. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an additive commutative monoid,\nif it admits a surjective map that preserves `0` and `+` to an additive commutative monoid."] +protected def commMonoid [CommMonoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₂ := + { hf.CommSemigroup f mul, hf.Monoid f one mul npow with } +#align function.surjective.comm_monoid Function.Surjective.commMonoid + +--See note [reducible non-instances] +/-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type +which has an involutive inversion. -/ +@[reducible, + to_additive + "A type has an involutive negation if it admits a surjective map that\npreserves `⁻¹` to a type which has an involutive inversion."] +protected def hasInvolutiveInv {M₂ : Type _} [Inv M₂] [HasInvolutiveInv M₁] (f : M₁ → M₂) (hf : Surjective f) + (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : HasInvolutiveInv M₂ where + inv := Inv.inv + inv_inv := hf.forall.2 fun x => by erw [← inv, ← inv, inv_inv] +#align function.surjective.has_involutive_inv Function.Surjective.hasInvolutiveInv + +variable [Inv M₂] [Div M₂] [Pow M₂ ℤ] + +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `div_inv_monoid` +if it admits a surjective map that preserves `1`, `*`, `⁻¹`, and `/` to a `div_inv_monoid`. +See note [reducible non-instances]. -/ +@[reducible, + to_additive SubNegMonoid + "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `sub_neg_monoid`\nif it admits a surjective map that preserves `0`, `+`, unary `-`, and binary `-` to\na `sub_neg_monoid`."] +protected def divInvMonoid [DivInvMonoid 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) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₂ := + { hf.Monoid f one mul npow, ‹Div M₂›, ‹Inv M₂› with zpow := fun n x => x ^ n, + zpow_zero' := hf.forall.2 fun x => by erw [← zpow, zpow_zero, ← one], + zpow_succ' := fun n => hf.forall.2 fun x => by erw [← zpow, ← zpow, zpow_of_nat, zpow_of_nat, pow_succ, ← mul], + zpow_neg' := fun n => hf.forall.2 fun x => by erw [← zpow, ← zpow, zpow_neg_succ_of_nat, zpow_coe_nat, inv], + div_eq_mul_inv := hf.Forall₂.2 fun x y => by erw [← inv, ← mul, ← div, div_eq_mul_inv] } +#align function.surjective.div_inv_monoid Function.Surjective.divInvMonoid + +/-- A type endowed with `1`, `*` and `⁻¹` is a group, +if it admits a surjective map that preserves `1`, `*` and `⁻¹` to a group. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an additive group,\nif it admits a surjective map that preserves `0` and `+` to 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)⁻¹) (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) + (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : Group M₂ := + { hf.DivInvMonoid f one mul inv div npow zpow with + mul_left_inv := hf.forall.2 fun x => by erw [← inv, ← mul, mul_left_inv, one] <;> rfl } +#align function.surjective.group Function.Surjective.group + +/-- A type endowed with `0`, `1`, `+` is an additive group with one, +if it admits a surjective map that preserves `0`, `1`, and `+` to an additive group with one. +See note [reducible non-instances]. -/ +protected def addGroupWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [Neg M₂] [Sub M₂] [HasSmul ℕ M₂] [HasSmul ℤ M₂] + [NatCast M₂] [IntCast M₂] [AddGroupWithOne M₁] (f : M₁ → M₂) (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) + (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) + (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) + (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₂ := + { hf.AddMonoidWithOne f zero one add nsmul nat_cast, hf.AddGroup f zero add neg sub nsmul zsmul with intCast := coe, + int_cast_of_nat := fun n => by rw [← int_cast, Int.cast_ofNat, nat_cast], + int_cast_neg_succ_of_nat := fun n => by + rw [← int_cast, Int.cast_neg, Int.cast_ofNat, neg, nat_cast] + rfl } +#align function.surjective.add_group_with_one Function.Surjective.addGroupWithOne + +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a commutative group, +if it admits a surjective map that preserves `1`, `*`, `⁻¹`, and `/` from a commutative group. +See note [reducible non-instances]. -/ +@[reducible, + to_additive + "A type endowed with `0` and `+` is an additive commutative group,\nif it admits a surjective map that preserves `0` and `+` to an additive commutative group."] +protected def commGroup [CommGroup 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) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₂ := + { hf.CommMonoid f one mul npow, hf.Group f one mul inv div npow zpow with } +#align function.surjective.comm_group Function.Surjective.commGroup + +end Surjective + +end Function + From 6ee3ec8f1972d1824bd2d205e0951744565e88aa Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 22 Nov 2022 23:37:25 -0600 Subject: [PATCH 02/13] add import to Mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 129e896df8063..261ecf92523ad 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5,6 +5,7 @@ import Mathlib.Algebra.Group.Basic import Mathlib.Algebra.Group.Commutator import Mathlib.Algebra.Group.Commute import Mathlib.Algebra.Group.Defs +import Mathlib.Algebra.Group.InjSurj import Mathlib.Algebra.Group.OrderSynonym import Mathlib.Algebra.Group.Semiconj import Mathlib.Algebra.Group.Units From 6921a7124fcc173dced06184e7052bc29e12ec49 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 23 Nov 2022 22:34:36 -0600 Subject: [PATCH 03/13] Make `to_additive` play nice with `pow` and `smul` --- Mathlib/Algebra/Group/Basic.lean | 2 +- Mathlib/Algebra/Group/Defs.lean | 66 +++++++++++++------------------- 2 files changed, 27 insertions(+), 41 deletions(-) diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index f4b4177d7904e..7ccbd882ae857 100644 --- a/Mathlib/Algebra/Group/Basic.lean +++ b/Mathlib/Algebra/Group/Basic.lean @@ -579,7 +579,7 @@ theorem leftInverse_inv_mul_mul_right (c : G) : #align left_inverse_inv_mul_mul_right leftInverse_inv_mul_mul_right #align left_inverse_neg_add_add_right leftInverse_neg_add_add_right --- TODO @[to_additive] +@[to_additive] theorem exists_npow_eq_one_of_zpow_eq_one {n : ℤ} (hn : n ≠ 0) {x : G} (h : x ^ n = 1) : ∃ n : ℕ, 0 < n ∧ x ^ n = 1 := by cases' n with n n diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index f6f6359d08a44..efee51f2fe297 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -51,14 +51,26 @@ class VAdd (G : Type _) (P : Type _) where class HasVsub (G : outParam (Type _)) (P : Type _) where vsub : P → P → G +/-- +The notation typeclass for heterogeneous scalar multiplication. +This enables the notation `a • b : γ` where `a : α`, `b : β`. +-/ +class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where + /-- `a • b` computes the product of `a` and `b`. + The meaning of this notation is type-dependent. -/ + hSMul : α → β → γ + /-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/ @[ext, to_additive] class SMul (M : Type _) (α : Type _) where smul : M → α → α +instance instHSmul [SMul α β] : HSMul α β β where + hSMul := SMul.smul + infixl:65 " +ᵥ " => VAdd.vadd infixl:65 " -ᵥ " => HasVsub.vsub -infixr:73 " • " => SMul.smul +infixr:73 " • " => HSMul.hSMul attribute [to_additive] Mul attribute [to_additive] Div @@ -70,7 +82,12 @@ attribute [to_additive] instHDiv attribute [to_additive_relevant_arg 3] HMul HAdd HAdd.hAdd HMul.hMul attribute [to_additive_reorder 1] HPow attribute [to_additive_reorder 1 5] HPow.hPow -attribute [to_additive] HPow +attribute [to_additive_reorder 1] Pow +attribute [to_additive_reorder 1 4] Pow.pow +attribute [to_additive SMul] Pow +attribute [to_additive_reorder 1] instHPow +attribute [to_additive instHSmul] instHPow +attribute [to_additive HSMul] HPow universe u @@ -507,24 +524,7 @@ attribute [to_additive AddMonoid.toAddZeroClass] Monoid.toMulOneClass instance AddMonoid.SMul {M : Type _} [AddMonoid M] : SMul ℕ M := ⟨AddMonoid.nsmul⟩ -attribute [to_additive AddMonoid.SMulNat] Monoid.Pow - -section --- FIXME The lemmas in this section should be done by `to_additive` below, but it fails. - -variable {M : Type _} [AddMonoid M] - -@[simp] -theorem nsmul_eq_smul (n : ℕ) (x : M) : AddMonoid.nsmul n x = n • x := - rfl - -theorem zero_nsmul (a : M) : 0 • a = 0 := - AddMonoid.nsmul_zero _ - -theorem succ_nsmul (a : M) (n : ℕ) : (n + 1) • a = a + n • a := - AddMonoid.nsmul_succ n a - -end +attribute [to_additive AddMonoid.SMul] Monoid.Pow section @@ -773,36 +773,22 @@ section DivInvMonoid variable [DivInvMonoid G] {a b : G} --- TODO restore @[to_additive zsmul_eq_smul] -@[simp] theorem zpow_eq_pow (n : ℤ) (x : G) : DivInvMonoid.zpow n x = x ^ n := rfl -theorem zsmul_eq_smul {G} [SubNegMonoid G] (n : ℤ) (x : G) : SubNegMonoid.zsmul n x = n • x := rfl -attribute [to_additive zsmul_eq_smul] zpow_eq_pow +@[simp, to_additive zsmul_eq_smul] theorem zpow_eq_pow (n : ℤ) (x : G) : + DivInvMonoid.zpow n x = x ^ n := + rfl --- TODO restore @[to_additive zero_zsmul] -@[simp] theorem zpow_zero (a : G) : a ^ (0 : ℤ) = 1 := +@[simp, to_additive zero_zsmul] theorem zpow_zero (a : G) : a ^ (0 : ℤ) = 1 := DivInvMonoid.zpow_zero' a -theorem zero_zsmul {G} [SubNegMonoid G] (a : G) : (0 : ℤ) • a = 0 := - SubNegMonoid.zsmul_zero' a -attribute [to_additive zero_zsmul] zpow_zero --- TODO restore @[to_additive ofNat_zsmul] -@[norm_cast] +@[norm_cast, to_additive ofNat_zsmul] theorem zpow_ofNat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n | 0 => (zpow_zero _).trans (pow_zero _).symm | n + 1 => calc a ^ (↑(n + 1) : ℤ) = a * a ^ (n : ℤ) := DivInvMonoid.zpow_succ' _ _ _ = a * a ^ n := congr_arg ((· * ·) a) (zpow_ofNat a n) _ = a ^ (n + 1) := (pow_succ _ _).symm -theorem ofNat_zsmul {G} [SubNegMonoid G] (a : G) : ∀ n : ℕ, (n : ℤ) • a = n • a - | 0 => (zero_zsmul _).trans (zero_nsmul _).symm - | n + 1 => calc - (↑(n + 1) : ℤ) • a = a + (n : ℤ) • a := SubNegMonoid.zsmul_succ' _ _ - _ = a + n • a := congr_arg ((· + ·) a) (ofNat_zsmul a n) - _ = (n + 1) • a := (succ_nsmul _ _).symm -attribute [to_additive ofNat_zsmul] zpow_ofNat --- TODO restore @[to_additive] -@[simp] +@[simp, to_additive] theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by rw [← zpow_ofNat] exact DivInvMonoid.zpow_neg' n a From 038a3fd85dc79ac7bb4d8669c9f7eb9420e77459 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 23 Nov 2022 23:04:00 -0600 Subject: [PATCH 04/13] Same fix for `SMul` to `VAdd` translation --- Mathlib/Algebra/Group/Defs.lean | 37 +++++++++++++++++++++++---------- 1 file changed, 26 insertions(+), 11 deletions(-) diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index efee51f2fe297..184426a00add5 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -43,13 +43,14 @@ actions and register the following instances: open Function -/-- Type class for the `+ᵥ` notation. -/ -class VAdd (G : Type _) (P : Type _) where - vadd : G → P → P - -/-- Type class for the `-ᵥ` notation. -/ -class HasVsub (G : outParam (Type _)) (P : Type _) where - vsub : P → P → G +/-- +The notation typeclass for heterogeneous scalar multiplication. +This enables the notation `a • b : γ` where `a : α`, `b : β`. +-/ +class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where + /-- `a +ᵥ b` computes the sum of `a` and `b`. + The meaning of this notation is type-dependent. -/ + hVAdd : α → β → γ /-- The notation typeclass for heterogeneous scalar multiplication. @@ -60,15 +61,26 @@ class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where The meaning of this notation is type-dependent. -/ hSMul : α → β → γ +/-- Type class for the `+ᵥ` notation. -/ +class VAdd (G : Type _) (P : Type _) where + vadd : G → P → P + +/-- Type class for the `-ᵥ` notation. -/ +class HasVsub (G : outParam (Type _)) (P : Type _) where + vsub : P → P → G + /-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/ @[ext, to_additive] class SMul (M : Type _) (α : Type _) where smul : M → α → α -instance instHSmul [SMul α β] : HSMul α β β where +instance instHVAdd [VAdd α β] : HVAdd α β β where + hVAdd := VAdd.vadd + +instance instHSMul [SMul α β] : HSMul α β β where hSMul := SMul.smul -infixl:65 " +ᵥ " => VAdd.vadd +infixl:65 " +ᵥ " => HVAdd.hVAdd infixl:65 " -ᵥ " => HasVsub.vsub infixr:73 " • " => HSMul.hSMul @@ -79,16 +91,19 @@ attribute [to_additive] instHMul attribute [to_additive] HDiv attribute [to_additive] instHDiv -attribute [to_additive_relevant_arg 3] HMul HAdd HAdd.hAdd HMul.hMul +attribute [to_additive_relevant_arg 3] HMul HAdd HPow HAdd.hAdd HMul.hMul HPow.hPow attribute [to_additive_reorder 1] HPow attribute [to_additive_reorder 1 5] HPow.hPow attribute [to_additive_reorder 1] Pow attribute [to_additive_reorder 1 4] Pow.pow attribute [to_additive SMul] Pow attribute [to_additive_reorder 1] instHPow -attribute [to_additive instHSmul] instHPow +attribute [to_additive instHSMul] instHPow attribute [to_additive HSMul] HPow +attribute [to_additive instHVAdd] instHSMul +attribute [to_additive HVAdd] HSMul + universe u variable {G : Type _} From 75511fafeb55770cf7003ca8c50cc1a7fffcad8b Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 23 Nov 2022 23:24:15 -0600 Subject: [PATCH 05/13] fix `ring` tactic by adding two type ascriptions --- Mathlib/Algebra/Group/Defs.lean | 3 ++- Mathlib/Tactic/Ring/Basic.lean | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 184426a00add5..e5ffa58058635 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -91,7 +91,8 @@ attribute [to_additive] instHMul attribute [to_additive] HDiv attribute [to_additive] instHDiv -attribute [to_additive_relevant_arg 3] HMul HAdd HPow HAdd.hAdd HMul.hMul HPow.hPow +attribute [to_additive_relevant_arg 3] HMul HAdd HPow HSMul +attribute [to_additive_relevant_arg 3] HAdd.hAdd HMul.hMul HPow.hPow HSMul.hSMul attribute [to_additive_reorder 1] HPow attribute [to_additive_reorder 1 5] HPow.hPow attribute [to_additive_reorder 1] Pow diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean index a77472d8e4201..518d443fbcebd 100644 --- a/Mathlib/Tactic/Ring/Basic.lean +++ b/Mathlib/Tactic/Ring/Basic.lean @@ -880,7 +880,7 @@ theorem mul_congr (_ : a = a') (_ : b = b') (_ : a' * b' = c) : (a * b : R) = c := by subst_vars; rfl theorem nsmul_congr (_ : (a : ℕ) = a') (_ : b = b') - (_ : a' • b' = c) : (a • b : R) = c := by subst_vars; rfl + (_ : a' • b' = c) : (a • (b : R)) = c := by subst_vars; rfl theorem pow_congr (_ : a = a') (_ : b = b') (_ : a' ^ b' = c) : (a ^ b : R) = c := by subst_vars; rfl @@ -920,7 +920,7 @@ partial def eval {u} {α : Q(Type u)} (sα : Q(CommSemiring $α)) pure ⟨c, vc, (q(mul_congr $pa $pb $p) : Expr)⟩ | _ => els | ``SMul.smul, _ => match e with - | ~q(($a : ℕ) • $b) => + | ~q(($a : ℕ) • ($b : «$α»)) => let ⟨_, va, pa⟩ ← eval sℕ .nat a let ⟨_, vb, pb⟩ ← eval sα c b let ⟨c, vc, p⟩ ← evalNSMul sα va vb From 2db544d12e1d57977fa54a19884a3ac21d7d012e Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 24 Nov 2022 01:39:55 -0600 Subject: [PATCH 06/13] fix abel --- Mathlib/Tactic/Abel.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Tactic/Abel.lean b/Mathlib/Tactic/Abel.lean index 67d9800fbf927..58ae79bf316a4 100644 --- a/Mathlib/Tactic/Abel.lean +++ b/Mathlib/Tactic/Abel.lean @@ -368,6 +368,10 @@ partial def eval (c : Context) (e : Expr) : MetaM (NormalExpr × Expr) := do evalSMul' c (eval c) true e e₁ e₂ | (``SMul.smul, #[.const ``Nat _, _, _, e₁, e₂]) => evalSMul' c (eval c) false e e₁ e₂ + | (``HSMul.hSMul, #[.const ``Int _, _, _, _, e₁, e₂]) => + evalSMul' c (eval c) true e e₁ e₂ + | (``HSMul.hSMul, #[.const ``Nat _, _, _, _, e₁, e₂]) => + evalSMul' c (eval c) false e e₁ e₂ | (``smul, #[_, _, e₁, e₂]) => evalSMul' c (eval c) false e e₁ e₂ | (``smulg, #[_, _, e₁, e₂]) => evalSMul' c (eval c) true e e₁ e₂ | (``OfNat.ofNat, #[_, .lit (.natVal 0), _]) From a135450aa7938393a20adeea5f47f751eae0e65d Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 24 Nov 2022 01:55:00 -0600 Subject: [PATCH 07/13] fix ring --- Mathlib/Tactic/Ring/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean index 518d443fbcebd..81bf42062b256 100644 --- a/Mathlib/Tactic/Ring/Basic.lean +++ b/Mathlib/Tactic/Ring/Basic.lean @@ -919,7 +919,7 @@ partial def eval {u} {α : Q(Type u)} (sα : Q(CommSemiring $α)) let ⟨c, vc, p⟩ := evalMul sα va vb pure ⟨c, vc, (q(mul_congr $pa $pb $p) : Expr)⟩ | _ => els - | ``SMul.smul, _ => match e with + | ``HSMul.hSMul, _ => match e with | ~q(($a : ℕ) • ($b : «$α»)) => let ⟨_, va, pa⟩ ← eval sℕ .nat a let ⟨_, vb, pb⟩ ← eval sα c b From e82781abc2191e7cf1c3de37c3d948f834dc8919 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 24 Nov 2022 02:41:58 -0600 Subject: [PATCH 08/13] get it compiling --- Mathlib/Algebra/Group/InjSurj.lean | 538 ++++++++++++++--------------- 1 file changed, 266 insertions(+), 272 deletions(-) diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean index f506153e429aa..cbf28ad80f39d 100644 --- a/Mathlib/Algebra/Group/InjSurj.lean +++ b/Mathlib/Algebra/Group/InjSurj.lean @@ -3,9 +3,9 @@ Copyright (c) 2020 Johan Commelin. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin -/ -import Mathbin.Algebra.Group.Defs -import Mathbin.Logic.Function.Basic -import Mathbin.Data.Int.Cast.Basic +import Mathlib.Algebra.Group.Defs +import Mathlib.Logic.Function.Basic +import Mathlib.Data.Int.Cast.Basic /-! # Lifting algebraic data classes along injective/surjective maps @@ -36,241 +36,239 @@ namespace Injective variable {M₁ : Type _} {M₂ : Type _} [Mul M₁] -/-- A type endowed with `*` is a semigroup, -if it admits an injective map that preserves `*` to a semigroup. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `+` is an additive semigroup,\nif it admits an injective map that preserves `+` to an additive semigroup."] -protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : - Semigroup M₁ := +/-- A type endowed with `*` is a semigroup, if it admits an injective map that preserves `*` to +a semigroup. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `+` is an additive semigroup, if it admits an +injective map that preserves `+` to an additive semigroup."] +protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) + (mul : ∀ x y, f (x * y) = f x * f y) : Semigroup M₁ := { ‹Mul M₁› with mul_assoc := fun x y z => hf <| by erw [mul, mul, mul, mul, mul_assoc] } #align function.injective.semigroup Function.Injective.semigroup -/-- A type endowed with `*` is a commutative semigroup, -if it admits an injective map that preserves `*` to a commutative semigroup. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `+` is an additive commutative semigroup,\nif it admits an injective map that preserves `+` to an additive commutative semigroup."] -protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : - CommSemigroup M₁ := - { hf.Semigroup f mul with mul_comm := fun x y => hf <| by erw [mul, mul, mul_comm] } +/-- A type endowed with `*` is a commutative semigroup, if it admits an injective map that +preserves `*` to a commutative semigroup. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `+` is an additive commutative semigroup,if it admits +an injective map that preserves `+` to an additive commutative semigroup."] +protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) + (mul : ∀ x y, f (x * y) = f x * f y) : CommSemigroup M₁ := + { hf.semigroup f mul with mul_comm := fun x y => hf <| by erw [mul, mul, mul_comm] } #align function.injective.comm_semigroup Function.Injective.commSemigroup -/-- A type endowed with `*` is a left cancel semigroup, -if it admits an injective map that preserves `*` to a left cancel semigroup. -See note [reducible non-instances]. -/ -@[reducible, - to_additive AddLeftCancelSemigroup - "A type endowed with `+` is an additive left cancel semigroup,\nif it admits an injective map that preserves `+` to an additive left cancel semigroup."] +/-- A type endowed with `*` is a left cancel semigroup, if it admits an injective map that +preserves `*` to a left cancel semigroup. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `+` is an additive left cancel +semigroup, if it admits an injective map that preserves `+` to an additive left cancel semigroup."] protected def leftCancelSemigroup [LeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : LeftCancelSemigroup M₁ := - { hf.Semigroup f mul with mul := (· * ·), - mul_left_cancel := fun x y z H => hf <| (mul_right_inj (f x)).1 <| by erw [← mul, ← mul, H] <;> rfl } + { hf.semigroup f mul with + mul := (· * ·), + mul_left_cancel := fun x y z H => hf <| (mul_right_inj (f x)).1 <| by erw [← mul, ← mul, H] } #align function.injective.left_cancel_semigroup Function.Injective.leftCancelSemigroup +#align function.injective.add_left_cancel_semigroup Function.Injective.addLeftCancelSemigroup -/-- A type endowed with `*` is a right cancel semigroup, -if it admits an injective map that preserves `*` to a right cancel semigroup. -See note [reducible non-instances]. -/ -@[reducible, - to_additive AddRightCancelSemigroup - "A type endowed with `+` is an additive right cancel semigroup,\nif it admits an injective map that preserves `+` to an additive right cancel semigroup."] +/-- A type endowed with `*` is a right cancel semigroup, if it admits an injective map that +preserves `*` to a right cancel semigroup. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `+` is an additive right +cancel semigroup, if it admits an injective map that preserves `+` to an additive right cancel +semigroup."] protected def rightCancelSemigroup [RightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : RightCancelSemigroup M₁ := - { hf.Semigroup f mul with mul := (· * ·), - mul_right_cancel := fun x y z H => hf <| (mul_left_inj (f y)).1 <| by erw [← mul, ← mul, H] <;> rfl } + { hf.semigroup f mul with + mul := (· * ·), + mul_right_cancel := fun x y z H => hf <| (mul_left_inj (f y)).1 <| by erw [← mul, ← mul, H] } #align function.injective.right_cancel_semigroup Function.Injective.rightCancelSemigroup +#align function.injective.add_right_cancel_semigroup Function.Injective.addRightCancelSemigroup variable [One M₁] -/-- A type endowed with `1` and `*` is a mul_one_class, -if it admits an injective map that preserves `1` and `*` to a mul_one_class. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an add_zero_class,\nif it admits an injective map that preserves `0` and `+` to an add_zero_class."] +/-- A type endowed with `1` and `*` is a mul_one_class, if it admits an injective map that +preserves `1` and `*` to a mul_one_class. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an add_zero_class, if it admits an +injective map that preserves `0` and `+` to an add_zero_class."] protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₁ := - { ‹One M₁›, ‹Mul M₁› with one_mul := fun x => hf <| by erw [mul, one, one_mul], + { ‹One M₁›, ‹Mul M₁› with + one_mul := fun x => hf <| by erw [mul, one, one_mul], mul_one := fun x => hf <| by erw [mul, one, mul_one] } #align function.injective.mul_one_class Function.Injective.mulOneClass variable [Pow M₁ ℕ] -/-- A type endowed with `1` and `*` is a monoid, -if it admits an injective map that preserves `1` and `*` to a monoid. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an additive monoid,\nif it admits an injective map that preserves `0` and `+` to an additive monoid.\nThis version takes a custom `nsmul` as a `[has_smul ℕ M₁]` argument."] -protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) - (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₁ := - { hf.Semigroup f mul, hf.MulOneClass f one mul with npow := fun n x => x ^ n, - npow_zero' := fun x => hf <| by erw [npow, one, pow_zero], - npow_succ' := fun n x => hf <| by erw [npow, pow_succ, mul, npow] } +/-- A type endowed with `1` and `*` is a monoid, if it admits an injective map that preserves `1` +and `*` to a monoid. See note [reducible non-instances]. -/ +@[reducible, to_additive] +protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₁ := + { hf.mulOneClass f one mul, hf.semigroup f mul with + npow := fun n x => x ^ n, + npow_zero := fun x => hf <| by erw [npow, one, pow_zero], + npow_succ := fun n x => hf <| by erw [npow, pow_succ, mul, npow] } #align function.injective.monoid Function.Injective.monoid /-- A type endowed with `0`, `1` and `+` is an additive monoid with one, if it admits an injective map that preserves `0`, `1` and `+` to an additive monoid with one. See note [reducible non-instances]. -/ @[reducible] -protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [HasSmul ℕ M₁] [NatCast M₁] [AddMonoidWithOne M₂] - (f : M₁ → M₂) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) - (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₁ := - { hf.AddMonoid f zero add nsmul with natCast := coe, nat_cast_zero := hf (by erw [nat_cast, Nat.cast_zero, zero]), - nat_cast_succ := fun n => hf (by erw [nat_cast, Nat.cast_succ, add, one, nat_cast]), one := 1 } +protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ M₁] [NatCast M₁] + [AddMonoidWithOne M₂] (f : M₁ → M₂) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) + (add : ∀ x y, f (x + y) = f x + f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) + (nat_cast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₁ := + { hf.addMonoid f zero add nsmul with + natCast := Nat.cast, + natCast_zero := hf (by erw [nat_cast, Nat.cast_zero, zero]), + natCast_succ := fun n => hf (by erw [nat_cast, Nat.cast_succ, add, one, nat_cast]), one := 1 } #align function.injective.add_monoid_with_one Function.Injective.addMonoidWithOne -/-- A type endowed with `1` and `*` is a left cancel monoid, -if it admits an injective map that preserves `1` and `*` to a left cancel monoid. -See note [reducible non-instances]. -/ -@[reducible, - to_additive AddLeftCancelMonoid - "A type endowed with `0` and `+` is an additive left cancel monoid,\nif it admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] -protected def leftCancelMonoid [LeftCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) - (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : LeftCancelMonoid M₁ := - { hf.LeftCancelSemigroup f mul, hf.Monoid f one mul npow with } +/-- A type endowed with `1` and `*` is a left cancel monoid, if it admits an injective map that +preserves `1` and `*` to a left cancel monoid. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive left cancel monoid, if it +admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] +protected def leftCancelMonoid [LeftCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) + (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : LeftCancelMonoid M₁ := + { hf.leftCancelSemigroup f mul, hf.monoid f one mul npow with } #align function.injective.left_cancel_monoid Function.Injective.leftCancelMonoid /-- A type endowed with `1` and `*` is a right cancel monoid, if it admits an injective map that preserves `1` and `*` to a right cancel monoid. See note [reducible non-instances]. -/ -@[reducible, - to_additive AddRightCancelMonoid - "A type endowed with `0` and `+` is an additive left cancel monoid,\nif it admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] -protected def rightCancelMonoid [RightCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) - (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : RightCancelMonoid M₁ := - { hf.RightCancelSemigroup f mul, hf.Monoid f one mul npow with } +@[reducible, to_additive "A type endowed with `0` and `+` is an additive left cancel monoid,if it +admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] +protected def rightCancelMonoid [RightCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) + (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : RightCancelMonoid M₁ := + { hf.rightCancelSemigroup f mul, hf.monoid f one mul npow with } #align function.injective.right_cancel_monoid Function.Injective.rightCancelMonoid -/-- A type endowed with `1` and `*` is a cancel monoid, -if it admits an injective map that preserves `1` and `*` to a cancel monoid. -See note [reducible non-instances]. -/ -@[reducible, - to_additive AddCancelMonoid - "A type endowed with `0` and `+` is an additive left cancel monoid,\nif it admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] +/-- A type endowed with `1` and `*` is a cancel monoid, if it admits an injective map that preserves +`1` and `*` to a cancel monoid. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive left cancel monoid,if it +admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] protected def cancelMonoid [CancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) - (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelMonoid M₁ := - { hf.LeftCancelMonoid f one mul npow, hf.RightCancelMonoid f one mul npow with } + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : + CancelMonoid M₁ := + { hf.leftCancelMonoid f one mul npow, hf.rightCancelMonoid f one mul npow with } #align function.injective.cancel_monoid Function.Injective.cancelMonoid -/-- A type endowed with `1` and `*` is a commutative monoid, -if it admits an injective map that preserves `1` and `*` to a commutative monoid. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an additive commutative monoid,\nif it admits an injective map that preserves `0` and `+` to an additive commutative monoid."] +/-- A type endowed with `1` and `*` is a commutative monoid, if it admits an injective map that +preserves `1` and `*` to a commutative monoid. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive commutative monoid, if it +admits an injective map that preserves `0` and `+` to an additive commutative monoid."] protected def commMonoid [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) - (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₁ := - { hf.CommSemigroup f mul, hf.Monoid f one mul npow with } + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : + CommMonoid M₁ := + { hf.commSemigroup f mul, hf.monoid f one mul npow with } #align function.injective.comm_monoid Function.Injective.commMonoid -/-- A type endowed with `1` and `*` is a cancel commutative monoid, -if it admits an injective map that preserves `1` and `*` to a cancel commutative monoid. -See note [reducible non-instances]. -/ -@[reducible, - to_additive AddCancelCommMonoid - "A type endowed with `0` and `+` is an additive cancel commutative monoid,\nif it admits an injective map that preserves `0` and `+` to an additive cancel commutative monoid."] -protected def cancelCommMonoid [CancelCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) - (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelCommMonoid M₁ := - { hf.LeftCancelSemigroup f mul, hf.CommMonoid f one mul npow with } +/-- A type endowed with `1` and `*` is a cancel commutative monoid, if it admits an injective map +that preserves `1` and `*` to a cancel commutative monoid. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive cancel commutative monoid, +if it admits an injective map that preserves `0` and `+` to an additive cancel commutative monoid."] +protected def cancelCommMonoid [CancelCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) + (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) + (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelCommMonoid M₁ := + { hf.leftCancelSemigroup f mul, hf.commMonoid f one mul npow with } #align function.injective.cancel_comm_monoid Function.Injective.cancelCommMonoid ---See note [reducible non-instances] /-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type -which has an involutive inversion. -/ -@[reducible, - to_additive - "A type has an involutive negation if it admits a surjective map that\npreserves `⁻¹` to a type which has an involutive inversion."] -protected def hasInvolutiveInv {M₁ : Type _} [Inv M₁] [HasInvolutiveInv M₂] (f : M₁ → M₂) (hf : Injective f) - (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : HasInvolutiveInv M₁ where +which has an involutive inversion. See note [reducible non-instances] -/ +@[reducible, to_additive "A type has an involutive negation if it admits a surjective map that +preserves `⁻¹` to a type which has an involutive inversion."] +protected def hasInvolutiveInv {M₁ : Type _} [Inv M₁] [HasInvolutiveInv M₂] (f : M₁ → M₂) + (hf : Injective f) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : HasInvolutiveInv M₁ where inv := Inv.inv inv_inv x := hf <| by rw [inv, inv, inv_inv] #align function.injective.has_involutive_inv Function.Injective.hasInvolutiveInv variable [Inv M₁] [Div M₁] [Pow 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`. -See note [reducible non-instances]. -/ -@[reducible, - to_additive SubNegMonoid - "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `sub_neg_monoid`\nif it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to\na `sub_neg_monoid`.\nThis version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and\n`[has_smul ℤ M₁]` arguments."] +/-- 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`. See note [reducible non-instances]. -/ +@[reducible, to_additive subNegMonoid "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`.\nThis version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and +`[has_smul ℤ M₁]` arguments."] protected def divInvMonoid [DivInvMonoid 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) - (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₁ := - { hf.Monoid f one mul npow, ‹Inv M₁›, ‹Div M₁› with zpow := fun n x => x ^ n, + (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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) + (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₁ := + { hf.monoid f one mul npow, ‹Inv M₁›, ‹Div M₁› with + zpow := fun n x => x ^ n, zpow_zero' := fun x => hf <| by erw [zpow, zpow_zero, one], - zpow_succ' := fun n x => hf <| by erw [zpow, mul, zpow_of_nat, pow_succ, zpow, zpow_of_nat], - zpow_neg' := fun n x => hf <| by erw [zpow, zpow_neg_succ_of_nat, inv, zpow, zpow_coe_nat], + zpow_succ' := fun n x => hf <| by erw [zpow, mul, zpow_ofNat, pow_succ, zpow, zpow_ofNat], + zpow_neg' := fun n x => hf <| by erw [zpow, zpow_negSucc, inv, zpow, zpow_ofNat], div_eq_mul_inv := fun x y => hf <| by erw [div, mul, inv, div_eq_mul_inv] } #align function.injective.div_inv_monoid Function.Injective.divInvMonoid --- See note [reducible non-instances] -/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_monoid` -if it admits an injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `division_monoid`. -/ -@[reducible, - to_additive - "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `subtraction_monoid`\nif it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to\na `subtraction_monoid`.\nThis version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and\n`[has_smul ℤ M₁]` arguments."] +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_monoid` if it admits an injective map +that preserves `1`, `*`, `⁻¹`, and `/` to a `division_monoid`. See note [reducible non-instances]-/ + +@[reducible, to_additive "A type endowed with `0`, `+`, unary `-`, and binary `-` is a +`subtraction_monoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and binary +`-` to a `subtraction_monoid`. This version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` +and `[has_smul ℤ M₁]` arguments."] protected def divisionMonoid [DivisionMonoid 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) - (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionMonoid M₁ := - { hf.DivInvMonoid f one mul inv div npow zpow, hf.HasInvolutiveInv f inv with + (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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) + (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionMonoid M₁ := + { hf.divInvMonoid f one mul inv div npow zpow, hf.hasInvolutiveInv f inv with mul_inv_rev := fun x y => hf <| by erw [inv, mul, mul_inv_rev, mul, inv, inv], - inv_eq_of_mul := fun x y h => hf <| by erw [inv, inv_eq_of_mul_eq_one_right (by erw [← mul, h, one])] } + inv_eq_of_mul := fun x y h => hf <| by + erw [inv, inv_eq_of_mul_eq_one_right (by erw [← mul, h, one])] } #align function.injective.division_monoid Function.Injective.divisionMonoid --- See note [reducible non-instances] -/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_comm_monoid` -if it admits an injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `division_comm_monoid`. +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_comm_monoid` if it admits an +injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `division_comm_monoid`. See note [reducible non-instances]. -/ -@[reducible, - to_additive SubtractionCommMonoid - "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `subtraction_comm_monoid`\nif it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to\na `subtraction_comm_monoid`.\nThis version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and\n`[has_smul ℤ M₁]` arguments."] -protected def divisionCommMonoid [DivisionCommMonoid 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) - (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionCommMonoid M₁ := - { hf.DivisionMonoid f one mul inv div npow zpow, hf.CommSemigroup f mul with } +@[reducible, to_additive subtractionCommMonoid "A type endowed with `0`, `+`, unary `-`, and binary +`-` is a `subtraction_comm_monoid` if it admits an injective map that preserves `0`, `+`, unary `-`, +and binary `-` to a `subtraction_comm_monoid`. This version takes custom `nsmul` and `zsmul` as +`[has_smul ℕ M₁]` and `[has_smul ℤ M₁]` arguments."] +protected def divisionCommMonoid [DivisionCommMonoid 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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) + (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionCommMonoid M₁ := + { hf.divisionMonoid f one mul inv div npow zpow, hf.commSemigroup f mul with } #align function.injective.division_comm_monoid Function.Injective.divisionCommMonoid -/-- A type endowed with `1`, `*` and `⁻¹` is a group, -if it admits an injective map that preserves `1`, `*` and `⁻¹` to a group. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an additive group,\nif it admits an injective map that preserves `0` and `+` to an additive group."] -protected def group [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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) +/-- A type endowed with `1`, `*` and `⁻¹` is a group, if it admits an injective map that preserves +`1`, `*` and `⁻¹` to a group. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive group, if it admits an +injective map that preserves `0` and `+` to an additive group."] +protected def group [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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : Group M₁ := - { hf.DivInvMonoid f one mul inv div npow zpow with + { hf.divInvMonoid f one mul inv div npow zpow with mul_left_inv := fun x => hf <| by erw [mul, inv, mul_left_inv, one] } #align function.injective.group Function.Injective.group -/-- A type endowed with `0`, `1` and `+` is an additive group with one, -if it admits an injective map that preserves `0`, `1` and `+` to an additive group with one. -See note [reducible non-instances]. -/ +/-- A type endowed with `0`, `1` and `+` is an additive group with one, if it admits an injective +map that preserves `0`, `1` and `+` to an additive group with one. See note +[reducible non-instances]. -/ @[reducible] -protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [HasSmul ℕ M₁] [Neg M₁] [Sub M₁] [HasSmul ℤ M₁] - [NatCast M₁] [IntCast M₁] [AddGroupWithOne M₂] (f : M₁ → M₂) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) - (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) - (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) - (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₁ := - { hf.AddGroup f zero add neg sub nsmul zsmul, hf.AddMonoidWithOne f zero one add nsmul nat_cast with intCast := coe, - int_cast_of_nat := fun n => hf (by simp only [nat_cast, int_cast, Int.cast_ofNat]), - int_cast_neg_succ_of_nat := fun n => hf (by erw [int_cast, neg, nat_cast, Int.cast_neg, Int.cast_ofNat]) } +protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁] + [SMul ℤ M₁] [NatCast M₁] [IntCast M₁] [AddGroupWithOne M₂] (f : M₁ → M₂) (hf : Injective f) + (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x) + (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) + (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n) + (int_cast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₁ := + { hf.addGroup f zero add neg sub nsmul zsmul, + hf.addMonoidWithOne f zero one add nsmul nat_cast with + intCast := Int.cast, + intCast_ofNat := fun n => hf (by rw [nat_cast, ←Int.cast, int_cast, Int.cast_ofNat]), --(by simp only [nat_cast, int_cast, Int.cast_ofNat]), + intCast_negSucc := fun n => hf (by erw [int_cast, neg, nat_cast, Int.cast_negSucc] ) } #align function.injective.add_group_with_one Function.Injective.addGroupWithOne -/-- A type endowed with `1`, `*` and `⁻¹` is a commutative group, -if it admits an injective map that preserves `1`, `*` and `⁻¹` to a commutative group. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an additive commutative group,\nif it admits an injective map that preserves `0` and `+` to an additive commutative group."] +/-- A type endowed with `1`, `*` and `⁻¹` is a commutative group, if it admits an injective map that +preserves `1`, `*` and `⁻¹` to a commutative group. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive commutative group, if it +admits an injective map that preserves `0` and `+` to an additive commutative group."] protected def commGroup [CommGroup 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) - (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₁ := - { hf.CommMonoid f one mul npow, hf.Group f one mul inv div npow zpow with } + (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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) + (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₁ := + { hf.commMonoid f one mul npow, hf.group f one mul inv div npow zpow with } #align function.injective.comm_group Function.Injective.commGroup end Injective @@ -284,156 +282,152 @@ namespace Surjective variable {M₁ : Type _} {M₂ : Type _} [Mul M₂] -/-- A type endowed with `*` is a semigroup, -if it admits a surjective map that preserves `*` from a semigroup. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `+` is an additive semigroup,\nif it admits a surjective map that preserves `+` from an additive semigroup."] -protected def semigroup [Semigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) : - Semigroup M₂ := +/-- A type endowed with `*` is a semigroup, if it admits a surjective map that preserves `*` from a +semigroup. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `+` is an additive semigroup, if it admits a +surjective map that preserves `+` from an additive semigroup."] +protected def semigroup [Semigroup M₁] (f : M₁ → M₂) (hf : Surjective f) + (mul : ∀ x y, f (x * y) = f x * f y) : Semigroup M₂ := { ‹Mul M₂› with mul_assoc := hf.forall₃.2 fun x y z => by simp only [← mul, mul_assoc] } #align function.surjective.semigroup Function.Surjective.semigroup -/-- A type endowed with `*` is a commutative semigroup, -if it admits a surjective map that preserves `*` from a commutative semigroup. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `+` is an additive commutative semigroup,\nif it admits a surjective map that preserves `+` from an additive commutative semigroup."] -protected def commSemigroup [CommSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) : - CommSemigroup M₂ := - { hf.Semigroup f mul with mul_comm := hf.Forall₂.2 fun x y => by erw [← mul, ← mul, mul_comm] } +/-- A type endowed with `*` is a commutative semigroup, if it admits a surjective map that preserves +`*` from a commutative semigroup. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `+` is an additive commutative semigroup, if it admits +a surjective map that preserves `+` from an additive commutative semigroup."] +protected def commSemigroup [CommSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) + (mul : ∀ x y, f (x * y) = f x * f y) : CommSemigroup M₂ := + { hf.semigroup f mul with + mul_comm := hf.forall₂.2 fun x y => by erw [← mul, ← mul, mul_comm] } #align function.surjective.comm_semigroup Function.Surjective.commSemigroup variable [One M₂] -/-- A type endowed with `1` and `*` is a mul_one_class, -if it admits a surjective map that preserves `1` and `*` from a mul_one_class. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an add_zero_class,\nif it admits a surjective map that preserves `0` and `+` to an add_zero_class."] +/-- A type endowed with `1` and `*` is a mul_one_class, if it admits a surjective map that preserves +`1` and `*` from a mul_one_class. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an add_zero_class, if it admits a +surjective map that preserves `0` and `+` to an add_zero_class."] protected def mulOneClass [MulOneClass M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₂ := - { ‹One M₂›, ‹Mul M₂› with one_mul := hf.forall.2 fun x => by erw [← one, ← mul, one_mul], + { ‹One M₂›, ‹Mul M₂› with + one_mul := hf.forall.2 fun x => by erw [← one, ← mul, one_mul], mul_one := hf.forall.2 fun x => by erw [← one, ← mul, mul_one] } #align function.surjective.mul_one_class Function.Surjective.mulOneClass variable [Pow M₂ ℕ] -/-- A type endowed with `1` and `*` is a monoid, -if it admits a surjective map that preserves `1` and `*` to a monoid. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an additive monoid,\nif it admits a surjective map that preserves `0` and `+` to an additive monoid.\nThis version takes a custom `nsmul` as a `[has_smul ℕ M₂]` argument."] -protected def monoid [Monoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) - (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₂ := - { hf.Semigroup f mul, hf.MulOneClass f one mul with npow := fun n x => x ^ n, - npow_zero' := hf.forall.2 fun x => by erw [← npow, pow_zero, ← one], - npow_succ' := fun n => hf.forall.2 fun x => by erw [← npow, pow_succ, ← npow, ← mul] } +/-- A type endowed with `1` and `*` is a monoid, if it admits a surjective map that preserves `1` +and `*` to a monoid. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive monoid, if it admits a +surjective map that preserves `0` and `+` to an additive monoid. This version takes a custom `nsmul` +as a `[has_smul ℕ M₂]` argument."] +protected def monoid [Monoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₂ := + { hf.semigroup f mul, hf.mulOneClass f one mul with + npow := fun n x => x ^ n, + npow_zero := hf.forall.2 fun x => by dsimp only; erw [←npow, pow_zero, ←one], + npow_succ := fun n => hf.forall.2 fun x => by dsimp only; erw [←npow, pow_succ, ←npow, ←mul] } #align function.surjective.monoid Function.Surjective.monoid -/-- A type endowed with `0`, `1` and `+` is an additive monoid with one, -if it admits a surjective map that preserves `0`, `1` and `*` from an additive monoid with one. -See note [reducible non-instances]. -/ +/-- A type endowed with `0`, `1` and `+` is an additive monoid with one, if it admits a surjective +map that preserves `0`, `1` and `*` from an additive monoid with one. See note +[reducible non-instances]. -/ @[reducible] -protected def addMonoidWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [HasSmul ℕ M₂] [NatCast M₂] [AddMonoidWithOne M₁] - (f : M₁ → M₂) (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) - (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₂ := - { hf.AddMonoid f zero add nsmul with natCast := coe, - nat_cast_zero := by - rw [← nat_cast, Nat.cast_zero, zero] - rfl, - nat_cast_succ := fun n => by - rw [← nat_cast, Nat.cast_succ, add, one, nat_cast] - rfl, +protected def addMonoidWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [SMul ℕ M₂] [NatCast M₂] + [AddMonoidWithOne M₁] (f : M₁ → M₂) (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) + (add : ∀ x y, f (x + y) = f x + f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) + (nat_cast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₂ := + { hf.addMonoid f zero add nsmul with + natCast := Nat.cast, + natCast_zero := by rw [← Nat.cast, ← nat_cast, Nat.cast_zero, zero] + natCast_succ := fun n => by rw [← Nat.cast, ← nat_cast, Nat.cast_succ, add, one, nat_cast] one := 1 } #align function.surjective.add_monoid_with_one Function.Surjective.addMonoidWithOne -/-- A type endowed with `1` and `*` is a commutative monoid, -if it admits a surjective map that preserves `1` and `*` from a commutative monoid. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an additive commutative monoid,\nif it admits a surjective map that preserves `0` and `+` to an additive commutative monoid."] +/-- A type endowed with `1` and `*` is a commutative monoid, if it admits a surjective map that +preserves `1` and `*` from a commutative monoid. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive commutative monoid, if it +admits a surjective map that preserves `0` and `+` to an additive commutative monoid."] protected def commMonoid [CommMonoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) - (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₂ := - { hf.CommSemigroup f mul, hf.Monoid f one mul npow with } + (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : + CommMonoid M₂ := + { hf.commSemigroup f mul, hf.monoid f one mul npow with } #align function.surjective.comm_monoid Function.Surjective.commMonoid ---See note [reducible non-instances] /-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type -which has an involutive inversion. -/ -@[reducible, - to_additive - "A type has an involutive negation if it admits a surjective map that\npreserves `⁻¹` to a type which has an involutive inversion."] -protected def hasInvolutiveInv {M₂ : Type _} [Inv M₂] [HasInvolutiveInv M₁] (f : M₁ → M₂) (hf : Surjective f) - (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : HasInvolutiveInv M₂ where +which has an involutive inversion. See note [reducible non-instances] -/ +@[reducible, to_additive "A type has an involutive negation if it admits a surjective map that +preserves `⁻¹` to a type which has an involutive inversion."] +protected def hasInvolutiveInv {M₂ : Type _} [Inv M₂] [HasInvolutiveInv M₁] (f : M₁ → M₂) + (hf : Surjective f) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : HasInvolutiveInv M₂ where inv := Inv.inv inv_inv := hf.forall.2 fun x => by erw [← inv, ← inv, inv_inv] #align function.surjective.has_involutive_inv Function.Surjective.hasInvolutiveInv variable [Inv M₂] [Div M₂] [Pow M₂ ℤ] -/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `div_inv_monoid` -if it admits a surjective map that preserves `1`, `*`, `⁻¹`, and `/` to a `div_inv_monoid`. -See note [reducible non-instances]. -/ -@[reducible, - to_additive SubNegMonoid - "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `sub_neg_monoid`\nif it admits a surjective map that preserves `0`, `+`, unary `-`, and binary `-` to\na `sub_neg_monoid`."] +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `div_inv_monoid` if it admits a surjective map +that preserves `1`, `*`, `⁻¹`, and `/` to a `div_inv_monoid`. See note [reducible non-instances]. -/ +@[reducible, to_additive subNegMonoid "A type endowed with `0`, `+`, unary `-`, and binary `-` is a +`sub_neg_monoid` if it admits a surjective map that preserves `0`, `+`, unary `-`, and binary `-` to +a `sub_neg_monoid`."] protected def divInvMonoid [DivInvMonoid 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) - (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₂ := - { hf.Monoid f one mul npow, ‹Div M₂›, ‹Inv M₂› with zpow := fun n x => x ^ n, - zpow_zero' := hf.forall.2 fun x => by erw [← zpow, zpow_zero, ← one], - zpow_succ' := fun n => hf.forall.2 fun x => by erw [← zpow, ← zpow, zpow_of_nat, zpow_of_nat, pow_succ, ← mul], - zpow_neg' := fun n => hf.forall.2 fun x => by erw [← zpow, ← zpow, zpow_neg_succ_of_nat, zpow_coe_nat, inv], - div_eq_mul_inv := hf.Forall₂.2 fun x y => by erw [← inv, ← mul, ← div, div_eq_mul_inv] } + (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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) + (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₂ := + { hf.monoid f one mul npow, ‹Div M₂›, ‹Inv M₂› with + zpow := fun n x => x ^ n, + zpow_zero' := hf.forall.2 fun x => by dsimp only; erw [← zpow, zpow_zero, ← one], + zpow_succ' := fun n => hf.forall.2 fun x => by + dsimp only + erw [← zpow, ← zpow, zpow_ofNat, zpow_ofNat, pow_succ, ← mul], + zpow_neg' := fun n => hf.forall.2 fun x => by + dsimp only + erw [← zpow, ← zpow, zpow_negSucc, zpow_ofNat, inv], + div_eq_mul_inv := hf.forall₂.2 fun x y => by erw [← inv, ← mul, ← div, div_eq_mul_inv] } #align function.surjective.div_inv_monoid Function.Surjective.divInvMonoid -/-- A type endowed with `1`, `*` and `⁻¹` is a group, -if it admits a surjective map that preserves `1`, `*` and `⁻¹` to a group. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an additive group,\nif it admits a surjective map that preserves `0` and `+` to 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)⁻¹) (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) +/-- A type endowed with `1`, `*` and `⁻¹` is a group, if it admits a surjective map that preserves +`1`, `*` and `⁻¹` to a group. See note [reducible non-instances]. -/ +@[reducible, 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."] +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)⁻¹) + (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : Group M₂ := - { hf.DivInvMonoid f one mul inv div npow zpow with - mul_left_inv := hf.forall.2 fun x => by erw [← inv, ← mul, mul_left_inv, one] <;> rfl } + { hf.divInvMonoid f one mul inv div npow zpow with + mul_left_inv := hf.forall.2 fun x => by erw [← inv, ← mul, mul_left_inv, one] } #align function.surjective.group Function.Surjective.group /-- A type endowed with `0`, `1`, `+` is an additive group with one, if it admits a surjective map that preserves `0`, `1`, and `+` to an additive group with one. See note [reducible non-instances]. -/ -protected def addGroupWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [Neg M₂] [Sub M₂] [HasSmul ℕ M₂] [HasSmul ℤ M₂] - [NatCast M₂] [IntCast M₂] [AddGroupWithOne M₁] (f : M₁ → M₂) (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) - (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) - (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) - (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₂ := - { hf.AddMonoidWithOne f zero one add nsmul nat_cast, hf.AddGroup f zero add neg sub nsmul zsmul with intCast := coe, - int_cast_of_nat := fun n => by rw [← int_cast, Int.cast_ofNat, nat_cast], - int_cast_neg_succ_of_nat := fun n => by - rw [← int_cast, Int.cast_neg, Int.cast_ofNat, neg, nat_cast] - rfl } +protected def addGroupWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [Neg M₂] [Sub M₂] [SMul ℕ M₂] + [SMul ℤ M₂] [NatCast M₂] [IntCast M₂] [AddGroupWithOne M₁] (f : M₁ → M₂) (hf : Surjective f) + (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x) + (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) + (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n) + (int_cast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₂ := + { hf.addMonoidWithOne f zero one add nsmul nat_cast, + hf.addGroup f zero add neg sub nsmul zsmul with + intCast := Int.cast, + intCast_ofNat := fun n => by rw [← Int.cast, ← int_cast, Int.cast_ofNat, nat_cast], + intCast_negSucc := fun n => by + rw [← Int.cast, ← int_cast, Int.cast_negSucc, neg, nat_cast] } #align function.surjective.add_group_with_one Function.Surjective.addGroupWithOne -/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a commutative group, -if it admits a surjective map that preserves `1`, `*`, `⁻¹`, and `/` from a commutative group. -See note [reducible non-instances]. -/ -@[reducible, - to_additive - "A type endowed with `0` and `+` is an additive commutative group,\nif it admits a surjective map that preserves `0` and `+` to an additive commutative group."] +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a commutative group, if it admits a surjective +map that preserves `1`, `*`, `⁻¹`, and `/` from a commutative group. See note +[reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an additive commutative group, if it +admits a surjective map that preserves `0` and `+` to an additive commutative group."] protected def commGroup [CommGroup 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) - (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₂ := - { hf.CommMonoid f one mul npow, hf.Group f one mul inv div npow zpow with } + (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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) + (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₂ := + { hf.commMonoid f one mul npow, hf.group f one mul inv div npow zpow with } #align function.surjective.comm_group Function.Surjective.commGroup end Surjective end Function - From f8311d51260c33f20fb2f56a2781858bf1680375 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 24 Nov 2022 02:59:06 -0600 Subject: [PATCH 09/13] do all the renaming --- Mathlib/Algebra/Group/InjSurj.lean | 93 ++++++++++++++++++------------ 1 file changed, 57 insertions(+), 36 deletions(-) diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean index cbf28ad80f39d..23dfb77ed70ee 100644 --- a/Mathlib/Algebra/Group/InjSurj.lean +++ b/Mathlib/Algebra/Group/InjSurj.lean @@ -14,13 +14,13 @@ This file provides definitions that are meant to deal with situations such as the following: Suppose that `G` is a group, and `H` is a type endowed with -`has_one H`, `has_mul H`, and `has_inv H`. +`One H`, `Mul H`, and `Inv H`. Suppose furthermore, that `f : G → H` is a surjective map that respects the multiplication, and the unit elements. Then `H` satisfies the group axioms. -The relevant definition in this case is `function.surjective.group`. -Dually, there is also `function.injective.group`. +The relevant definition in this case is `Function.Surjective.group`. +Dually, there is also `Function.Injective.group`. And there are versions for (additive) (commutative) semigroups/monoids. -/ @@ -44,6 +44,7 @@ protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : Semigroup M₁ := { ‹Mul M₁› with mul_assoc := fun x y z => hf <| by erw [mul, mul, mul, mul, mul_assoc] } #align function.injective.semigroup Function.Injective.semigroup +#align function.injective.add_semigroup Function.Injective.addSemigroup /-- A type endowed with `*` is a commutative semigroup, if it admits an injective map that preserves `*` to a commutative semigroup. See note [reducible non-instances]. -/ @@ -53,6 +54,7 @@ protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injec (mul : ∀ x y, f (x * y) = f x * f y) : CommSemigroup M₁ := { hf.semigroup f mul with mul_comm := fun x y => hf <| by erw [mul, mul, mul_comm] } #align function.injective.comm_semigroup Function.Injective.commSemigroup +#align function.injective.add_comm_semigroup Function.Injective.addCommSemigroup /-- A type endowed with `*` is a left cancel semigroup, if it admits an injective map that preserves `*` to a left cancel semigroup. See note [reducible non-instances]. -/ @@ -81,8 +83,8 @@ protected def rightCancelSemigroup [RightCancelSemigroup M₂] (f : M₁ → M variable [One M₁] -/-- A type endowed with `1` and `*` is a mul_one_class, if it admits an injective map that -preserves `1` and `*` to a mul_one_class. See note [reducible non-instances]. -/ +/-- A type endowed with `1` and `*` is a `MulOneClass`, if it admits an injective map that +preserves `1` and `*` to a `MulOneClass`. See note [reducible non-instances]. -/ @[reducible, to_additive "A type endowed with `0` and `+` is an add_zero_class, if it admits an injective map that preserves `0` and `+` to an add_zero_class."] protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) @@ -91,6 +93,7 @@ protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective one_mul := fun x => hf <| by erw [mul, one, one_mul], mul_one := fun x => hf <| by erw [mul, one, mul_one] } #align function.injective.mul_one_class Function.Injective.mulOneClass +#align function.injective.add_zero_class Function.Injective.addZeroClass variable [Pow M₁ ℕ] @@ -104,6 +107,7 @@ protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : npow_zero := fun x => hf <| by erw [npow, one, pow_zero], npow_succ := fun n x => hf <| by erw [npow, pow_succ, mul, npow] } #align function.injective.monoid Function.Injective.monoid +#align function.injective.add_monoid Function.Injective.addMonoid /-- A type endowed with `0`, `1` and `+` is an additive monoid with one, if it admits an injective map that preserves `0`, `1` and `+` to an additive monoid with one. @@ -128,10 +132,10 @@ protected def leftCancelMonoid [LeftCancelMonoid M₂] (f : M₁ → M₂) (hf : (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : LeftCancelMonoid M₁ := { hf.leftCancelSemigroup f mul, hf.monoid f one mul npow with } #align function.injective.left_cancel_monoid Function.Injective.leftCancelMonoid +#align function.injective.add_left_cancel_monoid Function.Injective.addLeftCancelMonoid -/-- A type endowed with `1` and `*` is a right cancel monoid, -if it admits an injective map that preserves `1` and `*` to a right cancel monoid. -See note [reducible non-instances]. -/ +/-- A type endowed with `1` and `*` is a right cancel monoid, if it admits an injective map that +preserves `1` and `*` to a right cancel monoid. See note [reducible non-instances]. -/ @[reducible, to_additive "A type endowed with `0` and `+` is an additive left cancel monoid,if it admits an injective map that preserves `0` and `+` to an additive left cancel monoid."] protected def rightCancelMonoid [RightCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) @@ -139,6 +143,7 @@ protected def rightCancelMonoid [RightCancelMonoid M₂] (f : M₁ → M₂) (hf (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : RightCancelMonoid M₁ := { hf.rightCancelSemigroup f mul, hf.monoid f one mul npow with } #align function.injective.right_cancel_monoid Function.Injective.rightCancelMonoid +#align function.injective.add_right_cancel_monoid Function.Injective.addRightCancelMonoid /-- A type endowed with `1` and `*` is a cancel monoid, if it admits an injective map that preserves `1` and `*` to a cancel monoid. See note [reducible non-instances]. -/ @@ -148,7 +153,7 @@ protected def cancelMonoid [CancelMonoid M₂] (f : M₁ → M₂) (hf : Injecti (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelMonoid M₁ := { hf.leftCancelMonoid f one mul npow, hf.rightCancelMonoid f one mul npow with } -#align function.injective.cancel_monoid Function.Injective.cancelMonoid +#align function.injective.add_cancel_monoid Function.Injective.addCancelMonoid /-- A type endowed with `1` and `*` is a commutative monoid, if it admits an injective map that preserves `1` and `*` to a commutative monoid. See note [reducible non-instances]. -/ @@ -159,6 +164,7 @@ protected def commMonoid [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f CommMonoid M₁ := { hf.commSemigroup f mul, hf.monoid f one mul npow with } #align function.injective.comm_monoid Function.Injective.commMonoid +#align function.injective.add_comm_monoid Function.Injective.addCommMonoid /-- A type endowed with `1` and `*` is a cancel commutative monoid, if it admits an injective map that preserves `1` and `*` to a cancel commutative monoid. See note [reducible non-instances]. -/ @@ -169,25 +175,27 @@ protected def cancelCommMonoid [CancelCommMonoid M₂] (f : M₁ → M₂) (hf : (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelCommMonoid M₁ := { hf.leftCancelSemigroup f mul, hf.commMonoid f one mul npow with } #align function.injective.cancel_comm_monoid Function.Injective.cancelCommMonoid +#align function.injective.add_cancel_comm_monoid Function.Injective.addCancelCommMonoid /-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type which has an involutive inversion. See note [reducible non-instances] -/ @[reducible, to_additive "A type has an involutive negation if it admits a surjective map that -preserves `⁻¹` to a type which has an involutive inversion."] +preserves `-` to a type which has an involutive negation."] protected def hasInvolutiveInv {M₁ : Type _} [Inv M₁] [HasInvolutiveInv M₂] (f : M₁ → M₂) (hf : Injective f) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : HasInvolutiveInv M₁ where inv := Inv.inv inv_inv x := hf <| by rw [inv, inv, inv_inv] #align function.injective.has_involutive_inv Function.Injective.hasInvolutiveInv +#align function.injective.has_involutive_neg Function.Injective.hasInvolutiveNeg variable [Inv M₁] [Div M₁] [Pow 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`. See note [reducible non-instances]. -/ +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivInvMonoid` if it admits an injective map +that preserves `1`, `*`, `⁻¹`, and `/` to a `DivInvMonoid`. See note [reducible non-instances]. -/ @[reducible, to_additive subNegMonoid "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`.\nThis version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and -`[has_smul ℤ M₁]` arguments."] +`SubNegMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to +a `SubNegMonoid`. This version takes custom `nsmul` and `zsmul` as `[SMul ℕ M₁]` and `[SMul ℤ M₁]` +arguments."] protected def divInvMonoid [DivInvMonoid 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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) @@ -199,14 +207,14 @@ protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injecti zpow_neg' := fun n x => hf <| by erw [zpow, zpow_negSucc, inv, zpow, zpow_ofNat], div_eq_mul_inv := fun x y => hf <| by erw [div, mul, inv, div_eq_mul_inv] } #align function.injective.div_inv_monoid Function.Injective.divInvMonoid - -/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_monoid` if it admits an injective map -that preserves `1`, `*`, `⁻¹`, and `/` to a `division_monoid`. See note [reducible non-instances]-/ - -@[reducible, to_additive "A type endowed with `0`, `+`, unary `-`, and binary `-` is a -`subtraction_monoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and binary -`-` to a `subtraction_monoid`. This version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` -and `[has_smul ℤ M₁]` arguments."] +#align function.injective.sub_neg_monoid Function.Injective.subNegMonoid + +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivisionMonoid` if it admits an injective map +that preserves `1`, `*`, `⁻¹`, and `/` to a `DivisionMonoid`. See note [reducible non-instances] -/ +@[reducible, to_additive subtractionMonoid "A type endowed with `0`, `+`, unary `-`, and binary `-` +is a `SubtractionMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and +binary `-` to a `SubtractionMonoid`. This version takes custom `nsmul` and `zsmul` as `[SMul ℕ M₁]` +and `[SMul ℤ M₁]` arguments."] protected def divisionMonoid [DivisionMonoid 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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) @@ -216,13 +224,14 @@ protected def divisionMonoid [DivisionMonoid M₂] (f : M₁ → M₂) (hf : Inj inv_eq_of_mul := fun x y h => hf <| by erw [inv, inv_eq_of_mul_eq_one_right (by erw [← mul, h, one])] } #align function.injective.division_monoid Function.Injective.divisionMonoid +#align function.injective.subtraction_monoid Function.Injective.subtractionMonoid -/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_comm_monoid` if it admits an -injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `division_comm_monoid`. +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivisionCommMonoid` if it admits an +injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `DivisionCommMonoid`. See note [reducible non-instances]. -/ @[reducible, to_additive subtractionCommMonoid "A type endowed with `0`, `+`, unary `-`, and binary -`-` is a `subtraction_comm_monoid` if it admits an injective map that preserves `0`, `+`, unary `-`, -and binary `-` to a `subtraction_comm_monoid`. This version takes custom `nsmul` and `zsmul` as +`-` is a `SubtractionCommMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, +and binary `-` to a `SubtractionCommMonoid`. This version takes custom `nsmul` and `zsmul` as `[has_smul ℕ M₁]` and `[has_smul ℤ M₁]` arguments."] protected def divisionCommMonoid [DivisionCommMonoid 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)⁻¹) @@ -230,6 +239,7 @@ protected def divisionCommMonoid [DivisionCommMonoid M₂] (f : M₁ → M₂) ( (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionCommMonoid M₁ := { hf.divisionMonoid f one mul inv div npow zpow, hf.commSemigroup f mul with } #align function.injective.division_comm_monoid Function.Injective.divisionCommMonoid +#align function.injective.subtraction_comm_monoid Function.Injective.subtractionCommMonoid /-- A type endowed with `1`, `*` and `⁻¹` is a group, if it admits an injective map that preserves `1`, `*` and `⁻¹` to a group. See note [reducible non-instances]. -/ @@ -242,6 +252,7 @@ protected def group [Group M₂] (f : M₁ → M₂) (hf : Injective f) (one : f { hf.divInvMonoid f one mul inv div npow zpow with mul_left_inv := fun x => hf <| by erw [mul, inv, mul_left_inv, one] } #align function.injective.group Function.Injective.group +#align function.injective.add_group Function.Injective.addGroup /-- A type endowed with `0`, `1` and `+` is an additive group with one, if it admits an injective map that preserves `0`, `1` and `+` to an additive group with one. See note @@ -270,6 +281,7 @@ protected def commGroup [CommGroup M₂] (f : M₁ → M₂) (hf : Injective f) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₁ := { hf.commMonoid f one mul npow, hf.group f one mul inv div npow zpow with } #align function.injective.comm_group Function.Injective.commGroup +#align function.injective.add_comm_group Function.Injective.addCommGroup end Injective @@ -290,6 +302,7 @@ protected def semigroup [Semigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) : Semigroup M₂ := { ‹Mul M₂› with mul_assoc := hf.forall₃.2 fun x y z => by simp only [← mul, mul_assoc] } #align function.surjective.semigroup Function.Surjective.semigroup +#align function.surjective.add_semigroup Function.Surjective.addSemigroup /-- A type endowed with `*` is a commutative semigroup, if it admits a surjective map that preserves `*` from a commutative semigroup. See note [reducible non-instances]. -/ @@ -300,19 +313,21 @@ protected def commSemigroup [CommSemigroup M₁] (f : M₁ → M₂) (hf : Surje { hf.semigroup f mul with mul_comm := hf.forall₂.2 fun x y => by erw [← mul, ← mul, mul_comm] } #align function.surjective.comm_semigroup Function.Surjective.commSemigroup +#align function.surjective.add_comm_semigroup Function.Surjective.addCommSemigroup variable [One M₂] -/-- A type endowed with `1` and `*` is a mul_one_class, if it admits a surjective map that preserves -`1` and `*` from a mul_one_class. See note [reducible non-instances]. -/ -@[reducible, to_additive "A type endowed with `0` and `+` is an add_zero_class, if it admits a -surjective map that preserves `0` and `+` to an add_zero_class."] +/-- A type endowed with `1` and `*` is a `MulOneClass`, if it admits a surjective map that preserves +`1` and `*` from a `MulOneClass`. See note [reducible non-instances]. -/ +@[reducible, to_additive "A type endowed with `0` and `+` is an `AddZeroClass`, if it admits a +surjective map that preserves `0` and `+` to an `AddZeroClass`."] protected def mulOneClass [MulOneClass M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₂ := { ‹One M₂›, ‹Mul M₂› with one_mul := hf.forall.2 fun x => by erw [← one, ← mul, one_mul], mul_one := hf.forall.2 fun x => by erw [← one, ← mul, mul_one] } #align function.surjective.mul_one_class Function.Surjective.mulOneClass +#align function.surjective.add_zero_class Function.Surjective.addZeroClass variable [Pow M₂ ℕ] @@ -328,6 +343,7 @@ protected def monoid [Monoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one npow_zero := hf.forall.2 fun x => by dsimp only; erw [←npow, pow_zero, ←one], npow_succ := fun n => hf.forall.2 fun x => by dsimp only; erw [←npow, pow_succ, ←npow, ←mul] } #align function.surjective.monoid Function.Surjective.monoid +#align function.surjective.add_monoid Function.Surjective.addMonoid /-- A type endowed with `0`, `1` and `+` is an additive monoid with one, if it admits a surjective map that preserves `0`, `1` and `*` from an additive monoid with one. See note @@ -353,24 +369,26 @@ protected def commMonoid [CommMonoid M₁] (f : M₁ → M₂) (hf : Surjective CommMonoid M₂ := { hf.commSemigroup f mul, hf.monoid f one mul npow with } #align function.surjective.comm_monoid Function.Surjective.commMonoid +#align function.surjective.add_comm_monoid Function.Surjective.addCommMonoid /-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type which has an involutive inversion. See note [reducible non-instances] -/ @[reducible, to_additive "A type has an involutive negation if it admits a surjective map that -preserves `⁻¹` to a type which has an involutive inversion."] +preserves `-` to a type which has an involutive negation."] protected def hasInvolutiveInv {M₂ : Type _} [Inv M₂] [HasInvolutiveInv M₁] (f : M₁ → M₂) (hf : Surjective f) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : HasInvolutiveInv M₂ where inv := Inv.inv inv_inv := hf.forall.2 fun x => by erw [← inv, ← inv, inv_inv] #align function.surjective.has_involutive_inv Function.Surjective.hasInvolutiveInv +#align function.surjective.has_involutive_neg Function.Surjective.hasInvolutiveNeg variable [Inv M₂] [Div M₂] [Pow M₂ ℤ] -/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `div_inv_monoid` if it admits a surjective map -that preserves `1`, `*`, `⁻¹`, and `/` to a `div_inv_monoid`. See note [reducible non-instances]. -/ +/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivInvMonoid` if it admits a surjective map +that preserves `1`, `*`, `⁻¹`, and `/` to a `DivInvMonoid`. See note [reducible non-instances]. -/ @[reducible, to_additive subNegMonoid "A type endowed with `0`, `+`, unary `-`, and binary `-` is a -`sub_neg_monoid` if it admits a surjective map that preserves `0`, `+`, unary `-`, and binary `-` to -a `sub_neg_monoid`."] +`SubNegMonoid` if it admits a surjective map that preserves `0`, `+`, unary `-`, and binary `-` to +a `SubNegMonoid`."] protected def divInvMonoid [DivInvMonoid 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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) @@ -386,6 +404,7 @@ protected def divInvMonoid [DivInvMonoid M₁] (f : M₁ → M₂) (hf : Surject erw [← zpow, ← zpow, zpow_negSucc, zpow_ofNat, inv], div_eq_mul_inv := hf.forall₂.2 fun x y => by erw [← inv, ← mul, ← div, div_eq_mul_inv] } #align function.surjective.div_inv_monoid Function.Surjective.divInvMonoid +#align function.surjective.sub_neg_monoid Function.Surjective.subNegMonoid /-- A type endowed with `1`, `*` and `⁻¹` is a group, if it admits a surjective map that preserves `1`, `*` and `⁻¹` to a group. See note [reducible non-instances]. -/ @@ -398,6 +417,7 @@ protected def group [Group M₁] (f : M₁ → M₂) (hf : Surjective f) (one : { hf.divInvMonoid f one mul inv div npow zpow with mul_left_inv := hf.forall.2 fun x => by erw [← inv, ← mul, mul_left_inv, one] } #align function.surjective.group Function.Surjective.group +#align function.surjective.add_group Function.Surjective.addGroup /-- A type endowed with `0`, `1`, `+` is an additive group with one, if it admits a surjective map that preserves `0`, `1`, and `+` to an additive group with one. @@ -427,6 +447,7 @@ protected def commGroup [CommGroup M₁] (f : M₁ → M₂) (hf : Surjective f) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₂ := { hf.commMonoid f one mul npow, hf.group f one mul inv div npow zpow with } #align function.surjective.comm_group Function.Surjective.commGroup +#align function.surjective.add_comm_group Function.Surjective.addCommGroup end Surjective From fe0a9766d9b11a3cb8d16b71921ae9179178ef6f Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 24 Nov 2022 03:01:01 -0600 Subject: [PATCH 10/13] fix docBlame --- Mathlib/Algebra/Group/InjSurj.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean index 23dfb77ed70ee..0b711762dd902 100644 --- a/Mathlib/Algebra/Group/InjSurj.lean +++ b/Mathlib/Algebra/Group/InjSurj.lean @@ -99,7 +99,9 @@ variable [Pow M₁ ℕ] /-- A type endowed with `1` and `*` is a monoid, if it admits an injective map that preserves `1` and `*` to a monoid. See note [reducible non-instances]. -/ -@[reducible, to_additive] +@[reducible, to_additive "A type endowed with `0` and `+` is an additive monoid, if it admits an +injective map that preserves `0` and `+` to an additive monoid. See note +[reducible non-instances]."] protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₁ := { hf.mulOneClass f one mul, hf.semigroup f mul with From cc29daae199fbf0b565376a548dfc4bd4d07333c Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 24 Nov 2022 03:06:55 -0600 Subject: [PATCH 11/13] fix > 100 chars --- Mathlib/Algebra/Group/InjSurj.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean index 0b711762dd902..b2122dd7fa12d 100644 --- a/Mathlib/Algebra/Group/InjSurj.lean +++ b/Mathlib/Algebra/Group/InjSurj.lean @@ -269,7 +269,7 @@ protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ { hf.addGroup f zero add neg sub nsmul zsmul, hf.addMonoidWithOne f zero one add nsmul nat_cast with intCast := Int.cast, - intCast_ofNat := fun n => hf (by rw [nat_cast, ←Int.cast, int_cast, Int.cast_ofNat]), --(by simp only [nat_cast, int_cast, Int.cast_ofNat]), + intCast_ofNat := fun n => hf (by rw [nat_cast, ←Int.cast, int_cast, Int.cast_ofNat]), intCast_negSucc := fun n => hf (by erw [int_cast, neg, nat_cast, Int.cast_negSucc] ) } #align function.injective.add_group_with_one Function.Injective.addGroupWithOne From 286db1153773e3e07e66cdf1b8b17b126b8080b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20W=C3=A4rn?= Date: Thu, 24 Nov 2022 12:18:21 +0100 Subject: [PATCH 12/13] casing in comments --- Mathlib/Algebra/Group/InjSurj.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean index b2122dd7fa12d..d99c03d3c0ee6 100644 --- a/Mathlib/Algebra/Group/InjSurj.lean +++ b/Mathlib/Algebra/Group/InjSurj.lean @@ -85,8 +85,8 @@ variable [One M₁] /-- A type endowed with `1` and `*` is a `MulOneClass`, if it admits an injective map that preserves `1` and `*` to a `MulOneClass`. See note [reducible non-instances]. -/ -@[reducible, to_additive "A type endowed with `0` and `+` is an add_zero_class, if it admits an -injective map that preserves `0` and `+` to an add_zero_class."] +@[reducible, to_additive "A type endowed with `0` and `+` is an `AddZeroClass`, if it admits an +injective map that preserves `0` and `+` to an `AddZeroClass`."] protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₁ := { ‹One M₁›, ‹Mul M₁› with @@ -234,7 +234,7 @@ See note [reducible non-instances]. -/ @[reducible, to_additive subtractionCommMonoid "A type endowed with `0`, `+`, unary `-`, and binary `-` is a `SubtractionCommMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to a `SubtractionCommMonoid`. This version takes custom `nsmul` and `zsmul` as -`[has_smul ℕ M₁]` and `[has_smul ℤ M₁]` arguments."] +`[SMul ℕ M₁]` and `[SMul ℤ M₁]` arguments."] protected def divisionCommMonoid [DivisionCommMonoid 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) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) From f440cbce812e040ee96898e61ba2393319703997 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 24 Nov 2022 12:08:28 -0600 Subject: [PATCH 13/13] fix --- Mathlib/Algebra/Group/Defs.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 7f9fff43d1f58..143536d63fb53 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -616,6 +616,8 @@ class AddCancelCommMonoid (M : Type u) extends AddLeftCancelMonoid M, AddCommMon @[to_additive] class CancelCommMonoid (M : Type u) extends LeftCancelMonoid M, CommMonoid M +attribute [to_additive AddCancelCommMonoid.toAddCommMonoid] CancelCommMonoid.toCommMonoid + -- see Note [lower instance priority] @[to_additive CancelCommMonoid.toAddCancelMonoid] instance (priority := 100) CancelCommMonoid.toCancelMonoid (M : Type u) [CancelCommMonoid M] :