English
Isomorphisms of residue fields induce equal stalk ranks; equivalently, rankAtStalk is invariant under extension by purely inseparable maps at the level of spectra.
Русский
Изоморфизмы тензорирования полей остатка сохраняют ранги локализации; ранг локализацииInvariant под чисто неразложимыми картами спектра.
LaTeX
$$$\\text{If } e: M \\simeq N, \\; \\operatorname{rankAtStalk}(M) = \\operatorname{rankAtStalk}(N).$$$
Lean4
/-- If the kernel of `f : R →+* S` consists of nilpotent elements and for every `x : S`,
there exists `n > 0` such that `x ^ n` is in the range of `f`, then `Spec f` is a homeomorphism.
Note: This does not hold for semirings, because `ℕ →+* ℤ` satisfies these conditions, but
`Spec ℕ` has one more point than `Spec ℤ`. -/
@[stacks 0BR8 "Homeomorphism part"]
theorem isHomeomorph_comap (f : R →+* S) (H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range)
(hker : RingHom.ker f ≤ nilradical R) : IsHomeomorph (comap f) :=
by
have h1 : Function.Injective (comap f) := by
intro q q' hqq'
ext x
obtain ⟨n, hn, y, hy⟩ := H x
rw [← q.2.pow_mem_iff_mem _ hn, ← q'.2.pow_mem_iff_mem _ hn, ← hy]
rw [PrimeSpectrum.ext_iff, SetLike.ext_iff] at hqq'
apply hqq'
have hint : f.kerLift.IsIntegral := fun x ↦
have ⟨n, hn, y, hy⟩ := H x
let _ := f.kerLift.toAlgebra
IsIntegral.of_pow hn (hy ▸ f.kerLift.isIntegralElem_map (x := ⟦y⟧))
have hbij : Function.Bijective (comap f) :=
⟨h1, (comap_quotientMk_bijective_of_le_nilradical hker).2.comp <| hint.specComap_surjective f.kerLift_injective⟩
refine ⟨(comap f).continuous, ?_, h1, hbij.2⟩
rw [isTopologicalBasis_basic_opens.isOpenMap_iff]
rintro - ⟨s, rfl⟩
obtain ⟨n, hn, r, hr⟩ := H s
have : (comap f) '' (basicOpen s) = basicOpen r :=
(Set.eq_preimage_iff_image_eq hbij).mp <| by rw [← basicOpen_pow _ n hn, ← hr]; rfl
exact this ▸ isOpen_basicOpen
