English
There is a base-change compatible group homomorphism between Weierstrass affine points when passing from F to K and from F to L along an intermediate base.
Русский
При переходе по базе из F в K и затем в L существует совместимый по группе гомомордый переход точек аффинной кривой Вейерштрасса.
LaTeX
$$$\mathrm{map}\_{W'} f: W'⟮F⟯ \to W'⟮K⟯ \quad\text{is a group homomorphism and respects base change}$$$
Lean4
/-- The group homomorphism from `W⟮F⟯` to `W⟮K⟯` induced by an algebra homomorphism `f : F →ₐ[S] K`,
where `W` is defined over a subring of a ring `S`, and `F` and `K` are field extensions of `S`. -/
noncomputable def map : W'⟮F⟯ →+ W'⟮K⟯
where
toFun
P :=
match P with
| 0 => 0
| some h => some <| (baseChange_nonsingular _ _ f.injective).mpr h
map_zero' := rfl
map_add' := by
rintro (_ | @⟨x₁, y₁, _⟩) (_ | @⟨x₂, y₂, _⟩)
any_goals rfl
by_cases hxy : x₁ = x₂ ∧ y₁ = (W'.baseChange F).toAffine.negY x₂ y₂
· rw [add_of_Y_eq hxy.left hxy.right, add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]
· simp only [add_some hxy, ← baseChange_addX, ← baseChange_addY, ← baseChange_slope]
rw [add_some fun h => hxy ⟨f.injective h.1, f.injective (W'.baseChange_negY f .. ▸ h).2⟩]
