The category of pointed objects of a concrete category

Stream: PR reviews

[Sina Hazratpour 𓃵]

Apparently we do not have the category of pointed groupoid, which i needed in a project, so , in #15055 , I define the category of pointed objects of a concrete category, and establish an equivalence to the category of elements of the forgetful functor forget C of the concrete category. This equivalence is used to show that a map of concrete categories induces a functor between the correponding category of pointed objects.

comments/reviews appreciated.

[Dagur Asgeirsson]

I left some comments

[Kim Morrison]

I think this is the wrong definition, and there should be no mention of concreteness. If C has an initial object, then Pointed C should just be Under (⊥_ C).

[Sina Hazratpour 𓃵]

Did you mean terminal instead of "initial"?
https://ncatlab.org/nlab/show/pointed+object

What I want from Pointed C is that its objects are pairs (X, x) where X is an object of C and x is in X. So for instance, Pointed Type is a category whose objects are types and an element of the type, or Pointed Grp is a category whose objects are groups and an element of group, say $(\mathbb{Z}, -2)$

On the other hand, the under category Under (⊤_ Grp) is Grp itself, which is not what I want.

Maybe, the name "pointed objects " is not good? maybe we want "objects with a point"?

[Sina Hazratpour 𓃵]

(also, sometimes a category might not have a terminal object but is concrete such as the category of fields.)

[Yaël Dillies]

I will add that you should feel free to refactor docs#Pointed

[Kim Morrison]

(Yes, I should have said terminal.)

[Kim Morrison]

Could you explain what you want this for? I don't think we should change the meaning of "pointed" here, but perhaps can work out a better name if we know the context.

[Sina Hazratpour 𓃵]

With Steve Awodey and Mario Carneiro, in groupoid_model_in_lean4 we are formalizing the groupoid model of HoTT in Lean, by interpreting the natural model of HoTT into groupoids. The Natural model comes equipped with a type $Ty$ of small types and a type $Tm$ of terms. In the groupoid model they are $grpd$ and $grpd_\bullet$ (i.e. the category of pairs $(G, g)$ where $G$ is a small groupoid and $g$ is an object of it).

Screenshot-2024-08-01-at-9.34.13AM.png

I need $grpd_\bullet$. Formalizing the construction $C_\bullet$ for a concrete category is a more general case of this construction.

[Andrew Yang]

For pointed groupoids, the Under (⊥_ C) approach is the right one though. Do you specifically need "pointed groups"?

[Sina Hazratpour 𓃵]

Indeed. However, I thought maybe in mathlib it would be better to have a construction that covers groups, rings, fields, topological spaces ..., as well as groupoids and categories? That's why I opted for this formalization. In this project I don't need groups.

[Kim Morrison]

But I think that general construction is not generally useful, while the Under (⊥_ C) construction is. I'd want to see actual applications!

[Sina Hazratpour 𓃵]

@Kim Morrison
I am gravitating to to your position. Other than the pair $(\mathbb{Z} [x], x)$ which is the initial object of pointed rings and $((\mathbb{Z},+), 1)$ which is the initial object of pointed groups, I know no other examples.

[Mario Carneiro]

I think the "under bot" definition is wrong in any category with a zero object. That's how we came up with the group example in the first place

[Mario Carneiro]

The fact that these are simply different constructions tells me that we should probably just have both, and if we do I think the concrete category definition is more deserving of the name "pointed C" than the Under (⊥_ C) definition, since it actually involves points and not just global elements.

[Mario Carneiro]

(NB: I discussed this example with Sina beforehand and suggested the concrete category generalization)

[Kim Morrison]

I think the established use of "pointed object" in the literature is sufficient for that version to claim the name.

[Joël Riou]

We could have Pointed for the general Under top construction, and PointedDiscrete for the concrete version. Also, why not making PointedDiscrete an abbreviation for (forget C).Elements?

[Sina Hazratpour 𓃵]

I like your suggestions of PointedConcrete and Pointed.

@Joël Riou wrote

Also, why not making PointedDiscrete an abbreviation for (forget C).Elements?

The reason I started with the current definition

class Pointed where
  obj : C
  pt : obj

is because I thought the API might be simpler to use compared to (forget C).Elements. I'll do a parallel formalization using (forget C).Elements and see which one works best. The advantage of the latter is lemmas/theorems of Elements become immediately available for PointedConcrete, before we prove the equivalence of the two. If the API is not too bad I prefer the second approach too.

[Joël Riou]

The API of Elements may require some improvements, but this is a good occasion to do so!