English
If X is an integral scheme universally closed over Spec K, then the global sections Γ(X, ⊤) form a field.
Русский
Если X интегральный схем, всемирно замкнут над Spec K, то Γ(X, ⊤) образует поле.
LaTeX
$$$[IsIntegral X] \land [UniversallyClosed f] \Rightarrow IsField(\Gamma(X, \top))$$$
Lean4
/-- If `X` is an integral scheme that is universally closed and of finite type over `Spec K`,
then `Γ(X, ⊤)` is a finite field extension over `K`. -/
theorem finite_appTop_of_universallyClosed (f : X ⟶ (Spec <| .of K)) [IsIntegral X] [UniversallyClosed f]
[LocallyOfFiniteType f] : f.appTop.hom.Finite :=
by
have x : X := Nonempty.some inferInstance
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
letI := ((Scheme.ΓSpecIso (.of K)).commRingCatIsoToRingEquiv.toMulEquiv.isField (Field.toIsField K)).toField
letI := (isField_of_universallyClosed K f).toField
have : Nonempty U := ⟨⟨x, hxU⟩⟩
apply
RingHom.finite_of_algHom_finiteType_of_isJacobsonRing (A := Γ(X, U)) (g := (X.presheaf.map (homOfLE le_top).op).hom)
exact LocallyOfFiniteType.finiteType_of_affine_subset ⟨⊤, isAffineOpen_top _⟩ ⟨U, hU⟩ (by simp)
