English
If ι is finite and M_i are modules over R, then the stalk rank of the product equals the sum of stalk ranks: rankAtStalk(Π_i M_i) = Σ_i rankAtStalk(M_i).
Русский
Пусть ι конечен и у каждого i имеется модуль M_i над R; тогда ранг на локализации произведения равен сумме рангов: rankAtStalk(Π_i M_i) = Σ_i rankAtStalk(M_i).
LaTeX
$$$[\\text{Finite } \\iota] \\Rightarrow \\operatorname{rankAtStalk}(\\prod_{i\\in\\iota} M_i) = \\sum_{i \\in \\iota}^{\\text{fin}} \\operatorname{rankAtStalk}(M_i)$$$
Lean4
/-- The rank of `Π i, M i` at a prime `p` is the sum of the ranks of `M i` at `p`. -/
theorem rankAtStalk_pi {ι : Type*} [Finite ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
[∀ i, Module.Flat R (M i)] [∀ i, Module.Finite R (M i)] (p : PrimeSpectrum R) :
rankAtStalk (Π i, M i) p = ∑ᶠ i, rankAtStalk (M i) p :=
by
cases nonempty_fintype ι
let f : (Π i, M i) →ₗ[R] Π i, LocalizedModule p.asIdeal.primeCompl (M i) :=
.pi (fun i ↦ mkLinearMap p.asIdeal.primeCompl (M i) ∘ₗ LinearMap.proj i)
let e :
LocalizedModule p.asIdeal.primeCompl (Π i, M i) ≃ₗ[Localization.AtPrime p.asIdeal]
Π i, LocalizedModule p.asIdeal.primeCompl (M i) :=
IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap _ _) f |>.extendScalarsOfIsLocalization
p.asIdeal.primeCompl _
have (i : ι) : Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (M i)) :=
free_of_flat_of_isLocalRing
simp_rw [rankAtStalk, e.finrank_eq, Module.finrank_pi_fintype, finsum_eq_sum_of_fintype]
