English
For i ≤ e, the rank of the image of P^i in S/(P^e) over R/p equals (e−i) times the rank of S/P over R/p.
Русский
Для i ≤ e ранг изображения P^i в S/(P^e) над R/p равен (e−i) умноженному на ранг S/P над R/p.
LaTeX
$$$\\\\operatorname{Module.rank} (R \\\\backslash p) (\\\\operatorname{Ideal.map} (\\\\operatorname{Ideal.Quotient.mk} (P^e)) (P^i)) = (e - i) \\\\cdot \\\\operatorname{Module.rank} (R \\\\backslash p) (S \\\\backslash P)$$$
Lean4
theorem rank_pow_quot [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥) (i : ℕ) (hi : i ≤ e) :
Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P) :=
by
let Q : ℕ → Prop := fun i =>
Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
refine Nat.decreasingInduction' (P := Q) (fun j lt_e _le_j ih => ?_) hi ?_
· dsimp only [Q]
rw [rank_pow_quot_aux p P _ lt_e, ih, ← succ_nsmul', Nat.sub_succ, ← Nat.succ_eq_add_one,
Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt lt_e)]
assumption
· dsimp only [Q]
rw [Nat.sub_self, zero_nsmul, map_quotient_self]
exact rank_bot (R ⧸ p) (S ⧸ P ^ e)
