of_surjective' — Mathlib

English

If f: R → S is a surjective ring homomorphism and R is local with S nontrivial, then S is local.

Русский

Если кольцо-гомоморфизм f: R → S сюрьективен и R локально, а S ненулевое, то S локально.

LaTeX

$$$[\\text{IsLocalRing } R]\\;[\\text{Nontrivial } S]\\;f:R\\to S\\text{ surjective} \\Rightarrow IsLocalRing(S)$$$

Lean4

theorem of_surjective' [Ring S] [Nontrivial S] (f : R →+* S) (hf : Function.Surjective f) : IsLocalRing S :=
  of_isUnit_or_isUnit_one_sub_self
    (by
      intro b
      obtain ⟨a, rfl⟩ := hf b
      apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _
      rw [← f.map_one, ← f.map_sub]
      apply f.isUnit_map)

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