NYLL
Module

RationalOneBranch.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.RationalOneBranch
2 declarations indexed from sourceView source ↗

Module documentation

Rational covers with at most one tame branch point

Riemann--Hurwitz and the fundamental identity of a place show that a finite separable extension of an algebraically closed rational function field, tame everywhere and unramified away from one place, has degree one. In characteristic zero the tameness hypothesis is automatic.

This is a function-field step towards the structure of the fundamental groups of the projective and affine lines. The scheme-theoretic comparison with finite etale covers is a separate step. The proof uses the proved Riemann--Hurwitz theorem and does not import the unproved surface presentation theorem.

Imports7
Imported by3

Declarations

theorem

finrank_eq_one_of_tame_one_branch

L39 ↗
AnabelianGeometry.GeometricFundamentalGroup.finrank_eq_one_of_tame_one_branch
Documentation

A tame cover of the rational function field with at most one branch place has degree one.

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]
Lean source · statement
theorem finrank_eq_one_of_tame_one_branch [Algebra.IsSeparable (RatFunc K) F]
    (v : Place K (RatFunc K))
    (htame : ∀ w : Place K F, (w.ramificationIndex (RatFunc K) : K) ≠ 0)
    (hunramified : ∀ w : Place K F, w.restrict (RatFunc K) ≠ v →
      w.ramificationIndex (RatFunc K) = 1) :
    Module.finrank (RatFunc K) F = 1
theorem

bijective_algebraMap_of_one_branch

L75 ↗
AnabelianGeometry.GeometricFundamentalGroup.bijective_algebraMap_of_one_branch
Documentation

In characteristic zero, a rational function-field cover ramified over at most one place is the original field: the given algebra map is bijective.

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]
Lean source · statement
theorem bijective_algebraMap_of_one_branch [CharZero K] (v : Place K (RatFunc K))
    (hunramified : ∀ w : Place K F, w.restrict (RatFunc K) ≠ v →
      w.ramificationIndex (RatFunc K) = 1) :
    Function.Bijective (algebraMap (RatFunc K) F)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.