English
If f: A → B is a local hom with f injective, and B is a field, then A is a field.
Русский
Если f: A → B является локальным гомоморфизмом с инъективностью, и B — поле, то A тоже является полем.
LaTeX
$$$\forall a \in A, a \neq 0 \Rightarrow \exists b \in A, ab = 1$ (i.e., $A$ is a field, given the conditions).$$
Lean4
protected theorem isField [FunLike F A B] [MonoidWithZeroHomClass F A B] {f : F} [IsLocalHom f]
(inj : Function.Injective f) (hB : IsField B) : IsField A
where
exists_pair_ne :=
have : Nontrivial B := ⟨hB.1⟩;
(domain_nontrivial f (map_zero f) (map_one f)).1
mul_comm x y := inj <| by rw [map_mul, map_mul, hB.mul_comm]
mul_inv_cancel
h :=
have ⟨a', he⟩ := hB.mul_inv_cancel ((inj.ne h).trans_eq <| map_zero f)
let _ := hB.toSemifield
((isUnit_of_mul_eq_one _ _ he).of_map).exists_right_inv
