NYLL
Module

CurveCoverRamification.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.CurveCoverRamification
2 declarations indexed from sourceView source ↗

Module documentation

Ramification of actual curve covers

A finite surjective morphism of smooth proper curve models supplies its own function-field homomorphism and place correspondence. At a point where its actual stalk map is formally unramified, the associated place has ramification index one. The comparison follows from the image of the maximal ideal and the discrete valuation of the target stalk.

Imports5
Imported by2

Declarations

theorem

exists_functionFieldMap_ramification_eq_one_at_unramified_stalk

L31 ↗
AnabelianGeometry.GeometricFundamentalGroup.exists_functionFieldMap_ramification_eq_one_at_unramified_stalk
Documentation

A finite flat cover supplies a function-field map whose ramification index is one where the actual scheme stalk map is formally unramified.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve IsLocalRing
namespace AnabelianGeometry.GeometricFundamentalGroup
open AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex in
Lean source · statement
theorem exists_functionFieldMap_ramification_eq_one_at_unramified_stalk
    {K F E : Type} [Field K] [IsAlgClosed K] [Field F] [Field E]
    [Algebra K F] [Algebra K E] [IsCurveOver K F] [IsCurveOver K E]
    [Algebra.EssFiniteType K F] [Algebra.EssFiniteType K E]
    (M : CurveModel K F) (N : CurveModel K E)
    (π : N.C ⟶ M.C) (hπ : π ≫ M.toBase = N.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
    (hsurj : Function.Surjective π.base) :
    ∃ φ : F →ₐ[K] E, FiniteAlong K φ ∧ ∃ hint : φ.toRingHom.IsIntegral,
      (∀ w : Place K E,
        (M.pointEquivPlace.symm (w.restrictAlong φ hint)).1 =
          (N.pointEquivPlace.symm w).1 ≫ π) ∧
      ∀ w : Place K E,
        RingHom.FormallyUnramified
          (π.stalkMap (pointEquivClosedPoint N.toBase (N.pointEquivPlace.symm w)).1).hom →
          w.ramificationIndexAlong φ = 1
theorem

exists_functionFieldMap_unramified_of_finite_etale

L96 ↗
AnabelianGeometry.GeometricFundamentalGroup.exists_functionFieldMap_unramified_of_finite_etale
Documentation

Every place in the function-field extension of an actual finite etale cover of smooth proper curve models is unramified.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve IsLocalRing
namespace AnabelianGeometry.GeometricFundamentalGroup
Lean source · statement
theorem exists_functionFieldMap_unramified_of_finite_etale
    {K F E : Type} [Field K] [IsAlgClosed K] [Field F] [Field E]
    [Algebra K F] [Algebra K E] [IsCurveOver K F] [IsCurveOver K E]
    [Algebra.EssFiniteType K F] [Algebra.EssFiniteType K E]
    (M : CurveModel K F) (N : CurveModel K E)
    (π : N.C ⟶ M.C) (hπ : π ≫ M.toBase = N.toBase)
    [IsFinite π] [Etale π] (hsurj : Function.Surjective π.base) :
    ∃ φ : F →ₐ[K] E, FiniteAlong K φ ∧ ∃ hint : φ.toRingHom.IsIntegral,
      (∀ w : Place K E,
        (M.pointEquivPlace.symm (w.restrictAlong φ hint)).1 =
          (N.pointEquivPlace.symm w).1 ≫ π) ∧
      ∀ w : Place K E, w.ramificationIndexAlong φ = 1

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