Constructing a groupoid bypassing category instances?

Stream: new members

[Rémi Bottinelli]

I want to build a kernel groupoid from a morphism in tactic mode, but I believe there is a hidden category instance messing with me.
How do I force lean to build things from scratch? Thanks!

variable (D : Type*)
variables {G : groupoid C} {H : groupoid D}

section hom

def ker (φ : @category_theory.functor C G.to_category D H.to_category) : groupoid C :=
begin
  constructor,
  -- not what I want!
  sorry
end

end hom

[Adam Topaz]

docs#category_theory.groupoid

[Adam Topaz]

Right so groupoid is an unbundled class.

[Adam Topaz]

There is nothing hidden.... you told lean that you wanted to construct a groupoid structure on C, and a groupoid is a category satisfying an additional condition.

[Adam Topaz]

What are you expecting to construct here?

[Andrew Yang]

Can you provide a self-contained #mwe? One that contains the imports and variables and works in a standalone file.

[Rémi Bottinelli]

mwe:

import category_theory.groupoid

open category_theory
open set

variables {C D : Type*} {G : groupoid C} {H : groupoid D}

def ker (φ : @category_theory.functor C G.to_category D H.to_category) : groupoid C :=
begin
  constructor,
  -- not what I want!
  sorry,
end

and the goal just before the sorry is:

  C : Type u_1,
  D : Type u_2,
  G : groupoid C,
  H : groupoid D,
  φ : C ⥤ D
  ⊢ Π {X Y : C}, (X ⟶ Y) → (Y ⟶ X)

which I believe to mean that lean already knows which category instance it wants to impose on C.

[Rémi Bottinelli]

Adam Topaz said:

What are you expecting to construct here?

I want to be able to construct a groupoid whose category part is also built by me, and not given by a preexisting instance.

[Yaël Dillies]

But then you would have two groupoids on C! This goes against the typeclass design and will probably cause more pain down the line.

[Kevin Buzzard]

I don't understand this question. A groupoid structure on a type extends a category structure and groupoid is a class, so {G : groupoid C} is not using the definition in the way it was designed and "I'm trying to put a category structure on a groupoid" is like saying "I'm trying to put a multiplication structure on a group" -- it's already there.

[Kevin Buzzard]

It's like saying "I let G be a group and now there's this multiplication which I wanted to define myself". If you want to define the structure yourself you don't say "let G be a group" you say "let's define multiplication on G this way" and then you build the group instance yourself. variable {G : groupoid C} means "let's choose a random category and groupoid structure on C (and let's add to the confusion by not telling the typeclass inference system about it)"

[Yaël Dillies]

I believe there really is a case for using groupoid C as a type on itself and perform operations on it, but do know that this will be an excursion out of the tracks and don't expect the usual tactics to work.

[Yaël Dillies]

The design-better thing to do would be to define groupoid' C which will be exactly the same as groupoid C except that it's not a class, but you can see how that leads to unwanted code duplication.

[Yaël Dillies]

Note that this is still what we've been doing in other places. See docs#add_group_seminorm vs docs#normed_add_comm_group.

[Yaël Dillies]

I guess there's still a tradeoff we can do to avoid that duplication. Namely everything that works with a single canonical structure should be stated with the class one, while everything that needs noncanonical structures should be stated with the structure one.

[Rémi Bottinelli]

Mmh, well, that becomes more complicated than I would have expected.

[Rémi Bottinelli]

Oh, and the name was misleading… the kernel is a subgroupoid, and that works fine with my definitions.

But then:

1. Assuming I add a groupoid' C structure, won't I also need a category' C structure, since e.g. in the current case, it's the category instance that's causing me troubles?
2. What would a mathlib-blessed approach be? I'd like to get all this basic groupoid stuff merged eventually, so better start with a compatible way.

[Reid Barton]

I think the question was intended simply as: what do you mean by "kernel groupoid"?

[Rémi Bottinelli]

Reid Barton said:

I think the question was intended simply as: what do you mean by "kernel groupoid"?

Re the question in letter: I got my names mixed up, and by "kernel groupoid": I really mean the subgroupoid of arrows mapping to identity arrows. And in this case I have no problem with instances.

Re the question in spirit: The MWE was meant to be about e.g. taking a quotient groupoid as in Higgin's papers where the underlying vertex set is fixed, and in this case the problem remains.

[Reid Barton]

OK this is some strange non-equivalence-invariant notion.

[Reid Barton]

Anyways the usual approach would be to make a type synonym (or structure) ker φ : Type* and put the new category/groupoid instance on that instead.

[Rémi Bottinelli]

Reid Barton said:

OK this is some strange non-equivalence-invariant notion.

Can you expand on this?

[Reid Barton]

If C is a contractible groupoid (with a unique morphism between every pair of objects, and with at least one object) then the kernel of the identity functor is of course just the subgroupoid consisting of all the objects of C and their identity morphisms; and this depends on the set of objects of C even though any two contractible groupoids are equivalent.

[Reid Barton]

Basically, "being an identity morphism" is not equivalence-invariant