Mathlib.Algebra.Group.InjSurj

Module docstring

{"# 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 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. And there are versions for (additive) (commutative) semigroups/monoids.

Implementation note

The nsmul and zsmul assumptions on any transfer definition for an algebraic structure involving both addition and multiplication (eg AddMonoidWithOne) is ∀ n x, f (n • x) = n • f x, which is what we would expect. However, we cannot do the same for transfer definitions built using to_additive (eg AddMonoid) as we want the multiplicative versions to be ∀ x n, f (x ^ n) = f x ^ n. As a result, we must use Function.swap when using additivised transfer definitions in non-additivised ones. ","### Injective ","### Surjective "}

Function.Injective.semigroup abbrev

[Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : Semigroup M₁

Full source

/-- A type endowed with `*` is a semigroup, if it admits an injective map that preserves `*` to
a semigroup. See note [reducible non-instances]. -/
@[to_additive "A type endowed with `+` is an additive semigroup, if it admits an
injective map that preserves `+` to an additive semigroup."]
protected abbrev 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 rw [mul, mul, mul, mul, mul_assoc] }

Lifting Semigroup Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a semigroup with multiplication $*$, and let $f : M_1 \to M_2$ be an injective function such that for all $x, y \in M_1$, $f(x * y) = f(x) * f(y)$. Then $M_1$ can be endowed with the structure of a semigroup where the multiplication is defined by $x * y := f^{-1}(f(x) * f(y))$.

Function.Injective.commMagma abbrev

[CommMagma M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : CommMagma M₁

Full source

/-- A type endowed with `*` is a commutative magma, if it admits a surjective map that preserves
`*` from a commutative magma. -/
@[to_additive -- See note [reducible non-instances]
"A type endowed with `+` is an additive commutative semigroup, if it admits
a surjective map that preserves `+` from an additive commutative semigroup."]
protected abbrev commMagma [CommMagma M₂] (f : M₁ → M₂) (hf : Injective f)
    (mul : ∀ x y, f (x * y) = f x * f y) : CommMagma M₁ where
  mul_comm x y := hf <| by rw [mul, mul, mul_comm]

Lifting Commutative Magma Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a commutative magma with multiplication $*$, and let $f : M_1 \to M_2$ be an injective function such that for all $x, y \in M_1$, $f(x * y) = f(x) * f(y)$. Then $M_1$ can be endowed with the structure of a commutative magma where the multiplication is defined by $x * y := f^{-1}(f(x) * f(y))$.

Function.Injective.commSemigroup abbrev

[CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : CommSemigroup M₁

Full source

/-- 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]. -/
@[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 abbrev commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f)
    (mul : ∀ x y, f (x * y) = f x * f y) : CommSemigroup M₁ where
  toSemigroup := hf.semigroup f mul
  __ := hf.commMagma f mul

Lifting Commutative Semigroup Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a commutative semigroup with multiplication $*$, and let $f : M_1 \to M_2$ be an injective function such that for all $x, y \in M_1$, $f(x * y) = f(x) * f(y)$. Then $M_1$ can be endowed with the structure of a commutative semigroup where the multiplication is defined by $x * y := f^{-1}(f(x) * f(y))$.

Function.Injective.leftCancelSemigroup abbrev

 [LeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) : LeftCancelSemigroup M₁

Full source

/-- 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]. -/
@[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 abbrev 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_left_cancel := fun x y z H => hf <| (mul_right_inj (f x)).1 <| by rw [← mul, ← mul, H] }

Lifting Left Cancellative Semigroup Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a left cancellative semigroup with multiplication $*$, and let $f : M_1 \to M_2$ be an injective function such that for all $x, y \in M_1$, $f(x * y) = f(x) * f(y)$. Then $M_1$ can be endowed with the structure of a left cancellative semigroup where the multiplication is defined by $x * y := f^{-1}(f(x) * f(y))$.

Function.Injective.rightCancelSemigroup abbrev

 [RightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) :
  RightCancelSemigroup M₁

Full source

/-- 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]. -/
@[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 abbrev 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_right_cancel := fun x y z H => hf <| (mul_left_inj (f y)).1 <| by rw [← mul, ← mul, H] }

Lifting Right Cancellative Semigroup Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a right cancellative semigroup with multiplication $*$, and let $f : M_1 \to M_2$ be an injective function such that for all $x, y \in M_1$, $f(x * y) = f(x) * f(y)$. Then $M_1$ can be endowed with the structure of a right cancellative semigroup where the multiplication is defined by $x * y := f^{-1}(f(x) * f(y))$.

Function.Injective.mulOneClass abbrev

 [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₁

Full source

/-- 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]. -/
@[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 abbrev 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 rw [mul, one, one_mul],
    mul_one := fun x => hf <| by rw [mul, one, mul_one] }

Lifting multiplicative identity structure along an injective homomorphism

Informal description

Let $M_1$ and $M_2$ be types, where $M_2$ is equipped with a multiplicative structure with identity (`MulOneClass`). Given an injective function $f : M_1 \to M_2$ that preserves the multiplicative identity ($f(1) = 1$) and multiplication ($f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$), then $M_1$ can be endowed with a `MulOneClass` structure induced by $f$.

Function.Injective.monoid abbrev

 [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₁

Full source

/-- 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]. -/
@[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 abbrev 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 rw [npow, one, pow_zero],
    npow_succ := fun n x => hf <| by rw [npow, pow_succ, mul, npow] }

Lifting Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a monoid and $f : M_1 \to M_2$ be an injective function that preserves the multiplicative identity ($f(1) = 1$), multiplication ($f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$), and natural number powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$). Then $M_1$ can be endowed with a monoid structure induced by $f$.

Function.Injective.addMonoidWithOne abbrev

 {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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
  (natCast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₁

Full source

/-- 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]. -/
protected abbrev 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (natCast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₁ :=
  { hf.addMonoid f zero add (swap nsmul) with
    natCast := Nat.cast,
    natCast_zero := hf (by rw [natCast, Nat.cast_zero, zero]),
    natCast_succ := fun n => hf (by rw [natCast, Nat.cast_succ, add, one, natCast]), one := 1 }

Lifting Additive Monoid with One Structure Along an Injective Homomorphism

Informal description

Let $M_1$ be a type equipped with operations $0$, $1$, $+$, natural number scalar multiplication $\cdot$, and a natural number casting function. Suppose there exists an additive monoid with one $M_2$ and an injective function $f : M_1 \to M_2$ that preserves: - zero: $f(0) = 0$, - one: $f(1) = 1$, - addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in M_1$, - scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in M_1$, - natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$. Then $M_1$ can be endowed with an additive monoid with one structure induced by $f$.

Function.Injective.leftCancelMonoid abbrev

 [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₁

Full source

/-- 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]. -/
@[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 abbrev 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 }

Lifting Left-Cancellative Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a left-cancellative monoid and $f : M_1 \to M_2$ be an injective function that preserves the multiplicative identity ($f(1) = 1$), multiplication ($f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$), and natural number powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$). Then $M_1$ can be endowed with the structure of a left-cancellative monoid induced by $f$.

Function.Injective.rightCancelMonoid abbrev

 [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₁

Full source

/-- 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]. -/
@[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 abbrev 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 }

Lifting Right-Cancellative Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a right-cancellative monoid with multiplication operation $*$, identity element $1$, and natural number power operation $x^n$. Given an injective function $f : M_1 \to M_2$ that preserves: 1. The identity: $f(1) = 1$, 2. Multiplication: $f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$, 3. Powers: $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$, then $M_1$ can be endowed with the structure of a right-cancellative monoid where the operations are defined via $f$.

Function.Injective.cancelMonoid abbrev

 [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₁

Full source

/-- 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]. -/
@[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 abbrev 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 }

Lifting Cancellative Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a cancellative monoid and $f : M_1 \to M_2$ be an injective function that preserves: 1. The multiplicative identity: $f(1) = 1$, 2. Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$, 3. Natural number powers: $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$. Then $M_1$ can be endowed with the structure of a cancellative monoid where the operations are defined via $f$.

Function.Injective.commMonoid abbrev

 [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₁

Full source

/-- 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]. -/
@[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 abbrev 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.monoid f one mul npow, hf.commSemigroup f mul with }

Lifting Commutative Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a commutative monoid and $f : M_1 \to M_2$ be an injective function that preserves the multiplicative identity ($f(1) = 1$), multiplication ($f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$), and natural number powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$). Then $M_1$ can be endowed with a commutative monoid structure induced by $f$.

Function.Injective.addCommMonoidWithOne abbrev

 {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ M₁] [NatCast M₁] [AddCommMonoidWithOne 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
  (natCast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne M₁

Full source

/-- A type endowed with `0`, `1` and `+` is an additive commutative monoid with one, if it admits an
injective map that preserves `0`, `1` and `+` to an additive commutative monoid with one.
See note [reducible non-instances]. -/
protected abbrev addCommMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ M₁] [NatCast M₁]
    [AddCommMonoidWithOne 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (natCast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne M₁ where
  __ := hf.addMonoidWithOne f zero one add nsmul natCast
  __ := hf.addCommMonoid _ zero add (swap nsmul)

Lifting Additive Commutative Monoid with One Structure Along an Injective Homomorphism

Informal description

Let $M_1$ be a type equipped with operations $0$, $1$, $+$, natural number scalar multiplication $\cdot$, and a natural number casting function. Suppose there exists an additive commutative monoid with one $M_2$ and an injective function $f : M_1 \to M_2$ that preserves: - zero: $f(0) = 0$, - one: $f(1) = 1$, - addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in M_1$, - scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in M_1$, - natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$. Then $M_1$ can be endowed with an additive commutative monoid with one structure induced by $f$.

Function.Injective.cancelCommMonoid abbrev

 [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₁

Full source

/-- 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]. -/
@[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 abbrev 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 }

Lifting Cancellative Commutative Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a cancellative commutative monoid and $f : M_1 \to M_2$ be an injective function that preserves the multiplicative identity ($f(1) = 1$), multiplication ($f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$), and natural number powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$). Then $M_1$ can be endowed with the structure of a cancellative commutative monoid induced by $f$.

Function.Injective.involutiveInv abbrev

 {M₁ : Type*} [Inv M₁] [InvolutiveInv M₂] (f : M₁ → M₂) (hf : Injective f) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) :
  InvolutiveInv M₁

Full source

/-- 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] -/
@[to_additive
"A type has an involutive negation if it admits a surjective map that
preserves `-` to a type which has an involutive negation."]
protected abbrev involutiveInv {M₁ : Type*} [Inv M₁] [InvolutiveInv M₂] (f : M₁ → M₂)
    (hf : Injective f) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₁ where
  inv := Inv.inv
  inv_inv x := hf <| by rw [inv, inv, inv_inv]

Injective Function Lifts Involutive Inversion Structure

Informal description

Let $M_1$ be a type equipped with an inversion operation, and $M_2$ be a type with an involutive inversion. Given an injective function $f \colon M_1 \to M_2$ such that $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$, then $M_1$ inherits the structure of an involutive inversion from $M_2$.

Function.Injective.invOneClass abbrev

 [InvOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) : InvOneClass M₁

Full source

/-- A type endowed with `1` and `⁻¹` is a `InvOneClass`, if it admits an injective map that
preserves `1` and `⁻¹` to a `InvOneClass`.  See note [reducible non-instances]. -/
@[to_additive
"A type endowed with `0` and unary `-` is an `NegZeroClass`, if it admits an
injective map that preserves `0` and unary `-` to an `NegZeroClass`."]
protected abbrev invOneClass [InvOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1)
    (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) : InvOneClass M₁ :=
  { ‹One M₁›, ‹Inv M₁› with
    inv_one := hf <| by rw [inv, one, inv_one] }

Injective Function Lifts Inverse-One Class Structure

Informal description

Let $M_1$ be a type with operations $1$ and $^{-1}$, and $M_2$ be an `InvOneClass`. If there exists an injective function $f : M_1 \to M_2$ such that $f(1) = 1$ and $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$, then $M_1$ inherits the structure of an `InvOneClass` from $M_2$.

Function.Injective.divInvMonoid abbrev

 [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₁

Full source

/-- 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]. -/
@[to_additive subNegMonoid
"A type endowed with `0`, `+`, unary `-`, and binary `-` is a
`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 abbrev 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 rw [zpow, zpow_zero, one],
    zpow_succ' := fun n x => hf <| by rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast],
    zpow_neg' := fun n x => hf <| by rw [zpow, zpow_negSucc, inv, zpow, zpow_natCast],
    div_eq_mul_inv := fun x y => hf <| by rw [div, mul, inv, div_eq_mul_inv] }

Lifting Division-Inversion Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a division-inversion monoid and $f \colon M_1 \to M_2$ be an injective function that satisfies the following properties: 1. $f(1) = 1$ (preserves the multiplicative identity), 2. $f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$ (preserves multiplication), 3. $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$ (preserves inversion), 4. $f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$ (preserves division), 5. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$ (preserves natural number powers), 6. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$ (preserves integer powers). Then $M_1$ can be endowed with a division-inversion monoid structure induced by $f$.

Function.Injective.divInvOneMonoid abbrev

 [DivInvOneMonoid 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) : DivInvOneMonoid M₁

Full source

/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivInvOneMonoid` if it admits an injective
map that preserves `1`, `*`, `⁻¹`, and `/` to a `DivInvOneMonoid`. See note
[reducible non-instances]. -/
@[to_additive
"A type endowed with `0`, `+`, unary `-`, and binary `-` is a
`SubNegZeroMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and binary
`-` to a `SubNegZeroMonoid`. This version takes custom `nsmul` and `zsmul` as `[SMul ℕ M₁]` and
`[SMul ℤ M₁]` arguments."]
protected abbrev divInvOneMonoid [DivInvOneMonoid 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) : DivInvOneMonoid M₁ :=
  { hf.divInvMonoid f one mul inv div npow zpow, hf.invOneClass f one inv with }

Lifting Division-Inversion-One Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a division-inversion-one monoid and $f \colon M_1 \to M_2$ be an injective function that satisfies: 1. $f(1) = 1$ (preserves the multiplicative identity), 2. $f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$ (preserves multiplication), 3. $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$ (preserves inversion), 4. $f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$ (preserves division), 5. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$ (preserves natural number powers), 6. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$ (preserves integer powers). Then $M_1$ can be endowed with a division-inversion-one monoid structure induced by $f$.

Function.Injective.divisionMonoid abbrev

 [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₁

Full source

/-- 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] -/
@[to_additive
"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 abbrev 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.involutiveInv f inv with
    mul_inv_rev := fun x y => hf <| by rw [inv, mul, mul_inv_rev, mul, inv, inv],
    inv_eq_of_mul := fun x y h => hf <| by
      rw [inv, inv_eq_of_mul_eq_one_right (by rw [← mul, h, one])] }

Lifting Division Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a division monoid and $f \colon M_1 \to M_2$ be an injective function that satisfies the following properties: 1. $f(1) = 1$ (preserves the multiplicative identity), 2. $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$ (preserves multiplication), 3. $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$ (preserves inversion), 4. $f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$ (preserves division), 5. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$ (preserves natural number powers), 6. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$ (preserves integer powers). Then $M_1$ can be endowed with a division monoid structure induced by $f$.

Function.Injective.divisionCommMonoid abbrev

 [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₁

Full source

/-- 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]. -/
@[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
`[SMul ℕ M₁]` and `[SMul ℤ M₁]` arguments."]
protected abbrev 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 }

Lifting Commutative Division Monoid Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a commutative division monoid and $f \colon M_1 \to M_2$ be an injective function that satisfies: 1. $f(1) = 1$ (preserves the multiplicative identity), 2. $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$ (preserves multiplication), 3. $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$ (preserves inversion), 4. $f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$ (preserves division), 5. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$ (preserves natural number powers), 6. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$ (preserves integer powers). Then $M_1$ can be endowed with a commutative division monoid structure induced by $f$.

Function.Injective.group abbrev

 [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₁

Full source

/-- 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]. -/
@[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 abbrev 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
    inv_mul_cancel := fun x => hf <| by rw [mul, inv, inv_mul_cancel, one] }

Lifting Group Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a group and $f \colon M_1 \to M_2$ be an injective function that satisfies the following properties: 1. $f(1) = 1$ (preserves the identity element), 2. $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$ (preserves multiplication), 3. $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$ (preserves inversion), 4. $f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$ (preserves division), 5. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$ (preserves natural number powers), 6. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$ (preserves integer powers). Then $M_1$ can be endowed with a group structure induced by $f$.

Function.Injective.addGroupWithOne abbrev

 {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 : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
  (intCast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₁

Full source

/-- 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]. -/
protected abbrev 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
    (intCast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₁ :=
  { hf.addGroup f zero add neg sub (swap nsmul) (swap zsmul),
    hf.addMonoidWithOne f zero one add nsmul natCast with
    intCast := Int.cast,
    intCast_ofNat := fun n => hf (by rw [natCast, intCast, Int.cast_natCast]),
    intCast_negSucc := fun n => hf (by rw [intCast, neg, natCast, Int.cast_negSucc] ) }

Lifting Additive Group with One Structure Along an Injective Homomorphism

Informal description

Let $M_1$ be a type equipped with operations $0$, $1$, $+$, natural number scalar multiplication $\cdot$, negation $-$, subtraction $-$, integer scalar multiplication $\cdot$, and natural and integer casting functions. Suppose there exists an additive group with one $M_2$ and an injective function $f \colon M_1 \to M_2$ that preserves: - zero: $f(0) = 0$, - one: $f(1) = 1$, - addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in M_1$, - negation: $f(-x) = -f(x)$ for all $x \in M_1$, - subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in M_1$, - natural scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in M_1$, - integer scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in M_1$, - natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$, - integer casting: $f(n) = n$ for all $n \in \mathbb{Z}$. Then $M_1$ can be endowed with an additive group with one structure induced by $f$.

Function.Injective.commGroup abbrev

 [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₁

Full source

/-- 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]. -/
@[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 abbrev 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 }

Lifting Commutative Group Structure Along an Injective Homomorphism

Informal description

Let $M_2$ be a commutative group and $f \colon M_1 \to M_2$ be an injective function that satisfies the following properties: 1. $f(1) = 1$ (preserves the identity element), 2. $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$ (preserves multiplication), 3. $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$ (preserves inversion), 4. $f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$ (preserves division), 5. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$ (preserves natural number powers), 6. $f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$ (preserves integer powers). Then $M_1$ can be endowed with a commutative group structure induced by $f$.

Function.Injective.addCommGroupWithOne abbrev

 {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁] [SMul ℤ M₁] [NatCast M₁] [IntCast M₁]
  [AddCommGroupWithOne 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
  (intCast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne M₁

Full source

/-- A type endowed with `0`, `1` and `+` is an additive commutative group with one, if it admits an
injective map that preserves `0`, `1` and `+` to an additive commutative group with one.
See note [reducible non-instances]. -/
protected abbrev addCommGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁]
    [SMul ℤ M₁] [NatCast M₁] [IntCast M₁] [AddCommGroupWithOne 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
    (intCast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne M₁ :=
  { hf.addGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast,
    hf.addCommMonoid _ zero add (swap nsmul) with }

Lifting Additive Commutative Group with One Structure via Injective Homomorphism

Informal description

Let $M_1$ be a type equipped with operations $0$, $1$, $+$, natural number scalar multiplication $\cdot$, negation $-$, subtraction $-$, integer scalar multiplication $\cdot$, and natural and integer casting functions. Suppose there exists an additive commutative group with one $M_2$ and an injective function $f \colon M_1 \to M_2$ that preserves: - zero: $f(0) = 0$, - one: $f(1) = 1$, - addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in M_1$, - negation: $f(-x) = -f(x)$ for all $x \in M_1$, - subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in M_1$, - natural scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in M_1$, - integer scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in M_1$, - natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$, - integer casting: $f(n) = n$ for all $n \in \mathbb{Z}$. Then $M_1$ can be endowed with an additive commutative group with one structure induced by $f$.

Function.Surjective.semigroup abbrev

[Semigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) : Semigroup M₂

Full source

/-- A type endowed with `*` is a semigroup, if it admits a surjective map that preserves `*` from a
semigroup. See note [reducible non-instances]. -/
@[to_additive
"A type endowed with `+` is an additive semigroup, if it admits a
surjective map that preserves `+` from an additive semigroup."]
protected abbrev 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] }

Lifting Semigroup Structure via Surjective Homomorphism

Informal description

Let $M_1$ be a semigroup and $f : M_1 \to M_2$ a surjective map to a type $M_2$ equipped with a multiplication operation. If $f$ preserves multiplication, i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$, then $M_2$ inherits a semigroup structure from $M_1$ via $f$.

Function.Surjective.commMagma abbrev

[CommMagma M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) : CommMagma M₂

Full source

/-- 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]. -/
@[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 abbrev commMagma [CommMagma M₁] (f : M₁ → M₂) (hf : Surjective f)
    (mul : ∀ x y, f (x * y) = f x * f y) : CommMagma M₂ where
  mul_comm := hf.forall₂.2 fun x y => by rw [← mul, ← mul, mul_comm]

Lifting Commutative Magma Structure via Surjective Homomorphism

Informal description

Let $M_1$ be a commutative magma and $f : M_1 \to M_2$ a surjective map to a type $M_2$ equipped with a multiplication operation. If $f$ preserves multiplication, i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$, then $M_2$ inherits a commutative magma structure from $M_1$ via $f$.

Function.Surjective.commSemigroup abbrev

 [CommSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ x y, f (x * y) = f x * f y) : CommSemigroup M₂

Full source

/-- 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]. -/
@[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 abbrev commSemigroup [CommSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f)
    (mul : ∀ x y, f (x * y) = f x * f y) : CommSemigroup M₂ where
  toSemigroup := hf.semigroup f mul
  __ := hf.commMagma f mul

Lifting Commutative Semigroup Structure via Surjective Homomorphism

Informal description

Let $M_1$ be a commutative semigroup and $f : M_1 \to M_2$ a surjective map to a type $M_2$ equipped with a multiplication operation. If $f$ preserves multiplication, i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$, then $M_2$ inherits a commutative semigroup structure from $M_1$ via $f$.

Function.Surjective.mulOneClass abbrev

 [MulOneClass M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
  MulOneClass M₂

Full source

/-- 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]. -/
@[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 abbrev 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 rw [← one, ← mul, one_mul],
    mul_one := hf.forall.2 fun x => by rw [← one, ← mul, mul_one] }

Lifting of Multiplicative Structure with Identity via Surjective Map

Informal description

Let $M_1$ be a type with a multiplicative structure and identity (i.e., a `MulOneClass`), and let $f : M_1 \to M_2$ be a surjective map to another type $M_2$ equipped with operations $1$ and $*$. If $f$ preserves the multiplicative identity ($f(1) = 1$) and the multiplication operation ($f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$), then $M_2$ inherits a `MulOneClass` structure from $M_1$ via $f$.

Function.Surjective.monoid abbrev

 [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₂

Full source

/-- 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]. -/
@[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 `[SMul ℕ M₂]` argument."]
protected abbrev 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 rw [← npow, pow_zero, ← one],
    npow_succ := fun n => hf.forall.2 fun x => by
      rw [← npow, pow_succ, ← npow, ← mul] }

Lifting Monoid Structure via Surjective Homomorphism

Informal description

Let $M_1$ be a monoid and $f : M_1 \to M_2$ a surjective map to a type $M_2$ equipped with operations $1$, $*$, and $(\cdot)^n$ (for $n \in \mathbb{N}$). If $f$ preserves the multiplicative identity ($f(1) = 1$), multiplication ($f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$), and powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$), then $M_2$ inherits a monoid structure from $M_1$ via $f$.

Function.Surjective.addMonoidWithOne abbrev

 {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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
  (natCast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₂

Full source

/-- 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]. -/
protected abbrev 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (natCast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₂ :=
  { hf.addMonoid f zero add (swap nsmul) with
    natCast := Nat.cast,
    natCast_zero := by rw [← natCast, Nat.cast_zero, zero]
    natCast_succ := fun n => by rw [← natCast, Nat.cast_succ, add, one, natCast]
    one := 1 }

Lifting Additive Monoid with One Structure via Surjective Homomorphism

Informal description

Let $M_1$ be an additive monoid with one, and let $M_2$ be a type equipped with operations $0$, $1$, $+$, natural number scalar multiplication $\cdot$, and a natural number embedding $\mathbb{N} \to M_2$. Given a surjective map $f : M_1 \to M_2$ that preserves: - the zero element: $f(0) = 0$, - the one element: $f(1) = 1$, - addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in M_1$, - scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in M_1$, - the natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$, then $M_2$ inherits the structure of an additive monoid with one from $M_1$ via $f$.

Function.Surjective.commMonoid abbrev

 [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₂

Full source

/-- 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]. -/
@[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 abbrev 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 }

Lifting Commutative Monoid Structure via Surjective Homomorphism

Informal description

Let $M_1$ be a commutative monoid and $f : M_1 \to M_2$ a surjective map to a type $M_2$ equipped with operations $1$, $*$, and $(\cdot)^n$ (for $n \in \mathbb{N}$). If $f$ preserves the multiplicative identity ($f(1) = 1$), multiplication ($f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$), and powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$), then $M_2$ inherits a commutative monoid structure from $M_1$ via $f$.

Function.Surjective.addCommMonoidWithOne abbrev

 {M₂} [Zero M₂] [One M₂] [Add M₂] [SMul ℕ M₂] [NatCast M₂] [AddCommMonoidWithOne 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
  (natCast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne M₂

Full source

/-- 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]. -/
protected abbrev addCommMonoidWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [SMul ℕ M₂] [NatCast M₂]
    [AddCommMonoidWithOne 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (natCast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne M₂ where
  __ := hf.addMonoidWithOne f zero one add nsmul natCast
  __ := hf.addCommMonoid _ zero add (swap nsmul)

Lifting Additive Commutative Monoid with One via Surjective Homomorphism

Informal description

Let $M_1$ be an additive commutative monoid with one, and let $M_2$ be a type equipped with operations $0$, $1$, $+$, natural number scalar multiplication $\cdot$, and a natural number embedding $\mathbb{N} \to M_2$. Given a surjective map $f : M_1 \to M_2$ that preserves: - the zero element: $f(0) = 0$, - the one element: $f(1) = 1$, - addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in M_1$, - scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in M_1$, - the natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$, then $M_2$ inherits the structure of an additive commutative monoid with one from $M_1$ via $f$.

Function.Surjective.involutiveInv abbrev

 {M₂ : Type*} [Inv M₂] [InvolutiveInv M₁] (f : M₁ → M₂) (hf : Surjective f) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) :
  InvolutiveInv M₂

Full source

/-- 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] -/
@[to_additive
"A type has an involutive negation if it admits a surjective map that
preserves `-` to a type which has an involutive negation."]
protected abbrev involutiveInv {M₂ : Type*} [Inv M₂] [InvolutiveInv M₁] (f : M₁ → M₂)
    (hf : Surjective f) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₂ where
  inv := Inv.inv
  inv_inv := hf.forall.2 fun x => by rw [← inv, ← inv, inv_inv]

Lifting Involutive Inversion via Surjective Map

Informal description

Let $M_1$ be a type with an involutive inversion operation (i.e., $(x^{-1})^{-1} = x$ for all $x \in M_1$), and let $M_2$ be a type equipped with an inversion operation. Given a surjective function $f : M_1 \to M_2$ that preserves inversion (i.e., $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$), then $M_2$ also has an involutive inversion operation.

Function.Surjective.divInvMonoid abbrev

 [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₂

Full source

/-- 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]. -/
@[to_additive subNegMonoid
"A type endowed with `0`, `+`, unary `-`, and binary `-` is a
`SubNegMonoid` if it admits a surjective map that preserves `0`, `+`, unary `-`, and binary `-` to
a `SubNegMonoid`."]
protected abbrev 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 rw [← zpow, zpow_zero, ← one],
    zpow_succ' := fun n => hf.forall.2 fun x => by
      rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul],
    zpow_neg' := fun n => hf.forall.2 fun x => by
      rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv],
    div_eq_mul_inv := hf.forall₂.2 fun x y => by rw [← inv, ← mul, ← div, div_eq_mul_inv] }

Lifting Division-Inversion Monoid Structure via Surjective Homomorphism

Informal description

Let $M_1$ be a division-inversion monoid and $f : M_1 \to M_2$ a surjective map to a type $M_2$ equipped with operations $1$, $*$, $(\cdot)^{-1}$, $/$, $(\cdot)^n$ (for $n \in \mathbb{N}$), and $(\cdot)^n$ (for $n \in \mathbb{Z}$). If $f$ preserves: - the multiplicative identity ($f(1) = 1$), - multiplication ($f(x * y) = f(x) * f(y)$ for all $x, y \in M_1$), - inversion ($f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$), - division ($f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$), - natural powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$), and - integer powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$), then $M_2$ inherits a division-inversion monoid structure from $M_1$ via $f$.

Function.Surjective.group abbrev

 [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₂

Full source

/-- 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]. -/
@[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 abbrev 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
    inv_mul_cancel := hf.forall.2 fun x => by rw [← inv, ← mul, inv_mul_cancel, one] }

Lifting Group Structure via Surjective Homomorphism

Informal description

Let $M_1$ be a group and $f : M_1 \to M_2$ a surjective map to a type $M_2$ equipped with operations $1$, $\cdot$, $^{-1}$, $/$, $(\cdot)^n$ (for $n \in \mathbb{N}$), and $(\cdot)^n$ (for $n \in \mathbb{Z}$). If $f$ preserves: - the multiplicative identity ($f(1) = 1$), - multiplication ($f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$), - inversion ($f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$), - division ($f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$), - natural powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$), and - integer powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$), then $M_2$ inherits a group structure from $M_1$ via $f$.

Function.Surjective.addGroupWithOne abbrev

 {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 : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
  (intCast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₂

Full source

/-- 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 abbrev 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
    (intCast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₂ :=
  { hf.addMonoidWithOne f zero one add nsmul natCast,
    hf.addGroup f zero add neg sub (swap nsmul) (swap zsmul) with
    intCast := Int.cast,
    intCast_ofNat := fun n => by rw [← intCast, Int.cast_natCast, natCast],
    intCast_negSucc := fun n => by
      rw [← intCast, Int.cast_negSucc, neg, natCast] }

Lifting Additive Group with One Structure via Surjective Homomorphism

Informal description

Let $M_1$ be an additive group with one, and let $M_2$ be a type equipped with operations $0$, $1$, $+$, $-$, $-$, natural number scalar multiplication $\cdot$, integer scalar multiplication $\cdot$, and natural and integer embeddings $\mathbb{N} \to M_2$ and $\mathbb{Z} \to M_2$. Given a surjective map $f : M_1 \to M_2$ that preserves: - the zero element: $f(0) = 0$, - the one element: $f(1) = 1$, - addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in M_1$, - negation: $f(-x) = -f(x)$ for all $x \in M_1$, - subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in M_1$, - natural scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in M_1$, - integer scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in M_1$, - natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$, - integer embedding: $f(n) = n$ for all $n \in \mathbb{Z}$, then $M_2$ inherits the structure of an additive group with one from $M_1$ via $f$.

Function.Surjective.commGroup abbrev

 [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₂

Full source

/-- 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]. -/
@[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 abbrev 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 }

Lifting Commutative Group Structure via Surjective Homomorphism

Informal description

Let $M_1$ be a commutative group and $f : M_1 \to M_2$ a surjective map to a type $M_2$ equipped with operations $1$, $\cdot$, $^{-1}$, $/$, $(\cdot)^n$ (for $n \in \mathbb{N}$), and $(\cdot)^n$ (for $n \in \mathbb{Z}$). If $f$ preserves: - the multiplicative identity ($f(1) = 1$), - multiplication ($f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_1$), - inversion ($f(x^{-1}) = (f(x))^{-1}$ for all $x \in M_1$), - division ($f(x / y) = f(x) / f(y)$ for all $x, y \in M_1$), - natural powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{N}$), and - integer powers ($f(x^n) = f(x)^n$ for all $x \in M_1$ and $n \in \mathbb{Z}$), then $M_2$ inherits a commutative group structure from $M_1$ via $f$.

Function.Surjective.addCommGroupWithOne abbrev

 {M₂} [Zero M₂] [One M₂] [Add M₂] [Neg M₂] [Sub M₂] [SMul ℕ M₂] [SMul ℤ M₂] [NatCast M₂] [IntCast M₂]
  [AddCommGroupWithOne 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
  (intCast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne M₂

Full source

/-- A type endowed with `0`, `1`, `+` is an additive commutative group with one, if it admits a
surjective map that preserves `0`, `1`, and `+` to an additive commutative group with one.
See note [reducible non-instances]. -/
protected abbrev addCommGroupWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [Neg M₂] [Sub M₂] [SMul ℕ M₂]
    [SMul ℤ M₂] [NatCast M₂] [IntCast M₂] [AddCommGroupWithOne 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 : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
    (intCast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne M₂ :=
  { hf.addGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast,
    hf.addCommMonoid _ zero add (swap nsmul) with }

Lifting Additive Commutative Group with One Structure via Surjective Homomorphism

Informal description

Let $M_1$ be an additive commutative group with one, and let $M_2$ be a type equipped with operations $0$, $1$, $+$, $-$, $-$, natural number scalar multiplication $\cdot$, integer scalar multiplication $\cdot$, and natural and integer embeddings $\mathbb{N} \to M_2$ and $\mathbb{Z} \to M_2$. Given a surjective map $f : M_1 \to M_2$ that preserves: - the zero element: $f(0) = 0$, - the one element: $f(1) = 1$, - addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in M_1$, - negation: $f(-x) = -f(x)$ for all $x \in M_1$, - subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in M_1$, - natural scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in M_1$, - integer scalar multiplication: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in M_1$, - natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$, - integer embedding: $f(n) = n$ for all $n \in \mathbb{Z}$, then $M_2$ inherits the structure of an additive commutative group with one from $M_1$ via $f$.