category of sets

Stream: new members

[Vasily Ilin]

Can anyone point me to the category of sets in Lean? I want to define an affine group scheme as a representable functor from k-algebras to sets. Thanks!

[Yaël Dillies]

docs#category_theory.types

[Kevin Buzzard]

(because lean uses type theory not set theory)

[Vasily Ilin]

Thank you! trying to get it to work. What's wrong with this?

import category_theory.types
variables (C : Type*) [category_theory.types C]
-- function expected at
--   category_theory.types
-- term has type
  -- category_theory.category (Type ?)

[Yaël Dillies]

The category of type is Type*. No need to call category_theory.types directly. Typeclass search will do it for you.

[Vasily Ilin]

Ah I see. What about this variable declaration? I want K_alg to be the category of K-algebras.

import category_theory.types
import algebra.category.Algebra.basic

variables (K : Type*) [comm_ring K]
variables {K_alg : Type*} [Algebra.category_theory.category K K_alg]

[Eric Wieser]

This mistake seems analogous to trying to use int.comm_ring to talk about the ring of integers, when the correct spelling is just int

[Yaël Dillies]

You're doing the same mistake here. Simply delete K_alg and use Algebra K instead.

[Eric Wieser]

To make an analogy; these typeclass instances are "painting" structure onto another type. What you're doing is trying to refer to the paint, int.comm_ring : ring int; but you should be referring to the thing being painted, int : Type

[Vasily Ilin]

Sorry but I am not understanding. This does not seem to declare K_alg as the category of K-algebras:

import category_theory.types
import algebra.category.Algebra.basic
open category_theory

variables (K : Type*) [comm_ring K]
variables (K_alg : Type*) [Algebra K]

class affine_scheme :=
(scheme : K_alg ⥤ Type*) -- does not work
(representable : scheme.representable)

[Vasily Ilin]

This seems to almost work! But not quite

import category_theory.types
import algebra.category.Algebra.basic
open category_theory

variables (K : Type*) [comm_ring K]
variables (K_alg : Type*) [category K_alg] [Algebra K_alg] -- ⊢ comm_ring K_alg

class affine_scheme :=
(scheme : K_algᵒᵖ ⥤ Type*)
(representable : scheme.representable)

[Eric Wieser]

Write Algebra K where you are writing K_alg

[Vasily Ilin]

Ah, it works!!! Thank you

[Eric Wieser]

You can tell immediately that you've gone wrong if you write [Foo X] when Foo is not a class

[Eric Wieser]

(docs#Algebra is not a class)

[Vasily Ilin]

I am trying to do the same with Group to get the category of groups but it throws an error:

import category_theory.types
import algebra.category.Algebra.basic
import algebra.category.Group.basic
open category_theory

variables (K : Type*) [comm_ring K]

class affine_group_scheme :=
(scheme : (Algebra K)ᵒᵖ ⥤ Group)
(representable : scheme.representable)

[Adam Topaz]

What does it mean for a functor to Group to be representable?
You want

import category_theory.types
import algebra.category.Algebra.basic
import algebra.category.Group.basic
open category_theory

variables (K : Type*) [comm_ring K]

class affine_group_scheme :=
(scheme : (Algebra K)ᵒᵖ ⥤ Group)
(representable : (scheme ⋙ forget _).representable)

[Adam Topaz]

BTW @Vasily Ilin if this is related to your work on Hopf algebras, then you should know that Algebra k is the category of possibly noncommutative algebras.

[Vasily Ilin]

AH, thanks! I do want my algebras to be commutative.
I am not familiar with the >>> notation. The definition of "representable" I am familiar with is that it is the hom-set out of an object. So I want to say that the functor scheme looks like $Hom(A,\_)$ for some K-algebra $A$.

[Vasily Ilin]

(I also messed up the op thing, it should not be there)

[Adam Topaz]

A Hom set (i.e. Hom type) is not a Hom group ;)

[Vasily Ilin]

Right. Is ⋙ the composition of functors?

[Vasily Ilin]

and forget _ -- the forgetful functor from Groups to Sets?

[Adam Topaz]

Yes, and forget _ is the forgetful functor from a concrete category. If you want to be explicit about it, you can write forget Group in this case, but lean can figure that out from context

[Vasily Ilin]

I've never had to think about this detail as a mathematician. Thank you!
Is there a category of commutative algebras in Lean? If not, is there a way to easily define one?

[Adam Topaz]

I don't know whether this category is in mathlib. Maybe docs#CommAlgebra ?

[Adam Topaz]

Bah, you can use docs#category_theory.under along with docs#CommRing

[Vasily Ilin]

I don't understand what that does. I can simply require that the representative objective of scheme is a commutative algebra

[Adam Topaz]

Of course you can define whatever you want, but a k-scheme can usually be viewed as a presheaf on the category of commutative k-algebras.

[Vasily Ilin]

I agree with you. I just don't understand how docs#category_theory.under helps.

[Adam Topaz]

The category of commutative k algebras is the category of commutative rings with a morphism from k, i.e. the under category associated to k as an object of CommRing.