English
Under integral conditions, the Δ_aux valuation equals the valuation of W.Δ at the maximal ideal: valuation_Δ_aux R W = valuation K (maximalIdeal R) W.Δ.
Русский
При интегральности Δ_aux равняется толщине Δ на максимальной идеале: valuation_Δ_aux R W = valuation K (maximalIdeal R) W.Δ.
LaTeX
$$$\\operatorname{valuation\\_Δ\\_aux} \\ R\\ W = \\operatorname{valuation} K (\\operatorname{maximalIdeal} R) W.\\Delta$$$
Lean4
theorem exists_isIntegral (W : WeierstrassCurve K) : ∃ C : VariableChange K, IsIntegral R (C • W) :=
by
let l₀ := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
let l := l₀.map (fun a ↦ valuation R K a)
let lmax : ValueGroup R K := l.maximum_of_length_pos (by simp [l₀, l])
have hlmax_mem : lmax ∈ l := List.maximum_of_length_pos_mem (by simp [l₀, l])
have hlmax : ∀ v ∈ l, v ≤ lmax := fun v hv ↦ List.le_maximum_of_length_pos_of_mem hv (by simp [l₀, l])
by_cases hlmax_le_1 : lmax ≤ 1
· use ⟨1, 0, 0, 0⟩
apply isIntegral_of_exists_lift R
all_goals
simpa [← mem_integer_iff, variableChange_def, Valuation.mem_integer_iff] using
(hlmax _ (by simp [l₀, l])).trans hlmax_le_1
· have hlmax_ge_1 : lmax ≥ 1 := le_of_not_ge hlmax_le_1
have h : ∃ a : K, valuation R K a = lmax := by
let i : ℕ := l.idxOf lmax
have hi : i < l.length := List.idxOf_lt_length_of_mem hlmax_mem
use l₀[i]
have hi₁ : (valuation R K) l₀[i] = l[i] := by simp [l]
simpa only [hi₁] using (List.getElem_idxOf hi)
choose a ha using h
have ha₀ : a ≠ 0 := by
by_contra ha₀; simp only [ha₀, map_zero] at ha
exact (ha ▸ hlmax_le_1) zero_le_one
use ⟨Units.mk0 a ha₀, 0, 0, 0⟩
apply isIntegral_of_exists_lift R
all_goals
apply (mem_integer_iff _ _ _).mp
simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero, inv_pow, zero_mul,
sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
apply (Valuation.mem_integer_iff _ _).mpr
simp only [map_mul, map_inv₀, map_pow, ha]
refine inv_mul_le_one_of_le₀ ?_ zero_le'
refine (hlmax _ (by simp [l₀, l])).trans ?_
any_goals
apply le_self_pow hlmax_ge_1.le
linarith
rfl
