Lawvere fixed point theorem

Stream: Is there code for X?

[Graham Leach-Krouse]

Is there a formalization of the Lawvere fixed point theorem in mathlib?

[Ruben Van de Velde]

Like https://mathstodon.xyz/@highergeometer/112098277610968736 ?

[Graham Leach-Krouse]

Maybe? I found this old doodle:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
import Mathlib.CategoryTheory.Closed.Monoidal

open CategoryTheory

noncomputable instance cartesian [Category α] [Limits.HasFiniteProducts α] : MonoidalCategory α where
  tensorObj x y := Limits.prod x y
  tensorUnit' := Limits.terminal α
  tensorHom := by
    intros X Y Z W f g
    simp
    exact Limits.prod.lift (Limits.prod.fst ≫ f) (Limits.prod.snd ≫ g)
  rightUnitor X := Limits.prod.rightUnitor X
  leftUnitor X := Limits.prod.leftUnitor X
  associator X Y Z := Limits.prod.associator X Y Z

structure interpreter [Category α] [Limits.HasFiniteProducts α] [mc : MonoidalClosed α]
  (A E Y : α) (i : E ⟶ Y)  where
  map : A ⟶ (A ⟶[α] E)
  interprets : ∀f : A ⟶ E, ∃c : cartesian.tensorUnit' ⟶ A,
    let lhs := (Limits.prod.rightUnitor A).inv ≫ (Limits.prod.map (𝟙 A) (c ≫  map)) ≫ (ihom.ev A).app E ≫ i
    let rhs := f ≫ i
    lhs = rhs

def fixedPointProperty [Category α] [Limits.HasFiniteProducts α] { E Y : α } (i : E ⟶ Y) :=
  ∀t : E ⟶ E, ∃c: cartesian.tensorUnit' ⟶ E, c ≫  t ≫ i = c ≫  i

theorem lawvereGeneralized [Category α] [Limits.HasFiniteProducts α] [MonoidalClosed α] {A E Y : α} {i : E ⟶ Y}
  : Nonempty (interpreter A E Y i) → fixedPointProperty i := by
    intros
    have ⟨int⟩ := ‹Nonempty (interpreter A E Y i)›
    clear ‹Nonempty (interpreter A E Y i)›
    let g := (Limits.prod.map (𝟙 A) int.map) ≫ (ihom.ev A).app E
    simp at g
    have fact : ∀f : A ⟶ E, ∃c : cartesian.tensorUnit' ⟶ A, ∀a : cartesian.tensorUnit' ⟶ A,
      (Limits.prod.lift a c) ≫ g ≫ i = a ≫ f ≫ i := by
        intros f
        have ⟨f',eq₀⟩ := int.interprets f
        refine ⟨f',?_⟩
        intros a
        have termEq₁ : a ≫ Limits.terminal.from A = 𝟙 cartesian.tensorUnit' := by simp
        simp [←eq₀, Limits.prod.comp_lift_assoc]
        have termEq₂ : a ≫ Limits.terminal.from A ≫ f' ≫ int.map = (a ≫ Limits.terminal.from A) ≫ f' ≫ int.map := by rw [Category.assoc]
        rw [termEq₂,termEq₁]
        simp
    intros t
    let k : A ⟶ E := Limits.diag A ≫ g ≫ t
    have ⟨k',eq₁⟩ := fact k
    have eq₂ := eq₁ k'
    simp at eq₂
    have rweq : Limits.prod.lift k' (k' ≫ int.map) = k' ≫ Limits.prod.lift (𝟙 A) int.map := by simp
    refine ⟨Limits.prod.lift k' (k' ≫ int.map) ≫  (ihom.ev A).app E, ?_⟩
    simp
    rw [eq₂, rweq, Category.assoc]

and I was thinking of cleaning it up. I think of the theorem as something about general Cartesian closed categories, and not specifically maps between types. But maybe I'm missing some insight about how that toot can be generalized, and over-complicating things?

[mdnestor]

Here is a proof using the current Mathlib implementation of cartesian closed categories:

-- Lawvere's fixed point theorem for Cartesian closed categories

import Mathlib.CategoryTheory.Closed.Cartesian
open CategoryTheory Limits CartesianClosed

def weakly_point_surjective {C : Type u} [Category.{v} C] [HasFiniteProducts C] [CartesianClosed C] {A X Y: C} (g: X ⟶ A ⟹ Y): Prop :=
  ∀ f: A ⟶ Y, ∃ x: ⊤_ C ⟶ X, ∀ a: ⊤_C ⟶ A, a ≫ (prod.rightUnitor A).inv ≫ uncurry (x ≫ g) = a ≫ f

def fixed_point_property {C : Type u} [Category.{v} C] [HasFiniteProducts C] [CartesianClosed C] (Y: C): Prop :=
  ∀ t: Y ⟶ Y, ∃ y: ⊤_ C ⟶ Y, y ≫ t = y

theorem lawvere_fixed_point_theorem {C : Type u} [Category.{v} C] [HasFiniteProducts C] [CartesianClosed C] {A Y: C} (g: A ⟶ A ⟹ Y) (h: weakly_point_surjective g): fixed_point_property Y := by
  intro t
  have h1 := h (diag A ≫ uncurry g ≫ t)
  obtain ⟨x, hx⟩ := h1
  exists x ≫ diag A ≫ uncurry g
  have h2 := hx x
  have h3: x ≫ (prod.rightUnitor A).inv ≫ uncurry (x ≫ g) = x ≫ diag A ≫ uncurry g := by
    rw [uncurry_natural_left x g]
    simp
    repeat rw [←Category.assoc]
    apply eq_whisker
    apply prod.hom_ext
    simp
    simp
    rw [←Category.assoc]
    calc
      (x ≫ terminal.from A) ≫ x = 𝟙 (⊤_ C) ≫ x := by rw [CategoryTheory.Limits.terminal.hom_ext (x ≫ terminal.from A) (𝟙 (⊤_ C))]
                               _ = x            := Category.id_comp x
  rw [h3] at h2
  simp [Eq.comm]
  exact h2