English
A high-level variant of relNorm_algebraMap across a tower R′ → R → S with extra algebra structures; relNorm_R(I.map(algebraMap_R′S)) = I.map(algebraMap_R′R)^{finrank}.
Русский
Высокий вариант relNorm_algebraMap через башню R′→R→S; 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}}$$$
Lean4
/-- A version of `relNorm_algebraMap` involving a tower of algebras `S/R/R'`. -/
theorem relNorm_algebraMap' {R'} [CommRing R'] (I : Ideal R') [Algebra R' R] [Algebra R' S] [IsScalarTower R' R S] :
relNorm R (I.map (algebraMap R' S)) = I.map (algebraMap R' R) ^ Module.finrank (FractionRing R) (FractionRing S) :=
by rw [← relNorm_algebraMap, Ideal.map_map, IsScalarTower.algebraMap_eq R' R S]
