English
If one has a commutative rings R,S and a ring hom f: R →+* S, and if comap f is a closed map for the induced map on spectra, then f is an integral extension.
Русский
Пусть R,S — коммутативные кольца и f: R →+* S гoмоморфизм, если comap f замкнуто в спектре, тогда расширение S над R интегрально.
LaTeX
$$$$ \text{If } \text{IsClosedMap}(\operatorname{comap}(\operatorname{mapRingHom}(f))) \Rightarrow f \text{ is integral}. $$$$
Lean4
theorem isIntegral_of_isClosedMap_comap_mapRingHom (h : IsClosedMap (comap (mapRingHom f))) : f.IsIntegral :=
by
algebraize [f]
suffices Algebra.IsIntegral R S by rwa [Algebra.isIntegral_def] at this
nontriviality R
nontriviality S
constructor
intro r
let p : S[X] := C r * X - 1
have : (1 : R[X]) ∈ Ideal.span { X } ⊔ (Ideal.span { p }).comap (mapRingHom f) :=
by
have H := h _ (isClosed_zeroLocus { p })
rw [← zeroLocus_span, ← closure_eq_iff_isClosed, closure_image_comap_zeroLocus] at H
rw [← Ideal.eq_top_iff_one, sup_comm, ← zeroLocus_empty_iff_eq_top, zeroLocus_sup, H]
suffices ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal by simpa [Set.eq_empty_iff_forall_notMem]
intro q hpq hXq
have : 1 ∈ q.asIdeal := by simpa [p] using (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)
exact q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)
obtain ⟨a, b, hb, e⟩ := Ideal.mem_span_singleton_sup.mp this
obtain ⟨c, hc : b.map (algebraMap R S) = _⟩ := Ideal.mem_span_singleton.mp hb
refine ⟨b.reverse * X ^ (1 + c.natDegree), ?_, ?_⟩
· refine Monic.mul ?_ (by simp)
have h : b.coeff 0 = 1 := by simpa using congr(($e).coeff 0)
have : b.natTrailingDegree = 0 := by simp [h]
rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]
· have : p.natDegree ≤ 1 := by simpa using natDegree_linear_le (a := r) (b := -1)
rw [eval₂_eq_eval_map, reverse, Polynomial.map_mul, ← reflect_map, Polynomial.map_pow, map_X, ← revAt_zero (1 + _),
← reflect_monomial, ← reflect_mul _ _ natDegree_map_le (by simp), pow_zero, mul_one, hc, ← add_assoc,
reflect_mul _ _ (this.trans (by simp)) le_rfl, eval_mul, reflect_sub, reflect_mul _ _ (by simp) (by simp)]
simp [← pow_succ']
