finrank_pow_ramificationIdx — Mathlib

English

If p is maximal and the ramification exponent e is nonzero, then the finite dimension of R/p over S/(P^e) equals e times the finite dimension of R/p over S/P.

Русский

Если p максимален и e ≠ 0, то размерность (финитная) R/p над S/(P^e) равна e кратному размерности S/P над R/p.

LaTeX

$$$$ \operatorname{finrank} (R \\backslash p) (S \\backslash P^e) = e \\cdot \\operatorname{finrank} (R \\backslash p) (S \\backslash P) $$$$

Lean4

theorem finrank_pow_ramificationIdx [p.IsMaximal] (P : (factors (map (algebraMap R S) p)).toFinset) :
    finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx (algebraMap R S) p P) =
      ramificationIdx (algebraMap R S) p P * inertiaDeg p (P : Ideal S) :=
  by
  rw [finrank_prime_pow_ramificationIdx, inertiaDeg_algebraMap]
  exacts [Factors.ne_bot p P, NeZero.ne _]

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