order isomorphisms preserve disjointness

Stream: Is there code for X?

[Eric Wieser]

Do we have these somewhere? Can they be stated more generally?

lemma disjoint.comap_order_iso {α β : Type*} [semilattice_inf_bot α]
  [complete_lattice β] {a b : α}
  (f : α ≃o β) (ha : disjoint a b) : disjoint (f a) (f b) :=
begin
  rw [disjoint, ←f.map_inf, ←f.map_bot],
  exact f.monotone ha,
end

lemma complete_lattice.independent.comap_order_iso {ι} {α β : Type*} [complete_lattice α]
  [complete_lattice β] {a : ι → α} (f : α ≃o β)
  (ha : complete_lattice.independent a) : complete_lattice.independent (f ∘ a) :=
λ i, ((ha i).comap_order_iso f).mono_right (f.monotone.le_map_supr2 _)

[Kevin Buzzard]

I think the first one is not true if f is assumed only to be an order-preserving injection, and is also not true if f is only assumed to be an order-preserving surjection. By "order-preserving" I mean a <=b -> f a <= f b, not <->. With <-> a surjection is enough I guess.

[Eric Wieser]

Is there a way of stating this about galois connections / insertions?

[Kevin Buzzard]

for the first one you don't need beta to be a complete lattice, just anything where the statement makes sense I guess. For me a Galois connection has a map in the other direction too -- you'd be happy to have such a thing? I don't immediately know the answer. Dumb category theory question: do adjoint functors take initial objects to initial objects?

[Eric Wieser]

Whoops, that was a typo in the first one, fixed

[Kevin Buzzard]

Here's a counterexample to something: I think the inclusion of subgroup G into set G is part of a Galois insertion, however it's not true that if H and K are two subgroups of G such that the subgroup they generate is all of G, then their union is all of G, and it's never true that if their intersection is trivial i.e. {1} then their intersection is empty, so that puts paid to some conjectural generalisations (it's also an example of an adjoint functor not sending bot to bot)

[Kevin Buzzard]

It's also not true that if two subsets of G have empty intersection then the subgroups generated by these subsets have trivial intersection (e.g. {2} and {3} in the integers)

[Kevin Buzzard]

The one thing that is true is that if two subsets of G have union equal to all of G then the subgroups they generate have join equal to all of G

[Kevin Buzzard]

If L -> M is part of a Galois insertion then is L^{op} -> M^{op} also part of a Galois insertion?

[Kevin Buzzard]

that doesn't look right to me -- it seems to be saying "if I'm a left adjoint, am I a right adjoint?" which I think is nonsense. So it might be the case that the union fact somehow generalises -- I don't think it's ruled out by the other counterexamples

[Kevin Buzzard]

For me a Galois insertion is a pair of adjoint functors F and G plus some fact that F(G(x))=x. If we op this then we seem to get a different definition -- does that sound right? The concept "F is left adjoint to G and F(G(x))=x" is different to the concept "F is right adjoint to G and F(G(x))=x". Is one of these concepts more useful than the other?

[Kevin Buzzard]

aah got it, that's the coinsertion.

[Mario Carneiro]

shouldn't you be flipping the order of F and G in the composition if you are opping things?

[Kevin Buzzard]

I don't think so.

[Kevin Buzzard]

If F : L -> M preserves <= then it preserves >= so you get a map L^{op} -> M^{op}

[Kevin Buzzard]

I think I just invented Galois coinsertions. So it might be true that there's a theorem for Galois coinertions that if a meet b is bot then f a meet f b is bot, where f is one of the two coinsertion maps. My only justification for this is "it's true for the group example above"

[Kevin Buzzard]

(the example being the coinsertions "subgroup generated by" and "carrier" in (set G)^{op} and (subgroup G)^{op})

[Eric Wieser]

I went ahead and PR'd the lemmas at the top of this thread in #10108

[Yaël Dillies]

I couldn't think of a sensible generalization.

[David Wärn]

I suppose the 'disjoint' version generalizes to functions which preserve bot and binary inf, and the 'independent' one to functions which preserve arbitrary sup and binary inf (basically 'frame homomorphisms')

[David Wärn]

There's no reason to expect a right adjoint to preserve initial objects (e.g. the forgetful functor from groups to sets). In the same way there's no reason to expect the right part of a Galois connection to preserve bot -- e.g. the inclusion of pnat in nat.

[Eric Wieser]

David Wärn said:

I suppose the 'disjoint' version generalizes to functions which preserve bot and binary inf, and the 'independent' one to functions which preserve arbitrary sup and binary inf (basically 'frame homomorphisms')

But we don't have those generalizations today, right?

[Kevin Buzzard]

I think that the Galois coinsertion generalisation might work out. Say l and u form a docs#galois_coinsertion and use notation as in that link. Say s,t in beta and s meet t is bot. Then for all b in beta, b<=s and b<=t implies b<=bot, and so for all a in alpha, l a <= s and l a <= t implies l a <= bot. So for all a in alpha, a <= u s and a <= u t implies a <= u (bot). So we're done (i.e. we've proved u s meet u t = bot) if u bot = bot for a Galois coinsertion. This feels right to me because u has to be a surjection, so u x = bot for some x, and bot <= x so u bot <= u x = bot. I think this is OK.

[Kevin Buzzard]

I would formalise but I'm about to get on a train to Oxford to go and evangelise to the undergrads.

[David Wärn]

Aha yes. You could say that u preserves infs since it's the right part of a Galois connection, and preserves the sup of any family of elements which are already of the form l x (so in particular the empty sup), basically because l preserves sups. The corresponding categorical fact would be that a coreflective subcategory is closed under colimits.

[Yury G. Kudryashov]

Why the first lemma is called comap? For me, comap moves things back along a map, not forward.

[Yury G. Kudryashov]

Probably we should have an @[simp] iff lemma at least about disjoint (f a) (f b).

[Eric Wieser]

I was emulating things like docs#equivalence.comap

[Eric Wieser]

But I guess it's not a good match. Should I rename to map?

[Yury G. Kudryashov]

equivalence.comap moves a statement back along f. Yes, I would prefer map.

[Eric Wieser]

I've updated #10108, but Ci is running on bad runners I think

[Eric Wieser]

Good point about the iff lemma, that made some proofs shorter