Theorems · Definition · commutative algebra

Module.Basis.localizationLocalization

{R : Type u_1} →
  (Rₛ : Type u_2) →
    [inst : CommSemiring R] →
      (S : Submonoid R) →
        [inst_1 : CommSemiring Rₛ] →
          [inst_2 : Algebra R Rₛ] →
            [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ₛ] →
                              [IsScalarTower R Rₛ Aₛ] →
                                [IsScalarTower R A Aₛ] →
                                  [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] →
                                    {ι : Type u_5} → Module.Basis ι R A → Module.Basis ι Rₛ Aₛ

If A has an R-basis, then localizing A at S has a basis over R localized at S. A suitable instance for [Algebra A Aₛ] is localizationAlgebra.

Defined in

Mathlib.RingTheory.Localization.Module

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraIsLocalizationCommSemiringAlgebraCommSemiringAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalization