isIntegral_of_exists_lift — Mathlib

English

If W is integral over R, then there exists r in R with algebraMap R K r = W.Δ.

Русский

Если кривая W целочислена над R, существует r ∈ R such that algebraMap R K r = W.Δ.

LaTeX

$$$\\exists r \\in R\\; (\\text{algebraMap } R K)(r) = W.\\Delta$$$

Lean4

theorem isIntegral_of_exists_lift {W : WeierstrassCurve K} (h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁)
    (h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂) (h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃)
    (h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄) (h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆) : IsIntegral R W :=
  by
  use ⟨h₁.choose, h₂.choose, h₃.choose, h₄.choose, h₆.choose⟩
  ext
  all_goals simp only [map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]
  · apply h₁.choose_spec.symm
  · apply h₂.choose_spec.symm
  · apply h₃.choose_spec.symm
  · apply h₄.choose_spec.symm
  · apply h₆.choose_spec.symm

Похожие утверждения