Module

LaurentKummerFiber.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerFiber

6 declarations indexed from sourceView source ↗

Module documentation

Roots as points of the Laurent Kummer fibre

The points of the actual Laurent Kummer algebra above a nonzero scalar are exactly the roots of its Kummer equation. Both directions are explicit ring homomorphisms and the inverse laws follow from the quotient universal property. No identification of a cover fibre with a root set is assumed.

Imports1

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerAlgebra

Imported by3

def

laurentScalarEvaluation

L28 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentScalarEvaluation

Documentation

Evaluation of the Laurent coordinate at a nonzero base-field scalar.

Source context 5 commands

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

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

Lean source · statement

def laurentScalarEvaluation (a : Kˣ) : LaurentPolynomial K →+* L

def

LaurentKummerFiberHom

L32 ↗

AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerFiberHom

Documentation

Points of the actual Kummer algebra above the specified Laurent point.

Source context 5 commands

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

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

Lean source · statement

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

theorem

laurentScalarEvaluation_coordinate

L38 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentScalarEvaluation_coordinate

Documentation

The Laurent coordinate specializes to the chosen base scalar.

Source context 5 commands

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

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

Lean source · statement

theorem laurentScalarEvaluation_coordinate (a : Kˣ) :
    laurentScalarEvaluation (L := L) a (LaurentPolynomial.T 1) =
      algebraMap K L (a : K)

theorem

laurentKummerFiberHom_root_pow

L45 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerFiberHom_root_pow

Documentation

The coordinate of a fibre point satisfies its Kummer equation.

Source context 5 commands

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

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

Lean source · statement

theorem laurentKummerFiberHom_root_pow (n : ℕ) (a : Kˣ)
    (f : LaurentKummerFiberHom (L := L) n a) :
    f.val (AdjoinRoot.root (X ^ n - C (LaurentPolynomial.T 1 : LaurentPolynomial K))) ^ n =
      algebraMap K L (a : K)

def

laurentKummerFiberHomOfRoot

L64 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerFiberHomOfRoot

Documentation

A root defines an actual point above the chosen Laurent scalar.

Source context 5 commands

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

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

Lean source · statement

def laurentKummerFiberHomOfRoot (n : ℕ) (a : Kˣ) (r : L)
    (hr : r ^ n = algebraMap K L (a : K)) : LaurentKummerFiberHom (L := L) n a

def

laurentKummerFiberEquivRoots

L72 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerFiberEquivRoots

Documentation

The fibre-point and root constructions are inverse, for the actual Laurent Kummer cover algebra.

Source context 5 commands

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

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

Lean source · full declaration

def laurentKummerFiberEquivRoots (n : ℕ) (a : Kˣ) :
    LaurentKummerFiberHom (L := L) n a ≃ {r : L // r ^ n = algebraMap K L (a : K)} where
  toFun f := ⟨f.val (AdjoinRoot.root _), laurentKummerFiberHom_root_pow n a f⟩
  invFun r := laurentKummerFiberHomOfRoot (L := L) n a r.val r.property
  left_inv f := by
    apply Subtype.ext
    apply AdjoinRoot.ringHom_ext
    · simp only [laurentKummerFiberHomOfRoot, AdjoinRoot.lift_comp_of]
      exact f.property.symm
    · simp only [laurentKummerFiberHomOfRoot, AdjoinRoot.lift_root]
  right_inv r := by
    apply Subtype.ext
    simp only [laurentKummerFiberHomOfRoot, AdjoinRoot.lift_root]

Module documentation

Roots as points of the Laurent Kummer fibre

Declarations

laurentScalarEvaluation

LaurentKummerFiberHom

laurentScalarEvaluation_coordinate

laurentKummerFiberHom_root_pow

laurentKummerFiberHomOfRoot

laurentKummerFiberEquivRoots