Refactoring torus definition

Stream: toric

[Michał Mrugała]

I think it's a good idea to adapt our definition of a torus with Andrew's work on group schemes. We essentially only need to lift his results to the over category.

[Yaël Dillies]

Where are Andrew's group schemes?

[Michał Mrugała]

GroupScheme.lean (currently not in mathlib)

[Michał Mrugała]

As a subtask, it would be good to replace the Mathlib import by smaller imports in that file.

[Andrew Yang]

We are lacking a fair bit of rudimentary API on group-objects though. #22168 would be a start.
But someone need to generalize the docs#CategoryTheory.Mon_ClassOfRepresentableBy to CommGrp_Class (where CommGrp_Class doesn't even exist yet)
Would be nice if developing them are a part of this project.

[Michał Mrugała]

I'd be happy to work on this after I manage to formalize the defintion of toric ideals. We will need basic results about tori for our first bigger objective, so developing the API is probably necessary.

[Andrew Yang]

Also one would need to change docs#FreeAbelianGroup to Finsupp so that the definition is defeq to MvLaurentPolynomial

[Andrew Yang]

(or just change docs#AddCommGrp.free if people are lazy like me)

[Yaël Dillies]

I am trying to understand what SplitTorus is defined as, informally. Am I right in saying it's something like R ⊗ ℤ[ℤⁿ]?

[Michał Mrugała]

That’s one way to view it yeah

[Yaël Dillies]

But is it defined like this?

[Michał Mrugała]

It’s defined as a pullback which will be isomorphic to the spectrum of the ring you wrote down

[Michał Mrugała]

The isomorphism should be in mathlib (if it’s not then we really ought to prove it)

[Kevin Buzzard]

A split torus over $R$ should really be Spec(R[G]) where G is a group isomorphic to $\Z^n$ (but without a fixed isomorphism) (or just R[G] if you're happy with the Hopf algebra rather than the affine R-group-scheme).

[Yaël Dillies]

But what about a split torus over an arbitrary scheme? This is what Andrew defined

[Kevin Buzzard]

Well that's relative Spec of O_X[G] where G is a group isomorphic to Z^n. Here O_X is the structure sheaf of the scheme (so O_X is to X as R is to Spec(R)) and given a sheaf of algebras for the sheaf of rings you can take relative spec and get a scheme mapping to X with affine fibres.

[Sophie Morel]

Do we have relative Specs already?

[Yaël Dillies]

Do you mean something like algSpec?

[Michał Mrugała]

That’s not it, this is what Kevin and Sophie are talking about: https://stacks.math.columbia.edu/tag/01LQ

[Sophie Morel]

And I realize that my question was naive, I don't think the theory of quasi-coherent sheaves is developed enough for that.

[Kevin Buzzard]

Oh I guess another definition of "split torus over S" is "S-group-scheme isomorphic to S x_Z Spec(Z[Z^n]) for some natural"

[Andrew Yang]

@Christian Merten has some code on relative specs IIRC.

[Andrew Yang]

Kevin Buzzard said:

S-group-scheme isomorphic to S x_Z Spec(Z[Z^n]) for some natural

Yeah that is the proposed definition.

[Christian Merten]

Andrew Yang said:

Christian Merten has some code on relative specs IIRC.

Not really anything usable, I gave up because, as Sophie said, it seemed pointless as long as we don't have more on quasi-coherent sheaves.