Theorems · Theorem · commutative algebra

Algebra.discr_localizationLocalization

∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
  [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] (M : Submonoid R) [inst_5 : IsLocalization M Rₘ] (Sₘ : Type u_5)
  [inst_6 : CommRing Sₘ] [inst_7 : Algebra S Sₘ] [inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ]
  [inst_10 : IsScalarTower R Rₘ Sₘ] [inst_11 : IsScalarTower R S Sₘ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {ι : Type u_6} [inst_13 : Fintype ι]
  [inst_14 : DecidableEq ι] (b : Module.Basis ι R S),
  Algebra.discr Rₘ ⇑(Module.Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (Algebra.discr R ⇑b)

Let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Let b be an R-basis of S. Then discriminant of the Rₘ-basis of Sₘ induced by b is the discriminant of b.

Defined in

Mathlib.RingTheory.Localization.NormTrace

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraIsLocalizationCommRingAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalizationFintypeDecidableEq