Module

FiniteEtaleRiemannHurwitz.lean

Nyll.AlgebraicCurves.Models.FiniteEtaleRiemannHurwitz

3 declarations indexed from sourceView source ↗

Module documentation

Riemann--Hurwitz for an actual finite étale morphism of curve models

The function-field homomorphism is induced by the scheme morphism. Unramifiedness at every place is proved from the actual étale morphism; there is no ramification or genus formula assumption.

Imports4

Imported by4

def

finiteEtaleFieldMap

L34 ↗

AlgebraicCurve.CurveModel.finiteEtaleFieldMap

Documentation

The function-field map of an actual finite étale curve morphism.

Source context 6 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
variable {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)
  [IsFinite d] [Etale d]

Lean source · statement

def finiteEtaleFieldMap : F →ₐ[K] E

theorem

ramificationIndexAlong_finiteEtaleFieldMap

L40 ↗

AlgebraicCurve.CurveModel.ramificationIndexAlong_finiteEtaleFieldMap

Documentation

Every place is unramified for the actual induced function-field map.

Source context 6 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
variable {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)
  [IsFinite d] [Etale d]

Lean source · statement

theorem ramificationIndexAlong_finiteEtaleFieldMap (w : Place K E) :
    Place.ramificationIndexAlong (M.finiteEtaleFieldMap N d hd) w = 1

theorem

two_mul_genus_sub_two_eq_finiteEtale

L70 ↗

AlgebraicCurve.CurveModel.two_mul_genus_sub_two_eq_finiteEtale

Documentation

The actual étale cover degree multiplies the Euler characteristic.

Source context 6 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
variable {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)
  [IsFinite d] [Etale d]

Lean source · statement

theorem two_mul_genus_sub_two_eq_finiteEtale
    [CharZero K]
    (hF : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    2 * (genusFF K E : ℤ) - 2 =
      (finrankAlong K (M.finiteEtaleFieldMap N d hd) : ℤ) *
        (2 * (genusFF K F : ℤ) - 2)

Module documentation

Riemann--Hurwitz for an actual finite étale morphism of curve models

Declarations

finiteEtaleFieldMap

ramificationIndexAlong_finiteEtaleFieldMap

two_mul_genus_sub_two_eq_finiteEtale