NYLL
Module

RationalEtaleFunctionField.lean

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

Module documentation

Function fields of etale covers of a proper rational curve

In characteristic zero, a finite etale surjective morphism from a smooth proper integral curve model to a rational curve model induces an isomorphism of function fields. The isomorphism retains the actual morphism's correspondence between points and places. This conclusion uses the stalk comparison and Riemann--Hurwitz, not a fundamental-group presentation or an assumed triviality of covers.

Imports5
Imported by2

Declarations

theorem

exists_functionFieldEquiv_of_finite_etale_rational

L31 ↗
AnabelianGeometry.GeometricFundamentalGroup.exists_functionFieldEquiv_of_finite_etale_rational
Documentation

A finite etale cover of a proper rational curve in characteristic zero has the same function field, with the isomorphism compatible with the actual map on curve points.

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 exists_functionFieldEquiv_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) :
    ∃ e : RatFunc K ≃ₐ[K] F, ∃ hint : e.toAlgHom.toRingHom.IsIntegral,
      ∀ w : Place K F,
        (M.pointEquivPlace.symm (w.restrictAlong e.toAlgHom hint)).1 =
          (N.pointEquivPlace.symm w).1 ≫ π

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