Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentProfiniteIntegers

Module documentation

The actual fundamental group of the multiplicative line

The finite-etale geometry supplies both a topological generator and actual quotients of every positive order. The normalized-coefficient construction identifies the fibre-functor automorphism group, with its original topology, with the inverse limit of all finite cyclic groups. The isomorphism depends on the choice of topological generator.

theorem

exists_fundamentalGroup_laurent_profiniteInteger_equiv

L33 ↗

AnabelianGeometry.GeometricFundamentalGroup.exists_fundamentalGroup_laurent_profiniteInteger_equiv

Documentation

Over an algebraically closed characteristic-zero field, the actual etale fundamental group of the multiplicative line is the full profinite integer group. The displayed generator and isomorphism are constructed, not supplied as comparison data.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace AnabelianGeometry.GeometricFundamentalGroup
open ProCGroups ProCGroups.Completion

Lean source · statement

theorem exists_fundamentalGroup_laurent_profiniteInteger_equiv
    {K Ω : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ Spec (.of (LaurentPolynomial K))) :
    ∃ (g : π₁ᵉᵗ(ξ))
      (e : π₁ᵉᵗ(ξ) ≃ₜ* Multiplicative
        (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))),
      Generation.TopologicallyGenerates ({g} : Set π₁ᵉᵗ(ξ)) ∧
      e g = proCIntegerOne (C := FiniteGroupClass.allFinite)

Module documentation

The actual fundamental group of the multiplicative line

Declarations

exists_fundamentalGroup_laurent_profiniteInteger_equiv