English
For a prime p, the fiber p.asIdeal.ResidueField ⊗_R S is nontrivial iff p lies in the range of algebraMap R S .specComap.
Русский
Для простого p, волокно p.asIdeal.ResidueField ⊗_R S ненулево тогда и только тогда, когда p принадлежит диапазону algebraMap R S .specComap.
LaTeX
$$$\\text{Nontrivial}(p.asIdeal.ResidueField \\otimes_R S) \\iff p \\in \\operatorname{range}(\\alpha)$$$
Lean4
/-- A prime `p` is in the range of `Spec S → Spec R` if the fiber over `p` is nontrivial. -/
theorem nontrivial_iff_mem_rangeComap {S : Type*} [CommRing S] [Algebra R S] (p : PrimeSpectrum R) :
Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔ p ∈ Set.range (algebraMap R S).specComap :=
by
let k := p.asIdeal.ResidueField
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· obtain ⟨m, hm⟩ := Ideal.exists_maximal (k ⊗[R] S)
use (Algebra.TensorProduct.includeRight).specComap ⟨m, hm.isPrime⟩
ext : 1
rw [← PrimeSpectrum.specComap_comp_apply, ← Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap,
specComap_comp_apply]
simp [Ideal.eq_bot_of_prime, k, ← RingHom.ker_eq_comap_bot]
· obtain ⟨q, rfl⟩ := h
let f : k ⊗[R] S →ₐ[R] q.asIdeal.ResidueField :=
Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ _ _ rfl) (IsScalarTower.toAlgHom _ _ _)
(fun _ _ ↦ Commute.all ..)
exact RingHom.domain_nontrivial f.toRingHom
