English
There is a characterization of when ramificationIdx ≠ 1 in terms of a bound by P^2 and the behavior of maps.
Русский
Существует характеристика того, когда ramificationIdx ≠ 1 через зависимость от P^2 и поведение отображений.
LaTeX
$$$ramificationIdx f p P \\neq 1 \\iff (map f p) \\le P^2$$$
Lean4
theorem ramificationIdx_ne_one_iff (hp : map f p ≤ P) : ramificationIdx f p P ≠ 1 ↔ p.map f ≤ P ^ 2 := by
classical
by_cases H : ∀ n : ℕ, ∃ k, p.map f ≤ P ^ k ∧ n < k
· obtain ⟨k, hk, h2k⟩ := H 2
simp [Ideal.ramificationIdx_eq_zero H, hk.trans (Ideal.pow_le_pow_right h2k.le)]
push_neg at H
rw [Ideal.ramificationIdx_eq_find H]
constructor
· intro he
have : 1 ≤ Nat.find H := Nat.find_spec H 1 (by simpa)
have := Nat.find_min H (m := 1) (by omega)
push_neg at this
obtain ⟨k, hk, h1k⟩ := this
exact hk.trans (Ideal.pow_le_pow_right (Nat.succ_le.mpr h1k))
· intro he
have := Nat.find_spec H 2 he
omega
