Theorems · Theorem · commutative algebra

Module.Basis.localizationLocalization_apply

∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {A : Type u_3} [inst_4 : CommSemiring A] [inst_5 : Algebra R A]
  (Aₛ : Type u_4) [inst_6 : CommSemiring Aₛ] [inst_7 : Algebra A Aₛ] [inst_8 : Algebra Rₛ Aₛ] [inst_9 : Algebra R Aₛ]
  [inst_10 : IsScalarTower R Rₛ Aₛ] [inst_11 : IsScalarTower R A Aₛ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Module.Basis ι R A) (i : ι),
  (Module.Basis.localizationLocalization Rₛ S Aₛ b) i = (algebraMap A Aₛ) (b i)

Defined in

Mathlib.RingTheory.Localization.Module

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraIsLocalizationCommSemiringAlgebraCommSemiringAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalization