English
If e is an algebra isomorphism, then inertiaDeg(p, P) equals inertiaDeg(p, P) after applying comap or map along e; the inertia degree is preserved by base change.
Русский
Инерия сохраняется под оператором сопряжения по эквиваленту алгебр; инерная степень не меняется при базисном изменении.
LaTeX
$$$\\\\operatorname{inertiaDeg} \\, p \\, (P^{\\\\comap e}) = \\,\\\\operatorname{inertiaDeg} \\, p \\, P$$$
Lean4
theorem inertiaDeg_comap_eq (e : S ≃ₐ[R] S₁) (P : Ideal S₁) [p.IsMaximal] : inertiaDeg p (P.comap e) = inertiaDeg p P :=
by
have he : (P.comap e).comap (algebraMap R S) = p ↔ P.comap (algebraMap R S₁) = p := by
rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
by_cases h : P.LiesOver p
· rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]
exact (Quotient.algEquivOfEqComap p e rfl).toLinearEquiv.finrank_eq
· rw [inertiaDeg, dif_neg (fun eq => h ⟨(he.mp eq).symm⟩)]
rw [inertiaDeg, dif_neg (fun eq => h ⟨eq.symm⟩)]
