golfing Lawvere's fixed-point theorem

Stream: new members

[Matt Diamond]

I'm trying to gain a better understanding of category theory, so I wrote up a proof of Lawvere's fixed-point theorem as an exercise (specifically the category-theoretical version... the proof using functions and types is much simpler and I've done that already). My solution feels a bit inelegant though, and I'm wondering if it could be shorter. I suspect that someone who knows what they're doing could golf it down to a few lines. I'm curious to see what that ideal proof looks like.

import category_theory.closed.cartesian

open category_theory category_theory.limits.prod

variables {C : Type*} [category C]
  [limits.has_finite_products C]
  [cartesian_closed C]
  {A B : C}

def point_surjective (Φ : A ⟶ B) : Prop :=
∀ (q : ⊤_ C ⟶ B), ∃ (p : ⊤_ C ⟶ A), p ≫ Φ = q

theorem lawvere (h : ∃ (Φ : A ⟶ (B ^^ A)), point_surjective Φ)
  : ∀ (f : End B), ∃ (s : ⊤_ C ⟶ B), f • s = s :=
begin
  intro f,
  cases h with Φ psurj_Φ,
  set g : A ⟶ B := lift (𝟙 A) Φ ≫ (exp.ev A).app B ≫ f with hg,
  set q : ⊤_ C ⟶ B ^^ A := internalize_hom g with hq,
  cases psurj_Φ q with x hx,
  set s : ⊤_ C ⟶ B := lift x q ≫ (exp.ev A).app B with hs,
  have h : lift x (𝟙 ⊤_ C) ≫ cartesian_closed.uncurry q = s, {
    rw [hs, cartesian_closed.uncurry_eq],
    simp,
  },
  rw [
    hq, internalize_hom, cartesian_closed.uncurry_curry,
    lift_fst_assoc, hg, comp_lift_assoc, category.comp_id,
    hx, ← category.assoc, ← hs
  ] at h,
  exact ⟨s, h⟩,
end

[Adam Topaz]

Aside from some very minor golfing, this looks like a good proof to me!

[Martin Harrison]

What is golfing? I am picturing a scene on the putting green where you take many extra steps, tapping the ball here and there before sinking it. Is that the meaning?

[Matt Diamond]

@Adam Topaz Thanks!

[Matt Diamond]

@Martin Harrison It's from "code golfing", which is when people try to write a piece of code in the shortest possible way

[Matt Diamond]

glossary#golfing

[Adam Topaz]

There may be a few smaller lemmas that would be useful and could shorten it.... I don't know if I'll have time to play around with this right now, but I'll try later.

[Matt Diamond]

Sounds good! No pressure, of course... I just wanted to make sure I wasn't missing something wildly obvious. Glad to hear it's on the right track.

[Kyle Miller]

@Martin Harrison In golf you're trying to take the fewest strokes to get the ball in the hole. In code golf you're trying to take the fewest keystrokes.

[David Wärn]

Personally I like the idea of working with Cartesian closed categories as if they were Type. In this spirit, here's what a statement and proof can look like:

lemma lawvere
  (φ : Γ ⟶ X ⟹ X ⟹ Y)
  (φ_surj : ∀ y : Γ ⟶ X ⟹ Y, ∃ x : Γ ⟶ X, φ x = y)
  (f : Γ ⟶ Y ⟹ Y) :
  ∃ s : Γ ⟶ Y, f s = s :=
let q : Γ ⟶ X ⟹ Y := by clear φ_surj; c_intro x; exact f (φ x x) in
let ⟨p, hp⟩ := φ_surj q in
⟨φ p p, by conv_rhs { rw [hp, beta, category.id_comp, category.id_comp] }⟩

It is based on a general c_intro tactic and associated (sorried!) lemma beta which can be found here

[David Michael Roberts]

With blatant self-promotion, you can prove Lawvere's theorem with much less https://arxiv.org/abs/2110.00239 so you can rely on less background material

[Matt Diamond]

@David Michael Roberts Nice! Do pointed magmoidal categories exist in mathlib?

[David Michael Roberts]

Not that I know! The axioms are so minimal it seems not terrible to formalise directly

[Matt Diamond]

@David Wärn It looks like you're applying morphisms as if they were functions... I didn't think that was possible in mathlib. Do you have some kind of has_coe_to_fn set up with quiver.hom?

[David Wärn]

Ah yes, it's this coercion in the gist

instance : has_coe_to_fun (Γ ⟶ X ⟹ Y) (λ _, (Γ ⟶ X) → (Γ ⟶ Y)) :=
⟨λ f g, prod.lift g f ≫ (exp.ev X).app Y⟩