AlgebraicCurve.CurveModel.two_mul_genus_add_openBoundary_sub_two_eq
The actual omitted-place counts satisfy the open Euler-characteristic formula. Unramifiedness is proved from the open restriction, and the boundary preimage is translated through the actual map on local rings.
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
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smoothLean source · statement
theorem two_mul_genus_add_openBoundary_sub_two_eq
{K F E : Type} [Field K] [IsAlgClosed K] [CharZero 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] (hsurj : Function.Surjective d)
{X Y : Scheme} [Nonempty X] [Nonempty Y]
(j : X ⟶ M.C) [IsOpenImmersion j]
(k : Y ⟶ N.C) [IsOpenImmersion k] [FormallyUnramified (k ≫ d)]
(hboundary : ∀ y : N.C, y ∉ Set.range k ↔ d y ∉ Set.range j) :
2 * (genusFF K E : ℤ) + (N.openBoundaryPlaces_finite k).toFinset.card - 2 =
(finrankAlong K (M.finiteCurveFieldMap N d hd hsurj) : ℤ) *
(2 * (genusFF K F : ℤ) + (M.openBoundaryPlaces_finite j).toFinset.card - 2)