Module

RationalKummer.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.RationalKummer

4 declarations indexed from sourceView source ↗

Module documentation

Power coordinates for rational covers with two branch places

The tame two-branch theorem supplies genus zero and the two singleton fibres. The genus-zero parameter theorem then supplies actual generating coordinates on both fields. Comparing their divisors makes the pulled-back base parameter a scalar times a power; an algebraic root of that scalar absorbs it into the source coordinate. This is a function-field classification, without using a presentation of an etale fundamental group.

Imports8

Imported by2

theorem

curve_of_finite_ratFunc

L32 ↗

AnabelianGeometry.GeometricFundamentalGroup.curve_of_finite_ratFunc

Source context 3 commands

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

noncomputable section
open AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup

Lean source · statement

theorem curve_of_finite_ratFunc
    {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] : IsCurveOver K F ∧ Algebra.EssFiniteType K F

theorem

power_parameter

L63 ↗

AnabelianGeometry.GeometricFundamentalGroup.power_parameter

Source context 4 commands

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

noncomputable section
open AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup
open Classical in

Lean source · full declaration

theorem power_parameter
    {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
    [IsCurveOver K F] [Algebra.EssFiniteType K F]
    (hg : genusFF K F = 0) (v₀ v₁ : Place K F) (hne : v₀ ≠ v₁)
    (x : F) (hx : x ≠ 0) (n : ℕ) (hn : 0 < n)
    (hord : ∀ v : Place K F, v.ord x =
      (n : ℤ) * ((if v = v₀ then 1 else 0) - (if v = v₁ then 1 else 0))) :
    ∃ t : F, IntermediateField.adjoin K ({t} : Set F) = ⊤ ∧ t ^ n = x := by
  obtain ⟨t, ht, htr, hgen, htord⟩ := exists_parameter_of_genus_zero hg v₀ v₁ hne
  have hfinite : FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F :=
    IsCurveOver.finiteDimensional_adjoin_simple_of_transcendental_of_essFiniteType htr
  have hquot : ∀ v : Place K F, v.ord (x / t ^ n) = 0 := by
    intro v
    rw [div_eq_mul_inv, v.ord_mul hx (inv_ne_zero (pow_ne_zero n ht)), v.ord_inv,
      ← zpow_natCast t n, v.ord_zpow, htord, hord]
    ring
  obtain ⟨c, hc⟩ := Place.mem_range_algebraMap_of_forall_ord_eq_zero_of_isAlgClosed t htr hquot
  have hc0 : c ≠ 0 := by
    intro h
    rw [h, map_zero] at hc
    exact div_ne_zero hx (pow_ne_zero n ht) hc.symm
  obtain ⟨a, ha⟩ := IsAlgClosed.exists_pow_nat_eq c hn
  have ha0 : a ≠ 0 := by
    intro h
    rw [h, zero_pow (Nat.ne_zero_of_lt hn)] at ha
    exact hc0 ha.symm
  refine ⟨t * algebraMap K F a, ?_, ?_⟩
  · rw [IntermediateField.adjoin_simple_mul_algebraMap t a ha0, hgen]
  · rw [mul_pow, ← map_pow, ha, hc, mul_div_cancel₀ _ (pow_ne_zero n ht)]

theorem

exists_power_coordinates_of_tame_two_branches

L95 ↗

AnabelianGeometry.GeometricFundamentalGroup.exists_power_coordinates_of_tame_two_branches

Documentation

Every tame finite separable rational-function-field cover unramified away from two distinct places has generating coordinates in which its field inclusion is the degree-th power map.

Source context 3 commands

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

noncomputable section
open AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup

Lean source · statement

theorem exists_power_coordinates_of_tame_two_branches
    {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]
    (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) :
    ∃ s : RatFunc K, ∃ t : F,
      IntermediateField.adjoin K ({s} : Set (RatFunc K)) = ⊤ ∧
      IntermediateField.adjoin K ({t} : Set F) = ⊤ ∧
      algebraMap (RatFunc K) F s = t ^ Module.finrank (RatFunc K) F

theorem

exists_power_coordinates_of_two_branches_charZero

L161 ↗

AnabelianGeometry.GeometricFundamentalGroup.exists_power_coordinates_of_two_branches_charZero

Documentation

In characteristic zero, the power-coordinate classification needs only the two-branch unramified condition: separability and tameness follow from the characteristic.

Source context 3 commands

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

noncomputable section
open AlgebraicCurve
namespace AnabelianGeometry.GeometricFundamentalGroup

Lean source · statement

theorem exists_power_coordinates_of_two_branches_charZero
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K] [Field F]
    [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [FiniteDimensional (RatFunc K) F]
    (v₀ v₁ : Place K (RatFunc K)) (hne : v₀ ≠ v₁)
    (hunramified : ∀ w : Place K F, w.restrict (RatFunc K) ≠ v₀ →
      w.restrict (RatFunc K) ≠ v₁ → w.ramificationIndex (RatFunc K) = 1) :
    ∃ s : RatFunc K, ∃ t : F,
      IntermediateField.adjoin K ({s} : Set (RatFunc K)) = ⊤ ∧
      IntermediateField.adjoin K ({t} : Set F) = ⊤ ∧
      algebraMap (RatFunc K) F s = t ^ Module.finrank (RatFunc K) F

Module documentation

Power coordinates for rational covers with two branch places

Declarations

curve_of_finite_ratFunc

power_parameter

exists_power_coordinates_of_tame_two_branches

exists_power_coordinates_of_two_branches_charZero