English
If f: K → L is injective and L is a Field with compatible structure, then K inherits a Field structure via pullback along f.
Русский
Если f: K → L инъективно и L — поле с совместимой структурой, то K наследует структуру поля через вытягивание по f.
LaTeX
$$$\\exists$ Field K with morphism preserving operations from K to L via f$$
Lean4
/-- Pullback a `Field` along an injective function. -/
-- See note [reducible non-instances]
protected abbrev semifield [Semifield L] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
(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)
(nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
(npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n)
(nnratCast : ∀ q : ℚ≥0, f q = q) : Semifield K
where
toCommSemiring := hf.commSemiring f zero one add mul nsmul npow natCast
__ := hf.commGroupWithZero f zero one mul inv div npow zpow
__ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
