inertiaDeg_pos — Mathlib

English

Under an algebra isomorphism e: S ≃ R S1, inertiaDeg p (P.comap e) equals inertiaDeg p P. This expresses the invariance of inertia degree under abstract algebraic equivalences.

Русский

При изоморфизме алгебр e: S ≃ R S1 инерционная степень сохраняется: inertiaDeg p (P.comap e) = inertiaDeg p P.

LaTeX

$$$\\\\operatorname{inertiaDeg} \\, p \, (P^{\\\\comap e}) = \\,\\\\operatorname{inertiaDeg} \\, p \\, P$$$

Lean4

theorem inertiaDeg_pos [p.IsMaximal] [Module.Finite R S] [P.LiesOver p] : 0 < inertiaDeg p P :=
  haveI : Nontrivial (S ⧸ P) := Quotient.nontrivial_of_liesOver_of_isPrime P p
  finrank_pos.trans_eq (inertiaDeg_algebraMap p P).symm

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