Theorems · Definition · commutative algebra

Module.Basis.ofIsLocalizedModule

{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ₛ] →
              {M : Type u_3} →
                {Mₛ : Type u_4} →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] →
                      [inst_6 : AddCommMonoid Mₛ] →
                        [inst_7 : Module R Mₛ] →
                          [inst_8 : Module Rₛ Mₛ] →
                            [IsScalarTower R Rₛ Mₛ] →
                              (f : M →ₗ[R] Mₛ) →
                                [IsLocalizedModule S f] → {ι : Type u_5} → Module.Basis ι R M → Module.Basis ι Rₛ Mₛ

If M has an R-basis, then localizing M at S has a basis over R localized at S.

Defined in

Mathlib.RingTheory.Localization.Module

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraIsLocalizationAddCommMonoidModuleAddCommMonoidModuleModuleIsScalarTowerIsLocalizedModule