NYLL
Module

LaurentKummerFiberGalois.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerFiberGalois
6 declarations indexed from sourceView source ↗

Module documentation

Galois stabilizers of Laurent Kummer fibre points

Postcomposition gives the actual Galois action on the algebra points of a Laurent Kummer fibre. Its point stabilizer fixes exactly the radical field. This identifies the arithmetic point data without a roots-of-unity assumption.

Imports3
Imported by3

Declarations

theorem

laurentScalarEvaluation_fixed

L29 ↗
AnabelianGeometry.GeometricFundamentalGroup.laurentScalarEvaluation_fixed
Documentation

Evaluation at a base-field scalar is fixed by every base-field automorphism.

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_fixed (a : Kˣ) (σ : L ≃ₐ[K] L)
    (p : LaurentPolynomial K) :
    σ (laurentScalarEvaluation a p) = laurentScalarEvaluation a p
instance

laurentKummerFiberMulAction

L42 ↗
AnabelianGeometry.GeometricFundamentalGroup.laurentKummerFiberMulAction
Documentation

Galois acts on actual algebra points by postcomposition.

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
instance laurentKummerFiberMulAction (n : ℕ) (a : Kˣ) :
    MulAction (L ≃ₐ[K] L) (LaurentKummerFiberHom (L := L) n a) where
  smul σ f := ⟨σ.toRingHom.comp f.val, by
    rw [RingHom.comp_assoc, f.property]
    apply RingHom.ext
    intro p
    exact laurentScalarEvaluation_fixed a σ p⟩
  one_smul f := by
    apply Subtype.ext
    apply RingHom.ext
    intro p
    rfl
  mul_smul σ τ f := by
    apply Subtype.ext
    apply RingHom.ext
    intro p
    rfl
theorem

mem_laurentKummerFiber_stabilizer_iff

L61 ↗
AnabelianGeometry.GeometricFundamentalGroup.mem_laurentKummerFiber_stabilizer_iff
Documentation

Fixing a fibre point is equivalent to fixing its radical coordinate.

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 mem_laurentKummerFiber_stabilizer_iff (n : ℕ) (a : Kˣ)
    (f : LaurentKummerFiberHom (L := L) n a) (σ : L ≃ₐ[K] L) :
    σ ∈ MulAction.stabilizer (L ≃ₐ[K] L) f ↔
      σ (f.val (AdjoinRoot.root _)) = f.val (AdjoinRoot.root _)
theorem

laurentKummerFiber_root_ne_zero

L77 ↗
AnabelianGeometry.GeometricFundamentalGroup.laurentKummerFiber_root_ne_zero
Documentation

A positive-degree fibre point has a nonzero radical coordinate.

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 laurentKummerFiber_root_ne_zero {n : ℕ} (hn : n ≠ 0) (a : Kˣ)
    (f : LaurentKummerFiberHom (L := L) n a) :
    f.val (AdjoinRoot.root _) ≠ 0
theorem

laurentKummerFiber_stabilizer

L87 ↗
AnabelianGeometry.GeometricFundamentalGroup.laurentKummerFiber_stabilizer
Documentation

The stabilizer of an actual fibre point is the fixing subgroup of its radical field, including in an infinite ambient extension.

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 laurentKummerFiber_stabilizer {n : ℕ} (hn : n ≠ 0) (a : Kˣ)
    (f : LaurentKummerFiberHom (L := L) n a) :
    MulAction.stabilizer (L ≃ₐ[K] L) f =
      (IntermediateField.adjoin K ({f.val (AdjoinRoot.root _)} : Set L)).fixingSubgroup
theorem

fixedField_laurentKummerFiber_stabilizer

L99 ↗
AnabelianGeometry.GeometricFundamentalGroup.fixedField_laurentKummerFiber_stabilizer
Documentation

Recover the radical field from the Galois stabilizer of the fibre 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
theorem fixedField_laurentKummerFiber_stabilizer [IsGalois K L]
    {n : ℕ} (hn : n ≠ 0) (a : Kˣ) (f : LaurentKummerFiberHom (L := L) n a) :
    IntermediateField.fixedField (MulAction.stabilizer (L ≃ₐ[K] L) f) =
      IntermediateField.adjoin K ({f.val (AdjoinRoot.root _)} : Set L)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.