Fano Varities

Stream: Is there code for X?

[Pietro Monticone]

Is there code for Fano varieties?

[Yaël Dillies]

No we don't have them

[Pietro Monticone]

How much algebraic geometry has been included in Mathlib?

[Gareth Ma]

You can take a look at https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/AlgebraicGeometry

[Adam Topaz]

We don’t even have “varieties” in any reasonable sense :-/

[Xiyu Zhai]

Looks like much more can be done there. Exciting

[Kevin Buzzard]

I propose putting a predicate IsVariety (or IsAlgebraicVariety) for a morphism of schemes S -> Spec(K), saying it's finite type separated etc etc (whatever a variety is, maybe for some people it also means geom connected but for others it doesn't).

Pietro if you're looking for a challenge in algebraic geometry which goes towards Fano varieties, then it's to construct the sheaf of Kaehler differentials Omega_{X/Y} associated to a morphism f : X -> Y of schemes (first as a sheaf of abelian groups, and then as an O_X-module).

[Kevin Buzzard]

The challenge after that is to define the canonical bundle. After those milestones we can start talking about Fano varieties.