API for Ordinal.toType

Stream: mathlib4

[Mirek Olšák]

I was recently playing with ordinals, and converting between Ordinal.toType & Ordinal still seemed more cumbersome that it should be. Would you agree having such functions / theorems in mathlib is reasonable? Or am I just using Ordinals wrong, and should be relying on other concepts than Ordinal.toType? The idea is just to provide a more user-friendly functions around Ordinal.enumIsoToType -- coercion, easier to write functions such as α.get instead of (Ordinal.enumIsoToType β).symm α ...

namespace Ordinal.toType

noncomputable
def mk {α : Ordinal} (β : Ordinal) (lt : β < α) : α.toType :=
  enumIsoToType _ ⟨β, lt⟩
@[coe]
noncomputable
def get {α : Ordinal} (β : α.toType) : Ordinal :=
  (enumIsoToType α).symm β

noncomputable
instance (α : Ordinal) : CoeOut (Ordinal.toType α) Ordinal where
  coe := get

theorem get_lt {α : Ordinal} (β : α.toType) : β.get < α :=
  (α.enumIsoToType.symm β).2
@[simp]
theorem get_mk {α : Ordinal} (β : Ordinal) (h : β < α) :
  (Ordinal.toType.mk β h).get = β := by simp [mk, get]
@[simp]
theorem mk_get {α : Ordinal} (β : α.toType) :
    mk β.get β.get_lt = β := by simp [mk, get]

@[simp, norm_cast, mono]
theorem coe_le_coe {α : Ordinal} (β γ : α.toType) :
    ↑β ≤ (↑γ : Ordinal) ↔ β ≤ γ := by
  unfold get
  simp
@[simp, norm_cast, mono]
theorem coe_lt_coe {α : Ordinal} (β γ : α.toType) :
    ↑β < (↑γ : Ordinal) ↔ β < γ := by
  unfold get
  simp

end Ordinal.toType

[Aaron Liu]

The idea is most cases you should be fine with Iio o instead of o.toType.

[Mirek Olšák]

Not if you want to put it into some structures without raising universe level.

[Mirek Olšák]

In my case, I wanted to do something funny like this

def Hierarchy2 (α : Ordinal) : Type :=
  if α = 0 then Nat
  else ∀ β : α.toType, Hierarchy2 β → Hierarchy2 β
termination_by α
decreasing_by simp [β.get_lt]

I also talked to a colleague mathematician who needed some ordinal-indexed family for his homological algebra (I don't know the details).

[Mirek Olšák]

So I thought that we could just use toType to ensure low universe level, but convert to a standard Ordinal as soon as we can. This conversion is somewhat annoying with enumIsoToType, and I didn't even figure out if it could be done with Ordinal.bfamilyOfFamily / Ordinal.familyOfBFamily

[Mirek Olšák]

If you think the conversion should be to Set.Iio instead of Ordinal separated with the < property, it could be considered too, but there should be some API in my view.

[Liran Shaul]

Here is a problem I ran into, and discussed with Mirek. I am trying to study the following structure:

def Submodule.IsCountablyGenerated (N : Submodule R M) : Prop :=
  ∃ s : Set N, s.Countable ∧ span R s = ⊤

def IsRelativeComplement (A B C : Submodule R M) : Prop :=
  A ≤ B ∧ C ≤ B ∧ Disjoint A C ∧ A ⊔ C = B

def Ordinal.IsLimitOrdinal (α : Ordinal) : Prop :=
  α ≠ 0 ∧ ∀ β, β + 1 ≠ α

/-! ### The Kaplansky Dévissage Structure -/




structure KaplanskyDevissage
(R : Type*) [Ring R] (M : Type*) [AddCommGroup M] [Module R M] (S : Ordinal) where
  seq : ∀ α : Ordinal, α < S → Submodule R M
  monotone : ∀ {α β : Ordinal} (hα : α < S) (hβ : β < S), α ≤ β → seq α hα ≤ seq β hβ
  zero_eq_bot : ∀ (h : 0 < S), seq 0 h = ⊥
  union_eq_top : (⨆ (α : Ordinal) (h : α < S), seq α h) = ⊤
  limit_continuity : ∀ (α : Ordinal) (hα : α < S),
    Ordinal.IsLimitOrdinal α →
    seq α hα = ⨆ (β : Ordinal) (hβ : β < α), seq β (hβ.trans hα)
  succ_step : ∀ (α : Ordinal) (h : Order.succ α < S),
    ∃ (C : Submodule R M),
      IsRelativeComplement
        (seq α (lt_of_lt_of_le (Order.lt_succ α) (le_of_lt h)))
        (seq (Order.succ α) h)
        C ∧
      C.IsCountablyGenerated

The difficulty with the code written like this is that the line

seq : ∀ α : Ordinal, α < S → Submodule R M

makes you move from one universe to the next one, becausde lean ignores the \alpha < S condition.

[Aaron Liu]

oh this is tricky

[Aaron Liu]

by the way, you should usually always be writing Ordinal.{u} with the explicit universe level instead of Ordinal in the case that the universe is an mvar

[Mirek Olšák]

With the API I was proposing this would be as follows. (as I mentioned, we could also try a conversion to Set.Iio instead)

variable {R : Type} [Ring R] {M : Type} [AddCommGroup M] [Module R M]
def Submodule.IsCountablyGenerated (N : Submodule R M) : Prop :=
  ∃ s : Set N, s.Countable ∧ span R s = ⊤

def IsRelativeComplement (A B C : Submodule R M) : Prop :=
  A ≤ B ∧ C ≤ B ∧ Disjoint A C ∧ A ⊔ C = B

def Ordinal.IsLimitOrdinal (α : Ordinal) : Prop :=
  α ≠ 0 ∧ ∀ β, β + 1 ≠ α

/-! ### The Kaplansky Dévissage Structure -/

structure KaplanskyDevissage (S : Ordinal.{0}) where
  seq : S.toType → Submodule R M
  monotone : ∀ {α β : Ordinal} (hα : α < S) (hβ : β < S), α ≤ β → seq (.mk α hα) ≤ seq (.mk β hβ)
  zero_eq_bot : ∀ (h : 0 < S), seq (.mk 0 h) = ⊥
  union_eq_top : (⨆ (α : Ordinal) (h : α < S), seq (.mk α h)) = ⊤
  limit_continuity : ∀ (α : Ordinal) (hα : α < S),
    Ordinal.IsLimitOrdinal α →
    seq (.mk α hα) = ⨆ (β : Ordinal) (hβ : β < α), seq (.mk β (hβ.trans hα))
  succ_step : ∀ (α : Ordinal) (h : Order.succ α < S),
    ∃ (C : Submodule R M),
      IsRelativeComplement
        (seq (.mk α (lt_of_lt_of_le (Order.lt_succ α) (le_of_lt h))))
        (seq (.mk (Order.succ α) h))
        C ∧
      C.IsCountablyGenerated

[Violeta Hernández]

Mirek Olšák said:

Not if you want to put it into some structures without raising universe level.

The general idea is that if you absolutely need a certain universe level, you can write definitions using a.toType, but then expose all of the API using just Iio a

[Violeta Hernández]

btw, we already have a predicate for limit ordinals! docs#Order.IsSuccLimit

[Mirek Olšák]

Violeta Hernández said:

The general idea is that if you absolutely need a certain universe level, you can write definitions using a.toType, but then expose all of the API using just Iio a

That was my idea too but even for implementing this exposure in individual cases, better API on the side of toType would be appreciated.

[Violeta Hernández]

I'm personally of the idea enumIsoToType is fine as is. Your proposal seems to be to unbundle the isomorphism, which just leads to a bunch of auxiliary lemmas that have to be reproved instead of being directly available.

[Aaron Liu]

also wasn't it used to be called Ordinal.ToType what happened to that

[Violeta Hernández]

Yeah, perhaps we could choose a less unwieldy name

[Violeta Hernández]

That I agree with

[Aaron Liu]

did Multiset.ToType also get renamed

[Aaron Liu]

or did I just remember wrong

[Mirek Olšák]

I thought if we could have coercions for example...

[Mirek Olšák]

or at least both directions without calling .symm

[Violeta Hernández]

Aaron Liu said:

did Multiset.ToType also get renamed

I think Ordinal.toType was Ordinal.Type in Lean 3 but got renamed because that was a protected name in Lean 4

[Aaron Liu]

oh ok

[Violeta Hernández]

Mirek Olšák said:

I thought if we could have coercions for example...

That's not a bad idea, a coercion from a.toType to Ordinal

[Violeta Hernández]

Though I do still worry about adding much API here, since the idea is that you are not working with a.toType under most circumstances

[Mirek Olšák]

Then I propose just this:

noncomputable
abbrev Ordinal.toType.mk {α : Ordinal} : Set.Iio α ≃o α.toType := enumIsoToType α

noncomputable
instance (α : Ordinal) : Coe (Ordinal.toType α) (Set.Iio α) where
  coe := (Ordinal.toType.mk).symm
noncomputable
instance (α : Ordinal) : CoeOut (Ordinal.toType α) Ordinal where
  coe x := (↑x : Set.Iio α)

theorem Ordinal.toType.coe_lt {α : Ordinal} (β : α.toType) : β < α := (β : Set.Iio α).prop

[Mirek Olšák]

enumIsoToType could be also just renamed to toType.mk

[Violeta Hernández]

I like that proposal :slight_smile:

[Mirek Olšák]

Good, I am just tweaking the details

[Violeta Hernández]

I think we need some theorems linking mk and coe as inverses but otherwise I'd like to see this in place of enumIsoToType

[Violeta Hernández]

I can PR it if you want, or perhaps you want to do it

[Mirek Olšák]

I discovered that if I don't name the coercion function, it will automatically expand

[Violeta Hernández]

oh! that seems like a good thing

[Mirek Olšák]

I would anyway make some name (like get) but make it an abbrev, so that simp can see through it

[Mirek Olšák]

and the coe_lt seems a bit silly when I #check, I think it is not needed after all

[Joël Riou]

An alternative approach would be to use the structure docs#CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape (see also the file https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.html where this is used to show that Grothendieck abelian categories have enough injectives).

[Mirek Olšák]

https://github.com/leanprover-community/mathlib4/pull/32408

[Dexin Zhang]

Mirek Olšák said:

Then I propose just this:

noncomputable
abbrev Ordinal.toType.mk {α : Ordinal} : Set.Iio α ≃o α.toType := enumIsoToType α

noncomputable
instance (α : Ordinal) : Coe (Ordinal.toType α) (Set.Iio α) where
  coe := (Ordinal.toType.mk).symm
noncomputable
instance (α : Ordinal) : CoeOut (Ordinal.toType α) Ordinal where
  coe x := (↑x : Set.Iio α)

theorem Ordinal.toType.coe_lt {α : Ordinal} (β : α.toType) : β < α := (β : Set.Iio α).prop

Would it be better to coerce toType α to Ordinal directly...?

[Mirek Olšák]

I don't have a strong opinion on this, if Set.Iio is used frequently in the context of ordinals, then both coercions could get used, although initially, I didn't count with Set.Iio.

[Violeta Hernández]

We do use Iio a lot, yes