inertiaDeg_map_eq — Mathlib

English

For any P,LiesOver p, inertiaDeg is preserved under moving P via an equivalence or a map to P. This shows functorial behaviour with respect to pullbacks/pushforwards.

Русский

Инерия сохраняется при переносе P через эквивалент или отображение; демонстрирует ковариантность по отношению к переходам.

LaTeX

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

Lean4

theorem inertiaDeg_map_eq [p.IsMaximal] (P : Ideal S) {E : Type*} [EquivLike E S S₁] [AlgEquivClass E R S S₁] (e : E) :
    inertiaDeg p (P.map e) = inertiaDeg p P :=
  by
  rw [show P.map e = _ from map_comap_of_equiv (e : S ≃+* S₁)]
  exact p.inertiaDeg_comap_eq (e : S ≃ₐ[R] S₁).symm P

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