Ordinal games

Stream: maths

[Violeta Hernández]

A quick design question. Currently, SetTheory.Surreal.Basic imports SetTheory.Game.Ordinal, and by extension, it imports a lot of ordinal and cardinal arithmetic, which are relatively beefy imports.

[Violeta Hernández]

This import is only used for docs#Ordinal.toSurreal.

[Violeta Hernández]

Should we not do this the other way around? The complete theory of surreal numbers is complicated and will definitely require even further imports, but this basic file should not require anything beyond basic combinatorial game theory, and it definitely should not involve ordinals.

[Violeta Hernández]

@Tristan Figueroa-Reid

[Tristan Figueroa-Reid]

I have no objection to making this the other way around, since Ordinals are a subclass of Surreals :+1:

[Violeta Hernández]

A nice corollary of doing this is that we will then be able to state the correct version of the surreal multiplication birthday conjecture :smile:

[Violeta Hernández]

Thinking about this a bit more. I don't think the reverse import makes much sense either, since surreals will also add a bunch of imports to a file that only otherwise deals with "basic" combinatorial games.

[Daniel Weber]

You could add a Surreal.Ordinal file which has Ordinal.toSurreal

[Violeta Hernández]

Way ahead of you: #21980

[Violeta Hernández]

Violeta Hernández said:

A nice corollary of doing this is that we will then be able to state the correct version of the surreal multiplication birthday conjecture :smile:

Unfortunately this isn't true, since this new file has no need to import birthdays.