NYLL
Module

RationalConnectedEtale.lean

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

Module documentation

Connected finite etale covers of a proper rational curve

A connected finite etale cover of a proper rational curve model is an isomorphism in characteristic zero. No curve model, function field, surjectivity, or integrality of the cover is assumed. Smoothness gives domain stalks and local Noetherianity; connectedness then gives integrality. The actual curve-model construction supplies the input for the rational-cover theorem.

Imports7
Imported by2

Declarations

theorem

isIso_of_connected_finite_etale_rational

L33 ↗
AnabelianGeometry.GeometricFundamentalGroup.isIso_of_connected_finite_etale_rational
Documentation

A connected finite etale cover of a proper rational curve over an algebraically closed field of characteristic zero is an isomorphism.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem isIso_of_connected_finite_etale_rational
    {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
    (M : CurveModel K (RatFunc K)) {Y : Scheme.{0}} [ConnectedSpace Y]
    (π : Y ⟶ M.C) [IsFinite π] [Etale π] : IsIso π

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