Mathlib.Algebra.GroupWithZero.InjSurj

Function.Injective.mulZeroClass abbrev

 [Mul M₀'] [Zero M₀'] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (mul : ∀ a b, f (a * b) = f a * f b) :
  MulZeroClass M₀'

Full source

/-- Pull back a `MulZeroClass` instance along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.mulZeroClass [Mul M₀'] [Zero M₀'] (f : M₀' → M₀)
    (hf : Injective f) (zero : f 0 = 0) (mul : ∀ a b, f (a * b) = f a * f b) :
    MulZeroClass M₀' where
  mul := (· * ·)
  zero := 0
  zero_mul a := hf <| by simp only [mul, zero, zero_mul]
  mul_zero a := hf <| by simp only [mul, zero, mul_zero]

Injective Lift of MulZeroClass Structure

Informal description

Let $M_0'$ be a type equipped with multiplication and zero operations, and let $f : M_0' \to M_0$ be an injective function. If $f$ preserves zero (i.e., $f(0) = 0$) and multiplication (i.e., $f(a * b) = f(a) * f(b)$ for all $a, b \in M_0'$), then $M_0'$ inherits a `MulZeroClass` structure from $M_0$ via $f$.

Function.Surjective.mulZeroClass abbrev

 [Mul M₀'] [Zero M₀'] (f : M₀ → M₀') (hf : Surjective f) (zero : f 0 = 0) (mul : ∀ a b, f (a * b) = f a * f b) :
  MulZeroClass M₀'

Full source

/-- Push forward a `MulZeroClass` instance along a surjective function.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.mulZeroClass [Mul M₀'] [Zero M₀'] (f : M₀ → M₀')
    (hf : Surjective f) (zero : f 0 = 0) (mul : ∀ a b, f (a * b) = f a * f b) :
    MulZeroClass M₀' where
  mul := (· * ·)
  zero := 0
  mul_zero := hf.forall.2 fun x => by simp only [← zero, ← mul, mul_zero]
  zero_mul := hf.forall.2 fun x => by simp only [← zero, ← mul, zero_mul]

Lifting `MulZeroClass` structure along a surjective map

Informal description

Let $M_0$ and $M_0'$ be types equipped with multiplication and zero operations. Given a surjective function $f : M_0 \to M_0'$ such that $f(0) = 0$ and $f(a * b) = f(a) * f(b)$ for all $a, b \in M_0$, then $M_0'$ inherits a `MulZeroClass` structure from $M_0$ via $f$.

Function.Injective.noZeroDivisors theorem

[NoZeroDivisors M₀'] : NoZeroDivisors M₀

Full source

/-- Pull back a `NoZeroDivisors` instance along an injective function. -/
protected theorem Function.Injective.noZeroDivisors [NoZeroDivisors M₀'] : NoZeroDivisors M₀ where
  eq_zero_or_eq_zero_of_mul_eq_zero {a b} H :=
    have : f a * f b = 0 := by rw [← mul, H, zero]
    (eq_zero_or_eq_zero_of_mul_eq_zero this).imp
      (fun H ↦ hf <| by rwa [zero]) fun H ↦ hf <| by rwa [zero]

Injective Function Preserves No-Zero-Divisors Property

Informal description

If a function $f : M_0' \to M_0$ is injective and the domain $M_0'$ has no zero divisors, then the codomain $M_0$ also has no zero divisors.

Function.Injective.isLeftCancelMulZero theorem

[IsLeftCancelMulZero M₀'] : IsLeftCancelMulZero M₀

Full source

protected theorem Function.Injective.isLeftCancelMulZero
    [IsLeftCancelMulZero M₀'] : IsLeftCancelMulZero M₀ where
  mul_left_cancel_of_ne_zero Hne He := by
    have := congr_arg f He
    rw [mul, mul] at this
    exact hf (mul_left_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

Injective functions preserve left cancellation by nonzero elements

Informal description

If a type $M_0'$ has the property that multiplication on the left by a nonzero element is cancellative (i.e., $a \neq 0$ and $a \cdot b = a \cdot c$ implies $b = c$), and there exists an injective function from $M_0$ to $M_0'$, then $M_0$ also has this left cancellation property for multiplication by nonzero elements.

Function.Injective.isRightCancelMulZero theorem

[IsRightCancelMulZero M₀'] : IsRightCancelMulZero M₀

Full source

protected theorem Function.Injective.isRightCancelMulZero
    [IsRightCancelMulZero M₀'] : IsRightCancelMulZero M₀ where
  mul_right_cancel_of_ne_zero Hne He := by
    have := congr_arg f He
    rw [mul, mul] at this
    exact hf (mul_right_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

Injective map preserves right cancellative multiplication with zero

Informal description

If $M_0'$ is a right cancellative multiplicative monoid with zero, and there exists an injective function $f \colon M_0' \to M_0$ that preserves multiplication and zero, then $M_0$ is also a right cancellative multiplicative monoid with zero.

Function.Injective.isCancelMulZero theorem

[IsCancelMulZero M₀'] : IsCancelMulZero M₀

Full source

protected theorem Function.Injective.isCancelMulZero
    [IsCancelMulZero M₀'] : IsCancelMulZero M₀ where
  __ := hf.isLeftCancelMulZero f zero mul
  __ := hf.isRightCancelMulZero f zero mul

Injective functions preserve cancellative multiplication with zero

Informal description

If $M_0'$ is a multiplicative monoid with zero where multiplication is cancellative (i.e., for all $a, b, c \in M_0'$, if $a \neq 0$ and $a \cdot b = a \cdot c$ or $b \cdot a = c \cdot a$, then $b = c$), and there exists an injective function from $M_0$ to $M_0'$ that preserves multiplication and zero, then $M_0$ is also a cancellative multiplicative monoid with zero.

Function.Injective.mulZeroOneClass abbrev

 [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (mul : ∀ a b, f (a * b) = f a * f b) : MulZeroOneClass M₀'

Full source

/-- Pull back a `MulZeroOneClass` instance along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.mulZeroOneClass [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀' → M₀)
    (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ a b, f (a * b) = f a * f b) :
    MulZeroOneClass M₀' :=
  { hf.mulZeroClass f zero mul, hf.mulOneClass f one mul with }

Lifting of Multiplicative Structure with Zero and One via Injective Map

Informal description

Let $M_0$ and $M_0'$ be types equipped with multiplication, zero, and one operations. Given an injective function $f : M_0' \to M_0$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(a * b) = f(a) * f(b)$ for all $a, b \in M_0'$, then $M_0'$ inherits a `MulZeroOneClass` structure from $M_0$ via $f$.

Function.Surjective.mulZeroOneClass abbrev

 [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀ → M₀') (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1)
  (mul : ∀ a b, f (a * b) = f a * f b) : MulZeroOneClass M₀'

Full source

/-- Push forward a `MulZeroOneClass` instance along a surjective function.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.mulZeroOneClass [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀ → M₀')
    (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ a b, f (a * b) = f a * f b) :
    MulZeroOneClass M₀' :=
  { hf.mulZeroClass f zero mul, hf.mulOneClass f one mul with }

Lifting of Multiplicative Structure with Zero and One via Surjective Map

Informal description

Let $M_0$ and $M_0'$ be types equipped with multiplication, zero, and one operations. Given a surjective function $f : M_0 \to M_0'$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(a * b) = f(a) * f(b)$ for all $a, b \in M_0$, then $M_0'$ inherits a `MulZeroOneClass` structure from $M_0$ via $f$.

Function.Injective.semigroupWithZero abbrev

 [Zero M₀'] [Mul M₀'] [SemigroupWithZero M₀] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0)
  (mul : ∀ x y, f (x * y) = f x * f y) : SemigroupWithZero M₀'

Full source

/-- Pull back a `SemigroupWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.semigroupWithZero [Zero M₀'] [Mul M₀'] [SemigroupWithZero M₀]
    (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (mul : ∀ x y, f (x * y) = f x * f y) :
    SemigroupWithZero M₀' :=
  { hf.mulZeroClass f zero mul, ‹Zero M₀'›, hf.semigroup f mul with }

Lifting Semigroup with Zero Structure Along an Injective Map

Informal description

Let $M_0$ be a semigroup with zero, and let $M_0'$ be a type equipped with multiplication and zero operations. Given an injective function $f : M_0' \to M_0$ such that: - $f(0) = 0$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in M_0'$, then $M_0'$ inherits a `SemigroupWithZero` structure from $M_0$ via $f$.

Function.Surjective.semigroupWithZero abbrev

 [SemigroupWithZero M₀] [Zero M₀'] [Mul M₀'] (f : M₀ → M₀') (hf : Surjective f) (zero : f 0 = 0)
  (mul : ∀ x y, f (x * y) = f x * f y) : SemigroupWithZero M₀'

Full source

/-- Push forward a `SemigroupWithZero` along a surjective function.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.semigroupWithZero [SemigroupWithZero M₀] [Zero M₀'] [Mul M₀']
    (f : M₀ → M₀') (hf : Surjective f) (zero : f 0 = 0) (mul : ∀ x y, f (x * y) = f x * f y) :
    SemigroupWithZero M₀' :=
  { hf.mulZeroClass f zero mul, ‹Zero M₀'›, hf.semigroup f mul with }

Lifting of Semigroup with Zero Structure via Surjective Homomorphism

Informal description

Let $M_0$ be a semigroup with zero and $M_0'$ a type equipped with multiplication and zero operations. Given a surjective function $f : M_0 \to M_0'$ such that: - $f(0) = 0$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in M_0$, then $M_0'$ inherits a semigroup with zero structure from $M_0$ via $f$.

Function.Injective.monoidWithZero abbrev

 [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] [MonoidWithZero M₀] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : MonoidWithZero M₀'

Full source

/-- Pull back a `MonoidWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.monoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ]
    [MonoidWithZero M₀] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
    MonoidWithZero M₀' :=
  { hf.monoid f one mul npow, hf.mulZeroClass f zero mul with }

Lifting Monoid with Zero Structure Along an Injective Homomorphism

Informal description

Let $M_0$ be a monoid with zero and $M_0'$ a type equipped with zero, multiplication, one, and natural number power operations. Given an injective function $f : M_0' \to M_0$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in M_0'$, - $f(x^n) = f(x)^n$ for all $x \in M_0'$ and $n \in \mathbb{N}$, then $M_0'$ inherits a monoid with zero structure from $M_0$ via $f$.

Function.Surjective.monoidWithZero abbrev

 [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] [MonoidWithZero M₀] (f : M₀ → M₀') (hf : Surjective f) (zero : f 0 = 0)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : MonoidWithZero M₀'

Full source

/-- Push forward a `MonoidWithZero` along a surjective function.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.monoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ]
    [MonoidWithZero M₀] (f : M₀ → M₀') (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
    MonoidWithZero M₀' :=
  { hf.monoid f one mul npow, hf.mulZeroClass f zero mul with }

Lifting Monoid with Zero Structure via Surjective Homomorphism

Informal description

Let $M_0$ be a monoid with zero and $M_0'$ a type equipped with zero, multiplication, identity, and natural power operations. Given a surjective function $f : M_0 \to M_0'$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in M_0$, - $f(x^n) = f(x)^n$ for all $x \in M_0$ and $n \in \mathbb{N}$, then $M_0'$ inherits a monoid with zero structure from $M_0$ via $f$.

Function.Injective.commMonoidWithZero abbrev

 [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] [CommMonoidWithZero M₀] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
  CommMonoidWithZero M₀'

Full source

/-- Pull back a `CommMonoidWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.commMonoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ]
    [CommMonoidWithZero M₀] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
    CommMonoidWithZero M₀' :=
  { hf.commMonoid f one mul npow, hf.mulZeroClass f zero mul with }

Lifting Commutative Monoid with Zero Structure via Injective Homomorphism

Informal description

Let $M_0$ be a commutative monoid with zero and $M_0'$ a type equipped with zero, multiplication, identity, and natural number power operations. Given an injective function $f : M_0' \to M_0$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_0'$, - $f(x^n) = f(x)^n$ for all $x \in M_0'$ and $n \in \mathbb{N}$, then $M_0'$ inherits a commutative monoid with zero structure from $M_0$ via $f$.

Function.Surjective.commMonoidWithZero abbrev

 [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] [CommMonoidWithZero M₀] (f : M₀ → M₀') (hf : Surjective f) (zero : f 0 = 0)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
  CommMonoidWithZero M₀'

Full source

/-- Push forward a `CommMonoidWithZero` along a surjective function.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.commMonoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ]
    [CommMonoidWithZero M₀] (f : M₀ → M₀') (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
    CommMonoidWithZero M₀' :=
  { hf.commMonoid f one mul npow, hf.mulZeroClass f zero mul with }

Lifting Commutative Monoid with Zero Structure via Surjective Homomorphism

Informal description

Let $M_0$ be a commutative monoid with zero and $M_0'$ a type equipped with zero, multiplication, identity, and natural power operations. Given a surjective function $f : M_0 \to M_0'$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in M_0$, - $f(x^n) = f(x)^n$ for all $x \in M_0$ and $n \in \mathbb{N}$, then $M_0'$ inherits a commutative monoid with zero structure from $M_0$ via $f$.

Function.Injective.cancelMonoidWithZero abbrev

 [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelMonoidWithZero M₀'

Full source

/-- Pull back a `CancelMonoidWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.cancelMonoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ]
    (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
    CancelMonoidWithZero M₀' :=
  { hf.monoid f one mul npow, hf.mulZeroClass f zero mul with
    mul_left_cancel_of_ne_zero := fun hx H =>
      hf <| mul_left_cancel₀ ((hf.ne_iff' zero).2 hx) <| by rw [← mul, ← mul, H],
    mul_right_cancel_of_ne_zero := fun hx H =>
      hf <| mul_right_cancel₀ ((hf.ne_iff' zero).2 hx) <| by rw [← mul, ← mul, H] }

Lifting Cancel Monoid with Zero Structure Along an Injective Homomorphism

Informal description

Let $M_0'$ be a type equipped with zero, multiplication, identity, and natural number power operations, and let $M_0$ be a cancel monoid with zero. Given an injective function $f : M_0' \to M_0$ that preserves zero ($f(0) = 0$), the multiplicative identity ($f(1) = 1$), multiplication ($f(x * y) = f(x) * f(y)$ for all $x, y \in M_0'$), and natural number powers ($f(x^n) = f(x)^n$ for all $x \in M_0'$ and $n \in \mathbb{N}$), then $M_0'$ inherits a cancel monoid with zero structure from $M_0$ via $f$.

Function.Injective.cancelCommMonoidWithZero abbrev

 [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CancelCommMonoidWithZero M₀'

Full source

/-- Pull back a `CancelCommMonoidWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.cancelCommMonoidWithZero [Zero M₀'] [Mul M₀'] [One M₀']
    [Pow M₀' ℕ] (f : M₀' → M₀) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) :
    CancelCommMonoidWithZero M₀' :=
  { hf.commMonoidWithZero f zero one mul npow, hf.cancelMonoidWithZero f zero one mul npow with }

Lifting Commutative Cancel Monoid with Zero via Injective Homomorphism

Informal description

Let $M_0$ be a commutative cancel monoid with zero and $M_0'$ a type equipped with zero, multiplication, identity, and natural number power operations. Given an injective function $f \colon M_0' \to M_0$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M_0'$, - $f(x^n) = f(x)^n$ for all $x \in M_0'$ and $n \in \mathbb{N}$, then $M_0'$ inherits a commutative cancel monoid with zero structure from $M_0$ via $f$.

Function.Injective.groupWithZero abbrev

 [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' ℕ] [Pow G₀' ℤ] (f : G₀' → G₀) (hf : Injective f)
  (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
  (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : GroupWithZero G₀'

Full source

/-- Pull back a `GroupWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.groupWithZero [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀']
    [Pow G₀' ℕ] [Pow G₀' ℤ] (f : G₀' → G₀) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
    (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : GroupWithZero G₀' :=
  { hf.monoidWithZero f zero one mul npow,
    hf.divInvMonoid f one mul inv div npow zpow,
    domain_nontrivial f zero one with
    inv_zero := hf <| by rw [inv, zero, inv_zero],
    mul_inv_cancel := fun x hx => hf <| by
      rw [one, mul, inv, mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)] }

Lifting Group with Zero Structure Along an Injective Homomorphism

Informal description

Let $G_0$ be a group with zero and $G_0'$ a type equipped with zero, multiplication, identity, inversion, division, and natural and integer power operations. Given an injective function $f \colon G_0' \to G_0$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in G_0'$, - $f(x^{-1}) = (f(x))^{-1}$ for all $x \in G_0'$, - $f(x / y) = f(x) / f(y)$ for all $x, y \in G_0'$, - $f(x^n) = f(x)^n$ for all $x \in G_0'$ and $n \in \mathbb{N}$, - $f(x^n) = f(x)^n$ for all $x \in G_0'$ and $n \in \mathbb{Z}$, then $G_0'$ inherits a group with zero structure from $G_0$ via $f$.

Function.Surjective.groupWithZero abbrev

 [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' ℕ] [Pow G₀' ℤ] (h01 : (0 : G₀') ≠ 1) (f : G₀ → G₀')
  (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
  (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : GroupWithZero G₀'

Full source

/-- Push forward a `GroupWithZero` along a surjective function.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.groupWithZero [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀']
    [Div G₀'] [Pow G₀' ℕ] [Pow G₀' ℤ] (h01 : (0 : G₀') ≠ 1) (f : G₀ → G₀') (hf : Surjective f)
    (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y)
    (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) :
    GroupWithZero G₀' :=
  { hf.monoidWithZero f zero one mul npow, hf.divInvMonoid f one mul inv div npow zpow with
    inv_zero := by rw [← zero, ← inv, inv_zero],
    mul_inv_cancel := hf.forall.2 fun x hx => by
        rw [← inv, ← mul, mul_inv_cancel₀ (mt (congr_arg f) fun h ↦ hx (h.trans zero)), one]
    exists_pair_ne := ⟨0, 1, h01⟩ }

Lifting Group with Zero Structure via Surjective Homomorphism

Informal description

Let $G_0$ be a group with zero and $G_0'$ a type equipped with zero, multiplication, identity, inversion, division, and power operations (for both natural and integer exponents). Given a surjective function $f : G_0 \to G_0'$ such that: - $0 \neq 1$ in $G_0'$, - $f(0) = 0$, - $f(1) = 1$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in G_0$, - $f(x^{-1}) = (f(x))^{-1}$ for all $x \in G_0$, - $f(x / y) = f(x) / f(y)$ for all $x, y \in G_0$, - $f(x^n) = f(x)^n$ for all $x \in G_0$ and $n \in \mathbb{N}$, - $f(x^n) = f(x)^n$ for all $x \in G_0$ and $n \in \mathbb{Z}$, then $G_0'$ inherits a group with zero structure from $G_0$ via $f$.

Function.Injective.commGroupWithZero abbrev

 [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' ℕ] [Pow G₀' ℤ] (f : G₀' → G₀) (hf : Injective f)
  (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
  (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroupWithZero G₀'

Full source

/-- Pull back a `CommGroupWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.commGroupWithZero [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀']
    [Div G₀'] [Pow G₀' ℕ] [Pow G₀' ℤ] (f : G₀' → G₀) (hf : Injective f) (zero : f 0 = 0)
    (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
    (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroupWithZero G₀' :=
  { hf.groupWithZero f zero one mul inv div npow zpow, hf.commSemigroup f mul with }

Lifting Commutative Group with Zero Structure Along an Injective Homomorphism

Informal description

Let $G_0$ be a commutative group with zero and $G_0'$ a type equipped with zero, multiplication, identity, inversion, division, and natural and integer power operations. Given an injective function $f \colon G_0' \to G_0$ such that: - $f(0) = 0$, - $f(1) = 1$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in G_0'$, - $f(x^{-1}) = (f(x))^{-1}$ for all $x \in G_0'$, - $f(x / y) = f(x) / f(y)$ for all $x, y \in G_0'$, - $f(x^n) = f(x)^n$ for all $x \in G_0'$ and $n \in \mathbb{N}$, - $f(x^n) = f(x)^n$ for all $x \in G_0'$ and $n \in \mathbb{Z}$, then $G_0'$ inherits a commutative group with zero structure from $G_0$ via $f$.

Function.Surjective.commGroupWithZero definition

 [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' ℕ] [Pow G₀' ℤ] (h01 : (0 : G₀') ≠ 1) (f : G₀ → G₀')
  (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
  (div : ∀ x y, f (x / y) = f x / f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroupWithZero G₀'

Full source

/-- Push forward a `CommGroupWithZero` along a surjective function.
See note [reducible non-instances]. -/
protected def Function.Surjective.commGroupWithZero [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀']
    [Div G₀'] [Pow G₀' ℕ] [Pow G₀' ℤ] (h01 : (0 : G₀') ≠ 1) (f : G₀ → G₀') (hf : Surjective f)
    (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y)
    (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) :
    CommGroupWithZero G₀' :=
  { hf.groupWithZero h01 f zero one mul inv div npow zpow, hf.commSemigroup f mul with }

Lifting Commutative Group with Zero Structure via Surjective Homomorphism

Informal description

Let $G_0$ be a commutative group with zero and $G_0'$ a type equipped with zero, multiplication, identity, inversion, division, and power operations (for both natural and integer exponents). Given a surjective function $f : G_0 \to G_0'$ such that: - $0 \neq 1$ in $G_0'$, - $f(0) = 0$, - $f(1) = 1$, - $f(x * y) = f(x) * f(y)$ for all $x, y \in G_0$, - $f(x^{-1}) = (f(x))^{-1}$ for all $x \in G_0$, - $f(x / y) = f(x) / f(y)$ for all $x, y \in G_0$, - $f(x^n) = f(x)^n$ for all $x \in G_0$ and $n \in \mathbb{N}$, - $f(x^n) = f(x)^n$ for all $x \in G_0$ and $n \in \mathbb{Z}$, then $G_0'$ inherits a commutative group with zero structure from $G_0$ via $f$.