ramificationIdx_map_eq — Mathlib

English

Under a suitable isomorphism, ramificationIdx remains the same between maps.

Русский

При подходящей изоморфности ramificationIdx сохраняется между отображениями.

LaTeX

$$$ramificationIdx(\\text{algebraMap } R S_1, p, P) = ramificationIdx(\\text{algebraMap } R S, p, P)$$$

Lean4

theorem ramificationIdx_map_eq [Algebra R S] {E : Type*} [EquivLike E S S₁] [AlgEquivClass E R S S₁] (P : Ideal S)
    (e : E) : ramificationIdx (algebraMap R S₁) p (P.map e) = ramificationIdx (algebraMap R S) p P :=
  by
  rw [show P.map e = _ from P.map_comap_of_equiv (e : S ≃+* S₁)]
  exact p.ramificationIdx_comap_eq (e : S ≃ₐ[R] S₁).symm P

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