Zulip Chat Archive

Stream: Is there code for X?

Topic: if the dual of a well order is also a well order then finite


view this post on Zulip Kenny Lau (Jun 11 2020 at 06:45):

import data.fintype.basic

universe u

theorem fintype_of_well_order {α : Type u} (r : α  α  Prop)
  (H1 : is_well_order α r) (H2 : is_well_order α (flip r)) : fintype α :=
sorry

view this post on Zulip Kenny Lau (Jun 11 2020 at 06:46):

"if the dual of a well order is also a well order then the set is finite"

view this post on Zulip Kenny Lau (Jun 11 2020 at 06:49):

also what is the canonical way to write this

view this post on Zulip Kenny Lau (Jun 11 2020 at 06:49):

also the goal is to build the ring (or field) of functions with well-ordered support

view this post on Zulip Kenny Lau (Jun 11 2020 at 06:54):

the domain being a linearly ordered group

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 07:35):

Are you doing this Hahn product thing?

view this post on Zulip Kenny Lau (Jun 11 2020 at 07:45):

oh so that's the name

view this post on Zulip Kenny Lau (Jun 11 2020 at 07:45):

https://en.wikipedia.org/wiki/Hahn_series

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 07:49):

They're mentioned in Wedhorn's adic spaces notes

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 07:49):

They play a role in the theory of valuations

view this post on Zulip Kenny Lau (Jun 11 2020 at 07:50):

so I assume it's already formalized in the perfectoid project?

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 08:06):

No we didn't need them. We only formalised what we needed for perfectoid spaces

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 08:06):

This is exactly the problem of formalising with an aim in mind


Last updated: May 16 2021 at 05:21 UTC