of_surjective — Mathlib

English

If f is a surjective local ring hom from a local ring R to a semiring S, then S is local.

Русский

Если локальный гомоморфизм из локального кольца R на полное кольцо S сюръективен, то S локально.

LaTeX

$$$\text{IsLocalRing } R \Rightarrow \text{Surjective}(f) \Rightarrow \text{IsLocalRing } S$$$

Lean4

theorem of_surjective [CommSemiring R] [IsLocalRing R] [Semiring S] [Nontrivial S] (f : R →+* S) [IsLocalHom f]
    (hf : Function.Surjective f) : IsLocalRing S :=
  of_isUnit_or_isUnit_of_isUnit_add
    (by
      intro a b hab
      obtain ⟨a, rfl⟩ := hf a
      obtain ⟨b, rfl⟩ := hf b
      rw [← map_add] at hab
      exact (isUnit_or_isUnit_of_isUnit_add <| IsLocalHom.map_nonunit _ hab).imp f.isUnit_map f.isUnit_map)

Похожие утверждения