ramificationIdx_eq_one_of_map_localization

English

Equality of ramification indices under comap with a ring equivalence.

Русский

Сохранение ramificationIdx при компап-переобразовании через эквивалентность колец.

LaTeX

$$$ramificationIdx(\\text{algebraMap } R S, p, P) = ramificationIdx(\\text{algebraMap } R S_1, p, P)$$$

Lean4

/-- The converse is true when `S` is a Dedekind domain.
See `Ideal.ramificationIdx_eq_one_iff_of_isDedekindDomain`. -/
theorem ramificationIdx_eq_one_of_map_localization [Algebra R S] {p : Ideal R} {P : Ideal S} [P.IsPrime]
    [IsNoetherianRing S] (hpP : map (algebraMap R S) p ≤ P) (hp : P ≠ ⊥) (hp' : P.primeCompl ≤ nonZeroDivisors S)
    (H : p.map (algebraMap R (Localization.AtPrime P)) = maximalIdeal (Localization.AtPrime P)) :
    ramificationIdx (algebraMap R S) p P = 1 :=
  by
  rw [← not_ne_iff (b := 1), Ideal.ramificationIdx_ne_one_iff hpP]
  intro h₂
  replace h₂ := Ideal.map_mono (f := algebraMap S (Localization.AtPrime P)) h₂
  rw [Ideal.map_pow, Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, ← IsScalarTower.algebraMap_eq, H,
    pow_two] at h₂
  have := Submodule.eq_bot_of_le_smul_of_le_jacobson_bot _ _ (IsNoetherian.noetherian _) h₂ (maximalIdeal_le_jacobson _)
  rw [← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_eq_bot_iff_of_injective] at this
  · exact hp this
  · exact IsLocalization.injective _ hp'

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