one-param structure for internal grading

Stream: mathlib4

[Kenny Lau]

import Mathlib.Tactic.TypeStar

structure Grading (ι σ : Type*) where grading : ι → σ

instance Grading.hasCoeToFun (ι σ : Type*) : CoeFun (Grading ι σ) (fun _ ↦ ι → σ) :=
  ⟨fun 𝒜 ↦ 𝒜.grading⟩

variable (ι σ : Type*) (𝒜 : Grading ι σ) (i : ι)
#check 𝒜 i

[Kenny Lau]

it has been noted that it might be difficult to unify the grading, so I propose to make grading a one-param structure

[Kenny Lau]

e.g. if we have a grading ℳ : ι → Submodule R M, then we can form its base change as fun i ↦ (ℳ i).baseChange S : ι → Submodule S (S ⊗[R] M), and then its 0th component is (ℳ 0).baseChange S, and now Lean can't figure out what the grading was

[Kenny Lau]

but if we have a one-param structure, then now given ℳ : Grading ι (Submodule R M), we can now have ℳ.baseChange S : Grading ι (Submodule S (S ⊗[R] M)), whose 0th component is ℳ.baseChange S 0, so it's obvious what the grading is

[Kenny Lau]

I think the argument by inertia "but we don't have a problem now" is because we haven't tested it enough

[Kenny Lau]

this thread hasn't received much response, I suppose people are fine with either way?

[Kenny Lau]

@Yaël Dillies you probably have some opinions

[Yaël Dillies]

We do have a problem now, in fact: For a grading A, we had to scope the instances on A 0 because they have very bad performance. If we bundle the grading as you suggest, that problem should disappear

[Kenny Lau]

one thing to note would be that the grading applications should not have @[simps] at all

[Kenny Lau]

because otherwise it would simplify A 0 to something else and bring up the problem again

[Kenny Lau]

right?

[Kenny Lau]

in my project I've experimented with this (bundling grading) and the results were very positive, I don't have #mwe yet but elaboration time for one of my definitions went from 12.5 seconds to 3.88 seconds

[Kenny Lau]

update: my attempt to minimise it has failed, but i'll post the code regardless:

import Mathlib

open TensorProduct

structure Graded (ι σ : Type*) where toFun : ι → σ

namespace Graded

instance (ι σ : Type*) : FunLike (Graded ι σ) ι σ where
  coe := toFun
  coe_injective' := by rintro ⟨_⟩ ⟨_⟩ h; congr

section Ring
variable {ι A σ : Type*} [DecidableEq ι] [AddMonoid ι] [Semiring A]
  [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ)

protected abbrev Ring (𝒜 : Graded ι σ) : Type _ :=
  GradedRing 𝒜

variable (𝒜 : Graded ι σ)

end Ring

section Algebra
variable {ι R A : Type*} [DecidableEq ι] [AddMonoid ι]
  [CommSemiring R] [Semiring A] [Algebra R A]

protected abbrev Algebra (𝒜 : Graded ι (Submodule R A)) : Type _ :=
  GradedAlgebra 𝒜

end Algebra

protected def Localization {ι A σ : Type*} [CommRing A] [SetLike σ A]
    (𝒜 : Graded ι σ) (x : Submonoid A) : Type _ :=
  HomogeneousLocalization 𝒜 x

section Ring
variable {ι A σ : Type*} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A]
  [AddCommMonoid ι] [DecidableEq ι]
  (𝒜 : Graded ι σ) [𝒜.Ring] (x : Submonoid A)

instance : CommRing (𝒜.Localization x) :=
  HomogeneousLocalization.homogeneousLocalizationCommRing

end Ring

section Algebra
variable {ι R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
  [AddCommMonoid ι] [DecidableEq ι]
  (𝒜 : Graded ι (Submodule R A)) [𝒜.Algebra] (x : Submonoid A)

instance : SMul R (𝒜.Localization x) :=
  HomogeneousLocalization.instSMul x

open HomogeneousLocalization

instance : Algebra R (𝒜.Localization x) where
  algebraMap := (fromZeroRingHom 𝒜 x).comp (algebraMap R (𝒜 0))
  commutes' := sorry
  smul_def' := sorry

instance : Algebra (𝒜.Localization x) (Localization x) :=
  inferInstanceAs (Algebra (HomogeneousLocalization 𝒜 x) (Localization x))

instance : IsScalarTower R (𝒜.Localization x) (Localization x) :=
  .of_algebraMap_eq' rfl

variable (S : Type*) [CommRing S] [Algebra R S]

def baseChange : Graded ι (Submodule S (S ⊗[R] A)) where
  toFun i := (𝒜 i).baseChange S

instance : (𝒜.baseChange S).Algebra := sorry

end Algebra

end Graded


namespace HomogeneousLocalization

variable {ι R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
  [AddCommMonoid ι] [DecidableEq ι]
  (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : Submonoid A)

instance : Algebra R (HomogeneousLocalization 𝒜 x) where
  algebraMap := (fromZeroRingHom 𝒜 x).comp (algebraMap R (𝒜 0))
  commutes' := sorry
  smul_def' := sorry

instance : Algebra (HomogeneousLocalization 𝒜 x) (Localization x) :=
  inferInstanceAs (Algebra (HomogeneousLocalization 𝒜 x) (Localization x))

instance : IsScalarTower R (HomogeneousLocalization 𝒜 x) (Localization x) :=
  .of_algebraMap_eq' rfl

variable (S : Type*) [CommRing S] [Algebra R S]

instance : GradedAlgebra (fun i ↦ (𝒜 i).baseChange S) := sorry

end HomogeneousLocalization


set_option trace.profiler true

variable {ι R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
  [AddCommMonoid ι] [DecidableEq ι]

variable (𝒜 : Graded ι (Submodule R A)) [𝒜.Algebra] (x : Submonoid A) in
#synth IsScalarTower R (𝒜.Localization x) (Localization x)

variable (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : Submonoid A) in
#synth IsScalarTower R (HomogeneousLocalization 𝒜 x) (Localization x)

variable (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : Submonoid A) in
#synth IsScalarTower R (HomogeneousLocalization (fun i ↦ 𝒜 i) x) (Localization x)

variable (S : Type*) [CommRing S] [Algebra R S]

variable (𝒜 : Graded ι (Submodule R A)) [𝒜.Algebra] (x : Submonoid (S ⊗[R] A)) in
#synth IsScalarTower S ((𝒜.baseChange S).Localization x) (Localization x)

variable (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : Submonoid (S ⊗[R] A)) in
#synth IsScalarTower S (HomogeneousLocalization (fun i ↦ (𝒜 i).baseChange S) x) (Localization x)