powQuotSuccInclusion — Mathlib

English

There is a canonical map on quotients sending R/p to S/P and compatibly mapping higher powers P^i to P^e via ramification idx, giving a natural tower of quotient maps.

Русский

Существует каноническая карта на квотиентных степенях, совместимая с переходами по степеням P^i → P^e через ramificationIdx.

LaTeX

$$$R/p \\to S/P \\\\to S/P^e$ with ramification$$

Lean4

/-- The inclusion `(P^(i + 1) / P^e) ⊂ (P^i / P^e)`. -/
@[simps]
noncomputable def powQuotSuccInclusion (i : ℕ) :
    Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ (i + 1)) →ₗ[R ⧸ p] Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i)
    where
  toFun x := ⟨x, Ideal.map_mono (Ideal.pow_le_pow_right i.le_succ) x.2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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