inertiaDeg_algebraMap — Mathlib

English

If P lies over p and p is maximal, then inertiaDeg(p,P) equals the finrank of the quotient extension after passing to quotients along the algebra map R/p → S/P (in particular, the case P.LiesOver p).

Русский

Если P лежит над p и p максимален, то inertiaDeg(p,P) равен размерности по R/p до S/P через отображение алгебры R/p → S/P.

LaTeX

$$$\\\\operatorname{inertiaDeg} \\, p \\, P = \\\\operatorname{finrank} \\, (R \\/ p) \, (S \\/ P)$$$

Lean4

@[simp]
theorem inertiaDeg_algebraMap [P.LiesOver p] [p.IsMaximal] : inertiaDeg p P = finrank (R ⧸ p) (S ⧸ P) :=
  by
  nontriviality S ⧸ P using inertiaDeg_of_subsingleton, finrank_zero_of_subsingleton
  rw [inertiaDeg, dif_pos (over_def P p).symm]

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