of_surjective — Mathlib

English

If f is surjective and IsLocalHom f, then f is a local homorphism.

Русский

Если отображение сюръективно и локальный гомоморфизм, тогда он локальный гомоморфизм.

LaTeX

$$$\text{IsLocalHom}(f) \Rightarrow \text{Surjective}(f) \Rightarrow \text{IsLocalHom}(f)$$$

Lean4

theorem _root_.IsLocalHom.of_surjective [CommRing R] [CommRing S] [Nontrivial S] [IsLocalRing R] (f : R →+* S)
    (hf : Function.Surjective f) : IsLocalHom f :=
  by
  have := IsLocalRing.of_surjective' f ‹_›
  refine ((local_hom_TFAE f).out 3 0).mp ?_
  have := Ideal.comap_isMaximal_of_surjective f hf (K := maximalIdeal S)
  exact ((maximal_ideal_unique R).unique (inferInstanceAs (maximalIdeal R).IsMaximal) this).le

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