Module

LaurentKummerArithmeticFiber.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerArithmeticFiber

7 declarations indexed from sourceView source ↗

Module documentation

Arithmetic fibres at rational Laurent points

Pull the named Kummer cover back along a rational point to obtain an actual finite-etale scheme over the base field. Its geometric fibre is identified with the algebra-point description, through the actual pullback square.

Imports3

Imported by2

theorem

laurentScalarEvaluation_monomial

AnabelianGeometry.GeometricFundamentalGroup.laurentScalarEvaluation_monomial

Documentation

Evaluate a Laurent monomial directly in the base field before scalar extension.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem laurentScalarEvaluation_monomial (a : Kˣ) (b : K) (m : ℤ) :
    laurentScalarEvaluation (L := L) a (LaurentPolynomial.C b * LaurentPolynomial.T m) =
      algebraMap K L (b * ((a ^ m : Kˣ) : K))

theorem

laurentScalarEvaluation_baseChange

AnabelianGeometry.GeometricFundamentalGroup.laurentScalarEvaluation_baseChange

Documentation

Laurent scalar evaluation commutes with extension of the base field.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem laurentScalarEvaluation_baseChange (a : Kˣ) :
    (algebraMap K L).comp (laurentScalarEvaluation (L := K) a) =
      laurentScalarEvaluation (L := L) a

theorem

laurentKummerPoint_baseChange

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerPoint_baseChange

Documentation

The geometric Laurent point is the scalar extension of its rational point.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem laurentKummerPoint_baseChange (a : Kˣ) :
    ξ K L ≫ laurentKummerPoint (L := K) a = laurentKummerPoint (L := L) a

def

laurentKummerArithmeticFiber

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerArithmeticFiber

Documentation

The actual finite-etale scheme over the base obtained by taking the Kummer fibre at the rational point.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

def laurentKummerArithmeticFiber [CharZero K] (n : ℕ) (hn : 0 < n) (a : Kˣ) :
    FiniteEtale (Spec (.of K))

def

laurentKummerArithmeticOverEquiv

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerArithmeticOverEquiv

Documentation

The pullback square identifies field-valued points with Laurent fibre points.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · full declaration

def laurentKummerArithmeticOverEquiv [CharZero K]
    (n : ℕ) (hn : 0 < n) (a : Kˣ) :
    (Over.mk (ξ K L) ⟶ (laurentKummerArithmeticFiber n hn a).toComma) ≃
      LaurentKummerSchemeFiber (L := L) n a where
  toFun z := ⟨z.left ≫ pullback.fst (laurentKummerProjection K n)
      (laurentKummerPoint (L := K) a), by
    change (z.left ≫ pullback.fst (laurentKummerProjection K n)
      (laurentKummerPoint (L := K) a)) ≫ laurentKummerProjection K n = _
    have hz : z.left ≫ pullback.snd (laurentKummerProjection K n)
        (laurentKummerPoint (L := K) a) = ξ K L := z.w
    have hcondition :
        pullback.fst (laurentKummerProjection K n) (laurentKummerPoint (L := K) a) ≫
          laurentKummerProjection K n =
        pullback.snd (laurentKummerProjection K n) (laurentKummerPoint (L := K) a) ≫
          laurentKummerPoint (L := K) a := pullback.condition
    erw [Category.assoc, hcondition, ← Category.assoc, hz]
    exact laurentKummerPoint_baseChange a⟩
  invFun f := Over.homMk
    (pullback.lift f.val (ξ K L) (f.property.trans (laurentKummerPoint_baseChange a).symm))
    (pullback.lift_snd _ _ _)
  left_inv z := by
    apply Over.OverMorphism.ext
    apply pullback.hom_ext
    · exact pullback.lift_fst _ _ _
    · exact (pullback.lift_snd _ _ _).trans z.w.symm
  right_inv f := by
    apply Subtype.ext
    exact pullback.lift_fst _ _ _

def

laurentKummerArithmeticFiberEquiv

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerArithmeticFiberEquiv

Documentation

The actual arithmetic geometric fibre is equivalent to the algebra points.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

def laurentKummerArithmeticFiberEquiv [CharZero K] [IsSepClosed L]
    (n : ℕ) (hn : 0 < n) (a : Kˣ) :
    (fib K L).obj (laurentKummerArithmeticFiber n hn a) ≃
      LaurentKummerFiberHom (L := L) n a

theorem

laurentKummerArithmeticFiberEquiv_spec

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerArithmeticFiberEquiv_spec

Documentation

The point map underlying the arithmetic comparison is the actual projection from the pullback scheme.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem laurentKummerArithmeticFiberEquiv_spec [CharZero K] [IsSepClosed L]
    (n : ℕ) (hn : 0 < n) (a : Kˣ)
    (z : (fib K L).obj (laurentKummerArithmeticFiber n hn a)) :
    Spec.map (CommRingCat.ofHom (laurentKummerArithmeticFiberEquiv n hn a z).val) =
      (fiberObjEquivHom (ξ K L) (laurentKummerArithmeticFiber n hn a) z).left ≫
        pullback.fst (laurentKummerProjection K n) (laurentKummerPoint (L := K) a)