English
An injective map that preserves 0, 1 and addition lifts an AddGroupWithOne structure back along the map.
Русский
Инъекция, сохраняющая ноль, единицу и сложение, поднимает структуру AddGroupWithOne обратно через отображение.
LaTeX
$$Pullback of AddGroupWithOne: using the injective map to transport additive structures with one.$$
Lean4
/-- 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 [Zero S] [One S] [Add S] [SMul ℕ S] [NatCast S] [AddMonoidWithOne R] (f : S → R)
(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 S :=
{ 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 }
