Theorems · Theorem · commutative algebra

Algebra.map_leftMulMatrix_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) [inst_7 : IsLocalization M Rₘ] [inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
  [inst_9 : Algebra Rₘ Sₘ] [inst_10 : Algebra R Sₘ] [inst_11 : IsScalarTower R Rₘ Sₘ] [inst_12 : IsScalarTower R S Sₘ]
  {ι : Type u_5} [inst_13 : Fintype ι] [inst_14 : DecidableEq ι] (b : Module.Basis ι R S) (a : S),
  (algebraMap R Rₘ).mapMatrix ((Algebra.leftMulMatrix b) a) =
    (Algebra.leftMulMatrix (Module.Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a)

Defined in

Mathlib.RingTheory.Localization.NormTrace

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraCommRingAlgebraIsLocalizationIsLocalizationAlgebraAlgebraIsScalarTowerIsScalarTowerFintypeDecidableEq