Toric variety

Stream: toric

[Yaël Dillies]

Re YaelDillies/Toric#10, @Andrew Yang do you really think we should be working with (X : Scheme) [X.Over (Spec R)] rather than (X : Over <| Spec R)?

[Andrew Yang]

Probably yes. Just like we work with {A : Type*} [CommRing A] [Algebra R A] instead of (A : AlgebraCat R).

[Yaël Dillies]

I'm mostly wondering because there seems to be less back and forth if we work with Over (Spec R) straight away

[Andrew Yang]

I am guessing this is because you have only been working with the category theory API and not interacting with other parts of AG. I'm thinking you could even use {X S : Scheme} (f : X ⟶ S) as the input.

[Michał Mrugała]

I think we should change the current definition of a toric variety. It would be best to ask for a finitely generated abelian group as an input rather than an natural number. There is no reason to fix a basis, and I think the Y_A construction shows that sometimes it's best not to fix one.

[Michał Mrugała]

After taking a look at that definition, I'm starting to think we should also refactor our definition of tori. Right now we define it as coming from a free abelian group generated by some type. I think it would be better to provide it with a free abelian group to begin with.