NYLL
Module

LaurentFundamentalGroupQuotients.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentFundamentalGroupQuotients
3 declarations indexed from sourceView source ↗

Module documentation

Cyclic finite quotients of the actual multiplicative-line fundamental group

The stabilizers of pointed Galois covers form a neighbourhood basis for the actual fibre-functor automorphism group. Each such stabilizer is the kernel of the quotient to the opposite cover automorphism group. The proved geometric cyclicity therefore implies cyclicity of every open normal quotient. No classification of covers or cofinal Kummer system is assumed.

Imports9
Imported by4

Declarations

theorem

isCyclic_openNormalQuotient_fundamentalGroup_laurent

L36 ↗
AnabelianGeometry.GeometricFundamentalGroup.isCyclic_openNormalQuotient_fundamentalGroup_laurent
Documentation

Every open normal quotient of the actual etale fundamental group of the multiplicative line is cyclic over an algebraically closed field of characteristic zero.

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 Topology
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem isCyclic_openNormalQuotient_fundamentalGroup_laurent
    {K Ω : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of (LaurentPolynomial K)))
    (U : OpenNormalSubgroup π₁ᵉᵗ(ξ)) : IsCyclic (π₁ᵉᵗ(ξ) ⧸ (U : Subgroup π₁ᵉᵗ(ξ)))
theorem

hasCyclicOpenNormalBasis_fundamentalGroup_laurent

L65 ↗
AnabelianGeometry.GeometricFundamentalGroup.hasCyclicOpenNormalBasis_fundamentalGroup_laurent
Documentation

The actual quotient topology on the multiplicative-line fundamental group admits an open normal basis with cyclic finite quotients.

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 Topology
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem hasCyclicOpenNormalBasis_fundamentalGroup_laurent
    {K Ω : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of (LaurentPolynomial K))) :
    ProCGroups.ProC.HasCyclicOpenNormalBasis π₁ᵉᵗ(ξ)
theorem

exists_topological_generator_fundamentalGroup_laurent

L74 ↗
AnabelianGeometry.GeometricFundamentalGroup.exists_topological_generator_fundamentalGroup_laurent
Documentation

The actual multiplicative-line fundamental group has a topological generator.

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 Topology
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem exists_topological_generator_fundamentalGroup_laurent
    {K Ω : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of (LaurentPolynomial K))) :
    ∃ g : π₁ᵉᵗ(ξ), ProCGroups.Generation.TopologicallyGenerates ({g} : Set π₁ᵉᵗ(ξ))

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