adjoint example

Stream: maths

[Iocta]

What do I mean here? I think the right answer is "yes, the preimage function works".

import tactic
import order.galois_connection

open set order

/-

For any set $X$ let $P X$ be the power set of set, namely the set of all subsets of $X$. It's easy to see that the subset relation $\subseteq$ makes $P X$ into a poset. Suppose we have any function between sets $ f: X \rightarrow Y $.
This gives a function $ f_{!}: P X \rightarrow P Y $
sending each subset $S \subseteq X$ to its image under $f : f_{!}(S)=\{y \in Y: y=f(x) \text { for some } x \in S\} $.
-/


variables X Y : Type
variables (f: X → Y)
variables (f' : set X → set Y)

def f' (s : set X) : set Y := {y : Y | ∃ x ∈ s, f x = y}

/-
Puzzle 17. Show that $f_{!}: P X \rightarrow P Y$ is a monotone function.
-/
example
(f: X → Y)
(f' : set X → set Y) (hf': ∀ s : set X, f' s = {y : Y | ∃ x ∈ s, f x = y})
(s s' : set X) (hs : s ⊆ s') :
f' s ⊆ f' s' :=
begin
  intros y hy,
  simp only [*, exists_prop, mem_set_of_eq] at *,
  cases hy with x hx,
  use x,
  split,
  { apply hs, exact hx.1, },
  { exact hx.2, },
end


/-
Puzzle 19. Does f! always have a right adjoint? If so, describe it. If not, give an example where it doesn't, and some conditions under which it does have a right adjoint.
-/
example : ∃ (g' : set Y → set X), galois_connection g' f' :=
begin
  unfold galois_connection,
  simp only [le_eq_subset],
  use λys, {x | f x ∈ ys},
end

failed to instantiate goal with fun (ys : 4._.40), (set_of (fun (x : 4._.41), ((frozen_name has_mem.mem) (f x) ys)))
state:
X Y : Type,
f' : set X → set Y
⊢ ∃ (g' : set Y → set X), ∀ (a : set Y) (b : set X), g' a ⊆ b ↔ a ⊆ f' b

[Kevin Buzzard]

You don't need hf' because that's true by definition. You don't need the variable f' either and indeed the only thing it can do is cause confusion. Lean already has a definition of f' by the way, it's called f ''. But it's fine to define it again of course.

[Kevin Buzzard]

Oh I see, you're not using f' in the example. This is very confusing.

[Kevin Buzzard]

I'm not at lean right now but I genuinely don't know whether your puzzle 19 example will pick up the definition f' or the variable f'

[Kevin Buzzard]

Looking at your goal it looks like it picked up the variable, which means your goal isn't provable in 19 because the variable f' has nothing to do with your function f

[Kevin Buzzard]

The reason for your error is that lean has no reason to put f in your local context because there is no mention of it in the statement of what you're trying to prove. There is the variable f' but this is unrelated to f. Why not do what you did in the first example and add f and hf' as assumptions?

[Kevin Buzzard]

You can also delete the definition of f' because you are using it nowhere

[Iocta]

/-
Puzzle 19. Does f! always have a right adjoint? If so, describe it. If not, give an example where it doesn't, and some conditions under which it does have a right adjoint.
-/
example : ∃ (g' : set Y → set X), galois_connection g' f' :=
begin
  unfold galois_connection,
  simp only [le_eq_subset],
  use (λys, ⋃ xs:set X, f' xs ⊆ ys),
end
failed to instantiate goal with fun (ys : 4._.6), (set.Union (fun (xs : set X), ((frozen_name has_subset.subset) (f' xs) ys)))
state:
X Y : Type,
f' : set X → set Y
⊢ ∃ (g' : set Y → set X), ∀ (a : set Y) (b : set X), g' a ⊆ b ↔ a ⊆ f' b

[Iocta]

Now I am using f'

[Iocta]

I guess some other notation for the setified version of f would be clearer

[Iocta]

I'll change that

[Iocta]

import tactic
import order.galois_connection

open set order classical

/-

For any set $X$ let $P X$ be the power set of set, namely the set of all subsets of $X$. It's easy to see that the subset relation $\subseteq$ makes $P X$ into a poset. Suppose we have any function between sets $ f: X \rightarrow Y $.
This gives a function $ f_{!}: P X \rightarrow P Y $
sending each subset $S \subseteq X$ to its image under $f : f_{!}(S)=\{y \in Y: y=f(x) \text { for some } x \in S\} $.
-/


variables X Y : Type
variables (f: X → Y)
variables (ff : set X → set Y)



/-
Puzzle 19. Does f! always have a right adjoint? If so, describe it. If not, give an example where it doesn't, and some conditions under which it does have a right adjoint.
-/
example : ∃ (gg : set Y → set X), galois_connection gg ff :=
begin
  unfold galois_connection,
  simp only [le_eq_subset],
  use (λys, ⋃ xs:set X, ff xs ⊆ ys),
end
failed to instantiate goal with fun (ys : 4._.6), (set.Union (fun (xs : set X), ((frozen_name has_subset.subset) (ff xs) ys)))
state:
X Y : Type,
ff : set X → set Y
⊢ ∃ (gg : set Y → set X), ∀ (a : set Y) (b : set X), gg a ⊆ b ↔ a ⊆ ff b

[Iocta]

ok changed the notation, not seeing much difference tho

[Iocta]

use doesn't even work here?

import tactic
import order.galois_connection

open set order classical

/-

For any set $X$ let $P X$ be the power set of set, namely the set of all subsets of $X$. It's easy to see that the subset relation $\subseteq$ makes $P X$ into a poset. Suppose we have any function between sets $ f: X \rightarrow Y $.
This gives a function $ f_{!}: P X \rightarrow P Y $
sending each subset $S \subseteq X$ to its image under $f : f_{!}(S)=\{y \in Y: y=f(x) \text { for some } x \in S\} $.
-/


variables X Y : Type
variables (f: X → Y)
variables (ff : set X → set Y)



/-
Puzzle 19. Does f! always have a right adjoint? If so, describe it. If not, give an example where it doesn't, and some conditions under which it does have a right adjoint.
-/
example : ∃ (gg : set Y → set X), galois_connection gg ff :=
begin
  unfold galois_connection,
  simp only [le_eq_subset],
  use _,
end
failed to instantiate goal with 6._.6
state:
X Y : Type,
ff : set X → set Y
⊢ ∃ (gg : set Y → set X), ∀ (a : set Y) (b : set X), gg a ⊆ b ↔ a ⊆ ff b

[Eric Wieser]

Your example says "do all functions called ff have a right adjoint" not what you claim it says in the comment

[Iocta]

I think I can state it now, but stuck on a next step.

import tactic
import order.galois_connection

open set order classical

/-

For any set $X$ let $P X$ be the power set of set, namely the set of all subsets of $X$. It's easy to see that the subset relation $\subseteq$ makes $P X$ into a poset. Suppose we have any function between sets $ f: X \rightarrow Y $.
This gives a function $ f_{!}: P X \rightarrow P Y $
sending each subset $S \subseteq X$ to its image under $f : f_{!}(S)=\{y \in Y: y=f(x) \text { for some } x \in S\} $.
-/


variables {X Y : Type }
variables (f: X → Y)


/-
Puzzle 17. Show that $f_{!}: P X \rightarrow P Y$ is a monotone function.
-/
example
(f: X → Y)
(fs : set X → set Y) (hf': ∀ s : set X, fs s = {y : Y | ∃ x ∈ s, f x = y})
(s s' : set X) (hs : s ⊆ s') :
fs s ⊆ fs s' :=
begin
  intros y hy,
  simp only [*, exists_prop, mem_set_of_eq] at *,
  cases hy with x hx,
  use x,
  split,
  { apply hs, exact hx.1, },
  { exact hx.2, },
end




def fs  (xs: set X) : set Y := { (f x) | x ∈ xs }



/-
Puzzle 19. Does f! always have a right adjoint? If so, describe it. If not, give an example where it doesn't, and some conditions under which it does have a right adjoint.
-/
example : ∃ (gs : set Y → set X), galois_connection gs (fs f) :=
begin
use (λys, {x | f x ∈ ys}),
unfold galois_connection,
intros ys xs,
split,
simp only [le_eq_subset],
{
  intro h,
--   XY: Type
-- f: X → Y
-- ys: set Y
-- xs: set X
-- h: {x : X | f x ∈ ys} ⊆ xs
-- ⊢ ys ⊆ fs f xs
  sorry,
},
{
  intro h,
  simp only [le_eq_subset],
--  XY: Type
-- f: X → Y
-- ys: set Y
-- xs: set X
-- h: ys ≤ fs f xs
-- ⊢ {x : X | f x ∈ ys} ⊆ xs
 sorry,
},
end

[Kevin Buzzard]

This looks promising now -- your fs is taking f as an input so it depends on f. The definition of A \subseteq B is \forall x, X in A implies x in B so you can make progress with intro y or intro x (choose an appropriate variable name)

[Iocta]

I'm starting to doubt that either of these conclusions is true. It seems like the first requires f to be onto and the second requires f to be injective. Does that sound right?

import tactic
import order.galois_connection

open set order classical

/-

For any set $X$ let $P X$ be the power set of set, namely the set of all subsets of $X$. It's easy to see that the subset relation $\subseteq$ makes $P X$ into a poset. Suppose we have any function between sets $ f: X \rightarrow Y $.
This gives a function $ f_{!}: P X \rightarrow P Y $
sending each subset $S \subseteq X$ to its image under $f : f_{!}(S)=\{y \in Y: y=f(x) \text { for some } x \in S\} $.
-/


variables {X Y : Type }
variables (f: X → Y)


/-
Puzzle 17. Show that $f_{!}: P X \rightarrow P Y$ is a monotone function.
-/
example
(f: X → Y)
(fs : set X → set Y) (hf': ∀ s : set X, fs s = {y : Y | ∃ x ∈ s, f x = y})
(s s' : set X) (hs : s ⊆ s') :
fs s ⊆ fs s' :=
begin
  intros y hy,
  simp only [*, exists_prop, mem_set_of_eq] at *,
  cases hy with x hx,
  use x,
  split,
  { apply hs, exact hx.1, },
  { exact hx.2, },
end




def fs  (xs: set X) : set Y := { (f x) | x ∈ xs }



/-
Puzzle 19. Does f! always have a right adjoint? If so, describe it. If not, give an example where it doesn't, and some conditions under which it does have a right adjoint.
-/
example : ∃ (gs : set Y → set X), galois_connection gs (fs f) :=
begin
use (λys, {x | f x ∈ ys}),
unfold galois_connection,
intros ys xs,
split,
simp only [le_eq_subset],
{
  intro h,
  intros y hy,
  -- This doesn't seem doable because it would rely on f being onto.
-- X Y: Type
-- f: X → Y
-- ys: set Y
-- xs: set X
-- h: {x : X | f x ∈ ys} ⊆ xs
-- y: Y
-- hy: y ∈ ys
-- ⊢ y ∈ fs f xs
  sorry,
},
{
  intro h,
  simp only [le_eq_subset] at *,
  intros x hx,
  have hx': x ∈  {x' : X | f x' ∈ fs f xs},
  from by {
    have hfx: f x ∈ ys, from by apply hx,
    have hfs: f x ∈ fs f xs, from @h (f x) hfx,
    simp only [mem_set_of_eq],
    exact hfs,
  },
  sorry,
-- X Y: Type
-- f: X → Y
-- ys: set Y
-- xs: set X
-- h: ys ⊆ fs f xs
-- x: X
-- hx: x ∈ {x : X | f x ∈ ys}
-- hx': x ∈ {x' : X | f x' ∈ fs f xs}
-- ⊢ x ∈ xs
},
end

[Kevin Buzzard]

If you're not sure about the maths then you should work out a paper proof first. I can genuinely never remember which one is a left adjoint and which is a right adjoint so I don't want to speculate on the answer to puzzle 19 :-)

[Kevin Buzzard]

Of course, if your proof doesn't work but you have got the adjointness the right way around, this might mean you've chosen the wrong definition of g

[Kevin Buzzard]

In this case you might have to find some results of the form "every function with a right adjoint has property X"' and show that $f_!$ does not have property X in order to solve the puzzle completely. I'll be the first to admit that I can't think of any other possibility for $g$ but of course this isn't a proof that no $g$ exists

[Kevin Buzzard]

I'm pretty sure f_! and g are adjoints by the way -- can you prove they're adjoints the other way around? The relation isn't symmetric and this is what always gets me

[Iocta]

I'm still trying to interpret this but Baez has a mnemonic for left/right:

So, while f has no inverse, it has two "approximate inverses". The left adjoint comes as close as possible to the (perhaps nonexistent) correct answer while making sure to never choose a number that's too small. The right adjoint comes as close as possible while making sure to never choose a number that's too big.

The two adjoints represent two opposing philosophies of life: make sure you never ask for too little and make sure you never ask for too much. This is why they're philosophically profound. But the great thing is that they are defined in a completely precise, systematic way that applies to a huge number of situations!

If you need a mnemonic to remember which is which, remember left adjoints are "left-wing" or "liberal" or "generous", while right adjoints are "right-wing" or "conservative" or "cautious".

[Iocta]

Switching the arguments worked. I think this is a right adjoint because it's on the right-hand side of the $\le$ in $l (a) ≤ b ↔ a ≤ u(b)$.

import tactic
import order.galois_connection

open set order classical

/-

For any set $X$ let $P X$ be the power set of set, namely the set of all subsets of $X$. It's easy to see that the subset relation $\subseteq$ makes $P X$ into a poset. Suppose we have any function between sets $ f: X \rightarrow Y $.
This gives a function $ f_{!}: P X \rightarrow P Y $
sending each subset $S \subseteq X$ to its image under $f : f_{!}(S)=\{y \in Y: y=f(x) \text { for some } x \in S\} $.
-/


variables {X Y : Type }
variables (f: X → Y)





def fs  (xs: set X) : set Y := { (f x) | x ∈ xs }



/-
Puzzle 19. Does f! always have a right adjoint? If so, describe it. If not, give an example where it doesn't, and some conditions under which it does have a right adjoint.
-/
example : ∃ (gs : set Y → set X), galois_connection (fs f) gs  :=
begin
use (λys, {x | f x ∈ ys}),
unfold galois_connection,
intros xs ys, split,
simp only [le_eq_subset] at *,
{
  intro h,
  intros x hx,
  apply h,
  have: f x ∈ f '' xs, from mem_image_of_mem f hx,
  unfold fs,
  unfold image at this,
  simp only [*, exists_prop] at *,
},
{
  intro h,
  simp only [le_eq_subset] at *,
  intros y hy,
  have yim: y ∈ f '' xs, from by {
    unfold image at *,
    unfold fs at *,
    simp only [*, exists_prop] at *,
  },
  have fim: f '' xs ⊆ f '' { x : X | f x ∈ ys}, by {
    intros y' hy',
    unfold image at *,
    unfold fs at *,
    simp * at *,
    cases hy' with x hx,
    use x,
    split,
    { apply h, exact hx.1, },
    {exact hx.2,},
  },
  have: y ∈ f '' {x : X | f x ∈ ys}, from @fim y yim,
  unfold image at *,
  simp only [*, and_imp, set_of_subset_set_of, mem_set_of_eq, forall_apply_eq_imp_iff₂, exists_imp_distrib] at *,
  cases this with x hx,
  cases hx,
  exact mem_of_eq_of_mem (eq.symm hx_right) hx_left,
}
end

[Iocta]

any obvious places to shrink that code?

[Kevin Buzzard]

My guess is that everything can be shrunk to a couple of lines and even done in term mode

[Kevin Buzzard]

You might want to start by looking at simp * at * and finding out what it actually is doing, eg by using squeeze_simp. It might just be doing some trivial rewrite

[Kevin Buzzard]

If you are happy to abuse definitional equality then probably most of the unfolds can go. You might find that a lot of rewrites are definitional in which case they can go too. The shorter the code gets, the more readability you sacrifice

[Eric Wieser]

Rewriting {f x | x \in s} as f '' s and similar should help make the proof shorter

[Iocta]

Why does it need the lambda?

example : ∃ (gs : set Y → set X), galois_connection (fs f) gs  :=
⟨λys, f⁻¹' ys, _⟩ -- ok

example : ∃ (gs : set Y → set X), galois_connection (fs f) gs  :=
⟨f⁻¹', _⟩ --invalid expression

[Ruben Van de Velde]

⁻¹' is an infix notation, so it needs an argument on either side

[Yaël Dillies]

Actually, couldn't we define it as the function it really is?

[Eric Wieser]

((⁻¹') f) should work

[Kevin Buzzard]

If you want to take this further, you can define a filter on a type, define how to push them forward and pull them back along morphisms of types, and show that these concepts also form a Galois connection, and then you can define the function from subsets to filters (the principal filter) and maybe the function "intersection of all sets in the filter" from filters to subsets(?) and then perhaps show that there is some sort of Galois insertion between these two ideas (although I've never checked this so I might be wrong).

[Iocta]

Got it cut down

example : ∃ (gs : set Y → set X), galois_connection (image f) gs  :=
⟨(⁻¹') f, λxs ys, image_subset_iff⟩

[Eric Wieser]

At this point you may as well eliminate the existential

[Eric Wieser]

example : galois_connection (image f) ((⁻¹') f) := λxs ys, image_subset_iff

[Eric Wieser]

I'd hope library_search can find that we have that exact statement already

[Iocta]

it finds set.image_preimage

[Iocta]

dropping the \exists is like saying "there's only one"?

[Eric Wieser]

Nope, it's just saying "I can tell you a specific GS, not just that one exists"

[Iocta]

Is this not what I mean?

import tactic
import order.galois_connection

open set order classical

noncomputable theory

/-

For any set $X$ let $P X$ be the power set of set, namely the set of all subsets of $X$. It's easy to see that the subset relation $\subseteq$ makes $P X$ into a poset. Suppose we have any function between sets $ f: X \rightarrow Y $.
This gives a function $ f_{!}: P X \rightarrow P Y $
sending each subset $S \subseteq X$ to its image under $f : f_{!}(S)=\{y \in Y: y=f(x) \text { for some } x \in S\} $.
-/


variables {X Y : Type }

/-
Puzzle 18. Does $f_!$ always have a left adjoint? If so, describe it. If not, give an example where it doesn't, and some conditions under which it does have a left adjoint.
-/
example : !∀ (h : X → Y), ∃(gs : set Y → set X), galois_connection gs (('') h) := sorry

failed to synthesize type class instance for
X Y : Type
⊢ decidable (∀ (h : X → Y), ∃ (gs : set Y → set X), galois_connection gs (image h))

[Floris van Doorn]

Remove the !, it is interpreted as boolean negation.

[Floris van Doorn]

use \neg for negation