Definition of group scheme?

Stream: mathlib4

[Kevin Buzzard]

For FLT I'm running into the issue that I don't really know how to say any of the following.

"Let G be an affine group scheme (or group scheme) over Spec(R) (or S)".

Thanks to work done essentially entirely by undergraduates in Edinburgh and London, I now have a way of saying "let G be an affine group scheme over Spec(R)", and it's "let H be a commutative Hopf algebra over R". Loads of the proofs in Oort-Tate and Raynaud's extension involve careful calculations in Hopf algebras, and perhaps this is the best way to think about it in the finite case. I will need to define what it means for $\rho: \mathrm{Gal}(\overline{\mathbb{Q}_p}/\mathbb{Q}_p)\to\mathrm{GL}_2(\mathbb{F}_p)$ to be flat; the definition is that it's the Galois representation attached to some finite (and hence affine) flat group scheme over the ring $\Z_p$" and I reckon all of that can be set up using module-finite Hopf algebras.

Where it gets a bit gnarlier for me is the theory of connected reductive algebraic groups. Again everything is affine (although this time only ring-finite (i.e. finite-dimensional), not module-finite) and we only need the theory over a perfect field base K to state the global Langlands conjectures for number fields. But now thinking of things as the Hopf algebra sounds ridiculous, we want to talk about the representation theory of this group (it's even in the definition of "reductive"), and I'm not sure I want to develop corepresentation theory in the category of R-coalgebras. What model of affine group schemes over a field do I want for the definition of a reductive group?

Finally, given a connected reductive group over the complexes (or more generally any smooth affine group scheme of finite type over the complexes), I would like to be able to take the associated complex Lie group, and I'd like to do the same thing over the $p$-adic numbers. Right now I'm a bit unclear about how best to state this in Lean.

When we finally get on to moduli spaces, we are going to have to be able to talk about families of elliptic curves over an arbitrary base scheme, because in general moduli spaces aren't affine, and when we're there we really will need non-affine group varieties over non-affine schemes.

[Christian Merten]

Eventually the definition should be "group object in the category of schemes over S" right? Are you saying you want a more concrete, intermediate definition, while the general group scheme theory is not sufficiently developed?

[Kevin Buzzard]

Is that definitely true? Writing Mon_ and Grp_ reminds me awfully of version 2 of schemes, which had SheafOfTypes and SheafOfCommRings. The prefix SheafOf is playing a very similar role to _ there. Version 3 of schemes used category theory (SheafOf Type, SheatOf CommRing) and was the version which made it into mathlib. Adam Topaz was suggesting a more lawvereian approach for monoid objects, group objects etc which works for all algebraic structures and is more natural.

[Kevin Buzzard]

It begins with #11248 so please feel free to review :-)

[Christian Merten]

Is there an outline somewhere? Or a followup PR to #11248?

[Kevin Buzzard]

@Adam Topaz ?

[Christian Merten]

Kevin Buzzard said:

Is that definitely true? Writing Mon_ and Grp_ reminds me awfully of version 2 of schemes, which had SheafOfTypes and SheafOfCommRings. The prefix SheafOf is playing a very similar role to _ there. Version 3 of schemes used category theory (SheafOf Type, SheatOf CommRing) and was the version which made it into mathlib. Adam Topaz was suggesting a more lawvereian approach for monoid objects, group objects etc which works for all algebraic structures and is more natural.

Maybe something like this works:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.ConcreteCategory.Basic
import Mathlib.CategoryTheory.Yoneda

open CategoryTheory

variable (C : Type) [Category C] (D : Type) [Category D] [ConcreteCategory D]

structure DObj : Type _ where
  X : C
  str : Cᵒᵖ ⥤ D
  fac : str ⋙ forget D = yoneda.obj X

[Christian Merten]

A group object in C is DObj C GroupCat.

[Adam Topaz]

You should just come to my (online) talk on Thursday

[Christian Merten]

Where do I find a link?

[Adam Topaz]

I’m not sure

[Adam Topaz]

I think there will be an announcement at some point.

[Adam Topaz]

FWIW I think the case of groups is sufficiently important that we should have various approaches, including using yoneda as above, and provide explicit equivalences between the various cats

[Adam Topaz]

I think the yoneda approach is actually quite good. But it’s not as elegant when you have an algebraic theory with more than one sort.

[Christian Merten]

Adam Topaz said:

I think the yoneda approach is actually quite good. But it’s not as elegant when you have an algebraic theory with more than one sort.

You mean, if you want to consider objects that have factorisations of yoneda.obj X for multiple categories D?

[Adam Topaz]

No not quite. With two sorts you will need two “carrier” objects, etc. So this means you will need a new bespoke structure for n-sorted internal objects, one for every n.

[Adam Topaz]

OTOH if you have a Lawvere theory L, the internal objects associated to L are always the product preserving functors from L to C, no matter how many sorts are involved.

[Adam Topaz]

The main thing I’ve been working on is setting this up in such a way so that this approach has good definitional properties.

[Christian Merten]

Adam Topaz said:

No not quite. With two sorts you will need two “carrier” objects, etc. So this means you will need a new bespoke structure for n-sorted internal objects, one for every n.

Ah, for example module objects over some monoid?

[Christian Merten]

I see, I will wait for your talk then before asking more questions :)

[Joël Riou]

Christian Merten said:

variable (C : Type) [Category C] (D : Type) [Category D] [ConcreteCategory D]

structure DObj : Type _ where
  X : C
  str : Cᵒᵖ ⥤ D
  fac : str ⋙ forget D = yoneda.obj X

With an isomorphism instead of an equality, this is what I do at https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Internal/Basic.lean#L16-L19

With this approach, it is very easy to construct some group schemes: 1) we first define a contravariant functor from schemes to groups (e.g. units, GL_n of global sections) and 2) we show that when forgetting the group structure it is representable.

In order to develop more localization of triangulated categories (e.g. derived categories), I would need some version of this (or at least that if F : C ⥤ D is a functor which preserves finite products (between categories where finite products exists), then there is a obvious functor from abelian group objects in C to abelian group objects in D).

[Christian Merten]

Where does this come up in localization of triangulated categories?

[Joël Riou]

This is to show that under suitable assumptions, a localization of an additive category is also additive. I do this by showing that every object in the localization is endowed with a natural abelian group structure https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Localization/Preadditive.lean#L21-L26

[Christian Merten]

Ah! Because being additive is the same as every object being an internal abelian group object via your https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Internal/Preadditive.lean. But I see you already have https://github.com/leanprover-community/mathlib4/blob/b8729820011e68f5c14374399e1db2ce89a11efb/Mathlib/CategoryTheory/Internal/AddCommGroup.lean#L365C19-L365C45 ?

[Joël Riou]

Yes, this is not speculation: I know how to do all this ;-) (But, if Adam's approach is better, I do not mind too much how exactly it is proved when it eventually reaches mathlib!)

[Adam Topaz]

Proving that a functor which preserves products sends abelian group objects to abelian group objects would be a triviality with my approach

[Adam Topaz]

But the focus isn’t on abelian group objects (or group objects more generally) in particular. I’m also interested in the multi sorted case, which should be useful for, e.g., sheaves of modules

[Adam Topaz]

There’s also some meta aspects to what I’m doing :)

[Joël Riou]

Actually, I have formalized a more direct construction of the preadditive structure on localized categories (using calculus of left fractions) #11728, so that we may have derived categories in mathlib sooner than expected...

[Johan Commelin]

I merged one prereq and left a comment on the other.