English
A variant of RelNorm_algebraMap when there is an intermediate R' with tower R'→R→S; relNorm_R'(I.map(algebraMap_R'S)) equals I.map(algebraMap_R'R) raised to finrank.
Русский
Вариант RelNorm_algebraMap в присутствии промежуточного R' с тензорной цепью: relNorm_R'(I.map(algebraMap_R'S)) = I.map(algebraMap_R'R)^{finrank}.
LaTeX
$$$\mathrm{relNorm}_{R'}(\mathrm{I.map}(\mathrm{algebraMap}_{R'S})) = \mathrm{I.map}(\mathrm{algebraMap}_{R'R})^{\mathrm{finrank}(\mathrm{FractionRing}(R), \mathrm{FractionRing}(S))}$$$
Lean4
theorem relNorm_algebraMap (I : Ideal R) :
relNorm R (I.map (algebraMap R S)) = I ^ Module.finrank (FractionRing R) (FractionRing S) :=
by
rw [← spanNorm_eq]
refine eq_of_localization_maximal (fun P hPd ↦ ?_)
let P' := Algebra.algebraMapSubmonoid S P.primeCompl
let Rₚ := Localization.AtPrime P
let K := FractionRing R
rw [← spanIntNorm_localization R _ _ P.primeCompl_le_nonZeroDivisors (Localization P'), Ideal.map_pow, I.map_map, ←
IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R Rₚ, ← I.map_map, ← (I.map _).span_singleton_generator,
Ideal.map_span, Set.image_singleton, spanNorm_singleton, Ideal.span_singleton_pow]
congr 2
apply IsFractionRing.injective Rₚ K
rw [Algebra.algebraMap_intNorm (L := FractionRing S), ← IsScalarTower.algebraMap_apply,
IsScalarTower.algebraMap_apply Rₚ K, Algebra.norm_algebraMap, map_pow]
