PR summary 85a0356966

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

Am I correct in saying this is pretty much OrdinalApprox.lfpApprox but generalized to other complete lattices? If so, then we should probably deal with deduplicating them.

Am I correct in saying this is pretty much OrdinalApprox.lfpApprox but generalized to other complete lattices? If so, then we should probably deal with deduplicating them.

I would be happy if this was a particular case of another construction, but please note that in the applications φ : I → I satisfies i ≤ φ i, but there is no reason that φ : I →o I.

Well, more precisely, I think OrdinalApprox.lfpApprox and TransfiniteIteration are both special cases of the following definition:

def transfiniteIterate {I J : Type*}
    [SupSet I] [PartialOrder J] [SuccOrder J] [WellFoundedLT J] (f : I → I) (n : J) : I → I :=
  SuccOrder.limitRecOn n
    (fun _ _ ↦ id) (fun _ _ g ↦ f ∘ g) (fun y _ IH ↦ ⨆ x : Set.Iio y, IH x.1 x.2)

There's no actual requirement that f be monotonic, but if isn't, then the limit case won't necessarily correspond to the limit. I'm not sure what works for your application, but I'd imagine that we'd actually want to use something like limsup instead of the supremum instead.

Well, more precisely, I think OrdinalApprox.lfpApprox and TransfiniteIteration are both special cases of the following definition:

def transfiniteIterate {I J : Type*}
    [SupSet I] [PartialOrder J] [SuccOrder J] [WellFoundedLT J] (f : I → I) (n : J) : I → I :=
  SuccOrder.limitRecOn n
    (fun _ _ ↦ id) (fun _ _ g ↦ f ∘ g) (fun y _ IH ↦ ⨆ x : Set.Iio y, IH x.1 x.2)

There's no actual requirement that f be monotonic, but if isn't, then the limit case won't necessarily correspond to the limit. I'm not sure what works for your application, but I'd imagine that we'd actually want to use something like limsup instead of the supremum instead.

Thanks very much for the shorter definition!

I think I still want to use the supremum. Under the assumption i ≤ φ i, I show that the function which sends j to the jth iteration evaluated at i₀ : I is a monotone function.

The advantage with using the limsup (or really any more proper notion of a limit on complete lattices) is that it also gives us the dual notion of a transfinite iterate for functions with i ≤ f i without having to declare it separately.

If you want we can discuss this further on Zulip. I think it'd be really nice to link this definition to our existing ordinal API.

The advantage with using the limsup (or really any more proper notion of a limit on complete lattices) is that it also gives us the dual notion of a transfinite iterate for functions with i ≤ f i without having to declare it separately.

If you want we can discuss this further on Zulip. I think it'd be really nice to link this definition to our existing ordinal API.

I am not sure there is a need to unify with OrdinalApprox.lfpApprox, as this definition is used only in one file, involves Ordinal rather than a well-ordered type J (which is very much what we want to consider in category theory, because J has a category structure) and in the file, it seems the definitional properties matter. It seems to me using limsup would only make things more complicated, and anyway in OrdinalApprox.lfpApprox, ⨆ is used, not limsup.

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style