galois insertion

Stream: general

[Kenny Lau]

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]

let's come up with more examples

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

same with natural/integer division

[Kenny Lau]

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]

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]

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

[Simon Hudon]

I certainly did :D

[Kevin Buzzard]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

Yes except metric spaces don't form a preorder

[Reid Barton]

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]

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]

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

[Kenny Lau]

I can't seem to prove it

[Kevin Buzzard]

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

[Kevin Buzzard]

succ is inclusion of a full subcategory

[Kevin Buzzard]

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

[Kevin Buzzard]

And pred is not an inclusion of a full subcategory

[Kevin Buzzard]

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

[Kevin Buzzard]

But it's not both

[Mario Carneiro]

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

[Mario Carneiro]

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