Module

CurveModelGeometricGenericLift.lean

Nyll.AlgebraicCurves.Models.CurveModelGeometricGenericLift

3 declarations indexed from sourceView source ↗

Module documentation

The actual geometric generic point on a scalar-extension curve

The structure morphism at the generic stalk is the spectrum of the actual base-field embedding. The pullback universal property then constructs the rational point over an extension of the function field.

Imports3

Nyll.AlgebraicCurves.Models.Basic
Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.Pullbacks

Imported by2

theorem

fromSpecStalk_generic_comp_toBase

L27 ↗

AlgebraicCurve.fromSpecStalk_generic_comp_toBase

Documentation

The generic point lies over the actual base-field homomorphism into the function field.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace AlgebraicCurve

Lean source · statement

theorem fromSpecStalk_generic_comp_toBase
    {K : Type} [Field K] {X : Scheme} [IsIntegral X]
    (c : X ⟶ Spec (.of K)) :
    X.fromSpecStalk (genericPoint X) ≫ c =
      Spec.map (CommRingCat.ofHom (baseToFunctionField c))

theorem

exists_geometricGenericPoint

L52 ↗

AlgebraicCurve.CurveModel.exists_geometricGenericPoint

Documentation

Construct the actual geometric generic point as a rational point of the scalar-extension curve, with its exact projection.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace AlgebraicCurve
namespace CurveModel

Lean source · statement

theorem exists_geometricGenericPoint
    {K F Ω F' : Type} [Field K] [Field F] [Algebra K F]
    [Field Ω] [Algebra K Ω] [Field F'] [Algebra Ω F']
    (M₀ : CurveModel K F) (M : CurveModel Ω F')
    (e : M.C ≅ pullback M₀.toBase
      (Spec.map (CommRingCat.ofHom (algebraMap K Ω))))
    (he : e.hom ≫ pullback.snd M₀.toBase
      (Spec.map (CommRingCat.ofHom (algebraMap K Ω))) = M.toBase)
    (ι : M₀.C.functionField →+* Ω)
    (hι : ∀ a : K, ι (baseToFunctionField M₀.toBase a) = algebraMap K Ω a) :
    ∃ x : {q : Spec (.of Ω) ⟶ M.C // q ≫ M.toBase = 𝟙 _},
      x.1 ≫ e.hom ≫ pullback.fst M₀.toBase
          (Spec.map (CommRingCat.ofHom (algebraMap K Ω))) =
        Spec.map (CommRingCat.ofHom ι) ≫ M₀.C.fromSpecStalk (genericPoint M₀.C)

theorem

generic_projection_fixed

L89 ↗

AlgebraicCurve.generic_projection_fixed

Documentation

Absolute Galois automorphisms fix the actual generic projection.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace AlgebraicCurve

Lean source · statement

theorem generic_projection_fixed
    {X : Scheme} [IsIntegral X] {Ω : Type} [Field Ω]
    [Algebra X.functionField Ω] (σ : Ω ≃ₐ[X.functionField] Ω) :
    Spec.map (CommRingCat.ofHom σ.toRingHom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap X.functionField Ω)) ≫
        X.fromSpecStalk (genericPoint X) =
      Spec.map (CommRingCat.ofHom (algebraMap X.functionField Ω)) ≫
        X.fromSpecStalk (genericPoint X)

Module documentation

The actual geometric generic point on a scalar-extension curve

Declarations

fromSpecStalk_generic_comp_toBase

exists_geometricGenericPoint

generic_projection_fixed