Graded Ring Hom

Stream: mathlib4

[Kenny Lau]

as part of the projective space project, I had to define graded ring hom. This thread is intended to be a space for discussion while I PR it into mathlib.

[Kenny Lau]

the first question would be whether I should just define them directly, or should I first define "graded hom", and then just define graded ring hom to extend both ringhom and gradedhom

[Kenny Lau]

(cc @Christian Merten)

[Kenny Lau]

#30312

[Yi.Yuan]

Just curious—does the ‘graded ring hom’ you’re referring to here have anything to do with what’s in #26862?

[Nailin Guan]

I think no, we only have it as ring homomorphism, but it is almost by definition it is graded ring hom.

[Kenny Lau]

I don't see any ring homomorphism in your linked PR

[Nailin Guan]

The only thing I am a bit curious about is that graded ring hom should work with different index set with a add monoid hom. Is there any usage of this generalization?

[Kenny Lau]

also, the linked PR constructs an "externally" graded ring, but my PR #30312 is concerned with morphisms between "internally" graded rings

[Kenny Lau]

Nailin Guan said:

The only thing I am a bit curious about is that graded ring hom should work with different index set with a add monoid hom. Is there any usage of this generalization?

do you have any usage in mind?

[Nailin Guan]

Kenny Lau 說：

I don't see any ring homomorphism in your linked PR

I think he mean #26862

[Nailin Guan]

Kenny Lau 說：

Nailin Guan said:

The only thing I am a bit curious about is that graded ring hom should work with different index set with a add monoid hom. Is there any usage of this generalization?

do you have any usage in mind?

Not yet, this idea came from @Wang Jingting , he may have some applications in mind.

[Kenny Lau]

how come the filtered rings have both FA and FA_lt?

[Nailin Guan]

This is another story, we can move to channel "Filtered Algebra" in PR review.

[Wang Jingting]

Nailin Guan said:

Kenny Lau 說：

Nailin Guan said:

The only thing I am a bit curious about is that graded ring hom should work with different index set with a add monoid hom. Is there any usage of this generalization?

do you have any usage in mind?

Not yet, this idea came from Wang Jingting , he may have some applications in mind.

Well, I know that this generalization is possible, but the reason why I didn't propose it here in the first place is exactly that I don't have any real applications in mind. But I discussed with Nailin, and he suggested maybe we can first post the idea here, and then see if it reminds anyone of something. (The community definitely has more expertise in math than us, so maybe someone will have something in mind?)

[Kenny Lau]

I would just like to note that under most reasonable assumptions, the map on gradings will be injective, which means that any graded ring equivs will make the map on gradings bijective

[Kenny Lau]

I have encountered one obstacle while applying graded ring hom: I have a setup of the form:

{ι A B σ τ : Type*}
[Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B]
[AddSubmonoidClass σ A] [AddSubmonoidClass τ B]
[DecidableEq ι] [AddMonoid ι]
(𝒜 : ι → σ) (ℬ : ι → τ) [GradedRing 𝒜] [GradedRing ℬ]
{F : Type*} [FunLike F A B] [GradedRingHomClass F 𝒜 ℬ]
(f : F) (x : A)

and my problematic expression had the form f x and 𝒜 could not be inferred.

[Kenny Lau]

naturally the first solution might to be make 𝒜 an outparam depending on F... I already did that, or maybe I did it worng

[Kenny Lau]

I don't really know how outparams work

[Kenny Lau]

after more thinking the cause is very obvious, it's because the coercion instance in the expression f x is just derived from the FunLike F A B, which means there is completely no information of 𝒜 within that expression itself

[Kenny Lau]

so the solution might be that I should define a typeclass to extend FunLike instead of being a mixin, like how Ring extends both Add and Mul

[Matthew Ballard]

If you have a homomorphism that is compatible with homomorphism of grading groups, then I think calling it an equivariant (graded) ring hom is reasonable. When the gradings arise as character groups of groups acting on affine schemes, then this corresponds to a homomorphism of groups that is compatible with the morphism of spaces.

[Kenny Lau]

I'm not sure what comment you're addressing. Are you suggesting that I should change the name in #30312?

[Matthew Ballard]

Three comments:

1. I think the name is ok. There is some room for confusion depending you math life experience.
2. There is a lot of utility in the generalization above.
3. The generalization can be called Equivariant…

If we go by library precedent, then we would probably go with the general notion and the specialize down to an id hom for one of the arguments.

[Kenny Lau]

I don't think we currently have a generalisation that encompasses both "external" and "internal" grading

[Kenny Lau]

import Mathlib

structure EquivariantHom {A B ι : Type*}
  (𝒜 : ι → Type*) (ℬ : ι → Type*) {F G : ι → Type*}
  [∀ i, FunLike (F i) (𝒜 i) A] [∀ i, FunLike (G i) (ℬ i) B]
  {φ : ι → Type*} [∀ i, FunLike (φ i) (𝒜 i) (ℬ i)]
  {ψ : Type*} [FunLike ψ A B]
  (ofA : ∀ {i}, F i) (ofB : ∀ {i}, G i) where
  underlying : ψ
  component (i : ι) : φ i
  commutes' {i : ι} (x : 𝒜 i) : underlying (ofA x) = ofB (component i x)

[Kenny Lau]

@Matthew Ballard this would be the generalisation you seek, I don't think this has much point

[Kenny Lau]

Matthew Ballard said:

If we go by library precedent

I think we need to be wary of these "generalisation for generalisation's sake"

[Kenny Lau]

import Mathlib

set_option autoImplicit false

structure EquivariantHom {A B ι : Type*}
    (𝒜 : ι → Type*) (ℬ : ι → Type*) {F G : ι → Type*}
    [∀ i, FunLike (F i) (𝒜 i) A] [∀ i, FunLike (G i) (ℬ i) B]
    (ofA : ∀ {i}, F i) (ofB : ∀ {i}, G i)
    (φ : ι → Type*) [∀ i, FunLike (φ i) (𝒜 i) (ℬ i)]
    (ψ : Type*) [FunLike ψ A B] where
  underlying : ψ
  component (i : ι) : φ i
  commutes' {i : ι} (x : 𝒜 i) : underlying (ofA x) = ofB (component i x)

abbrev GradedRingHom {A B ι σ τ : Type*}
    [Semiring A] [Semiring B] [DecidableEq ι] [AddMonoid ι]
    [SetLike σ A] [AddSubmonoidClass σ A] [SetLike τ B] [AddSubmonoidClass τ B]
    (𝒜 : ι → σ) (ℬ : ι → τ) [GradedRing 𝒜] [GradedRing ℬ] :=
  EquivariantHom (fun {i} ↦ 𝒜 i) (fun {i} ↦ ℬ i)
    (fun {i} ↦ AddSubmonoid.subtype (.ofClass <| 𝒜 i))
    (fun {i} ↦ AddSubmonoid.subtype (.ofClass <| ℬ i))
    (fun {i} ↦ 𝒜 i →+ ℬ i)
    (A →+* B)

[Kenny Lau]

is this what you have in mind?

[Kenny Lau]

if you want to generalise in this way, you'll first need to unify the external and internal gradings, so you want to generalise SetLike to any constructively injective map, which means you'll get the following:

import Mathlib

set_option autoImplicit false

class SetLike' (σ : Type*) (α : outParam Type*) where
  coe : σ → α
  carrier : Set α
  uncoe : Subtype carrier → σ
  coe_injective : coe.Injective
  coe_mem_carrier (x) : coe x ∈ carrier
  left_inv (x) : uncoe ⟨coe x, coe_mem_carrier x⟩ = x
  right_inv (x h) : coe (uncoe ⟨x, h⟩) = x

[Kenny Lau]

internal grading would have σ:Type and α:outParam Type, but external grading would have α:Type and σ:outParam Type so maybe we can't put outParam at all