Skip to content 
import GlimpseOfLean.Library.Basic

open PiNotation

Abstract non-sense 101: Galois adjunctions

In this file we will play with the simplest examples of adjunctions: Galois connections between complete lattices. There is a lot about this topic in Mathlib, the mathematical library of Lean, but here we will roll our own version for practice. This file builds the fundamental theory of these objects and each lemma you prove in this file is named and can be reused to prove the next lemmas.

namespace Tutorial

section InfSup
variable [PartialOrder X]

In this section, X is a type equipped with a partial order relation. So you have access to lemmas: * le_rfl {a : X} : a ≤ a * le_trans {a b c : X} (h : a ≤ b) (h' : b ≤ c) : a ≤ c * le_antisymm {a b : X} (h : a ≤ b) (h' : b ≤ a) : a = b

Curly braces around arguments mean these arguments are implicit, so Lean will never require them, because they can certainly be inferred from context; in particular, when applying a lemma that contains variables in curly braces, you should not provide the corresponding values.

We will also use the definition of the set of lower bounds of a set s

lowerBounds s = {x | ∀ a ∈ s, x ≤ a}

and similarly

upperBounds s = {x | ∀ a ∈ s, a ≤ x}

  • An element x₀ is an infimum of a set s in X if every element of X is a lower bound of s if and only if it is below x₀.
def isInf (s : Set X) (x₀ : X) :=
  ∀ x, x ∈ lowerBounds s ↔ x ≤ x₀

lemma isInf.lowerBound {s : Set X} {x₀ : X} (h : isInf s x₀) : x₀ ∈ lowerBounds s := by
  -- sorry
  rw [h]
  -- Slower alternative:
  -- specialize h x₀
  -- apply h.2
  -- apply le_rfl
  -- sorry
  • A set has at most one infimum.
def isInf.eq {s : Set X} {x₀ x₁ : X} (hx₀ : isInf s x₀) (hx₁ : isInf s x₁) : x₀ = x₁ := by
  -- sorry
  apply le_antisymm
  · exact (hx₁ x₀).1 (isInf.lowerBound hx₀)
    -- Slower alternative:
    -- apply (hx₁ x₀).1
    -- apply isInf.lowerBound hx₀
  · exact (hx₀ x₁).1 (isInf.lowerBound hx₁)
  -- sorry
  • An element x₀ is a supremum of a set s in X if every element of X is a lower bound of s if and only if it below x₀.
def isSup (s : Set X) (x₀ : X) :=
  ∀ x, x ∈ upperBounds s ↔ x₀ ≤ x

The next lemma is proven by applying isInf.lowerBound to X equipped with the opposite order relation. You don't need to understand precisely how this is achieved since all proofs using this trick will be offered.

lemma isSup.upperBound {s : Set X} {x₀ : X} (h : isSup s x₀) : x₀ ∈ upperBounds s :=
  isInf.lowerBound (X := OrderDual X) h
  • A set has at most one supremum.
lemma isSup.eq {s : Set X} {x₀ x₁ : X} (hx₀ : isSup s x₀) (hx₁ : isSup s x₁) : x₀ = x₁ :=
  isInf.eq (X := OrderDual X) hx₀ hx₁
  • A function from Set X to X is an infimum function if it sends every set to an infimum of this set.
def isInfFun (I : Set X → X) :=
  ∀ s : Set X, isInf s (I s)
  • A function from Set X to X is an supremum function if it sends every set to a supremum of this set.
def isSupFun (S : Set X → X) :=
  ∀ s : Set X, isSup s (S s)

The next lemma is the first crucial result in this file. If X admits an infimum function then it automatically admits a supremum function.

lemma isSup_of_isInf {I : Set X → X} (h : isInfFun I) : isSupFun (fun s ↦ I (upperBounds s)) := by
  -- sorry
  intro s x
  constructor
  · intro hx
    exact (h _).lowerBound hx
  · intros hx y hy
    calc
      y ≤ I (upperBounds s) := (h _ y).mp (fun z hz ↦ hz hy)
      _ ≤ x                 := hx
  -- sorry

Of course we also have the dual result constructing an infimum function from a supremum one.

lemma isInf_of_isSup {S : Set X → X} (h : isSupFun S) : isInfFun (fun s ↦ S (lowerBounds s)) :=
  isSup_of_isInf (X := OrderDual X) h

We are now ready for the first main definition of this file: complete lattices.

  • A complete lattice is a type equipped with a partial order, an infimum function and a supremum function. For instance X = Set Y equipped with the inclusion order, the intersection function and the union function is a complete lattice. I particular, the word “lattice” here has nothing to do with lattices as discrete subgroups in Euclidean spaces.
class CompleteLattice (X : Type) [PartialOrder X] where
  I : Set X → X
  I_isInf : isInfFun I
  S : Set X → X
  S_isSup : isSupFun S
  • Turning a complete lattice X into the dual one. Lean will automatically pickup this construction when using the OrderDual trick as above.
instance (X : Type) [PartialOrder X] [CompleteLattice X] : CompleteLattice (OrderDual X) where
  I := CompleteLattice.S (X := X)
  I_isInf := CompleteLattice.S_isSup (X := X)
  S := CompleteLattice.I (X := X)
  S_isSup := CompleteLattice.I_isInf (X := X)

We can now use the first main result above to build a complete lattice from either an infimum or a supremum function on a partially ordered type.

  • Building a complete lattice structure from an infimum function on a partially ordered type.
def CompleteLattice.mk_of_Inf {I : Set X → X} (h : isInfFun I) : CompleteLattice X where
 I := I
 I_isInf := h
 S := fun s ↦ I (upperBounds s)
 S_isSup := isSup_of_isInf h
  • Building a complete lattice structure from a supremum function on a partially ordered type.
def CompleteLattice.mk_of_Sup {S : Set X → X} (h : isSupFun S) : CompleteLattice X where
 I := fun s ↦ S (lowerBounds s)
 I_isInf := isInf_of_isSup h
 S := S
 S_isSup := h

Until the end of this section, X will be a complete lattice.

variable [CompleteLattice X]
  • The infimum function on a complete lattice.
notation "Inf" => CompleteLattice.I
  • The supremum function on a complete lattice.
notation "Sup" => CompleteLattice.S

We now restate a couple of lemmas proven above in terms of complete lattices.

lemma lowerBound_Inf (s : Set X) : Inf s ∈ lowerBounds s :=
  (CompleteLattice.I_isInf _).lowerBound

lemma upperBound_Sup (s : Set X) : Sup s ∈ upperBounds s :=
  (CompleteLattice.S_isSup _).upperBound

We now prove a series of lemmas asserting that Inf (and then Sup by duality) behave according to your intuition. You should feel free to skip those and jump to the adjunction section if you think you would be able to prove them and you want to see more interesting things.

In the first lemma below, you will probably want to use lowerBounds_mono_set ⦃s t : Set α⦄ (hst : s ⊆ t) : lowerBounds t ⊆ lowerBounds s or reprove it as part of your proof.

lemma Inf_pair {x x' : X} : x ≤ x' ↔ Inf {x, x'} = x := by
  -- sorry
  constructor
  · intro h
    apply (CompleteLattice.I_isInf _).eq
    intro z
    constructor
    · intro hz
      apply hz
      simp
    · intro hz
      simp
      constructor
      · apply hz
      · calc z ≤ x  := by apply hz -- or simply `:= hz`
             _ ≤ x' := by apply h -- or simply `:= h`
  · intro h
    calc
      x = Inf {x, x'} := by rw [h]
      _ ≤ x' := by apply lowerBound_Inf; simp
  -- sorry

lemma Sup_pair {x x' : X} : x ≤ x' ↔ Sup {x, x'} = x' := by
  rw [Set.pair_comm x x']
  exact Inf_pair (X := OrderDual X)

Let us prove that Set forms a complete lattice.

lemma isInfInter {Y : Type} (S : Set (Set Y)) : isInf S (⋂₀ S) := by
  -- sorry
  intro t
  constructor
  · intro ht x hx u hu
    exact ht hu hx
  · intro ht u hu x hx
    exact ht hx _ hu
  -- sorry

lemma isSupUnion {Y : Type} (S : Set (Set Y)) : isSup S (⋃₀ S) := by
  -- sorry
  intro t
  constructor
  · intro ht x hx
    rcases hx with ⟨s, hs, hx⟩
    exact ht hs hx
  · intro ht u hu x hx
    apply ht
    use u
  -- sorry

instance {Y : Type} : CompleteLattice (Set Y) where
  I := Set.sInter
  I_isInf := fun S ↦ isInfInter S
  S := Set.sUnion
  S_isSup := fun S ↦ isSupUnion S

end InfSup

section Adjunction

We are now ready for the second central definition of this file: adjunctions between ordered types.

  • A pair of functions l and r between ordered types are adjoint if ∀ x y, l x ≤ y ↔ x ≤ r y. One also says they form a Galois connection. Here l stands for "left" and r stands for "right".
def adjunction [PartialOrder X] [PartialOrder Y] (l : X → Y) (r : Y → X) :=
  ∀ x y, l x ≤ y ↔ x ≤ r y

The example you need to keep in mind is the adjunction between direct image and inverse image. Given f : α → β, we have: * Set.image f : Set α → Set β with notation f '' * Set.preimage f : Set β → Set α with notation f ⁻¹'

lemma image_preimage_adjunction {α β : Type} (f : α → β) :
    adjunction (Set.image f) (Set.preimage f) := by
  intros s t
  exact Set.image_subset_iff

lemma adjunction.dual [PartialOrder X] [PartialOrder Y] {l : X → Y} {r : Y → X}
    (h : adjunction l r) :
    adjunction (X := OrderDual Y) (Y := OrderDual X) r l := by
  -- sorry
  intros y x
  constructor
  exact (h x y).2
  exact (h x y).1
  -- sorry

In the remaining of the section, X and Y are complete lattices.

variable [PartialOrder X] [CompleteLattice X] [PartialOrder Y] [CompleteLattice Y]

We now come to the second main theorem of this file: the adjoint functor theorem for complete lattices. This theorem says that a function between complete lattices is a left adjoint (resp. right adjoint) if and only if it commutes with Sup (resp. with Inf).

We first define the candidate right adjoint (without making any assumption on the original map).

  • Constructs a candidate right adjoint for a map between complete lattices. This is an actual adjoint if the map commutes with Sup, see adjunction_of_Sup.
def mk_right (l : X → Y) : Y → X := fun y ↦ Sup {x | l x ≤ y}

The proof of the theorem below isn't long but it isn't completely obvious either. First you need to understand the notations in the statement. l '' s is the direct image of s under l. This '' is notation for Set.image. Putting your cursor on this notation and using the contextual menu to "jump to definition" will bring you to the file defining Set.image and containing lots of lemmas about it. The ones that are used in the reference solutions are

  • Set.image_pair : (f : α → β) (a b : α) : f '' {a, b} = {f a, f b}
  • Set.image_preimage_subset (f : α → β) (s : Set β) : f '' (f ⁻¹' s) ⊆ s

Proof hint: one direction is easy and doesn't use the crucial assumption. For the other direction, you should probably first prove that Monotone l, ie ∀ ⦃a b⦄, a ≤ b → l a ≤ l b, and then prove that, for every y, Sup (l '' { x | l x ≤ y }) ≤ y.

theorem adjunction_of_Sup {l : X → Y} (h : ∀ s : Set X, l (Sup s) = Sup (l '' s)) :
    adjunction l (mk_right l) := by
  -- sorry
  intro x y
  constructor
  · intro h'
    exact (CompleteLattice.S_isSup {x | l x ≤ y}).upperBound h'
  · intro h'
    have l_mono : Monotone l := by
      intro a b hab
      have := h {a, b}
      rw [Sup_pair.1 hab, Set.image_pair] at this
      exact Sup_pair.2 this.symm
    have Sup_le_y : Sup (l '' { x | l x ≤ y }) ≤ y := by
      apply (CompleteLattice.S_isSup (l '' { x | l x ≤ y }) y).1
      intro y' hy'
      rcases hy' with ⟨x, hx, hxy'⟩
      rw [← hxy']
      apply hx
    calc
      l x ≤ l (mk_right l y) := l_mono h'
      _   = Sup (l '' { x | l x ≤ y }) := h {x | l x ≤ y}
      _   ≤ y := Sup_le_y
  -- sorry

Of course we can play the same game to construct left adjoints.

  • Constructs a candidate left adjoint for a map between complete lattices. This is an actual adjoint if the map commutes with Inf, see adjunction_of_Inf.
def mk_left (r : Y → X) : X → Y := fun x ↦ Inf {y | x ≤ r y}

theorem adjunction_of_Inf {r : Y → X} (h : ∀ s : Set Y, r (Inf s) = Inf (r '' s)) :
    adjunction (mk_left r) r :=
  fun x y ↦ (adjunction_of_Sup (X := OrderDual Y) (Y := OrderDual X) h y x).symm

end Adjunction

section Topology

In this section we apply the theory developed above to point-set topology. Our first goal is to endow the type Topology X of topologies on a given type with a complete lattice structure. We then turn any map f : X → Y into an adjunction (f⁎, f ^*) between Topology X and Topology Y and use it to build the product topology. Of course mathlib knows all this, but we'll continue to build our own theory.

@[ext]
structure Topology (X : Type) where
  isOpen : Set X → Prop
  isOpen_iUnion : ∀ {ι : Type}, ∀ {s : ι → Set X}, (∀ i, isOpen (s i)) → isOpen (⋃ i, s i)
  isOpen_iInter : ∀ {ι : Type}, ∀ {s : ι → Set X}, (∀ i, isOpen (s i)) → Finite ι → isOpen (⋂ i, s i)

Let's run two quick sanity checks on our definition since so many textbooks include redundant conditions it the definition of topological spaces.

lemma isOpen_empty (T : Topology X) : T.isOpen ∅ := by
  have : (∅ : Set X) = ⋃ i : Empty, i.rec := by
    rw [Set.iUnion_of_empty]
  rw [this]
  exact T.isOpen_iUnion Empty.rec

lemma isOpen_univ (T : Topology X) : T.isOpen Set.univ := by
  have : (Set.univ : Set X) = ⋂ i : Empty, i.rec := by
    rw [Set.iInter_of_empty]
  rw [this]
  exact T.isOpen_iInter  Empty.rec (Finite.of_fintype Empty)

The ext attribute on the definition of Topology tells Lean to automatically build the following extensionality lemma: Topology.ext_iff (T T' : Topology X), T = T' ↔ x.isOpen = y.isOpen and it also registers this lemma for use by the ext tactic (we will come back to this below).

  • We order Topology X using the order dual to the order induced by Set (Set X). There are good reasons for this choice but they are beyond the scope of this tutorial.
instance : PartialOrder (Topology X) :=
PartialOrder.lift (β := OrderDual $ Set (Set X)) Topology.isOpen (fun _ _ ↦ (Topology.ext_iff).2)
  • The supremum function on Topology X.
def SupTop (s : Set (Topology X)) : Topology X where
  isOpen := fun V ↦ ∀ T ∈ s, T.isOpen V
  isOpen_iUnion := by
    intros ι t ht a ha
    exact a.isOpen_iUnion fun i ↦ ht i a ha

  isOpen_iInter := by
    intros ι t ht hι a ha
    exact a.isOpen_iInter (fun i ↦ ht i a ha) hι

Because the supremum function above comes from the supremum function of OrderDual (Set (Set X)), it is indeed a supremum function. We could state an abstract lemma saying that, but here a direct proof is just as easy and a lot of fun.

lemma isSup_SupTop : isSupFun (SupTop : Set (Topology X) → Topology X) :=
fun _ _ ↦ ⟨fun hT _ hV _ hs ↦ hT hs hV, fun hT T' hT' _ hV ↦ hT hV T' hT'⟩

We can use our abstract theory to get an infimum function for free, hence a complete lattice structure on Topology X. Note that our abstract theory is indeed doing non-trivial work: the infimum function does not come from OrderDual (Set (Set X)).

instance : CompleteLattice (Topology X) := CompleteLattice.mk_of_Sup isSup_SupTop

Let us restate in complete lattice notation what our construction of Sup was. The proof is simply saying "this is true by definition".

lemma isOpen_Sup {s : Set (Topology X)} {V : Set X} : (Sup s).isOpen V ↔ ∀ T ∈ s, T.isOpen V :=
  Iff.rfl

We now start building our adjunction between Topology X and Topology Y induced by any map f : X → Y. We will build the left adjoint by hand and then invoke our adjoint functor theorem.

def push (f : X → Y) (T : Topology X) : Topology Y where
  isOpen := fun V ↦ T.isOpen (f ⁻¹' V)
  isOpen_iUnion := by
    -- sorry
    intros ι s hs
    rw [Set.preimage_iUnion]
    exact T.isOpen_iUnion hs
    -- sorry

  isOpen_iInter := by
    -- sorry
    intros ι s hs hι
    rw [Set.preimage_iInter]
    exact T.isOpen_iInter hs hι
    -- sorry

postfix:1024 "⁎" => push -- type using `\_*`
  • A map f : X → Y is continuous with respect to topologies T and T' if the preimage of every open set is open.
def Continuous (T : Topology X) (T' : Topology Y) (f : X → Y) :=  f ⁎ T ≤ T'

Let us check the definition is indeed saying what we claimed it says.

example (T : Topology X) (T' : Topology Y) (f : X → Y) :
  Continuous T T' f ↔ ∀ V, T'.isOpen V → T.isOpen (f ⁻¹' V) :=
Iff.rfl

Note how the following proof uses the ext tactic which knows that two topologies are equal iff they have the same open sets thanks to the ext attribute on the definition of Topology.

lemma push_push (f : X → Y) (g : Y →Z) (T : Topology X) :
    g ⁎ (f ⁎ T) = (g ∘ f) ⁎ T := by
  ext V
  exact Iff.rfl

We want a right adjoint for f ⁎ so we need to check it commutes with Sup. You may want to use Set.ball_image_iff : (∀ y ∈ f '' s, p y) ↔ ∀ x ∈ s, p (f x) where "ball" stands for "bounded for all", ie ∀ x ∈ ....

lemma push_Sup (f : X → Y) {t : Set (Topology X)} : f ⁎ (Sup t) = Sup (f ⁎ '' t) := by
  -- sorry
  ext V
  rw [isOpen_Sup, Set.forall_mem_image]
  exact Iff.rfl
  -- sorry

def pull (f : X → Y) (T : Topology Y) : Topology X := mk_right (push f) T

postfix:1024 "^*" => pull

def ProductTopology {ι : Type} {X : ι → Type} (T : Π i, Topology (X i)) : Topology (Π i, X i) :=
Inf (Set.range (fun i ↦ (fun x ↦ x i) ^* (T i)))

lemma ContinuousProductTopIff {ι : Type} {X : ι → Type} (T : Π i, Topology (X i))
  {Z : Type} (TZ : Topology Z) {f : Z → Π i, X i}:
    Continuous TZ (ProductTopology T) f ↔ ∀ i,  Continuous TZ (T i) (fun z ↦ f z i) := by
  -- sorry
  calc
    Continuous TZ (ProductTopology T) f
    _ ↔ f ⁎ TZ ∈ lowerBounds (Set.range (fun i ↦ (fun x ↦ x i) ^* (T i))) := by
          rw [CompleteLattice.I_isInf]
          exact Iff.rfl

    _ ↔ ∀ i, f ⁎ TZ ≤ (fun x ↦ x i) ^* (T i)        := by rw [lowerBounds_range]
    _ ↔ ∀ i, (fun x ↦ x i) ⁎ (f ⁎ TZ) ≤ T i        := by
          apply forall_congr'
          intro i
          rw [pull, ← adjunction_of_Sup (fun s ↦ push_Sup _), push_push]

    _ ↔ ∀ i,  Continuous TZ (T i) (fun z ↦ f z i)  := Iff.rfl

unfold Continuous ProductTopology rw [← CompleteLattice.I_isInf, lowerBounds_range] apply forall_congr' intro i unfold pull rw [← adjunction_of_Sup (fun s ↦ push_Sup _), push_push] rfl

  -- sorry

end Topology

namespace Subgroups

@[ext]
structure Subgroup (G : Type) [Group G] where
  carrier : Set G
  one_mem : 1 ∈ carrier
  mul_mem : ∀ ⦃x y : G⦄, x ∈ carrier → y ∈ carrier → x*y ∈ carrier
  inv_mem : ∀ ⦃x : G⦄, x ∈ carrier → x⁻¹ ∈ carrier

instance [Group G] : Membership G (Subgroup G) := ⟨fun H x ↦ x ∈ H.carrier⟩

variable {G : Type} [Group G]

instance : PartialOrder (Subgroup G) :=
  PartialOrder.lift Subgroup.carrier (fun _ _ ↦ (Subgroup.ext_iff).2)

An intersection of subgroups is a subgroup.

def SubgroupInf (s : Set (Subgroup G)) : Subgroup G where
  carrier := ⋂ H ∈ s, H.carrier
  one_mem := by
    -- sorry
    rw [Set.mem_iInter₂]
    intro H _
    exact H.one_mem
    -- sorry

  mul_mem := by
    -- sorry
    intro x y hx hy
    rw [Set.mem_iInter₂] at hx hy ⊢
    intro H hH
    exact H.mul_mem (hx H hH) (hy H hH)
    -- sorry

  inv_mem := by
    -- sorry
    intro x hx
    rw [Set.mem_iInter₂] at hx ⊢
    intro H hH
    exact H.inv_mem (hx H hH)
    -- sorry


lemma SubgroupInf_carrier (s : Set (Subgroup G)) :
  (SubgroupInf s).carrier = ⋂₀ (Subgroup.carrier '' s) :=
by simp [SubgroupInf]
-- omit

lemma isInf.lift [PartialOrder X] {f : Y → X} (hf : Function.Injective f) {s : Set Y} {y : Y}
  (hy : isInf (f '' s) (f y)) : @isInf Y (PartialOrder.lift f hf) s y := by
  intro y'
  erw [← hy (f y')]
  constructor
  · intro hy' x hx
    rcases hx with ⟨y'', hy'', H⟩
    rw [← H]
    exact hy' hy''
  · intro hy' y'' hy''
    apply hy'
    exact Set.mem_image_of_mem f hy''

-- omit
lemma SubgroupInf_is_Inf : isInfFun (SubgroupInf : Set (Subgroup G) → Subgroup G) := by
  -- sorry
  intro s H
  apply isInf.lift (fun _ _ ↦ (Subgroup.ext_iff).2)
  rw [SubgroupInf_carrier]
  apply isInfInter
  -- sorry

instance : CompleteLattice (Subgroup G) := CompleteLattice.mk_of_Inf SubgroupInf_is_Inf

lemma Inf_carrier (s : Set (Subgroup G)) : (Inf s).carrier = ⋂₀ (Subgroup.carrier '' s) :=
  SubgroupInf_carrier s

def forget (H : Subgroup G) : Set G := H.carrier

def generate : Set G → Subgroup G := mk_left forget

lemma generate_forget_adjunction : adjunction (generate : Set G → Subgroup G) forget := by
  -- sorry
  exact adjunction_of_Inf SubgroupInf_carrier
  -- sorry

variable {G' : Type} [Group G']

def pull (f : G →* G') (H' : Subgroup G') : Subgroup G where
  carrier := f ⁻¹' H'.carrier
  one_mem := by
    -- sorry
    show f 1 ∈ H'
    rw [f.map_one]
    exact H'.one_mem
    -- sorry

  mul_mem := by
    -- sorry
    intro x y hx hy
    show f (x*y) ∈ H'
    rw [f.map_mul]
    exact H'.mul_mem hx hy
    -- sorry

  inv_mem := by
    -- sorry
    intro x hx
    show f x⁻¹ ∈ H'
    rw [f.map_inv]
    exact H'.inv_mem hx
    -- sorry


lemma pull_carrier (f : G →* G') (H' : Subgroup G') : (pull f H').carrier = f ⁻¹' H'.carrier :=
  rfl

Let's be really lazy and define subgroup push-forward by adjunction.

def push (f : G →* G') : Subgroup G → Subgroup G' := mk_left (pull f)

lemma push_pull_adjunction (f : G →* G') : adjunction (push f) (pull f) := by
  -- sorry
  apply adjunction_of_Inf
  intro S
  ext x
  simp [Inf_carrier, Set.image_image, pull, Set.preimage_iInter]
  -- sorry

end Subgroups

section

Our next concrete target is push_generate (f : G →* G') (S : Set G) : push f (generate S) = generate (f '' S)

which will require a couple more abstract lemmas.

variable {X : Type} [PartialOrder X]
         {Y : Type} [PartialOrder Y]

lemma unique_left {l l' : X → Y} {r : Y → X} (h : adjunction l r) (h' : adjunction l' r) :
    l = l' := by
  -- sorry
  ext x
  apply le_antisymm
  · rw [h, ← h']
  · rw [h', ← h]
  -- sorry

lemma unique_right {l : X → Y} {r r' : Y → X} (h : adjunction l r) (h' : adjunction l r') :
    r = r' := by
  -- sorry
  exact (unique_left h'.dual h.dual).symm
  -- sorry

variable {Z : Type} [PartialOrder Z]

lemma adjunction.compose {l : X → Y} {r : Y → X} (h : adjunction l r)
  {l' : Y → Z} {r' : Z → Y} (h' : adjunction l' r') : adjunction (l' ∘ l) (r ∘ r') := by
  -- sorry
  intro x z
  rw [Function.comp_apply, h', h]
  rfl
  -- sorry

-- omit
lemma left_comm_of_right_comm {W : Type} [PartialOrder W] [CompleteLattice W]
    {lYX : X → Y} {uXY : Y → X} (hXY : adjunction lYX uXY)
    {lWZ : Z → W} {uZW : W → Z} (hZW : adjunction lWZ uZW)
    {lWY : Y → W} {uYW : W → Y} (hWY : adjunction lWY uYW)
    {lZX : X → Z} {uXZ : Z → X} (hXZ : adjunction lZX uXZ)
    (h : uXZ ∘ uZW = uXY ∘ uYW) : lWZ ∘ lZX = lWY ∘ lYX := by
  have A₁ := hXZ.compose hZW
  rw [h] at A₁
  exact unique_left A₁ (hXY.compose hWY)
-- omit

end

namespace Subgroups
variable {G : Type} [Group G] {G' : Type} [Group G']

As a last challenge, we propose the following lemma.

  • The image under a group morphism of the subgroup generated by some set S is generated by the image of S.
lemma push_generate (f : G →* G') : push f ∘ generate = generate ∘ (Set.image f) := by
  -- sorry
  apply left_comm_of_right_comm
  apply image_preimage_adjunction
  apply push_pull_adjunction
  apply generate_forget_adjunction
  apply generate_forget_adjunction
  ext H
  exact Iff.rfl
  -- sorry

end Subgroups
end Tutorial