map-comap adjunction for relations

Stream: Is there code for X?

[Aaron Liu]

I am looking for the way to comap a relation by two functions, that gives a docs#GaloisConnection between docs#Relation.Map and the relation comap, for each pair of functions. It should be defeq to fun x y => r (f x) (g y) for comapping the relation r by the two functions f and g.

[Anatole Dedecker]

We have docs#Setoid.comap and docs#Function.onFun, but no Galois connection in sight :(

[Aaron Liu]

I have these proofs

import Mathlib

-- import Mathlib.Order.GaloisConnection.Defs
-- I don't think it should go in GaloisConnection/Defs
#min_imports in
theorem Relation.gc_map_comap {α β γ δ : Type*} (f : α → γ) (g : β → δ) :
    GaloisConnection (fun r => Relation.Map r f g) (fun r x y => r (f x) (g y)) := by
  intro r s
  apply not_iff_not.1
  simp [Pi.le_def, Relation.map_apply]

-- import Mathlib.Data.Setoid.Basic
-- probably fine to go in Setoid/Basic
#min_imports in
theorem Setoid.gc_map_comap {α β : Type*} (f : α → β) :
    GaloisConnection (fun s => Setoid.map s f) (Setoid.comap f) :=
  fun _ _ => Setoid.gi.gc.le_iff_le.trans (Relation.gc_map_comap f f).le_iff_le

Are these theorems good to go into mathlib as-is? Which file should they go in?

[Kevin Buzzard]

Is there a Mathlib.Order.GaloisConnection.Basic?

[Aaron Liu]

file#Order/GaloisConnection/Basic

[Aaron Liu]

looks like it exists

[Kevin Buzzard]

I think the rule is: if it could go in defs, put it in basic.

[Aaron Liu]

I don't think it should go in there either

[Aaron Liu]

there's nothing about Relation.foo in GaloisConnection/Basic