of_specComap_surjective — Mathlib

English

If f.specComap is surjective, then f is a local homomorphism; i.e., it preserves nonunits in a precise way.

Русский

Если f.specComap сюръективно, то f является локальным гомоморфизмом; он сохраняет немодуля на точном уровне.

LaTeX

$$$\\text{IsLocalHom } f\\text{ из } hf: \\text{Surjective } f.{\\rm specComap} \\Rightarrow \\text{IsLocalHom } f$$$

Lean4

theorem of_specComap_surjective [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Surjective f.specComap) :
    IsLocalHom f where
  map_nonunit x
    hfx := by
    by_contra hx
    obtain ⟨p, hp, _⟩ := exists_max_ideal_of_mem_nonunits hx
    obtain ⟨⟨q, hqp⟩, hq⟩ := hf ⟨p, hp.isPrime⟩
    simp only [PrimeSpectrum.mk.injEq] at hq
    exact hqp.ne_top (q.eq_top_of_isUnit_mem (q.mem_comap.mp (by rwa [hq])) hfx)

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