inertiaDeg_eq_of_isGalois — Mathlib

English

If p is maximal and K/L is a Galois extension, the inertia degrees over p for P and Q lying over p are equal: inertiaDeg p P = inertiaDeg p Q.

Русский

Если p максимален и K/L Галуа-расширение, то инерциальные степени над p для P и Q, лежащих над p, равны: inertiaDeg p P = inertiaDeg p Q.

LaTeX

$$$\\mathrm{inertiaDeg}_p(p\\; B)\\; P = \\mathrm{inertiaDeg}_p(p\\; B)\\; Q$$$

Lean4

/-- All the `inertiaDeg` over a fixed maximal ideal are the same. -/
theorem inertiaDeg_eq_of_isGalois [p.IsMaximal] [IsGalois K L] : inertiaDeg p P = inertiaDeg p Q :=
  by
  rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩
  rw [← hs]
  exact (inertiaDeg_map_eq p P σ).symm

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