Nyll.EtaleFundamentalGroups.Kummer.GenericCharacterRootCover

Module documentation

Actual root fields of characters of the generic fundamental group

The separable field Kummer equivalence supplies a function and a root for each finite Kummer character of the scheme fundamental group. Its generic kernel fixes the actual field generated by that root, so that field is the literal generic fiber of an actual finite etale cover of the original scheme.

theorem

exists_finiteEtale_genericKummerRoot

L37 ↗

EtaleFundamentalGroups.Kummer.exists_finiteEtale_genericKummerRoot

Documentation

A character of the actual scheme fundamental group is represented by an actual Kummer root whose generated field extends to a finite etale cover. The exponent need only be nonzero in the function field.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
open scoped IntermediateField
open ClassFieldTower.Martinet.Shafarevich KummerTheory
namespace EtaleFundamentalGroups.Kummer

Lean source · statement

theorem exists_finiteEtale_genericKummerRoot
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (n : ℕ+) [NeZero ((n : ℕ) : X.functionField)]
    (hmu : (primitiveRoots (n : ℕ) X.functionField).Nonempty)
    (χ : Aut (FiniteEtale.fiber
      (X.genericExtensionMorphism (AlgebraicClosure X.functionField))) →ₜ*
        DiscreteNthRootsSubgroup (SeparableClosure X.functionField) (n : ℕ)) :
    ∃ (a : X.functionFieldˣ) (β : (SeparableClosure X.functionField)ˣ),
      β ^ (n : ℕ) = Units.map
        (algebraMap X.functionField (SeparableClosure X.functionField)).toMonoidHom a ∧
      (∀ σ : Gal(SeparableClosure X.functionField / X.functionField),
        (χ (FiniteEtale.genericAbsoluteGaloisHom X σ) :
          (SeparableClosure X.functionField)ˣ) = rootQuotient β σ) ∧
      ∃ (Y : Scheme.{u}) (f : Y ⟶ X), IsFinite f ∧ Etale f ∧
        ∃ e : Limits.pullback f (X.fromSpecStalk (genericPoint X)) ≅
            Spec (.of (X.functionField⟮(β : SeparableClosure X.functionField)⟯)),
          e.hom ≫ Spec.map (CommRingCat.ofHom
            (algebraMap X.functionField
              (X.functionField⟮(β : SeparableClosure X.functionField)⟯))) =
                Limits.pullback.snd f (X.fromSpecStalk (genericPoint X))

Module documentation

Actual root fields of characters of the generic fundamental group

Declarations

exists_finiteEtale_genericKummerRoot