ModuleGenusZeroFundamentalGroup.lean
Nyll.AnabelianGeometry.GeometricFundamentalGroup.GenusZeroFundamentalGroup
2 declarations indexed from sourceView source ↗ Module documentation
+# The étale fundamental group of a proper genus-zero curve
We construct two distinct places and a generating rational parameter from the genus-zero hypothesis. The resulting function-field isomorphism gives an actual rational curve model. Pullback along the model isomorphism transports the proved rational-curve fundamental-group theorem to the original curve and its original geometric point.
Declarations
AnabelianGeometry.GeometricFundamentalGroup.nonempty_ratFunc_algEquiv_of_genus_zero
DocumentationA genus-zero curve function field over an algebraically closed field of characteristic zero is isomorphic to the rational function field, without chosen places or a chosen parameter.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup
variable {K F : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field F] [Algebra K F]
[IsCurveOver K F] [Algebra.EssFiniteType K F]
AnabelianGeometry.GeometricFundamentalGroup.subsingleton_fundamentalGroup_of_genus_zero
DocumentationThe actual étale fundamental group of a proper genus-zero curve model is trivial at every geometric point over a separably closed field. No rational coordinate or model is assumed.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup
variable {K F : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field F] [Algebra K F]
[IsCurveOver K F] [Algebra.EssFiniteType K F]