dealing with OrderHom.dual

Stream: mathlib4

[Ira Fesefeldt]

For a theorem I contributed recently (fixedPoints.gfp_eq_sInf_iterate), I would like to proof the premise on a complete lattice. Since mathlib does not have either ωCoScottContinuous nor CoScottContinuous, the theorem requires ωScottContinuous ⇑(OrderHom.dual f)).

However, proving any goal including OrderHom.dual f seems very annoying to me, as all lattice operations are the wrong way around. Is there a clever trick to make the goal look nicer again?

Simple example:

import Mathlib

open ENNReal OmegaCompletePartialOrder

noncomputable def f (n : ENNReal) : ENNReal := n + 1

noncomputable def f_hom : OrderHom ENNReal ENNReal := ⟨f, sorry⟩

example : ωScottContinuous (OrderHom.dual f_hom) := by
  rw [ωScottContinuous_iff_map_ωSup_of_orderHom]
  dsimp only [OrderDual, Chain, OrderHom.dual, OrderDual.toDual, Equiv.coe_refl, OrderDual.ofDual,
    Function.comp_id, Function.id_comp, Equiv.coe_fn_mk, ωSup, OrderHom.coe_mk, Chain.map,
    OrderHom.comp_coe, Function.comp_apply]
  sorry

[Yaël Dillies]

Note that ωScottContinuous ⇑(OrderHom.dual f)) should be written ωScottContinuous (toDual ∘ f ∘ ofDual). Do you still have in mind the time where the Scott continuity predicate took in an OrderHom?

[Yaël Dillies]

Also note that there is a comment saying that the dual predicates for the different versions of Scott continuity were not defined because we didn't find any use in the literature and didn't need them at the time. If you need them now, you might want to consider adding them.

[Ira Fesefeldt]

Yaël Dillies said:

Note that ωScottContinuous ⇑(OrderHom.dual f)) should be written ωScottContinuous (toDual ∘ f ∘ ofDual). Do you still have in mind the time where the Scott continuity predicate took in an OrderHom?

Ooops, yes.

[Ira Fesefeldt]

Yaël Dillies said:

Also note that there is a comment saying that the dual predicates for the different versions of Scott continuity were not defined because we didn't find any use in the literature and didn't need them at the time. If you need them now, you might want to consider adding them.

I saw that comment. I know that our group uses it quite heavily for connecting fixed point semantics with operational semantics on Markovian models. And could probably find a bit of literature using it. But I couldn't be bothered yet to add cocontinuity myself :sweat_smile:

[Yaël Dillies]

Should be easier than dealing with toDual ∘ f ∘ ofDual everywhere!