English
Push forward a GroupWithZero along a surjective function; the codomain inherits the group with zero structure.
Русский
Перемещаем GroupWithZero вдоль сюръективной функции; кодомон наследует структуру группы с нулём.
LaTeX
$$$\\text{GroupWithZero } M_0' = \\text{ pushforward along } f$$$
Lean4
/-- Push forward a `GroupWithZero` along a surjective function.
See note [reducible non-instances]. -/
protected abbrev 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⟩ }
