Stream: general

Topic: Cat theory example to learn from?

Daniel Donnelly (Aug 28 2019 at 15:20):

Hi, I am in the middle of coding critical parts to BananaCats. I am confident enough now in Lean that I can start doing project-motivated learning, and my project is about category theory. So could someone point me to the simplest (takes least effort in the long-run to use) way of "defining a variable C, that is an abstract category?" And why not declare an object X in Ob(C) as well.

Chris Hughes (Aug 28 2019 at 15:24):

import category_theory.category

open category_theory

variables {C : Type*} [category C] (X : C)


Chris Hughes (Aug 28 2019 at 15:25):

X : C means X is an object in C.

Daniel Donnelly (Aug 28 2019 at 15:25):

What does Type* mean?

Klean closure?

Johan Commelin (Aug 28 2019 at 15:26):

@Chris Hughes You'll have some hidden universe variables that way...

Johan Commelin (Aug 28 2019 at 15:26):

maybe just use large_category for now.

Daniel Donnelly (Aug 28 2019 at 15:26):

that includes all categories?

Daniel Donnelly (Aug 28 2019 at 15:26):

I.e. does it mean not-neccessarily large category?

Johan Commelin (Aug 28 2019 at 15:27):

@EnjoysMath Type* mean that C is a type.

Johan Commelin (Aug 28 2019 at 15:27):

Lean uses type theory in its foundations, see TPIL

Daniel Donnelly (Aug 28 2019 at 15:27):

I thought C : Type would accomplish that

Daniel Donnelly (Aug 28 2019 at 15:29):

I will work with the Chris Hughes example for now, since I'm okay with any implications regarding Universes for now

Johan Commelin (Aug 28 2019 at 15:29):

Type* is Type u for a fresh univers u

Daniel Donnelly (Aug 28 2019 at 15:29):

Should BananaCats have a Universe setting as well, where needed?

Daniel Donnelly (Aug 28 2019 at 15:30):

That's as easy as adding a GUI field from my perspective

Johan Commelin (Aug 28 2019 at 15:33):

You can add that later

Daniel Donnelly (Aug 28 2019 at 15:33):

Category lives in Universe: [int spinbox] Use first free universe: [*]

Johan Commelin (Aug 28 2019 at 15:33):

Just use Type for now.

Daniel Donnelly (Aug 28 2019 at 15:33):

@Johan Commelin sure thing. I will use Type for now :)

Daniel Donnelly (Aug 28 2019 at 15:35):

I'ma use Jinja2 (a python library) for making a "create new category" template, and so on...

Daniel Donnelly (Aug 28 2019 at 15:37):

The question is, can I get away with generalizing the template to declaring a variable of a certain type?

Daniel Donnelly (Aug 28 2019 at 15:38):

And another question is what does the application in brackets [category C] do to the declaration?

Daniel Donnelly (Aug 28 2019 at 15:38):

Finallly is variable declaration the formal term for this?

Daniel Donnelly (Aug 28 2019 at 15:38):

*formal vocabulary

Daniel Donnelly (Aug 28 2019 at 15:40):

Btw, the comm to / from Lean VSCode will be 2-way, I.e. a change in the code which Bancats cares about will be detected and reflected in the PyQt5 app ("BananaCats"), and obviously vise versa is the typical usage.

Daniel Donnelly (Aug 28 2019 at 15:45):

To answer one question, I shouldn't generalize, as that would move more logic framework over to BananaCats by necessity, since I'd have to call multiple atomic calls, and organize them correctly. Whereas if I just do the hard coded script for Create a Category, and do the same for each thing, then I should be okay in finishing this.

Daniel Donnelly (Aug 28 2019 at 15:46):

If I need to generalize it should be done with lean code I think

Daniel Donnelly (Aug 28 2019 at 15:48):

I take back that lean should drive BananaCats

Daniel Donnelly (Aug 28 2019 at 15:48):

That would necessitate parsing of Lean!

Daniel Donnelly (Aug 28 2019 at 15:49):

I have to KISS keep it simple

Johan Commelin (Aug 28 2019 at 15:54):

@EnjoysMath [category C] means that C is endowed with the structure of a category.

Thx

Daniel Donnelly (Aug 28 2019 at 15:58):

{% if "category_theory.category" not in context.imported_names %}
import category_theory.category
{% endif %}

{% if "category_theory" not in context.open_modules %}
open category_theory
{% endif %}

variables {{{decl.name}} : {{decl.type}}} [category {{decl.name}}]


It's a Jinja2 template for declaring a variable an abstract category

Scott Morrison (Aug 28 2019 at 23:33):

If universe polymorphism doesn't matter to you (this is pretty much synonymous with "you're not trying to write library code"), then I'd recommend:

import category_theory.category

open category_theory

variables {C : Type} [small_category C] (X : C)


Scott Morrison (Aug 28 2019 at 23:34):

If universe polymorphism does matter to you, and you want the most general case (which in "real maths" means that you either have a small category, where the objects and morphisms live in the same universe, or a large category, where the objects live in a universe one higher than the morphisms, but in "Lean math", because we can't specify this dichotomy, the objects and morphisms just live in two entirely independent universes, I'd recommend:

import category_theory.category

universes v u
open category_theory

variables {C : Type u} [𝒞 : category.{v} C] (X : C)
include 𝒞


Scott Morrison (Aug 28 2019 at 23:37):

Here we need include𝒞because Lean's typeclass inference algorithm is not willing to pull in the instance C until it is sure that the universe parameter v is the desired one, and often it can't tell this without explicit universe annotations everywhere --- instead we just tell Lean to include 𝒞 as an argument to every definition that follows. This is a little dangerous, as you need to be careful to then explicitly omit it again if you write any functions that don't refer to C. (Such functions probably belong higher in the file, or in another file, in any case...)

Last updated: May 08 2021 at 19:11 UTC