Module

LaurentKummerGeometricFiber.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerGeometricFiber

7 declarations indexed from sourceView source ↗

Module documentation

The geometric fibre of the actual Laurent Kummer cover

The quotient-algebra description is compared with scheme morphisms using full faithfulness of Spec, and then with the existing geometric fibre functor. Consequently the actual finite-etale fibre is equivalent to the set of roots of its defining Kummer equation.

Imports4

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerFiber
Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerCovers
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Nyll.EtaleFundamentalGroups.GeometricFiber.FundamentalGroup

Imported by2

def

laurentKummerProjection

L31 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerProjection

Documentation

The spectrum morphism of the explicit Laurent Kummer algebra.

Source context 5 commands

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

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

Lean source · statement

def laurentKummerProjection (K : Type u) [Field K] (n : ℕ) :
    Spec (.of (LaurentKummerAlgebra K n)) ⟶ Spec (.of (LaurentPolynomial K))

def

laurentKummerPoint

L37 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerPoint

Documentation

The geometric Laurent point determined by a nonzero scalar.

Source context 5 commands

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

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

Lean source · statement

def laurentKummerPoint (a : Kˣ) : Spec (.of L) ⟶ Spec (.of (LaurentPolynomial K))

def

LaurentKummerSchemeFiber

L41 ↗

AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerSchemeFiber

Documentation

Scheme-valued points above the specified Laurent point.

Source context 5 commands

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

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

Lean source · statement

def LaurentKummerSchemeFiber (n : ℕ) (a : Kˣ)

def

laurentKummerSchemeFiberEquiv

L46 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerSchemeFiberEquiv

Documentation

The affine scheme fibre points are exactly the previously constructed algebra points.

Source context 5 commands

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

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

Lean source · full declaration

def laurentKummerSchemeFiberEquiv (n : ℕ) (a : Kˣ) :
    LaurentKummerSchemeFiber (L := L) n a ≃ LaurentKummerFiberHom (L := L) n a where
  toFun f := ⟨(Spec.preimage f.val).hom, by
    have h := congrArg (fun g : Spec (.of L) ⟶ Spec (.of (LaurentPolynomial K)) =>
      (Spec.preimage g).hom) f.property
    simpa only [laurentKummerProjection, laurentKummerPoint, Spec.preimage_comp,
      Spec.preimage_map, CommRingCat.hom_comp, CommRingCat.hom_ofHom] using h⟩
  invFun f := ⟨Spec.map (CommRingCat.ofHom f.val), by
    change Spec.map (CommRingCat.ofHom f.val) ≫
      Spec.map (CommRingCat.ofHom (AdjoinRoot.of _)) =
        Spec.map (CommRingCat.ofHom (laurentScalarEvaluation a))
    rw [← Spec.map_comp]
    exact congrArg (fun g : LaurentPolynomial K →+* L => Spec.map (CommRingCat.ofHom g))
      f.property⟩
  left_inv f := by
    apply Subtype.ext
    exact Spec.map_preimage f.val
  right_inv f := by
    apply Subtype.ext
    exact congrArg (fun g : CommRingCat.of (LaurentKummerAlgebra K n) ⟶ CommRingCat.of L =>
      g.hom) (Spec.preimage_map (CommRingCat.ofHom f.val))

def

laurentKummerCover

L69 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerCover

Documentation

The named actual finite-etale Laurent Kummer cover of positive degree.

Source context 5 commands

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

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

Lean source · statement

def laurentKummerCover (K : Type u) [Field K] [CharZero K]
    (n : ℕ) (hn : 0 < n) : FiniteEtale (Spec (.of (LaurentPolynomial K)))

def

laurentKummerGeometricFiberEquivScheme

L84 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerGeometricFiberEquivScheme

Documentation

Compare the actual geometric fibre functor with its scheme-valued points.

Source context 5 commands

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

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

Lean source · statement

def laurentKummerGeometricFiberEquivScheme [CharZero K] [IsSepClosed L]
    (n : ℕ) (hn : 0 < n) (a : Kˣ) :
    (fiber (laurentKummerPoint (L := L) a)).obj (laurentKummerCover K n hn) ≃
      LaurentKummerSchemeFiber (L := L) n a

def

laurentKummerGeometricFiberEquivRoots

L96 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerGeometricFiberEquivRoots

Documentation

The actual geometric fibre of the named finite-etale cover consists precisely of the roots of its Kummer equation.

Source context 5 commands

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

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

Lean source · statement

def laurentKummerGeometricFiberEquivRoots [CharZero K] [IsSepClosed L]
    (n : ℕ) (hn : 0 < n) (a : Kˣ) :
    (fiber (laurentKummerPoint (L := L) a)).obj (laurentKummerCover K n hn) ≃
      {r : L // r ^ n = algebraMap K L (a : K)}

Module documentation

The geometric fibre of the actual Laurent Kummer cover

Declarations

laurentKummerProjection

laurentKummerPoint

LaurentKummerSchemeFiber

laurentKummerSchemeFiberEquiv

laurentKummerCover

laurentKummerGeometricFiberEquivScheme

laurentKummerGeometricFiberEquivRoots