AlgebraicCurve.CurveModel.isRational_pointEquivPlace
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isRational_pointEquivPlace
open CategoryTheory AlgebraicGeometry
universe u vLean source · statement
theorem _root_.AlgebraicCurve.CurveModel.isRational_pointEquivPlace
{K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
(M : AlgebraicCurve.CurveModel K L)
(x : {p : Spec (CommRingCat.of K) ⟶ M.C // p ≫ M.toBase = 𝟙 _}) :
(M.pointEquivPlace x).IsRational