Module

RationalTwoBranches.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.RationalTwoBranches

1 declaration indexed from sourceView source ↗

Module documentation

Tame rational covers with at most two branch places

A finite separable extension of an algebraically closed rational function field, tame everywhere and unramified away from two distinct places, has genus zero and exactly one place above each of the two possible branch places. This is proved directly from Riemann--Hurwitz and the two local fundamental identities. It is the ramification step towards classifying covers of the punctured affine line; a Kummer description and the geometric fundamental-group comparison are separate.

Imports6

Imported by2

theorem

genus_and_fibres_of_tame_two_branches

L36 ↗

AnabelianGeometry.GeometricFundamentalGroup.genus_and_fibres_of_tame_two_branches

Documentation

With at most two tame branch places, the cover has genus zero and a singleton fibre over each possible branch place.

Source context 4 commands

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

noncomputable section
open AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup
variable {K F : Type*} [Field K] [IsAlgClosed K] [Field F]
  [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
  [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]

Lean source · statement

theorem genus_and_fibres_of_tame_two_branches
    (v₀ v₁ : Place K (RatFunc K)) (hne : v₀ ≠ v₁)
    (htame : ∀ w : Place K F, (w.ramificationIndex (RatFunc K) : K) ≠ 0)
    (hunramified : ∀ w : Place K F, w.restrict (RatFunc K) ≠ v₀ →
      w.restrict (RatFunc K) ≠ v₁ → w.ramificationIndex (RatFunc K) = 1) :
    genusFF K F = 0 ∧ (v₀.fiberOver F).card = 1 ∧ (v₁.fiberOver F).card = 1

Module documentation

Tame rational covers with at most two branch places

Declarations

genus_and_fibres_of_tame_two_branches