Zulip Chat Archive

Stream: general

Topic: galois correspondences


view this post on Zulip Johan Commelin (Nov 17 2018 at 06:29):

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.

view this post on Zulip Johannes Hölzl (Nov 17 2018 at 09:01):

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})

view this post on Zulip Johannes Hölzl (Nov 17 2018 at 09:01):

its in data.set.lattice

view this post on Zulip Johan Commelin (Nov 17 2018 at 09:02):

Thanks


Last updated: May 06 2021 at 22:13 UTC