Module

OpenBoundary.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.OpenBoundary

4 declarations indexed from sourceView source ↗

Module documentation

Boundary terms in Riemann--Hurwitz

The boundary upstairs is the actual union of valuation fibers. Its weighted cardinality is obtained from the finite-extension degree formula. Thus the boundary correction cancels the ramification term for an extension that is unramified off this boundary.

Imports4

Imported by2

def

boundaryAbove

L33 ↗

AlgebraicCurve.boundaryAbove

Documentation

The actual finite set of places above the specified finite boundary.

Source context 4 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  [IsCurveOver K F] [Algebra.EssFiniteType K F]
  [IsCurveOver K E] [Algebra.EssFiniteType K E]

Lean source · statement

def boundaryAbove (φ : F →ₐ[K] E) (hφ : φ.toRingHom.IsIntegral)
    (S : Finset (Place K F)) : Finset (Place K E)

theorem

mem_boundaryAbove_iff

L41 ↗

AlgebraicCurve.mem_boundaryAbove_iff

Source context 5 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  [IsCurveOver K F] [Algebra.EssFiniteType K F]
  [IsCurveOver K E] [Algebra.EssFiniteType K E]
omit [IsAlgClosed K] [IsCurveOver K F] [Algebra.EssFiniteType K F]
  [Algebra.EssFiniteType K E] in

Lean source · statement

theorem mem_boundaryAbove_iff
    (φ : F →ₐ[K] E) (hφ : φ.toRingHom.IsIntegral)
    (S : Finset (Place K F)) (w : Place K E) :
    w ∈ boundaryAbove φ hφ S ↔ w.restrictAlong φ hφ ∈ S

theorem

sum_boundaryAbove_ramification

L57 ↗

AlgebraicCurve.sum_boundaryAbove_ramification

Documentation

Actual ramification weights above the boundary sum to degree times the number of omitted places.

Source context 4 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  [IsCurveOver K F] [Algebra.EssFiniteType K F]
  [IsCurveOver K E] [Algebra.EssFiniteType K E]

Lean source · statement

theorem sum_boundaryAbove_ramification
    (φ : F →ₐ[K] E) (hφ : φ.toRingHom.IsIntegral)
    (hfin : FiniteAlong K φ) (hsep : SeparableAlong K φ)
    (S : Finset (Place K F)) :
    ∑ w ∈ boundaryAbove φ hφ S, (Place.ramificationIndexAlong φ w : ℤ) =
      (S.card : ℤ) * (finrankAlong K φ : ℤ)

theorem

two_mul_genus_add_boundary_sub_two_eq

L83 ↗

AlgebraicCurve.two_mul_genus_add_boundary_sub_two_eq

Documentation

Riemann--Hurwitz with the actual finite boundary correction. The unramifiedness premise is supplied geometrically by the actual open restriction; this theorem performs only the subsequent divisor calculation.

Source context 4 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  [IsCurveOver K F] [Algebra.EssFiniteType K F]
  [IsCurveOver K E] [Algebra.EssFiniteType K E]

Lean source · statement

theorem two_mul_genus_add_boundary_sub_two_eq
    [CharZero K]
    (φ : F →ₐ[K] E) (hφ : φ.toRingHom.IsIntegral)
    (hfin : FiniteAlong K φ) (hsep : SeparableAlong K φ)
    (hF : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (S : Finset (Place K F))
    (hunramified : ∀ w : Place K E, w.restrictAlong φ hφ ∉ S →
      Place.ramificationIndexAlong φ w = 1) :
    2 * (genusFF K E : ℤ) + (boundaryAbove φ hφ S).card - 2 =
      (finrankAlong K φ : ℤ) * (2 * (genusFF K F : ℤ) + S.card - 2)

Module documentation

Boundary terms in Riemann--Hurwitz

Declarations

boundaryAbove

mem_boundaryAbove_iff

sum_boundaryAbove_ramification

two_mul_genus_add_boundary_sub_two_eq