English
The stalk rank of a product M × N equals the sum of stalk ranks: rankAtStalk(M × N) = rankAtStalk(M) + rankAtStalk(N).
Русский
Ранг на локализации произведения M × N равен сумме рангов: rankAtStalk(M × N) = rankAtStalk(M) + rankAtStalk(N).
LaTeX
$$$\\operatorname{rankAtStalk}(M \\times N) = \\operatorname{rankAtStalk}(M) + \\operatorname{rankAtStalk}(N)$$$
Lean4
/-- The rank of `M × N` at `p` is equal to the sum of the ranks. -/
theorem rankAtStalk_prod (N : Type*) [AddCommGroup N] [Module R N] [Module.Flat R N] [Module.Finite R N] :
rankAtStalk (R := R) (M × N) = rankAtStalk M + rankAtStalk N :=
by
ext p
let e :
LocalizedModule p.asIdeal.primeCompl (M × N) ≃ₗ[Localization.AtPrime p.asIdeal]
LocalizedModule p.asIdeal.primeCompl M × LocalizedModule p.asIdeal.primeCompl N :=
IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap _ _)
(.prodMap (mkLinearMap _ M) (mkLinearMap _ N)) |>.extendScalarsOfIsLocalization
p.asIdeal.primeCompl _
simp [rankAtStalk, e.finrank_eq]
