English
Let f: R → S be surjective. If R has an AddGroupWithOne structure, then S inherits AddGroupWithOne via pullback.
Русский
Пусть f: R → S сюръективна. Если у R есть AddGroupWithOne, то S наследует AddGroupWithOne через перенос.
LaTeX
$$$\\exists\\; \\mathcal{S}: \\text{AddGroupWithOne}(S)$$$
Lean4
/-- 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 [AddGroupWithOne R] (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 S :=
{ 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] }
