Transfinite recursion

Stream: maths

[Jack McKoen]

I'm trying to recreate this proof in Lean, but I'm having a hard time figuring out transfinite recursion. I don't think the specifics of the proof are that important here, but my basic problem is this:

For a fixed ordinal $\alpha$ I need to recursively define morphisms $\{ u_{\gamma } \} _{\gamma \leq \alpha }$ satisfying certain properties which depend on the morphisms $\{ u_{\beta } \} _{ \beta < \gamma }$, but I haven't been able to come up with a good way to package this.

docs#WellFounded.recursion seems close to what I need but I don't think it's enough (I think it would work if I just had to assign each ordinal to a proposition, but I have to assign morphisms as well).

Can anyone suggest a way to do this?

[Violeta Hernández]

Recursion is what you're looking for

[Violeta Hernández]

Note the signature C : α → Sort, meaning C can contain propositions or data

[Violeta Hernández]

We don't have a way to do bounded recursion on ordinals directly just yet, so as a way to sidestep it you could define, for all ordinals x, an element of x < α → M where M is the type of your morphisms

[Jack McKoen]

Violeta Hernández said:

We don't have a way to do bounded recursion on ordinals directly just yet, so as a way to sidestep it you could define, for all ordinals x, an element of x < α → M where M is the type of your morphisms

Thank you, I think this has put me back on track

[Joël Riou]

Doing such an induction is quite technical. I have already completely formalized the small object argument, but I am PRing it slowly to mathlib. If I understand the language properly, the fact that the class of morphisms which satisfy the left lifting property with respect to a class of morphisms is stable by transfinite composition is the last declaration in this file https://github.com/joelriou/k-injective/blob/main/KInjective/SmallObject/Lifting.lean

[Jack McKoen]

Joël Riou said:

https://github.com/joelriou/k-injective/blob/main/KInjective/SmallObject/Lifting.lean

This is great, Joël. It looks like much of this repo will be useful to me :+1: