English
If there is a surjective map from M1 with 1 and multiplication to a monoid M2, then M2 being a monoid implies M1 is a monoid.
Русский
Если существует сюръективное отображение f: M1 → M2 сохраняющее 1 и умножение, то если M2 — моноид, то и M1 — моноид.
LaTeX
$$$\exists f: M_1 \to M_2\,\big(\text{Surjective}(f) \land f(1)=1 \land (\forall x,y: M_1)\, f(xy)=f(x)f(y) \big) \Rightarrow \text{Monoid}(M_2) \Rightarrow \text{Monoid}(M_1)$$
Lean4
/-- 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] }
