Nyll.AnabelianGeometry.GeometricFundamentalGroup.RationalCyclicGalois

Module documentation

The cyclic Galois group of a two-branch rational cover

In characteristic zero, a finite extension of an algebraically closed rational function field unramified away from two places is Galois and cyclic. Its actual automorphism group identifies with the degree-th roots of unity in the constant field, and this identification acts by scaling a generating coordinate. The power-coordinate theorem supplies the Kummer generator; neither normality nor cyclicity is assumed.

theorem

cyclic_galois_of_two_branches_charZero

L29 ↗

AnabelianGeometry.GeometricFundamentalGroup.cyclic_galois_of_two_branches_charZero

Documentation

A two-branch rational function-field cover in characteristic zero is cyclic Galois, with its automorphisms acting on a generating coordinate through roots of unity in the constant field.

Source context 3 commands

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

noncomputable section
open AlgebraicCurve Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup

Lean source · statement

theorem cyclic_galois_of_two_branches_charZero
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field F]
    [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [FiniteDimensional (RatFunc K) F]
    (v₀ v₁ : Place K (RatFunc K)) (hne : v₀ ≠ v₁)
    (hunramified : ∀ w : Place K F, w.restrict (RatFunc K) ≠ v₀ →
      w.restrict (RatFunc K) ≠ v₁ → w.ramificationIndex (RatFunc K) = 1) :
    IsGalois (RatFunc K) F ∧ IsCyclic (F ≃ₐ[RatFunc K] F) ∧
      ∃ t : F, ∃ e : (F ≃ₐ[RatFunc K] F) ≃* rootsOfUnity (Module.finrank (RatFunc K) F) K,
        IntermediateField.adjoin K ({t} : Set F) = ⊤ ∧
        ∀ σ : F ≃ₐ[RatFunc K] F, σ t = algebraMap K F ((e σ : Kˣ) : K) * t

Module documentation

The cyclic Galois group of a two-branch rational cover

Declarations

cyclic_galois_of_two_branches_charZero