Module

LaurentKummerSplittingField.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerSplittingField

4 declarations indexed from sourceView source ↗

Module documentation

Recovering root fields from the whole Kummer fibre

The pointwise stabilizer of all algebra points of a Laurent Kummer fibre fixes precisely its full root field. After choosing one fibre point this is the field generated by its coordinate and the corresponding roots of unity. Thus the field is recovered from the actual Galois action on the fibre rather than from an assumed character comparison.

Imports2

Imported by2

theorem

mem_laurentKummerFiber_pointwise_stabilizer_iff

L31 ↗

AnabelianGeometry.GeometricFundamentalGroup.mem_laurentKummerFiber_pointwise_stabilizer_iff

Documentation

Fixing all fibre points is exactly fixing all roots of the Kummer equation.

Source context 6 commands

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

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

Lean source · statement

theorem mem_laurentKummerFiber_pointwise_stabilizer_iff
    (n : ℕ) (a : Kˣ) (σ : L ≃ₐ[K] L) :
    σ ∈ (⨅ f : LaurentKummerFiberHom (L := L) n a,
      MulAction.stabilizer (L ≃ₐ[K] L) f) ↔
        ∀ r : L, r ^ n = algebraMap K L (a : K) → σ r = r

theorem

laurentKummerFiber_pointwise_stabilizer

L48 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentKummerFiber_pointwise_stabilizer

Documentation

The pointwise stabilizer of the fibre is the fixing subgroup of its root field.

Source context 6 commands

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

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

Lean source · statement

theorem laurentKummerFiber_pointwise_stabilizer (n : ℕ) (a : Kˣ) :
    (⨅ f : LaurentKummerFiberHom (L := L) n a,
      MulAction.stabilizer (L ≃ₐ[K] L) f) =
        (rootField (L := L) n (a : K)).fixingSubgroup

theorem

fixedField_laurentKummerFiber_pointwise_stabilizer

L69 ↗

AnabelianGeometry.GeometricFundamentalGroup.fixedField_laurentKummerFiber_pointwise_stabilizer

Documentation

Recover the full Kummer root field from the action on the entire fibre.

Source context 6 commands

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

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

Lean source · statement

theorem fixedField_laurentKummerFiber_pointwise_stabilizer [IsGalois K L]
    (n : ℕ) (a : Kˣ) :
    IntermediateField.fixedField
      (⨅ f : LaurentKummerFiberHom (L := L) n a,
        MulAction.stabilizer (L ≃ₐ[K] L) f) = rootField (L := L) n (a : K)

theorem

fixedField_laurentKummerFiber_eq_adjoin

L78 ↗

AnabelianGeometry.GeometricFundamentalGroup.fixedField_laurentKummerFiber_eq_adjoin

Documentation

The field detected by the whole fibre is generated by one point's coordinate and the roots of unity, without assuming those roots lie in the base.

Source context 6 commands

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

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

Lean source · statement

theorem fixedField_laurentKummerFiber_eq_adjoin [IsGalois K L]
    {n : ℕ} (hn : n ≠ 0) (a : Kˣ) (f : LaurentKummerFiberHom (L := L) n a) :
    IntermediateField.fixedField
      (⨅ g : LaurentKummerFiberHom (L := L) n a,
        MulAction.stabilizer (L ≃ₐ[K] L) g) =
      IntermediateField.adjoin K
        (insert (f.val (AdjoinRoot.root _)) {ξ : L | ξ ^ n = 1})

Module documentation

Recovering root fields from the whole Kummer fibre

Declarations

mem_laurentKummerFiber_pointwise_stabilizer_iff

laurentKummerFiber_pointwise_stabilizer

fixedField_laurentKummerFiber_pointwise_stabilizer

fixedField_laurentKummerFiber_eq_adjoin