English
For maximal P and prime P in a Dedekind domain S, the R/p-rank of the image of P^i in P^e matches the sum of the fixed rank of S/P with the rank of the image of P^{i+1}. This describes a step-by-step rank relation in the filtration by powers of P.
Русский
При максимальном P и простом P в корректном домене S ранговая величина над R/p для изображения P^i в P^e равна сумме фиксированного ранга S/P и ранга изображения P^{i+1}. Описывает зависимость ранга в фильтрации по степеням P.
LaTeX
$$$\\\\operatorname{Module.rank} (R \\\\backslash p) (\\\\operatorname{Ideal.map} (\\\\operatorname{Ideal.Quotient.mk} (P^e)) (P^i)) = \\\\operatorname{Module.rank} (R \\\\backslash p) (S \\\\backslash P) + \\\\operatorname{Module.rank} (R \\\\backslash p) (\\\\operatorname{Ideal.map} (\\\\operatorname{Ideal.Quotient.mk} (P^e)) (P^{i+1}))$$
Lean4
/-- Since the inclusion `(P^(i + 1) / P^e) ⊂ (P^i / P^e)` has a kernel isomorphic to `P / S`,
`[P^i / P^e : R / p] = [P^(i+1) / P^e : R / p] + [P / S : R / p]` -/
theorem rank_pow_quot_aux [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)) =
Module.rank (R ⧸ p) (S ⧸ P) + Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ (i + 1))) :=
by
rw [← rank_range_of_injective _ (powQuotSuccInclusion_injective p P i),
(quotientRangePowQuotSuccInclusionEquiv p P hP0 hi).symm.rank_eq]
exact (Submodule.rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion p P i))).symm
