Hi, All,

I'm Dean. I'm new here and excited to learn more about Coq.

Can someone point me towards documentation for varieties?

Also, can someone point me towards wherever the Whitehead theorem is proven in Coq?

If I understand correctly, there's a form of WT at https://github.com/HoTT/Coq-HoTT/blob/master/theories/Homotopy/WhiteheadsPrinciple.v, @Ali Caglayan might be able to comment better on this.

This is however the "synthetic result" about "oo-groupoids", which in AT terms is a version of Whiteheads theorem that holds in an Grothendieck (oo,1)-topos. So in one case, holds for simplicial sets. I am not aware if anybody has formalized topological spaces and proven Whiteheads theorem about them.

Also, this only works for n-truncated objects, i.e. simplicial sets whose k>=n k-homotopy groups are trivial.

For whiteheads theorem to work for an arbitrary object of a topos, you need the topos to be hypercomplete.

There is more detail in the HoTT book about that. But for regular topological spaces I have no idea. Maybe mathcomp people have formalized some topology in that direction, but I doubt we have a statement of Whitehead yet. (I would assume the proof is quite classical relying on lots of AC).

Regarding varieties, I am guessing you mean from Algebraic Geomtry. I am not aware of any serious AG formalizations in Coq. There is no reason they could not happen however, it's just that many serious formalization projects are currently focusing on other topics.

Here is a dumb formalization of localizations of rings by me based on the HoTT library for example https://github.com/Alizter/AlgGeom/tree/main/theories. I just never had the time to improve on it.

I had written down at some point a Gothendieck topology for CRing etc. allowing me to define a scheme as a functor of points. There are a lot of small subtle details that need to be correct for this to work however.

I know that Lean people have a definition of scheme as a locally ringed space and have been able to formalize some serious AG with it.

See https://leanprover-community.github.io/lean-perfectoid-spaces/

Roughly anything that can be done in Lean can also be done in Coq, if it hasn't been done, its probably just that nobody has tried yet.

Last updated: Jun 18 2024 at 09:02 UTC