Applications of SupHom/InfHom

Stream: mathlib4

[Damien Thomine]

I don't have a good vision of all the order stuff on mathlib, and would like a sanity check before I contribute something.

There is a SupHom structure, i.e. maps which commute with sup of two elements.

I can get a few non-obvious instances of SupHom (e.g. limsup, or topological entropy). I was thinking about proving a general finitary version of SupHom, which would look like

lemma supHom_improved  {α β ι : Type*} [Sup α] [Sup β] [Fintype ι]
[Nonempty ι] (f : ι → α) (g : SupHom α β) :
g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i) := by
sorry

to put in Algebra.Order.Hom.Lattice. Does it sound reasonable?

[Yury G. Kudryashov]

Please assume Finite, not Fintype

[Yaël Dillies]

Can somebody move this to #mathlib4 ?

[Notification Bot]

This topic was moved here from #lean4 > Applications of SupHom/InfHom by Yury G. Kudryashov.

[Yury G. Kudryashov]

Done. Tagging @Damien Thomine to notify about this.

[Damien Thomine]

Thanks Yaël, I msihandled the posting.

Anyways, I found some answer: the Finset version of what I want is map_finset_sup. I didn't find it because it is not in the same file, it calls SupBotHomClass instead of SupBotHom (so Loogle didn't catch it), and there is no documentation which explains this. This feels weird (instead of having a simple statement for a single SupBotHom map, everything is handled through an implicit class of maps), but works well enough.

I can write a iSup version from there.

@Yury G. Kudryashov : That's noted. Is there a preference for finite sets ? What is prefered between (s : Finset X) and {s : Set X} (h : s.Finite)? I've used the former in my current project, but if the latter works better (maybe fewer coercion issues?), a quick refactor is no big deal.

[Yaël Dillies]

Damien Thomine said:

This feels weird (instead of having a simple statement for a single SupBotHom map, everything is handled through an implicit class of maps)

The motivation is that people don't usually deal with SupBotHom directly, but rather with OrderHoms, OrderIsos, etc... Having a statement about f : SupBotHom α β rather than f : F , SubBotHomClass F α β would needlessly limit the applicability of the lemma.

[Patrick Massot]

Damien, you can read about this design in Chapter 7 of MIL.