preorder (opposite X)

Stream: Is there code for X?

[Kevin Buzzard]

import tactic

example (α : Type) [preorder α] :
  preorder αᵒᵖ := infer_instance -- fails

Am I missing an import or do we not want this for some reason?

[Kevin Buzzard]

import data.opposite

open opposite

instance (α : Type) [preorder α] : preorder αᵒᵖ :=
{ le := λ a b, unop b ≤ unop a,
  le_refl := λ _, le_refl _,
  le_trans := λ _ _ _ hba hcb, le_trans hcb hba }

[Yaël Dillies]

I assume you have a reason to not use docs#order_dual?

[Kevin Buzzard]

Oh this will work fine. I was wondering whether you could get a Galois insertion with l^{op} and u^{op} if l and u made a Galois insertion

[Kevin Buzzard]

What is the map X -> order_dual X?

[Yaël Dillies]

docs#to_dual, docs#of_dual

[Kevin Buzzard]

lol in a completely different file. No wonder I couldn't find them!

[Kevin Buzzard]

import order.order_dual
import order.galois_connection

open order_dual

example (α β : Type*) [preorder α] [preorder β] (l : α → β) (u : β → α)
  (gi : galois_insertion l u) : galois_insertion
    (to_dual ∘ l ∘ of_dual : order_dual α → order_dual β)
    (to_dual ∘ u ∘ of_dual : order_dual β → order_dual α) :=
sorry

was what I was wondering

[Yaël Dillies]

Sounds elementary enough that something like that should work and either you got the right statement and it's easy or you got the wrong one and it's easily false.

[Reid Barton]

You need to swap l and u as well

[Kevin Buzzard]

but it remains an insertion and not a coinsertion?

[Kevin Buzzard]

Oh so you're saying op sends insertions to coinsertions?

[Reid Barton]

Oh I didn't notice that part

[Reid Barton]

The category theory version is docs#adjunction.op_adjoint_op_of_adjoint

[Eric Wieser]

docs#galois_connection.dual looks like what you want

[Kevin Buzzard]

That's just for connections, I have an insertion

[Yaël Dillies]

That's the same, because the non-connection bit of the insertion doesn't depend on the order.

[Kevin Buzzard]

docs#galois_coinsertion.dual

[Kevin Buzzard]

Rather easy to find once you know what you're looking for!

[Kevin Buzzard]

duality turns insertions into coinsertions

[Kevin Buzzard]

I may as well ask the actual question I'm interested in. Subgroups, subrings, subfields of a group, ring field etc are all Galois insertions into subsets of the group/ring/field, and in all cases top and inf and Inf coincide in the subset lattice and the subobject lattice. Is that a general fact about Galois insertions? I kind of suspect not because I can't find it in the API. I was wondering if I could get a cheap counterexample using duals but it seems that I can't.

[Kevin Buzzard]

Note that bot and sup and Sup don't coincide at all.

[Kevin Buzzard]

(empty set isn't a group, union of two groups isn't a group etc)

[Reid Barton]

Yes (or more generally, right adjoints preserve limits)

[Kevin Buzzard]

import order.galois_connection

example (α β : Type*) [complete_lattice α] [complete_lattice β] (l : α → β) (u : β → α)
  (gi : galois_insertion l u) : u ⊤ = ⊤ := by library_search -- fails

Do I also need that the complete lattice structure on beta is the one coming from alpha or is this automatic? I'm a bit confused

[Kevin Buzzard]

Oh this must be automatic. So then I'm surprised I can't find this. In the examples in my head, alpha is set L, beta is intermediate_field K L or subalgebra K L or subgroup L, l is "adjoin" and u is "coe" or "forget" and it's true. Are these examples leading me astray?

[Eric Wieser]

Certainly all those examples have u x ≤ u y ↔ x ≤ y by definition; is that always true by consequence of the insertion alone?

[Eric Wieser]

docs#galois_connection.u_top

[Eric Wieser]

Library search doesn't know to decay your insertion to a connection before looking for the lemma

[Kevin Buzzard]

Oh I see, I don't need the insertion, right adjoints preserve limits is a statement about connections