NYLL
Module

LaurentQuotientsEveryOrder.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentQuotientsEveryOrder
1 declaration indexed from sourceView source ↗

Module documentation

Cyclic quotients of every order of the actual Laurent fundamental group

The degree-n Kummer cover supplies a transitive action on n actual geometric points. Its finite image is cyclic by the already proved geometric quotient theorem. Evaluation at one point is then injective as well as surjective, so this image has order n.

Imports6
Imported by2

Declarations

theorem

exists_openNormalQuotient_fundamentalGroup_laurent_card

L32 ↗
AnabelianGeometry.GeometricFundamentalGroup.exists_openNormalQuotient_fundamentalGroup_laurent_card
Documentation

The actual etale fundamental group of the Laurent chart has a cyclic open normal quotient of every positive order. The quotient is constructed from a Kummer cover.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped IsMulCommutative
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem exists_openNormalQuotient_fundamentalGroup_laurent_card
    {K Ω : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of (LaurentPolynomial K)))
    {n : ℕ} (hn : 0 < n) :
    ∃ U : OpenNormalSubgroup π₁ᵉᵗ(ξ),
      IsCyclic (π₁ᵉᵗ(ξ) ⧸ (U : Subgroup π₁ᵉᵗ(ξ))) ∧
        Nat.card (π₁ᵉᵗ(ξ) ⧸ (U : Subgroup π₁ᵉᵗ(ξ))) = n

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