Theorems · Theorem · commutative algebra

Algebra.norm_eq_iff

∀ (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}
  {b : R},
  M ≤ nonZeroDivisors R → ((Algebra.norm R) a = b ↔ (Algebra.norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) b)

The norm of a : S in R can be computed in Sₘ.

Defined in

Mathlib.RingTheory.Localization.NormTrace

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraCommRingAlgebraIsLocalizationIsLocalizationAlgebraAlgebraIsScalarTowerIsScalarTowerModule.FreeModule.Finite