NYLL
Module

LaurentKummerArithmeticAction.lean

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

Module documentation

The actual arithmetic action on Kummer fibres

The canonical Galois action on the geometric fibre of the pulled-back finite-etale scheme agrees with postcomposition on the root algebra points. Its pointwise stabilizer therefore recovers the full root field. This is a comparison theorem for the existing geometric-fibre functor, not a newly transported action defined to make the comparison true.

Imports2
Imported by1

Declarations

theorem

laurentKummerArithmeticFiberEquiv_smul

L33 ↗
AnabelianGeometry.GeometricFundamentalGroup.laurentKummerArithmeticFiberEquiv_smul
Documentation

The arithmetic-fibre comparison intertwines the existing geometric Galois action with literal postcomposition on algebra points.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open AnabelianGeometry.KummerTheory
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] [CharZero K]
  {L : Type u} [Field L] [Algebra K L] [IsSepClosed L]
Lean source · statement
theorem laurentKummerArithmeticFiberEquiv_smul
    (n : ℕ) (hn : 0 < n) (a : Kˣ) (σ : L ≃ₐ[K] L)
    (z : (fib K L).obj (laurentKummerArithmeticFiber n hn a)) :
    laurentKummerArithmeticFiberEquiv n hn a (σ • z) =
      σ • laurentKummerArithmeticFiberEquiv n hn a z
theorem

laurentKummerArithmeticFiber_pointwise_stabilizer

L62 ↗
AnabelianGeometry.GeometricFundamentalGroup.laurentKummerArithmeticFiber_pointwise_stabilizer
Documentation

The kernel of the actual arithmetic fibre action is the fixing subgroup of the root field.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open AnabelianGeometry.KummerTheory
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] [CharZero K]
  {L : Type u} [Field L] [Algebra K L] [IsSepClosed L]
Lean source · statement
theorem laurentKummerArithmeticFiber_pointwise_stabilizer
    (n : ℕ) (hn : 0 < n) (a : Kˣ) :
    (⨅ z : (fib K L).obj (laurentKummerArithmeticFiber n hn a),
      MulAction.stabilizer (L ≃ₐ[K] L) z) =
      (rootField (L := L) n (a : K)).fixingSubgroup
theorem

fixedField_laurentKummerArithmeticFiber

L73 ↗
AnabelianGeometry.GeometricFundamentalGroup.fixedField_laurentKummerArithmeticFiber
Documentation

The pointwise stabilizer of the actual arithmetic geometric fibre fixes exactly the full Kummer root field.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open AnabelianGeometry.KummerTheory
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] [CharZero K]
  {L : Type u} [Field L] [Algebra K L] [IsSepClosed L]
Lean source · statement
theorem fixedField_laurentKummerArithmeticFiber [IsGalois K L]
    (n : ℕ) (hn : 0 < n) (a : Kˣ) :
    IntermediateField.fixedField
      (⨅ z : (fib K L).obj (laurentKummerArithmeticFiber n hn a),
        MulAction.stabilizer (L ≃ₐ[K] L) z) = rootField (L := L) n (a : K)
theorem

rootField_eq_of_arithmeticFiber_equiv

L84 ↗
AnabelianGeometry.GeometricFundamentalGroup.rootField_eq_of_arithmeticFiber_equiv
Documentation

An equivariant bijection of the actual arithmetic fibres determines the same full Kummer root field.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open AnabelianGeometry.KummerTheory
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] [CharZero K]
  {L : Type u} [Field L] [Algebra K L] [IsSepClosed L]
Lean source · statement
theorem rootField_eq_of_arithmeticFiber_equiv [IsGalois K L]
    (n : ℕ) (hn : 0 < n) (a b : Kˣ)
    (e : (fib K L).obj (laurentKummerArithmeticFiber n hn a) ≃
      (fib K L).obj (laurentKummerArithmeticFiber n hn b))
    (he : ∀ (σ : L ≃ₐ[K] L) (z : (fib K L).obj (laurentKummerArithmeticFiber n hn a)),
      e (σ • z) = σ • e z) :
    rootField (L := L) n (a : K) = rootField (L := L) n (b : K)
theorem

fixedField_two_arithmeticFiber_stabilizers

L97 ↗
AnabelianGeometry.GeometricFundamentalGroup.fixedField_two_arithmeticFiber_stabilizers
Documentation

Simultaneous pointwise fixing in two actual finite-etale fibres recovers the compositum of their root fields.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open AnabelianGeometry.KummerTheory
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] [CharZero K]
  {L : Type u} [Field L] [Algebra K L] [IsSepClosed L]
Lean source · statement
theorem fixedField_two_arithmeticFiber_stabilizers [IsGalois K L]
    (n : ℕ) (hn : 0 < n) (a b : Kˣ) :
    IntermediateField.fixedField
      ((⨅ z : (fib K L).obj (laurentKummerArithmeticFiber n hn a),
        MulAction.stabilizer (L ≃ₐ[K] L) z) ⊓
       (⨅ z : (fib K L).obj (laurentKummerArithmeticFiber n hn b),
        MulAction.stabilizer (L ≃ₐ[K] L) z)) =
      rootField (L := L) n (a : K) ⊔ rootField (L := L) n (b : K)
theorem

iInf_fixedField_twisted_arithmeticFibers

L111 ↗
AnabelianGeometry.GeometricFundamentalGroup.iInf_fixedField_twisted_arithmeticFibers
Documentation

The common-twist family of actual arithmetic fibre actions recovers the root field of the ratio.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open AnabelianGeometry.KummerTheory
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u
variable {K : Type u} [Field K] [CharZero K]
  {L : Type u} [Field L] [Algebra K L] [IsSepClosed L]
Lean source · statement
theorem iInf_fixedField_twisted_arithmeticFibers [IsGalois K L] [IsAlgClosed L]
    (n : ℕ) (hn : 0 < n) (x y : Kˣ) :
    (⨅ c : Kˣ, IntermediateField.fixedField
      ((⨅ z : (fib K L).obj (laurentKummerArithmeticFiber n hn (c * x)),
        MulAction.stabilizer (L ≃ₐ[K] L) z) ⊓
       (⨅ z : (fib K L).obj (laurentKummerArithmeticFiber n hn (c * y)),
        MulAction.stabilizer (L ≃ₐ[K] L) z))) =
      rootField (L := L) n ((y / x : Kˣ) : K)

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