Theorems · Theorem · commutative algebra

Algebra.norm_localization

∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
  {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] [inst_5 : CommRing Sₘ] [inst_6 : Algebra S Sₘ]
  (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_9 : Algebra Rₘ Sₘ]
  [inst_10 : Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [Module.Free R S] [Module.Finite R S] (a : S),
  (Algebra.norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((Algebra.norm R) a)

Let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Then the norm of a : Sₘ over Rₘ is the norm of a : S over R if S is free as R-module.

Defined in

Mathlib.RingTheory.Localization.NormTrace

Cited by

8 results in Mathlib

Foundations

Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraCommRingAlgebraIsLocalizationIsLocalizationAlgebraAlgebraIsScalarTowerIsScalarTowerModule.FreeModule.Finite