inertiaDeg_of_subsingleton — Mathlib

English

The inertia degree is preserved when pulling back along an algebra equivalence. Specifically, if e is an R-algebra isomorphism between S and S1, then inertiaDeg p (P comap e) = inertiaDeg p P.

Русский

Инерсия остаётся неизменной при обратном сопряжении по эквиваленту R-алгебр: inertiaDeg p (P comap e) = inertiaDeg p P.

LaTeX

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

Lean4

@[simp]
theorem inertiaDeg_of_subsingleton [hp : p.IsMaximal] [hQ : Subsingleton (S ⧸ P)] : inertiaDeg p P = 0 :=
  by
  have := Ideal.Quotient.subsingleton_iff.mp hQ
  subst this
  exact dif_neg fun h => hp.ne_top <| h.symm.trans comap_top

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