# 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: Aug 03 2023 at 10:10 UTC