Lean companion to Category Theory in Context

Stream: new members

[Rado Kirov]

On a whim I decided to see whether I can start writing a Lean companion to @Emily Riehl 's Category Theory in Context book (freely available https://emilyriehl.github.io/files/context.pdf :partying_face: ) in a similar manner to https://github.com/teorth/analysis. I am not an expert in category theory nor mathlib or lean, so no idea whether this will work or blow up in my face, but got Section 1.1 done in a few hours today.

If anyone wants to challenge themselves in completing the sorries, take a look (very few so far, but I will try to add more in upcoming days).

If anyone wants to join this companion writing by submitting PRs, I am open to reviewing them.

[Rado Kirov]

The repo - https://github.com/rkirov/category-theory-in-context-lean

[Adrian Marti]

Interesting project, I really like that book. I'll try running your file through Aristotle, lets see what happens.

[Rado Kirov]

Added Section 1.2 too

[Adrian Marti]

Here is the result of running section 1.1 through it Category.lean. It seems to have proved all the lemmas except the partial order one, which is false since you are considering a partial order and a category structure on the same type, which is not what you want.

[Adrian Marti]

Also, keep in mind that these AI proofs can be improved (it's spamming aesop :unamused: ), but they can give you some proof ideas.

[Rado Kirov]

Nice, thanks for sharing. I got a proof for the poset one - https://github.com/rkirov/category-theory-in-context-lean/blob/main/CategoryTheoryInContextLean/Section_1_1.lean#L140-L155 Indeed [Category \alpha] had to be removed so that we get the Poset generated instance one.

[Rado Kirov]

Here is the latest thing I am struggling with (and Claude couldn't figure out) - https://github.com/rkirov/category-theory-in-context-lean/blob/main/CategoryTheoryInContextLean/Section_1_3.lean#L35

[Kevin Buzzard]

Can you either make a mwe which depends only on mathlib, or report the error you're getting with your proposed construction?

[Rado Kirov]

sure, here it is

import Mathlib

namespace CategoryTheoryInContext

class Category (α : Type*) where
  -- objects
  -- morphisms
  Hom : α → α → Type*
  -- identity morphism
  id : (X : α) → Hom X X
  -- composition of morphisms
  -- we use left-to-right notation for composition to match mathlib
  -- while the book uses right-to-left notation to match traditional notation for functions
  comp : {X Y Z : α} → Hom X Y → Hom Y Z → Hom X Z
  -- propositions / laws
  id_comp : ∀ {X Y : α} (f : Hom X Y), comp (id X) f = f
  comp_id : ∀ {X Y : α} (f : Hom X Y), comp f (id Y) = f
  assoc : ∀ {W X Y Z : α} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp (comp f g) h = comp f (comp g h)

scoped infixr:80 " ≫ " => Category.comp -- type as \gg

-- example 1.1.3.i
-- difference from the book, we use Sets from a fixed Type X, not all sets
instance Category.Sets (α : Type*) : Category (Set α) where
  Hom X Y := X → Y
  id _ x := x
  comp f g := g ∘ f
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

open Category

class Functor (α β : Type*) [C : Category α] [D : Category β] where
  -- data
  -- map on objects
  F : α → β
  -- map on morphisms
  homF {X Y : α} : C.Hom X Y → D.Hom (F X) (F Y)
  -- properties / laws
  -- need to qualify id to avoid clash with id in root namespace.
  map_id (X : α) : homF (id X) = Category.id (F X)
  map_comp {X Y Z : α} (f : C.Hom X Y) (g : C.Hom Y Z) :
    homF (f ≫ g) = homF f ≫ homF g

-- examples 1.3.2.i
def PowerSetFunctor (α : Type*) : Functor (Set α) (Set (Set α)) where
  F X := Set.powerset X
  homF f := Set.image f
  map_id X := by sorry
  map_comp f g := by sorry

[Kevin Buzzard]

You are confusing Set.powerset (s : Set A) with Set (\u s : Type); these are probably a long way from defeq.

[Kevin Buzzard]

instance Category.Sets (α : Type*) : Category (Set α) where
  Hom X Y := X → Y

is kind of horrible. You have X : Set alpha (a term) and you are coercing it to a type (because → eats types) so there are now coercion arrows everywhere. Why not stick with what the book says and use Type (the collection of all types, which is the type-theoretic analogue to the collection of all sets) rather than Set alpha? Otherwise you are confusing types and terms.

[Kevin Buzzard]

-- example 1.1.3.i
-- no longer different from the book
instance Category.Types : Category Type where
  Hom X Y := X → Y
  id _ x := x
  comp f g := g ∘ f
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

-- now works
def PowerSetFunctor (α : Type*) : Functor Type Type where
  F X := Set X
  homF f := Set.image f
  map_id X := by sorry
  map_comp f g := by sorry

[Rado Kirov]

Ah, nice I wanted to make the Type category work too, but couldn't previously - https://github.com/rkirov/category-theory-in-context-lean/blob/main/CategoryTheoryInContextLean/Section_1_1.lean#L44-L50. Looks like you got that working. Indeed the Types category is probably the closest to Sets while working in Lean which has type theory not set theory foundations.

[Kevin Buzzard]

instance Category.Types : Category (Type u) where
  Hom X Y := X → Y
  id _ x := x
  comp f g := g ∘ f
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

works fine for me.

[Rado Kirov]

I still think that for a fixed type \alpha, Sets \alpha is valid Lean category, where the powerset functor makes mathematical sense, but might be messier to work with. WDYT?

[Kenny Lau]

@Rado Kirov that is only because you used Type u without first defining u by writing universe u in the beginning

[Kenny Lau]

Rado Kirov said:

Sets \alpha is valid Lean category

Lean's Set α translates to maths' "powerset of X", so the correct category structure is from the ordering

[Rado Kirov]

I swear I had a gnarlier universe error earlier, but I think I changed the category definition ot use Type* instead of explicit universes, which seems to have helped :)

[Rado Kirov]

Lean's Set α translates to maths' "powerset of X", so the correct category structure is from the ordering

yes, the category obj = powerset X, but we can still do a powerset functor to powerset ( powerset X)), no?

[Rado Kirov]

but I agree, that this is not in the book, and kinda my invention to get the simplest example going, and if I have Types category I will swap with that can call it a day :)

[Kenny Lau]

Rado Kirov said:

functor

where's your category

[Rado Kirov]

I have a Category instance for every Set \alpha so Set (Set \alpha) gets one too.

[Kenny Lau]

but you can still have the powerset functor if you use Type instead

[Rado Kirov]

Yes, powerSet on Type is cleaner and better, no argument there and I think the moral equivalent of Set in the book

[Rado Kirov]

ok, here it is - https://github.com/rkirov/category-theory-in-context-lean/blob/main/CategoryTheoryInContextLean/Section_1_3.lean . Thanks for the help and the nudge to complete the Type category :)

[Rado Kirov]

I guess my ask was a classic https://en.wikipedia.org/wiki/XY_problem, kudos to @Kevin Buzzard for spotting it

[Kenny Lau]

we all do it subconsciously

[Rado Kirov]

ok one more if you will indulge me (asked claude and it failed), no math content here, just lean type class shenanigans

import Mathlib

namespace CategoryTheoryInContext

class Category (α : Type*) where
  -- objects
  -- morphisms
  Hom : α → α → Type*
  -- identity morphism
  id : (X : α) → Hom X X
  -- composition of morphisms
  -- we use left-to-right notation for composition to match mathlib
  -- while the book uses right-to-left notation to match traditional notation for functions
  comp : {X Y Z : α} → Hom X Y → Hom Y Z → Hom X Z
  -- propositions / laws
  id_comp : ∀ {X Y : α} (f : Hom X Y), comp (id X) f = f
  comp_id : ∀ {X Y : α} (f : Hom X Y), comp f (id Y) = f
  assoc : ∀ {W X Y Z : α} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp (comp f g) h = comp f (comp g h)

scoped infixr:80 " ≫ " => Category.comp -- type as \gg

open Category

universe u
-- moral equivalent to Set in the book, but working with types in Lean.
instance Category.Type : Category (Type u) where
  Hom X Y := X → Y
  id _ x := x
  comp f g := g ∘ f
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

def Category.opp {α: Type*} (C : Category α) : Category α where
  Hom X Y := C.Hom Y X
  id X := id X
  comp f g := C.comp g f
  id_comp := by simp [comp_id]
  comp_id := by simp [id_comp]
  assoc := by simp [← assoc]

class Functor (α β : Type*) [C : Category α] [D : Category β] where
  -- data
  -- map on objects
  F : α → β
  -- map on morphisms
  homF {X Y : α} : C.Hom X Y → D.Hom (F X) (F Y)
  -- properties / laws
  -- need to qualify id to avoid clash with id in root namespace.
  map_id (X : α) : homF (id X) = Category.id (F X)
  map_comp {X Y Z : α} (f : C.Hom X Y) (g : C.Hom Y Z) :
    homF (f ≫ g) = homF f ≫ homF g

-- definition 1.3.12
instance CatProduct {α β : Type*} [C : Category α] [D : Category β] : Category (Prod α β) where
  Hom X Y := (C.Hom X.1 Y.1) × (D.Hom X.2 Y.2)
  id X := (id X.1, id X.2)
  comp f g := (f.1 ≫ g.1, f.2 ≫ g.2)
  id_comp _ := by repeat rw [id_comp]
  comp_id _ := by repeat rw [comp_id]
  assoc _ _ _ := by repeat rw [assoc]

-- definition 1.3.13
def Hom_bifunctor (α : Type*) [C: Category α] :
  @Functor (Prod α α) Type (@CatProduct α α C.opp C) _ where sorry

I thought using @ will allow me to explicitly construct the right product category, using C.opp instead of C, but Lean still complains that it finds the implicitly constructed C x C category.

[Aaron Liu]

Well if you have a noncanonical instance you can't use where

[Rado Kirov]

so just replace with := ?

[Rado Kirov]

I see the same error with :=

[Rado Kirov]

github copilot spit out this as a body of the def

def Hom_bifunctor (α : Type*) [C: Category α] :
  @Functor (Prod α α) Type (@CatProduct α α C.opp C) _ := {
  F := fun X => Hom X.1 X.2,
  homF := fun {X Y} f g => g ≫ f.1
  map_id X := by
    funext g
    simp [Category.id]
    rw [id_comp]
  map_comp f g := by
    funext h
    simp [comp]
    rw [assoc]
    rfl
  }

but lean has the type class error before even beginning to check it.

[Rado Kirov]

that doesn't even look right should be homF := fun {X Y} f g => f.1 ≫ g ≫ f.2 but in any case I get that far

[Kenny Lau]

@Rado Kirov the mathlib solution is that we use type synonyms, i.e. the op category will be on the type Opposite X instead of on X

[Kenny Lau]

if we don't follow the one-type-one-instance axiom we're gonna run into a lot of trouble

[Rado Kirov]

Yep, that's what I am learning the hard instructive way.

[Rado Kirov]

which keyword creates type synonyms?

[Kevin Buzzard]

def

[Rado Kirov]

so I need a def αᵒᵖ := α somewhere and make sure that Category.opp builds an Category instance for αᵒᵖ not α. But where do I put this def in the opp definition or the hom_bifunctor?

[Kenny Lau]

it's a global definition

[Kenny Lau]

a type synonym is just any other definition

[Rado Kirov]

ok, made some progress, Opposite is now

def Opposite (α : Type*) := α

-- definition 1.2.1
def Category.opp {α : Type*} (C : Category α) : Category (Opposite α) where ...

and def Hom_bifunctor (α : Type*) [C: Category α] : Functor (Prod (Opposite α) α) Type where ... should work, but now I get

failed to synthesize
  Category (Opposite α × α)

do I need to make Prod work with Opposite types too explicitly?

[Kenny Lau]

@Rado Kirov you didn't make it an instance

[Rado Kirov]

That did it, thanks! I am learning a lot by writing this companion, but it's dawning to me that if someone is just to do the exercises I am leaving behind they won't be learning the same stuff (like this very concrete issue with typeclasses). Maybe the answer is get more people to write textbook companions, it's kinda fun.

[Rado Kirov]

Narrowed the original issue to #new members > Custom typeclass instances problem , type-classes continue to be somewhat mysterious. From software eng perspective not surprising, various dependency injection frameworks like Dagger have similar "too much magic, what to do when things don't work as expected" problems.

for the purposes of the companion, going with the type synonym solution as it matches mathlib, but good opportunity to dig deeper into typeclass inference rules.

[Julian Berman]

(I've had this book on my list to read as well, so I'm also excited to see where this goes).

It might be premature considering it's really a lead-in to the book, but I was trying to find some of the machinery in Mathlib mentioned at the beginning of Chapter 1before the actual "start" of the material. Specifically, not knowing anything about group extensions mathematically, I see Mathlib has them, but in Mathlib #check GroupExtension says none of the groups there need to be CommGroups? And then is the Ext referred to there what is in Mathlib.CategoryTheory.Abelian.Ext? And if so, the book is clearly talking about some relationship between group extensions and that object, and saying Ext(H, G) forms a CommGroup, are either of those facts somewhere? I can't find anything about Prufer p groups in Mathlib either, let alone the Ext equivalence with Z_p.

I'm sure I should just ignore all of the above given the book hasn't yet gotten to explaining them in the lens of category theory, and I should just keep reading, but let me know if anyone actually found any additional Mathlib objects that I missed from that one page.

[Joël Riou]

GroupExtension is a notion about groups, while Ext^1 makes sense in abelian categories (in particular in the abelian category of abelian groups). (These two notions "intersect" in the case of abelian groups.) The Ext in Emily's book identifies to docs#CategoryTheory.Abelian.Ext (in degree 1). To any short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0, a class in that group is defined docs#CategoryTheory.ShortComplex.ShortExact.extClass. It can be shown that this abelian group Ext^1(X₃, X₁) identifies, at least as a set, to the quotient of the type of the short exact sequences diagrams as above modulo a certain equivalence relation. In Lean 3, I had a definition of this quotient type of equivalence classes of extensions https://github.com/joelriou/homotopical_algebra/blob/697f49d6744b09c5ef463cfd3e35932bdf2c78a3/src/for_mathlib/category_theory/abelian/extensions.lean#L393

[Rado Kirov]

I just pushed section_1_3, but basically I am punting on most of "the context", i.e. examples and exercises in the categories of mathematical objects like Groups, Topologies, etc. Not sure if it is even possible to define such categories, and I had plenty of rough time just defining the pure category theory objects like comma categories. This is surprisingly hard and challenging my Lean skills, so I might take a break and go back to finishing Tao's Real Analysis exercises, which are walk in the park compared to defining fancy cat theory objects that get universe errors.

I someone completes the exercises as written for 1.1 to 1.3, maybe that will motivate me to formulate more of the exercises for rest of chapter 1.