Zulip Chat Archive

Stream: new members

Topic: golfing Lawvere's fixed-point theorem

Matt Diamond (Oct 15 2022 at 19:19):

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 :=
  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],
  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⟩,

Adam Topaz (Oct 15 2022 at 19:43):

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

Martin Harrison (Oct 15 2022 at 19:49):

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 (Oct 15 2022 at 19:50):

@Adam Topaz Thanks!

Matt Diamond (Oct 15 2022 at 19:52):

@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 (Oct 15 2022 at 19:53):


Adam Topaz (Oct 15 2022 at 19:55):

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 (Oct 15 2022 at 19:56):

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 (Oct 15 2022 at 20:20):

@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 (Oct 16 2022 at 09:02):

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 (Oct 16 2022 at 10:15):

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 (Oct 16 2022 at 19:21):

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

David Michael Roberts (Oct 16 2022 at 22:00):

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

Matt Diamond (Oct 16 2022 at 22:23):

@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 (Oct 17 2022 at 07:55):

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

Last updated: Dec 20 2023 at 11:08 UTC