Module

GenericEtaleDivisibility.lean

Nyll.EtaleFundamentalGroups.Kummer.GenericEtaleDivisibility

2 declarations indexed from sourceView source ↗

Module documentation

Divisibility of orders from an actual finite étale generic root cover

A root in the field forming the generic fiber of a finite étale cover has integral order at every point of the covering curve. The actual ramification index is one, so the original orders are divisible by the root exponent.

Imports11

Imported by2

theorem

ord_dvd_of_model_root

L37 ↗

EtaleFundamentalGroups.ord_dvd_of_model_root

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicCurves.Models.Proofs
open
  CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace EtaleFundamentalGroups

Lean source · statement

theorem ord_dvd_of_model_root
    (K : Type) [Field K] [IsAlgClosed K]
    {F E L : Type} [Field F] [Field E] [Field L] [Algebra K F] [Algebra K E]
    (M : CurveModel K F) (N : CurveModel K E) [Algebra M.C.functionField L]
    (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase) [IsFinite d] [Etale d]
    (p : Spec (.of L) ⟶ N.C) [IsDominant p] [IsPreimmersion p]
    (hp : p ≫ d = Spec.map (CommRingCat.ofHom (algebraMap M.C.functionField L)) ≫
      M.C.fromSpecStalk (genericPoint M.C))
    (a : M.C.functionField) (b : L) (n : ℕ)
    (hb : b ^ n = algebraMap M.C.functionField L a) :
    ∀ v : Place K F, (n : ℤ) ∣ v.ord (M.ffEquiv.symm a)

theorem

ord_dvd_of_finiteEtale_generic_root

L127 ↗

EtaleFundamentalGroups.ord_dvd_of_finiteEtale_generic_root

Documentation

If the actual generic fiber of a finite étale cover contains an nth root of a rational function, its order at every place is divisible by n.