ramificationIdx_eq_of_isGalois — Mathlib

English

Over a fixed maximal p, all ramification indices across primes lying over p are equal, i.e., ramificationIdxIn p B = ramificationIdx (algebraMap A B) p P for any P with P.LiesOver p.

Русский

Для фиксированного максимального p все ramification индексы над p совпадают для любых P, лежащих над p: ramificationIdxIn p B = ramificationIdx (algebraMap A B) p P.

LaTeX

$$$\\mathrm{ramificationIdxIn}\\ p\\ B = \\mathrm{ramificationIdx}(\\mathrm{algebraMap}\\ A B)\\ p\\ P$$$

Lean4

/-- All the `ramificationIdx` over a fixed maximal ideal are the same. -/
theorem ramificationIdx_eq_of_isGalois [IsGalois K L] :
    ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) p Q :=
  by
  rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩
  rw [← hs]
  exact (ramificationIdx_map_eq p P σ).symm

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