Module

FiniteEtaleHyperbolicGenus.lean

Nyll.AlgebraicCurves.Models.FiniteEtaleHyperbolicGenus

2 declarations indexed from sourceView source ↗

Module documentation

Proper hyperbolicity under actual finite étale covers

Imports3

Nyll.AlgebraicCurves.Models.FiniteEtaleRiemannHurwitz
Nyll.AlgebraicCurves.Models.IsCurveOver_of_isIntegral_of_smoothOfRelativeDimension_one
Mathlib.Tactic.Linarith

Imported by3

theorem

finrankAlong_finiteEtaleFieldMap_pos

L23 ↗

AlgebraicCurve.CurveModel.finrankAlong_finiteEtaleFieldMap_pos

Documentation

The actual field degree of a finite étale morphism of connected curve models is strictly positive.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace AlgebraicCurve.CurveModel

Lean source · statement

theorem finrankAlong_finiteEtaleFieldMap_pos
    {K F E : Type} [Field K] [IsAlgClosed K]
    [Field F] [Field E] [Algebra K F] [Algebra K E]
    (M : CurveModel K F) (N : CurveModel K E)
    (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase) [IsFiniteEtale d] :
    0 < finrankAlong K (M.finiteEtaleFieldMap N d hd)

theorem

genus_ge_two_of_finiteEtale

L38 ↗

AlgebraicCurve.CurveModel.genus_ge_two_of_finiteEtale