theorem
L22 ↗nonempty_rationalPoint
AlgebraicCurve.CurveModel.nonempty_rationalPoint
A curve model has a rational point over an algebraically closed base. The point is constructed from an actual closed point of its Jacobson space.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
namespace AlgebraicCurve.CurveModelLean source · statement
theorem nonempty_rationalPoint
{K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
(M : CurveModel K F) :
Nonempty (SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)