Implementing a functor category

Stream: new members

[VayusElytra]

Hi, my goal right now is to attempt to write some code implementing the basics of the theory of persistence modules into Lean as a research project. I have a couple of questions relating to this. For context, the key definition in this setting is functors from poset categories (usually (ℝ, ≤)) into Vect.

1) What are the must-reads so I can get started on this implementation? I have already read Chapter 6 of Mathematics in Lean about classes and structures, which seems to be the most relevant one, but I do not feel like it would be enough on its own.

2) Are there specific resources on the implementation of category theory into mathlib that would be worth looking into?

3) Are there similar objects already implemented into mathlib I could look to for comparison? Some other structure or class that is composed of functors from one category to another?

Thank you very much for answers.

[Kevin Buzzard]

What's Vect?

[Kevin Buzzard]

Usually the best way to learn is to just learn on the job, ie get started, and ask questions when you're stuck (beginner questions are fine in this channel and lots of questions are also fine).

[VayusElytra]

Vect as in the category of vector spaces over some base field. And thank you! I will not hesitate to ask.

[VayusElytra]

The fact that R-modules over some field R form a category seems to not be implemented in mathlib, so I think I would need to implement the fact that vector spaces form an instance of a category on my own. So this would mean something like:

variable (V : Type u) (K : Type v) [DivisionRing K] [AddCommGroup V] [Module K V]

instance instCategory : CategoryTheory.Category (Module K V) where
-- other stuff

However this is not really what I would want, because I would just be showing that one specific vector space has the structure of a category, as opposed to showing that the type of vector spaces is a category. How can I work around this?

[Andrew Yang]

docs#ModuleCat

[VayusElytra]

Thanks, I wonder how I missed this

[Kevin Buzzard]

FWIW CategoryTheory.Category (Module K V) actually means "the set of all the ways you can make V into a K-module forms a category" (not what you said, and not what you wanted either).

[VayusElytra]

I think this makes sense to me. Is it accurate to think of Module K V as the set of all possible K-module structures on V?

A related question: what is the appropriate type to speak about "the set of all K-modules"? This question came up again as I was implementing this snippet:

--IntervalObj is meant to be a function that takes as input 2 elements in ℝ, a and b, as
--well as some other real number x, and associates to x a K-vector space.
--If x is between a and b, that vector space is K itself, viewed as a 1 dimensional K vector space
--Otherwise, it is the trivial K-vector space {0}.

variable (K : Type*) [DivisionRing K]

def IntervalObj (a : ℝ) (b : ℝ) (x : ℝ) : (Module K K) :=
  if a ≤ x ∧ x ≤ b then
    ⟨K⟩
  else
    ⟨0⟩

It is clear to me in light of what you have said that Module K K is not the right type for this function: it would take values in the set of all possible K-module structures on K, as opposed to in the set of all K-modules. I would have expected the set of all K-modules to be Module K _ but this returns an error (the typeclass instance problem gets stuck). What is the proper way to do this?

(I am aware that the matching afterwards would not work properly even with the correct domain for this function, but let's ignore this for the moment).

[Kyle Miller]

The "set" of all K-modules is ModuleCat K. ("Set" is in quotes for two reasons. (1) I just want to point out that this goes up a universe level since the collection of all K-modules is big. (2) Terms of ModuleCat K "are" K-modules -- while each term is everything you need for a normal Lean K-module all packaged up, there is some magic using coercions to make them behave as if they actually were normal Lean K-modules.)

[VayusElytra]

Sorry, I think there is a nuance here that I do not quite understand. The documentation for ModuleCat refers to ModuleCat R as the category of all R-modules and their morphisms.
This seems like a different concept to me than the collection (thank you for the correction!) of all K-modules? For instance, ModuleCat R would also contain morphism sets between objects.

Does this work the same for every other algebraic structure? For instance, say I wanted to define a function that takes as arguments a group and an element in the group and did some operation on it. Would I then want to write something like this?

def foo (G : GroupCat) (a : G) :=
--something

[Kyle Miller]

ModuleCat R is a type whose terms correspond to R-modules. There's an additional structure attached to ModuleCat R that provides the morphisms, via a typeclass, in a similar way to how the [Module R M] typeclass can attach a module structure to a type M.

[Kyle Miller]

You could write def foo (G : GroupCat) (a : G) :=, but writing def foo (G : Type*) [Group G] (a : G) := is more common and more likely to avoid annoying minor technical challenges.

[Kyle Miller]

This is an example of an "impedance mismatch" between the category theory library and the rest of the library.

[Kyle Miller]

The nuance between these is that with G : GroupCat, this G is not itself a type, but a "bundled" object that contains both a type and the Group G instance; you can write (a : G) because there is a coercion from G to a type (this coercion merely accesses the carrier field from G). But with the second one, G is already a type, and it "is" a group since there is a Group G instance in context.

[Kyle Miller]

The GroupCat version is the one that's "actually" working with groups, like in the "a group is a 4-tuple $(G,\cdot,{}^{-1},1)$" sense.

[VayusElytra]

I see, thank you very much. I think this is completely clear now.

To check if I understand right: if I wanted to define a function that maps, say, a real number to a group, I could either write:

def foo (a : ℝ) : GroupCat :=
--definition

which would not be preferable as you say, or I could write

def foo (a : ℝ) :=
--definition

skipping the type ascription entirely and relying on typeclass inference to recover that structure later on?

[Kevin Buzzard]

Perhaps

def foo (a : ℝ) : Type :=
--definition of the underlying set

would be better, and then later on

instance (a : ℝ)  : Group (foo a) := -- multiplication, inverse, identity and axioms go here

[Kyle Miller]

Yeah, what Kevin says is the way you'd formulate it in the "non-bundled" way, which is very prevalent in mathlib.

These are each solutions to the problem of implementing synecdoche in mathematics, which is a figure of speech that both refers to referring to something by one of its parts or vice versa.

With (G : GroupCat), you can write g : G because there is a typeclass for coercing G -> Type, letting you refer to G as if it were its set of elements.

With (G : Type) [Group G], you can write g h : G and g * h, letting you to refer to G as if it were a group structure even though it's just its set of elements.

[Kyle Miller]

There are two reasons for not bundling:

1. It lets you add new structure to a pre-existing type. You do not need to worry about giving an algebraic object the strongest possible structure at its definition.
2. It lets you work with terms of the pre-existing type, rather than needing to phrase the type as, say, NatMonoid with NatMonoid.carrier := Nat. You would have to be consistent with using NatMonoid rather than Nat for theorems about monoids to apply.

However, when you are interested about working with groups in general, rather than reasoning about individual pre-defined groups, bundling makes sense. In other words, when you're reasoning about the category of such objects in the abstract it's more-or-less necessary to work with the bundled objects.