Dean Young (Feb 22 2023 at 04:13): Dean Young (Feb 22 2023 at 04:13):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?
Alexander Gryzlov (Feb 22 2023 at 11:43):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.
Ali Caglayan (Feb 22 2023 at 11:46):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.
Ali Caglayan (Feb 22 2023 at 11:48):Also, this only works for n-truncated objects, i.e. simplicial sets whose k>=n k-homotopy groups are trivial.
Ali Caglayan (Feb 22 2023 at 11:49):For whiteheads theorem to work for an arbitrary object of a topos, you need the topos to be hypercomplete.
Ali Caglayan (Feb 22 2023 at 11:50):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).
Ali Caglayan (Feb 22 2023 at 11:52):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.
Ali Caglayan (Feb 22 2023 at 11:54):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.
Ali Caglayan (Feb 22 2023 at 11:55):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.
Ali Caglayan (Feb 22 2023 at 11:56):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.
Ali Caglayan (Feb 22 2023 at 11:56):See https://leanprover-community.github.io/lean-perfectoid-spaces/
Ali Caglayan (Feb 22 2023 at 11:57):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: Oct 13 2024 at 01:02 UTC