Theorems · Theorem · commutative algebra

Algebra.traceMatrix_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.traceMatrix Rₘ ⇑(Module.Basis.localizationLocalization Rₘ M Sₘ b) =
    (algebraMap R Rₘ).mapMatrix (Algebra.traceMatrix R ⇑b)

Defined in

Mathlib.RingTheory.Localization.NormTrace

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraIsLocalizationCommRingAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalizationFintypeDecidableEq