Proj should take GradedRing

Stream: mathlib4

[Kenny Lau]

Is there a reason docs#AlgebraicGeometry.Proj takes in a docs#GradedAlgebra instead of a docs#GradedRing? I think this is wrong.

[Kenny Lau]

@Christian Merten

[Christian Merten]

I don't think there is any technical reason why it must be docs#GradedAlgebra. What cases do you want to have supported for σ?

[Kenny Lau]

well i think the existing AddSubmonoidClass is fine because I end up having to compare across different base rings when I use Submodule

[Kenny Lau]

and I end up with assuming R1 and R2 are the base rings and they are algebras over a common ring R

[Kenny Lau]

maybe it makes sense to have R2 be an algebra over R1 instead?

[Christian Merten]

I am not following, can you give some more details on what your setup is?

[Kenny Lau]

https://github.com/kckennylau/EllipticCurve/blob/9a891db3938c36b94e5a96d39e0703b89c272545/EllipticCurve/ProjectiveSpace/TensorProduct/Proj.lean#L428

Here I construct map Proj(S ⊗[R] 𝒜) ⟶ Spec(S) ×[Spec(R)] Proj(𝒜) by using the UMP of pullback, which means I need to construct a map Proj(S ⊗[R] 𝒜) ⟶ Proj(𝒜), which requires a "graded hom" 𝒜 →ᵍᵃ S ⊗ 𝒜 (a class I defined in my project as well), but the problem is that 𝒜 n is R-submodule, and (S ⊗ 𝒜) n := (𝒜 n).baseChange S is S-submodule.

[Kenny Lau]

btw I also had to redefine docs#HomogeneousLocalization.map because the current one again assumes same base ring

[Kenny Lau]

Actually when I defined GradedAlgHom in my project I just threw away the base rings

[Kenny Lau]

but once again let me repeat that in real applications most likely it will be R2 that is an algebra over R1, not the other way round, so I'm willing to assume that in the (future) mathlib PR

[Kevin Buzzard]

Surely it's handy to have Proj for graded algebras because then you get a map down to Spec of the base for free. Isn't it like how we don't really want group schemes because there are essentially no examples (other than GL_n and SL_n etc); we actually want group R-schemes where R is a base, and it's thus good to make everything be an R-algebra from the start.

[Kenny Lau]

every graded algebra is by definition a graded ring so you don't lose on any generality

[Kenny Lau]

the setup is a bit confusing, GradedRing actually takes in any AddSubmonoidClass, and GradedAlgebra is an abbrev for GradedRing (with the AddSubmonoidClass specialised to Submodule over some ring)

[Christian Merten]

The naming is confusing here, GradedRing is also a graded algebra in informal terms.

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/586e9c386274d740624bd33abe9a67f7365a92fc/Mathlib/RingTheory/GradedAlgebra/Basic.lean#L164-L167

/-- A special case of `GradedRing` with `σ = Submodule R A`. This is useful both because it
can avoid typeclass search, and because it provides a more concise name. -/
abbrev GradedAlgebra :=
  GradedRing 𝒜

[Kenny Lau]

and any graded ring gives you a map Proj A -> Spec A0

[Kenny Lau]

so... graded ring?

[Kenny Lau]

I need to change docs#HomogeneousLocalization as well

[Kenny Lau]

but it should just be literally as simple as changing it to GradedRing

[Kenny Lau]

my only concern here is performance -- GradedAlgebra explicitly says it's there to speed up typeclass search

[Kenny Lau]

(but actually don't you need to synthesize the same class every time you call GradedAlgebra anyway? idk how this works; i've also heard "premature optimisation is the root of all evil")

[Christian Merten]

The only way to know for sure is to try it and measure the effect.

[Kenny Lau]

yeah, i'm trying

[Kenny Lau]

i'll bench afterwards

[Kenny Lau]

(i can't read the result anyway, it's all in the order of 10^9, idk what that means)

[Eric Wieser]

I fear that generalizing away from Submodule leads to duplication between rings and semirings

[Eric Wieser]

Because AddSubmonoidClass doesn't go very far in unifying them

[Kenny Lau]

sorry, I didn't understand what you meant, what sort of duplication?

[Eric Wieser]

I guess the question is whether you end up having to specialize to AddSubmonoid and AddSubgroup in your generalization, rather than being able to stick with AddSubmonoidClass throughout

[Kenny Lau]

what's wrong with using the AddSubmonoidClass infrastructure?

[Kenny Lau]

i'll however tell you one obstacle i'm facing right now:

[Eric Wieser]

You can't write \sup or map with AddSubmonoidClass

[Kenny Lau]

hmm...

[Kenny Lau]

should we extend AddSubmonoidClass?

[Kenny Lau]

Kenny Lau said:

i'll however tell you one obstacle i'm facing right now:

I need a way to say that "N has a smul on submodules that commute with inclusion"

[Eric Wieser]

But it's possible that's my concern not relevant to Proj; my comment was meant as a of a problem you might run into, not an objection to you trying

[Kenny Lau]

Kenny Lau said:

I need a way to say that "N has a smul on submodules that commute with inclusion"

This is covered by IsScalarTower if 1 exists, but if there's no 1 then it's a bit trickier to say that

[Kenny Lau]

and I don't think SMulMemClass works, because that class defines its own smul

[Eric Wieser]

What's the statement you want?

[Kenny Lau]

@Eric Wieser

import Mathlib

-- `σ` is a class of subsets of `M`
-- and `α` acts on both
variable (α σ M : Type*) [SetLike σ M] [SMul α M] [∀ s : σ, SMul α s]
/-- The `Prop` that says the two actions commute -/
class CoeSMulClass : Prop where
  coe_smul {s : σ} (c : α) (x : s) : ((c • x : s) : M) = c • x

[Kenny Lau]

actually i didn't need any of the add stuff, modified

[Kenny Lau]

actually i could move s out as well

[Kenny Lau]

wait, this just says coe satisfies map_smul??

[Kenny Lau]

nah i don't think that helps

[Eric Wieser]

[∀ s : σ, SMul α s] combined with coe_smul is basically saying thatσ is a submodule, isn't it?

[Kenny Lau]

it's interesting isn't it, we set up all this infrastructure for SetLike etc to solve all the problems, and now you're kinda telling me to not use it

[Eric Wieser]

I'm telling you where it will stop working for you, not that you shouldn't try using it

[Kenny Lau]

Eric Wieser said:

[∀ s : σ, SMul α s] combined with coe_smul is basically saying thatσ is a submodule, isn't it?

I think you'll understand more when I give you the example (give me 1 min)

[Eric Wieser]

Kenny Lau said:

I need a way to say that "N has a smul on submodules that commute with inclusion"

Do you mean ℕ?

[Kenny Lau]

yes

[Eric Wieser]

coe_nsmul should be a lemma for AddSubmonoidClass, docs#AddSubmonoidClass.coe_nsmul

[Kenny Lau]

i don't want to call a lemma for each possible scalar type...

[Eric Wieser]

Kenny Lau said:

Eric Wieser said:

Do you mean ℕ?

yes

So you mean "yes, but also every other semiring too"?

[Kenny Lau]

import Mathlib

-- `σ` is a class of add-subgroups of `M`
-- and `α` acts on both
variable (α σ M : Type*)

section
variable [SetLike σ M] [SMul α M] [∀ s : σ, SMul α s]

/-- The `Prop` that says the two actions commute -/
class CoeSMulClass : Prop where
  coe_smul {s : σ} (c : α) (x : s) : ((c • x : s) : M) = c • x

end

section AddCommMonoid
variable [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M]

instance : CoeSMulClass ℕ σ M where
  coe_smul n x := AddSubmonoidClass.coe_nsmul x n

end AddCommMonoid

[Kenny Lau]

Eric Wieser said:

Kenny Lau said:

Eric Wieser said:

Do you mean ℕ?

yes

So you mean "yes, but also every other semiring too"?

and their units, and their Finsets, and their Sets, ...

[Kenny Lau]

ok maybe not finset/set

[Eric Wieser]

Eric Wieser said:

What's the statement you want?

You seems to have given me the implementation that you think solves your problem (#xy). Without defining any new classes or generalizing, what's the concrete statement you want?

[Kenny Lau]

@[simp] theorem HomogeneousLocalization.val_smul
    {ι : Type u_1} {R : Type u_2} {A : Type u_3}
    [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} (x : Submonoid A)
    {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] [IsScalarTower α A A]
    (n : α) (y : HomogeneousLocalization 𝒜 x) :
    (n • y).val = n • y.val

[Kenny Lau]

I want to define a smul on HomogeneousLocalization

[Kenny Lau]

now HomogeneousLocalization is a quotient of HomogeneousLocalization.NumDenSameDeg

[Kenny Lau]

which is an expression of the form (a : 𝒜 i) / (s : 𝒜 i ∩ x) (x is the submonoid we're localization at)

[Kenny Lau]

to define the action of a scalar c : α, you define it on this expression as (c • a) / s

[Kenny Lau]

to prove that it's well-defined, you embed everything to Localization x, where you can pull the smul out precisely because of the coe_smul lemma above

[Kenny Lau]

I haven't made any new generalisation because docs#HomogeneousLocalization.val_smul already has a general scalar type α

[Kenny Lau]

Kenny Lau said:

to prove that it's well-defined, you embed everything to Localization x, where you can pull the smul out precisely because of the coe_smul lemma above

more precisely, the proof is:

• Localization.mk (↑(c • a)) (s)
• = Localization.mk (c • ↑a) (s)
• = c • Localization.mk (↑a) (s)
• = c • Localization.mk (↑a') (s')
• = reverse the order

[Kenny Lau]

the second bullet point is coe_smul

[Kenny Lau]

the fact that in that file you have nsmul and zsmul as separate lemmas imply to me that the class hasn't been set up and the class needs to be set up

[Eric Wieser]

The class you're describing already exists, it's SmulMemClass

[Kenny Lau]

right, except that SMulMemClass creates its own smul instance

[Eric Wieser]

That's the right thing to do

[Eric Wieser]

[∀ s : σ, SMul α s] is not a reasonable thing to assume

[Kenny Lau]

no, because nsmul has a separate instance

[Kenny Lau]

it is reasonable because that's how it works for N

[Eric Wieser]

It's defeq, or should be

[Kenny Lau]

I don't think so

[Kenny Lau]

no, nsmul is always "add this n times"

[Kenny Lau]

or it should be

[Eric Wieser]

The whole point of docs#AddMonoid.nsmul is to allow it to _not_ be defeq to "add this n times", so that it can instead be defeq to a different smul

[Kenny Lau]

there's no reason nsmul should look at a setlike and be like "oh wow this is a setlike i'm not gonna add it n times"

[Kenny Lau]

your link doesn't work

[Eric Wieser]

Reason or not, that's what it does

[Kenny Lau]

hmm, lemme try again, i thought it didn't work the first time i tried smulmemclass

[Eric Wieser]

Eric Wieser said:

The class you're describing already exists, it's SmulMemClass

You can't use it because the action is an outParam, and so we can't have both SmulMemClass Nat (s : Subgroup A) and SmulMemClass Int (s : Subgroup A)

[Kenny Lau]

right, ok, that's where the problem was

[Kenny Lau]

(i switched back to smulmemclass and saw where the problem was)

[Kenny Lau]

i'm getting the error:

failed to synthesize
  HSMul ℕ (HomogeneousLocalization 𝒜 x) ?m.25

[Kenny Lau]

does that mean i need to define nsmul separately?

[Kenny Lau]

like now i really see where the #xy was, i saw this error and thought "aha i need my own smul instance"

[Kenny Lau]

yep now i found that AddSubmonoidClass.nsmulMemClass is a theorem (so "local instance")

[Eric Wieser]

does that mean i need to define nsmul separately?

No, it should be provided through the AddCommMonoid instance on HomogeneousLocalization , assuming one exists

[Kenny Lau]

aha ok

[Eric Wieser]

The ?m.25 suggests to me you might want a type ascription in order to see the real error

[Aaron Liu]

Eric Wieser said:

The ?m.25 suggests to me you might want a type ascription in order to see the real error

It's an outparam so having a type ascription won't make the metavariable go away

[Kenny Lau]

Created #30302. There is a strange thing happening that I need to investigate further

[Kenny Lau]

ah actually i misread the code and it's actually fine

[Kenny Lau]

Eric Wieser said:

No, it should be provided through the AddCommMonoid instance on HomogeneousLocalization , assuming one exists

I agree with this in principle, but I notice that in the file the CommRIng instance is defined using the injective map to Localization, so I wonder if it's correct to actually define nsmul separately first

[Kenny Lau]

and I think in light of that, I think before the refactor it actually went through the same path

[Kenny Lau]

they just didn't have to write out the instances explicitly, but in effect before the refactor they also had a separate nsmul and zsmul instance before defining the commring structure

[Kenny Lau]

I think this refactor has confirmed my suspicion - we actually haven't talked about the base ring at all (and indeed i had to add those lemmas in my projective space project)