AlgebraicCurve.RationalFunctionField.exists_algEquiv_congrRingEquiv_placeInfty_eq_placeOfPoint_zero_eq
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurves.Places.Rational.Proofs in
open RationalFunctionField_exists_algEquiv_congrRingEquiv_placeInfty_eq_placeOfPoint_zero_eq in
open AlgebraicCurve in
Lean source · full declarationtheorem exists_algEquiv_congrRingEquiv_placeInfty_eq_placeOfPoint_zero_eq
(k : Type*) [Field k] [DecidableEq (RatFunc k)]
(v w : Place k (RatFunc k)) (hvw : v ≠ w)
(hv : v = RationalFunctionField.placeInfty k ∨ ∃ c : k, v = RationalFunctionField.placeOfPoint
k c)
(hw : w = RationalFunctionField.placeInfty k ∨ ∃ c : k, w = RationalFunctionField.placeOfPoint
k c) :
∃ φ : RatFunc k ≃ₐ[k] RatFunc k,
Place.congrRingEquiv φ.toRingEquiv (fun a => φ.commutes a) (RationalFunctionField.placeInfty
k) = v ∧
Place.congrRingEquiv φ.toRingEquiv (fun a => φ.commutes a)
(RationalFunctionField.placeOfPoint k 0) = w := by
classical
suffices H : ∃ ψ : RatFunc k ≃ₐ[k] RatFunc k,
Place.congrRingEquiv ψ.symm.toRingEquiv (fun a => ψ.symm.commutes a)
(RationalFunctionField.placeInfty k) = v ∧
Place.congrRingEquiv ψ.symm.toRingEquiv (fun a => ψ.symm.commutes a)
(RationalFunctionField.placeOfPoint k 0) = w by
obtain ⟨ψ, h⟩ := H
exact ⟨ψ.symm, h⟩
have hX0 : (RatFunc.X : RatFunc k) ≠ 0 := RatFunc.X_ne_zero
have hC : ∀ (ψ : RatFunc k ≃ₐ[k] RatFunc k) (a : k), ψ (RatFunc.C a) = RatFunc.C a := fun ψ a =>
ψ.commutes a
have hX1 : (RatFunc.X + 1 : RatFunc k) = RatFunc.X - RatFunc.C (-1) :=
by rw [map_neg, map_one, sub_neg_eq_add]
have hX1ne : (RatFunc.X + 1 : RatFunc k) ≠ 0 := by rw [hX1]; exact LMOB.X_sub_C_ne_zero (-1)
rcases hv with rfl | ⟨c, rfl⟩ <;> rcases hw with rfl | ⟨d, rfl⟩
· exact absurd rfl hvw
· obtain ⟨ψ, hψ⟩ := RatFunc.exists_algEquiv_apply_X_eq_moebius (1 : k) d 0 1 (by norm_num)
have hψX : ψ RatFunc.X = RatFunc.X + RatFunc.C d := by
rw [hψ, map_one, map_zero, one_mul, zero_mul, zero_add, div_one]
refine ⟨ψ, ?_, ?_⟩
· apply RationalFunctionField.eq_placeInfty_of_ord_X_neg
rw [LMOB.ord_congr_symm, hψX,
show (RatFunc.X + RatFunc.C d : RatFunc k) = RatFunc.X - RatFunc.C (-d)
by rw [map_neg, sub_neg_eq_add],
LMOB.ord_placeInfty_X_sub_C]
norm_num
· apply LMOB.eq_placeOfPoint_of_ord_pos
rw [LMOB.ord_congr_symm, map_sub, hC, hψX, add_sub_cancel_right, LMOB.ord_placeOfPoint_zero_X]
norm_num
· obtain ⟨ψ, hψ⟩ := RatFunc.exists_algEquiv_apply_X_eq_moebius c (1 : k) 1 0 (by norm_num)
have hψX : ψ RatFunc.X = (RatFunc.C c * RatFunc.X + 1) / RatFunc.X := by
rw [hψ, map_one, map_zero, one_mul, add_zero]
refine ⟨ψ, ?_, ?_⟩
· apply LMOB.eq_placeOfPoint_of_ord_pos
rw [LMOB.ord_congr_symm, map_sub, hC, hψX]
have hid : ((RatFunc.C c * RatFunc.X + 1) / RatFunc.X - RatFunc.C c : RatFunc k) =
(RatFunc.X)⁻¹ := by
field_simp
ring
rw [hid, Place.ord_inv, RationalFunctionField.ord_placeInfty_X]
norm_num
· apply RationalFunctionField.eq_placeInfty_of_ord_X_neg
rw [LMOB.ord_congr_symm, hψX]
by_cases hc : c = 0
· subst hc
rw [map_zero, zero_mul, zero_add, one_div, Place.ord_inv, LMOB.ord_placeOfPoint_zero_X]
norm_num
· have hCc : (RatFunc.C c : RatFunc k) ≠ 0 := (map_ne_zero RatFunc.C).mpr hc
have hfac : (RatFunc.C c * RatFunc.X + 1 : RatFunc k) = RatFunc.C c * (RatFunc.X -
RatFunc.C (-c⁻¹)) := by
rw [map_neg, map_inv₀, sub_neg_eq_add, mul_add, mul_inv_cancel₀ hCc]
have hnum : (RatFunc.C c * RatFunc.X + 1 : RatFunc k) ≠ 0 := by
rw [hfac]; exact mul_ne_zero hCc (LMOB.X_sub_C_ne_zero _)
rw [div_eq_mul_inv, Place.ord_mul _ hnum (inv_ne_zero hX0), Place.ord_inv, hfac,
Place.ord_mul _ hCc (LMOB.X_sub_C_ne_zero _), LMOB.ord_C _ hc,
LMOB.ord_placeOfPoint_X_sub_C_of_ne (b := -c⁻¹) (b' := 0) (neg_ne_zero.mpr (inv_ne_zero
hc)),
LMOB.ord_placeOfPoint_zero_X]
norm_num
· have hcd : c ≠ d := fun h => hvw (by rw [h])
obtain ⟨ψ, hψ⟩ := RatFunc.exists_algEquiv_apply_X_eq_moebius c d 1 1
(by rw [mul_one, mul_one]; exact sub_ne_zero.mpr hcd)
have hψX : ψ RatFunc.X = (RatFunc.C c * RatFunc.X + RatFunc.C d) / (RatFunc.X + 1) := by
rw [hψ, map_one, one_mul]
have hcd' : (RatFunc.C (d - c) : RatFunc k) ≠ 0 := (map_ne_zero RatFunc.C).mpr (sub_ne_zero.mpr
(Ne.symm hcd))
have hcd'' : (RatFunc.C (c - d) : RatFunc k) ≠ 0 := (map_ne_zero RatFunc.C).mpr
(sub_ne_zero.mpr hcd)
refine ⟨ψ, ?_, ?_⟩
· apply LMOB.eq_placeOfPoint_of_ord_pos
rw [LMOB.ord_congr_symm, map_sub, hC, hψX]
have hid : ((RatFunc.C c * RatFunc.X + RatFunc.C d) / (RatFunc.X + 1) - RatFunc.C c : RatFunc
k)
= RatFunc.C (d - c) * (RatFunc.X + 1)⁻¹ := by
rw [map_sub]
field_simp
ring
rw [hid, Place.ord_mul _ hcd' (inv_ne_zero hX1ne), Place.ord_inv, LMOB.ord_C _
(sub_ne_zero.mpr (Ne.symm hcd)),
hX1, LMOB.ord_placeInfty_X_sub_C]
norm_num
· apply LMOB.eq_placeOfPoint_of_ord_pos
rw [LMOB.ord_congr_symm, map_sub, hC, hψX]
have hid : ((RatFunc.C c * RatFunc.X + RatFunc.C d) / (RatFunc.X + 1) - RatFunc.C d : RatFunc
k)
= RatFunc.C (c - d) * RatFunc.X * (RatFunc.X + 1)⁻¹ := by
rw [map_sub]
field_simp
ring
rw [hid, Place.ord_mul _ (mul_ne_zero hcd'' hX0) (inv_ne_zero hX1ne), Place.ord_mul _ hcd''
hX0, Place.ord_inv,
LMOB.ord_C _ (sub_ne_zero.mpr hcd), hX1,
LMOB.ord_placeOfPoint_X_sub_C_of_ne (b := -1) (b' := 0) (neg_ne_zero.mpr one_ne_zero),
LMOB.ord_placeOfPoint_zero_X]
norm_num