Some algebra instance for graded algebra and homog loc

Stream: mathlib4

[Kenny Lau]

I kinda need the following two instances:

import Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

set_option autoImplicit false

instance (R₀ R A ι : Type*) [CommRing R₀] [CommRing R] [CommRing A]
    [Algebra R₀ R] [Algebra R A] [Algebra R₀ A] [IsScalarTower R₀ R A]
    [DecidableEq ι] [AddCommMonoid ι] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] :
    Algebra R₀ (𝒜 0) :=
  Algebra.compHom _ <| algebraMap _ R

instance (R₀ R A ι : Type*) [CommRing R₀] [CommRing R] [CommRing A]
    [Algebra R₀ R] [Algebra R A] [Algebra R₀ A] [IsScalarTower R₀ R A]
    [DecidableEq ι] [AddCommMonoid ι] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜]
    (x : Submonoid A) :
    Algebra R₀ (HomogeneousLocalization 𝒜 x) :=
  Algebra.compHom _ <| algebraMap _ (𝒜 0)

[Kenny Lau]

Are these good instances to have? Would they lead to some unforeseen issues?

[Kevin Buzzard]

Does this make a diamond when R₀ = \Z?

[Kenny Lau]

since the time the message has been written I've realised that I needed to change the definition

[Kenny Lau]

and also I eventually did not use the first instance here

[Kevin Buzzard]

And can there also be problems when R₀ = R?

[Kenny Lau]

and it's now a PR #30408

[Kenny Lau]

@Kevin Buzzard and now the following two tests pass:

example (R₀ R A ι : Type*) [CommRing R₀] [CommRing R] [CommRing A]
    [Algebra R₀ R] [Algebra R A] [Algebra R₀ A] [IsScalarTower R₀ R A]
    [DecidableEq ι] [AddCommMonoid ι] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜]
    (x : Submonoid A) :
    (inferInstanceAs (Algebra R (HomogeneousLocalization 𝒜 x))).toSMul =
    inferInstanceAs (SMul R (HomogeneousLocalization 𝒜 x)) := rfl

example (R₀ R A ι : Type*) [CommRing R₀] [CommRing R] [CommRing A]
    [Algebra R₀ R] [Algebra R A] [Algebra R₀ A] [IsScalarTower R₀ R A]
    [DecidableEq ι] [AddCommMonoid ι] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜]
    (x : Submonoid A) :
    (inferInstanceAs (Algebra ℤ (HomogeneousLocalization 𝒜 x))).toSMul =
    inferInstanceAs (SMul ℤ (HomogeneousLocalization 𝒜 x)) := rfl

[Kenny Lau]

and by clicking in the goal I have verified that the SMul instances come from docs#HomogeneousLocalization.instSMul and docs#SubNegMonoid.toZSMul respectively

[Kenny Lau]

(and the latter comes from docs#HomogeneousLocalization.homogeneousLocalizationCommRing)