Zulip Chat Archive

Stream: general

Topic: galois insertion


Kenny Lau (Sep 25 2018 at 05:32):

import algebra.archimedean

example (α : Type*) [floor_ring α] : galois_insertion (ceil : α  ) coe :=
{ choice := λ x _, x,
  gc := λ x n, ceil_le,
  le_l_u := λ _, le_of_eq (ceil_coe _).symm,
  choice_eq := λ _ _, rfl }

Kenny Lau (Sep 25 2018 at 05:32):

let's come up with more examples

Mario Carneiro (Sep 25 2018 at 05:35):

nice observation. Of course floor is also in an adjoint pair, this time on the right side

Mario Carneiro (Sep 25 2018 at 05:39):

also natural number subtraction is best understood in terms of the galois connection it forms with addition

Mario Carneiro (Sep 25 2018 at 05:39):

same with natural/integer division

Kenny Lau (Sep 25 2018 at 05:43):

also natural number subtraction is best understood in terms of the galois connection it forms with addition

previously unsaid sentence in human history @Kevin Buzzard

Simon Hudon (Sep 25 2018 at 05:46):

Sorry, I have to contradict you. I wrote those Galois connection and PRed them to the core library while I was interning at Galois. And I thought that was a beautiful coincidence and wouldn't shut up about it :P

Mario Carneiro (Sep 25 2018 at 05:47):

did you make any galois connections while you were there? :)

Simon Hudon (Sep 25 2018 at 05:47):

I certainly did :D

Kevin Buzzard (Sep 25 2018 at 07:05):

Kenny can you remind me what a Galois connection and Galois insertion is?

Reid Barton (Sep 25 2018 at 11:59):

If it helps, Galois connection ~ adjunction and Galois insertion ~ reflective subcategory, i.e. one of the adjoints is the inclusion of a full subcategory (or possibly coreflective, probably the other one is called a Galois coinsertion)

Reid Barton (Sep 25 2018 at 11:59):

where ~ means "is what you get by specializing to preorders = categories with at most one morphism in each hom set"

Kevin Buzzard (Sep 25 2018 at 12:24):

so a pair of adjoint functors and one is inclusion of a full subcategory. Aren't there lots of examples then? e.g. metric spaces <-> complete metric spaces and lots of other examples of when you drop a property of X and then find some adjoint?

Reid Barton (Sep 25 2018 at 12:29):

Yes except metric spaces don't form a preorder

Reid Barton (Sep 25 2018 at 12:31):

So the flavor of the examples tends to be a bit different, e.g., sub-R-modules inside all subsets or these floor/ceiling examples. But the theorems are largely the same--the left half of the connection preserves sups and so on

Kevin Buzzard (Sep 25 2018 at 12:35):

Aah! At most one morphism between two objects, and a pair of adjoint functors, and inclusion of a full subcategory. That's the question.

Kenny Lau (Sep 29 2018 at 10:59):

Is nat.pred and nat.succ a galois insertion?

Kenny Lau (Sep 29 2018 at 11:00):

I can't seem to prove it

Kevin Buzzard (Sep 29 2018 at 11:29):

a<= succ b iff pred a <= b looks true to me

Kevin Buzzard (Sep 29 2018 at 11:29):

succ is inclusion of a full subcategory

Kevin Buzzard (Sep 29 2018 at 11:30):

succ a <= b iff a <= pred b is false though

Kevin Buzzard (Sep 29 2018 at 11:31):

And pred is not an inclusion of a full subcategory

Kevin Buzzard (Sep 29 2018 at 11:35):

So it's 50-50 from where I'm sitting as to whether it's an insertion or a coinsertion

Kevin Buzzard (Sep 29 2018 at 11:35):

But it's not both

Mario Carneiro (Sep 29 2018 at 11:50):

I was surprised to find that this wasn't already proven... more accurately there were some silly assumptions

Mario Carneiro (Sep 29 2018 at 11:51):

a - b <= c <-> a <= b + c is the galois connection, which is an insertion since (a + b) - b = a. Take b = 1 and you have succ/pred


Last updated: Dec 20 2023 at 11:08 UTC