Module

LaurentKummerCovers.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerCovers

1 declaration indexed from sourceView source ↗

Module documentation

Actual connected finite-etale Kummer covers of every positive degree

Taking the spectrum of the explicit Kummer algebra produces the cover. Its source is connected because the algebra is a domain, and its actual geometric fibre has the prescribed cardinality by the power basis and the finite-etale rank comparison.

Imports6

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentKummerAlgebra
Nyll.EtaleFundamentalGroups.GaloisCovers.Basic
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Imported by3

theorem

exists_connected_finite_etale_laurent_of_degree

L33 ↗

AnabelianGeometry.GeometricFundamentalGroup.exists_connected_finite_etale_laurent_of_degree

Documentation

Every positive degree occurs for an actual connected finite-etale cover of the Laurent chart, uniformly at every separably closed geometric point.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u

Lean source · statement

theorem exists_connected_finite_etale_laurent_of_degree
    (K : Type u) [Field K] [CharZero K] {n : ℕ} (hn : 0 < n) :
    ∃ Y : FiniteEtale (Spec (CommRingCat.of (LaurentPolynomial K))),
      ConnectedSpace Y.left ∧
      ∀ (Ω : Type u) [Field Ω] [IsSepClosed Ω]
        (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of (LaurentPolynomial K))),
        Nat.card ((fiber ξ).obj Y) = n

Module documentation

Actual connected finite-etale Kummer covers of every positive degree

Declarations

exists_connected_finite_etale_laurent_of_degree