English
For field K and f: Spec(κ(K)) ⟶ X, the same compatibility holds: Spec.map (descResidueField (stalkClosedPointTo f)) ≫ X.fromSpecResidueField (f.base (closedPoint K)) = f.
Русский
Для поля K и f: Spec(κ(K)) → X, выполняется аналогичное совместимость: Spec.map (descResidueField (stalkClosedPointTo f)) ≫ X.fromSpecResidueField (f.base (closedPoint K)) = f.
LaTeX
$$∀ (K : Type u) [Field K] (X : Scheme) (f : Spec (.of K) ⟶ X),\n Spec.map (X.descResidueField (Scheme.stalkClosedPointTo f)) ≫ X.fromSpecResidueField (f.base (closedPoint K)) = f$$
Lean4
/-- A helper lemma to work with `AlgebraicGeometry.Scheme.SpecToEquivOfField`. -/
theorem SpecToEquivOfField_eq_iff {K : Type*} [Field K] {X : Scheme}
{f₁ f₂ : Σ x : X.carrier, X.residueField x ⟶ .of K} :
f₁ = f₂ ↔ ∃ e : f₁.1 = f₂.1, f₁.2 = (X.residueFieldCongr e).hom ≫ f₂.2 :=
by
constructor
· rintro rfl
simp
· obtain ⟨f, _⟩ := f₁
obtain ⟨g, _⟩ := f₂
rintro ⟨(rfl : f = g), h⟩
simpa
