AnabelianGeometry.GeometricFundamentalGroup.exists_fundamentalGroup_profiniteInteger_equiv_of_finrank_H1_eq_zero_complement_pair
The actual etale fundamental group of a smooth proper genus-zero curve minus two distinct closed points is topologically isomorphic to the full profinite integers in characteristic zero. No rational model, affine coordinates, or comparison morphism is part of the input.
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.CompletionLean source · statement
theorem exists_fundamentalGroup_profiniteInteger_equiv_of_finrank_H1_eq_zero_complement_pair
{K : Type} [Field K] [IsAlgClosed K] [CharZero K]
(X : Scheme.{0}) [IsIntegral X] (c : X ⟶ Spec (.of K))
[IsProper c] [SmoothOfRelativeDimension 1 c] (𝒱 : X.TwoAffineOpenCover)
(hg : Module.finrank K (𝒱.structureSheafSections c).H1 = 0)
(x y : closedPoints X) (hne : x ≠ y)
(U : X.Opens) (hU : (U : Set X) = {x.1, y.1}ᶜ)
{Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U.toScheme) :
∃ (g : π₁ᵉᵗ(ξ))
(e : π₁ᵉᵗ(ξ) ≃ₜ* Multiplicative
(ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))),
Generation.TopologicallyGenerates ({g} : Set π₁ᵉᵗ(ξ)) ∧
e g = proCIntegerOne (C := FiniteGroupClass.allFinite)