Theorems · Definition · commutative algebra

localizationAlgebra

{R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            {Rₘ : Type u_4} →
              {Sₘ : Type u_5} →
                [inst_3 : CommSemiring Rₘ] →
                  [inst_4 : CommSemiring Sₘ] →
                    [inst_5 : Algebra R Rₘ] →
                      [IsLocalization M Rₘ] →
                        [inst_7 : Algebra S Sₘ] →
                          [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] → Algebra Rₘ Sₘ

Definition of the natural algebra induced by the localization of an algebra. Given an algebra R → S, a submonoid R of M, and a localization Rₘ for M, let Sₘ be the localization of S to the image of M under algebraMap R S. Then this is the natural algebra structure on Rₘ → Sₘ, such that the entire square commutes, where localization_map.map_comp gives the commutativity of the underlying maps. This instance can be helpful if you define Sₘ := Localization (Algebra.algebraMapSubmonoid S M), however we will instead use the hypotheses [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] in lemmas since the algebra structure may arise in different ways.

Defined in

Mathlib.RingTheory.Localization.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringCommSemiringAlgebraIsLocalizationAlgebraIsLocalization