Module

RationalEtaleIsomorphism.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.RationalEtaleIsomorphism

1 declaration indexed from sourceView source ↗

Module documentation

Finite etale covers of proper rational curve models

In characteristic zero, a finite etale surjection from an integral curve model to a proper rational curve model is itself an isomorphism. The function-field equivalence constructs a model isomorphism. Its action on valuation subrings agrees with restriction along the original field map, so the two scheme morphisms agree on every closed point. Geometric-point density on the reduced source then identifies the actual morphisms.

No fundamental-group presentation is used. Passing from arbitrary connected finite etale covers to curve models and identifying the fundamental group are separate steps.

Imports5

Imported by2

theorem

isIso_of_finite_etale_rational

L38 ↗

AnabelianGeometry.GeometricFundamentalGroup.isIso_of_finite_etale_rational

Documentation

Every finite etale surjection between integral proper curve models with rational target over an algebraically closed field of characteristic zero is an isomorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup
open AlgebraicCurves.Geometry.Schemes.Proofs
open SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
open RigKerGeomPoints renaming ext_of_forall_geometric_point → geometricHomExt in

Lean source · statement

theorem isIso_of_finite_etale_rational
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field F]
    [Algebra K F] [IsCurveOver K F] [Algebra.EssFiniteType K F]
    (M : CurveModel K (RatFunc K)) (N : CurveModel K F)
    (π : N.C ⟶ M.C) (hπ : π ≫ M.toBase = N.toBase)
    [IsFinite π] [Etale π] (hsurj : Function.Surjective π.base) : IsIso π

Module documentation

Finite etale covers of proper rational curve models

Declarations

isIso_of_finite_etale_rational