(l₁ S).map σ ≤ l₂ (S.map ⇑σ)

Stream: Is there code for X?

[Kevin Buzzard]

Much to my annoyance I'm stuck on both of these, although I can prove that each implies the other.

import field_theory.galois
import topology.algebra.filter_basis

lemma foo {K L : Type*} [field K] [field L] [algebra K L]
  (S : set L) {M : Type*} [field M] [algebra K M] (σ : L →ₐ[K] M) :
(intermediate_field.adjoin K S).map σ ≤
intermediate_field.adjoin K (σ '' S) := sorry -- they're equal but I can do ≥

lemma foo2 {K L : Type*} [field K] [field L] [algebra K L]
  (S : set L) {M : Type*} [field M] [algebra K M] (σ : L →ₐ[K] M) :
  ∀ (F : intermediate_field K M),
  σ '' S ⊆ F → (intermediate_field.adjoin K S).map σ ≤ F := sorry -- this is
  -- an iff but the other way is easy

  -- Note we have `intermediate_field.gi`

The Galois insertion info:

  -- α is set L or set M
  -- β is intermediate_field L or intermediate_field M
  -- l is `adjoin K`
  -- u is `coe`

I don't know if there's a general statement about Galois insertions. Here there are two involved.

[Andrew Yang]

Is docs#intermediate_field.adjoin_map what you are looking for?

[Patrick Massot]

Yes, this is what he is looking for

[Patrick Massot]

But the Galois connection magic he is asking for is also interesting, I think we still miss the relevant lemma.

[Patrick Massot]

@Kevin Buzzard is docs#intermediate_field.map part of a Galois connection?

[Patrick Massot]

@Kevin Buzzard I wrote what I think is a bit of Galois connection magic that mathlib is missing, together with a sample application (I could have used your example if you had answered my previous message).

import group_theory.subgroup.basic


variables
  {X : Type*} [partial_order X] {Y : Type*} [partial_order Y]


lemma galois_connection.eq_l {l : X → Y} {u : Y → X} (h : galois_connection l u) {x : X} {z : Y} :
  l x = z ↔ ∀ y, z ≤ y ↔ x ≤ u y :=
begin
  split,
  { rintros rfl y,
    exact h x y },
  { intros H,
    exact ((h _ _).mpr $ (H z).mp le_rfl).antisymm ((H $ l x).mpr (h.le_u_l x)) }
end

lemma galois_connection.eq_u {l : X → Y} {u : Y → X} (h : galois_connection l u) {z : X} {y : Y} :
  u y  = z ↔ ∀ x, x ≤ z ↔ l x ≤ y :=
begin
  split,
  { rintros rfl x,
    exact (h x y).symm },
  { intros H,
    exact ((H $ u y).mpr (h.l_u_le y)).antisymm ((h _ _).mp $ (H z).mp le_rfl) }
end

variables
  {Z : Type*} [partial_order Z] {W : Type*} [partial_order W]

lemma gc_magic
  {lYX : X → Y} {rXY : Y → X} (hXY : galois_connection lYX rXY)
  {lWZ : Z → W} {rZW : W → Z} (hZW : galois_connection lWZ rZW)
  {lWY : Y → W} {rYW : W → Y} (hWY : galois_connection lWY rYW)
  {lZX : X → Z} {rXZ : Z → X} (hXZ : galois_connection lZX rXZ)
  (h : rXY ∘ rYW = rXZ ∘ rZW) : lWZ ∘ lZX = lWY ∘ lYX :=
begin
  ext x,
  rw hZW.eq_l,
  intros w,
  calc
  lWY (lYX x) ≤ w ↔ lYX x ≤ rYW w : by rw hWY
              ... ↔ x ≤ rXY (rYW w) : by rw ← hXY
              ... ↔ x ≤ rXY (rYW w) : by rw ← hXY
              ... ↔ x ≤ rXZ (rZW w) : by rw show rXY (rYW w) = rXZ (rZW w), from congr_fun h w
              ... ↔ lZX x ≤ rZW w : by rw hXZ
end

open subgroup set

/- We can now reprove: -/
#check @monoid_hom.map_closure

/-- The image by a group morphism of the subgroup generated by a set is the subgroup generated by
the image of this set. -/
example {G H : Type*} [group G] [group H] (f : G →* H) :
  map f ∘ closure = closure ∘ (image f) :=
gc_magic set.image_preimage (gc_map_comap f) (subgroup.gi H).gc (subgroup.gi G).gc rfl

[Patrick Massot]

Note that I don't use galois_connection.eq_u and I was too lazy to derive it using the previous one and order_dual.

[Patrick Massot]

Those lemmas prove that both sides of a Galois adjunction are characterized by their universal property, this bit already seems to be missing. But the part I really like is gc_magic.

[Patrick Massot]

@Yaël Dillies do you know whether this is already somewhere?

[Eric Wieser]

gc_magic looks new to me, I think docs#galois_connection.composw was the only lemma I found about more than one connection

[Yaël Dillies]

If eq_u and eq_l exist, I know where to find them.

[Eric Wieser]

Do they exist as l_eq?

[Patrick Massot]

No.

[Patrick Massot]

And I should indeed rename those lemmas, I switched sides after naming them.

[Yaël Dillies]

What about docs#galois_connection.is_least_l ?

[Patrick Massot]

It should certainly help

[Yaël Dillies]

But indeed those specific lemmas eem to be missing, maybe because you're meant to go through the lemma I just gave + the correct is_least/is_greatest lemma (which don't seem to exist either? :thinking:)

[Patrick Massot]

At least it would help if it had correct binders :angry:

[Patrick Massot]

I don't think the "correct is_least/is_greatest lemma" can exist. Here we also need to use that the set appearing in docs#galois_connection.is_least_l is upward closed.

[Bhavik Mehta]

Here's another way to show gc_magic:

lemma gc_magic
  {lYX : X → Y} {rXY : Y → X} (hXY : galois_connection lYX rXY)
  {lWZ : Z → W} {rZW : W → Z} (hZW : galois_connection lWZ rZW)
  {lWY : Y → W} {rYW : W → Y} (hWY : galois_connection lWY rYW)
  {lZX : X → Z} {rXZ : Z → X} (hXZ : galois_connection lZX rXZ)
  (h : rXY ∘ rYW = rXZ ∘ rZW) : lWZ ∘ lZX = lWY ∘ lYX :=
funext $ λ x, (hXZ.compose hZW).is_least_l.unique (h ▸ (hXY.compose hWY).is_least_l)

[Patrick Massot]

This is nice but less fun in my opinion.

[Bhavik Mehta]

The proofs are ultimately the same; they're both an easy case of a general category theory fact. is_least_l characterises the left side of a Galois connection already.

[Patrick Massot]

Yes, I understand.

[Patrick Massot]

But I like the calc block

[Patrick Massot]

Actually the result is even closer to be already here:

import order.galois_connection


variables
  {X : Type*} [partial_order X] {Y : Type*} [partial_order Y]

variables
  {Z : Type*} [partial_order Z] {W : Type*} [partial_order W]

lemma l_comm_of_u_comm
  {lYX : X → Y} {uXY : Y → X} (hXY : galois_connection lYX uXY)
  {lWZ : Z → W} {uZW : W → Z} (hZW : galois_connection lWZ uZW)
  {lWY : Y → W} {uYW : W → Y} (hWY : galois_connection lWY uYW)
  {lZX : X → Z} {uXZ : Z → X} (hXZ : galois_connection lZX uXZ)
  (h : uXY ∘ uYW = uXZ ∘ uZW) : lWZ ∘ lZX = lWY ∘ lYX :=
funext $ λ x, (hXZ.compose hZW).l_unique (hXY.compose hWY) (λ b, congr_fun h.symm b)

[Patrick Massot]

And if we go for an applied version and commute some equality we get to:

import order.galois_connection


variables
  {X : Type*} [partial_order X] {Y : Type*} [partial_order Y]

variables
  {Z : Type*} [partial_order Z] {W : Type*} [partial_order W]

lemma l_comm_of_u_comm
  {lYX : X → Y} {uXY : Y → X} (hXY : galois_connection lYX uXY)
  {lWZ : Z → W} {uZW : W → Z} (hZW : galois_connection lWZ uZW)
  {lWY : Y → W} {uYW : W → Y} (hWY : galois_connection lWY uYW)
  {lZX : X → Z} {uXZ : Z → X} (hXZ : galois_connection lZX uXZ)
  (h : ∀ w, uXZ (uZW w) = uXY (uYW w)) {x : X} : lWZ (lZX x) = lWY (lYX x) :=
(hXZ.compose hZW).l_unique (hXY.compose hWY) h

[Patrick Massot]

Maybe I'm starting to like that way of telling the story.

[Patrick Massot]

Fun fact: X and Z only need preorders here.

[Patrick Massot]

Clearly I'm having way too much fun with this stuff. I should stop and go to bed.

[Patrick Massot]

#11114. I still kept my le_eq and u_eq lemmas just in case they turn out to be useful for something else. Concerning applications, I only replaced the subgroup proof.

[Kevin Buzzard]

This is really nice. Thanks!