galois correspondences

Stream: general

[Johan Commelin]

Do we already have the Galois correspondence for set.map and set.comap (aka, range and preimage)?
Is there machinery to glue Galois correspondences together? E.g. I would like to get a Galois correspondence for opens.map and opens.comap more or less for free.

[Johannes Hölzl]

its between set.image and set.preimage (and there is one between preimage and kern_image f s := {y | ∀x, f x = y → x ∈ s})

[Johannes Hölzl]

its in data.set.lattice

[Johan Commelin]

Thanks