redefine Graded Algebra

Stream: mathlib4

[Kenny Lau]

This is not part of the projective space project, but I think this might make some things smoother. I propose the following redefinition:

import Mathlib.RingTheory.GradedAlgebra.Basic

#check GradedAlgebra
/-
GradedAlgebra.{u_1, u_2, u_3} {ι : Type u_1} {R : Type u_2} {A : Type u_3}
  [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A]
  (𝒜 : ι → Submodule R A) : Type (max u_1 u_3)
-/

abbrev GradedAlgebra' {ι R A σ : Type*}
    [DecidableEq ι] [AddMonoid ι]
    [Semiring A] [SMul R A]
    [SetLike σ A] [AddSubmonoidClass σ A] [SMulMemClass σ R A]
    (𝒜 : ι → σ) :=
  GradedRing 𝒜

Alternatively, I propose to not touch the existing GradedAlgebra, but when defining GradedAlgHom we secretly use the new assumptions

[Kenny Lau]

basically i just want to unbundle the "base ring" from a graded ring

[Eric Wieser]

But I would guess that's not your motivation

[Eric Wieser]

Currently the only class that satisfies AddSubmonoidClass and SMulMemClass and GradedRing is Submodule, unless LieSubmodule somehow fits

[Kenny Lau]

right, ok, my "real" motivation is to characterise the following map:

given a Nat-graded R-algebra A, and an R-algebra S,
one can construct a Nat-grading on the S-algebra S ⊗[R] A.

the map A -> S ⊗[R] A preserves the grading and R-action, but the LHS is a graded R-algebra and the RHS is a graded S-algebra.

[Kenny Lau]

so, under my new proposal, I would be able to write toTensor : 𝒜 →ₐᵍ[R] S ⊗ᵍ 𝒜

[Kenny Lau]

actually I suppose in my definition above the base ring is still baked in...

[Kenny Lau]

which brings me to the second suggestion:

[Kenny Lau]

Kenny Lau said:

Alternatively, I propose to not touch the existing GradedAlgebra, but when defining GradedAlgHom we secretly use the new assumptions

[Kenny Lau]

so as objects they are just graded rings, but I can now package into a class the statement that "the morphism preserves the R-actions"

[Kenny Lau]

so as cursed as it is, a GradedAlgHom is a map between two GradedRing's

[Kenny Lau]

Eric Wieser said:

Currently the only class that satisfies AddSubmonoidClass and SMulMemClass and GradedRing is Submodule

The catch is that it isn't Submodule, it's Submodule R, meaning that the base ring is tied down to the type, which I want to avoid, because I want to restrict to a smaller ring.

I guess I can still do that via (𝒜 : ι → Submodule S A) [GradedAlgebra 𝒜] [Algebra R S] and then just refer to R all of the time, but is that really better than [SMulMemClass R σ A] (𝒜 : ι → σ) [GradedRing 𝒜]? This latter formulation allows me to avoid mentioning S at all (at the expense of , uh, σ := Submodule S A I guess...)

ok maybe I can reconsider this a bit

[Kenny Lau]

this brings me back actually to an old proposal of mine:

[Algebra R R₁] (𝒜 : ι → Submodule R₁ A) [IsScalarTower R R₁ A]
[Algebra R R₂] (ℬ : ι → Submodule R₂ A) [IsScalarTower R R₂ A]
structure 𝒜 →ₐ[R] ℬ where

[Kenny Lau]

compare this to:

[SMulMemClass R σ A] (𝒜 : ι → σ)
[SMulMemClass R τ B] (ℬ : ι → τ)
structure 𝒜 →ₐ[R] ℬ where

[Kenny Lau]

I think "on paper" σ and τ look cleaner but in practice maybe fixing it to Submodule R1/2 is faster

[Kenny Lau]

let me really type out the two proposals so that we can concretely see the fuller picture:

import Mathlib

set_option autoImplicit false

namespace Proposal1

structure GradedAlgHom (R : Type*) {S T A B ι : Type*}
    [CommRing R] [CommRing S] [CommRing T] [Ring A] [Ring B]
    [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A]
    [Algebra R T] [Algebra T B] [Algebra R B] [IsScalarTower R T B]
    [DecidableEq ι] [AddMonoid ι]
    (𝒜 : ι → Submodule S A) (ℬ : ι → Submodule T B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ]
    extends A →ₐ[R] B where
  map_mem' {i} {x} : x ∈ 𝒜 i → toFun x ∈ ℬ i

end Proposal1


namespace Proposal2

structure GradedAlgHom (R : Type*) {A B ι σ τ: Type*}
    [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B]
    [DecidableEq ι] [AddMonoid ι]
    [SetLike σ A] [AddSubmonoidClass σ A] [SMulMemClass σ R A]
    [SetLike τ B] [AddSubmonoidClass τ B] [SMulMemClass τ R B]
    (𝒜 : ι → σ) (ℬ : ι → τ) [GradedRing 𝒜] [GradedRing ℬ]
    extends A →ₐ[R] B where
  map_mem' {i} {x} : x ∈ 𝒜 i → toFun x ∈ ℬ i

end Proposal2

[Kenny Lau]

/poll Which one do you prefer?
:one:
:two:

[Kenny Lau]

made #30365

[Eric Wieser]

I agree that :one: isn't a perfect solution (but I think it's a better compromise than :two:)

[Kenny Lau]

I did use 1 in #30365

[Antoine Chambert-Loir]

I would like to have graded algebras graded by a monoid (not an addmonoid). This stuff appears in Berkovich's theory.

[Kenny Lau]

is there a difference that is not covered by Additive?

[Antoine Chambert-Loir]

Since there is no mathematical difference, no, but that will force (eventually, when people will want to formalize this) to insert many toAdditive in formulas.

[Kenny Lau]

should we call it MulGradedAlgebra?