AnabelianGeometry.GeometricFundamentalGroup.exists_ratFunc_algEquiv_zero_infinity_of_genus_zero
A genus-zero coordinate can match both specified distinct places, as zero and infinity.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
[IsCurveOver K F] [Algebra.EssFiniteType K F]
open Classical inLean source · full declaration
theorem exists_ratFunc_algEquiv_zero_infinity_of_genus_zero (hg : genusFF K F = 0)
(v₀ vInfty : Place K F) (hne : v₀ ≠ vInfty) :
∃ e : RatFunc K ≃ₐ[K] F,
Place.congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
(RationalFunctionField.placeOfPoint K 0) = v₀ ∧
Place.congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
(RationalFunctionField.placeInfty K) = vInfty := by
classical
obtain ⟨t, _, htr, hgen, hord⟩ := exists_parameter_of_genus_zero hg v₀ vInfty hne
let e : RatFunc K ≃ₐ[K] F := (RatFunc.algEquivOfTranscendental t htr).trans
((IntermediateField.equivOfEq hgen).trans IntermediateField.topEquiv)
have heX : e RatFunc.X = t := by
change ((RatFunc.algEquivOfTranscendental t htr) RatFunc.X : F) = t
rw [RatFunc.algEquivOfTranscendental_X]
have hzero : (RationalFunctionField.placeOfPoint K 0).ord (RatFunc.X : RatFunc K) = 1 := by
have h := RationalFunctionField.ord_X_sub_C K 0 (RationalFunctionField.placeOfPoint K 0)
rw [Polynomial.C_0, sub_zero, RatFunc.algebraMap_X, Finsupp.add_apply,
Finsupp.single_eq_same,
Finsupp.single_eq_of_ne (RationalFunctionField.placeOfPoint_ne_placeInfty K 0),
add_zero] at h
exact h
refine ⟨e, ?_, ?_⟩
· let u := Place.congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
(RationalFunctionField.placeOfPoint K 0)
have hpos : u.ord t = 1 := by
rw [← heX]
exact (Place.ord_congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
(RationalFunctionField.placeOfPoint K 0) RatFunc.X).trans hzero
by_contra huv
rw [hord, ite_eq_right huv] at hpos
split_ifs at hpos <;> omega
· let u := Place.congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
(RationalFunctionField.placeInfty K)
have hneg : u.ord t = -1 := by
rw [← heX]
exact (Place.ord_congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
(RationalFunctionField.placeInfty K) RatFunc.X).trans
(RationalFunctionField.ord_placeInfty_X K)
by_contra huv
rw [hord, ite_eq_right huv] at hneg
split_ifs at hneg <;> omega