Zulip Chat Archive

Stream: new members

Topic: Dependent map on quotient: closing the `eq.rec` goal?


Rémi Bottinelli (Sep 19 2022 at 10:19):

I'm trying to define the quotient of a groupoid by a normal subgroupoid below (following Bourbaki's Topologie Algébrique), and to do so I need first to define the vertices as a quotient, and then the arrows as another one (see below). I'm getting into troubles when trying to define the identity and composition morphisms, since their types depend on the element(s) on which they are defined.
quot.rec seems to be the correct way to proceed, but then I get stuck trying to prove the "soundness" of my recursion, which involves an eq.rec. Am I off-base, or missing something?
Note that for the identity morphism, I can get around this problem since I can first define a non-dependent lift, but it's not really "pretty" and wouldn't work for the composition without ugly tricks, I believe.

Thanks!

import category_theory.groupoid

open set

namespace category_theory

universes u v

variables {C : Type u}

namespace groupoid

section subgroupoid

variable (G : groupoid C)

@[ext]
structure subgroupoid :=
  (arrws :  (c d : C), set (G.hom c d))
  (inv' :  {c d} {p : G.hom c d} (hp : p  arrws c d),
            groupoid.inv p  arrws d c)
  (mul' :  {c d e} {p} (hp : p  arrws c d) {q} (hq : q  arrws d e),
            p  q  arrws c e)

variable {G}

def is_normal (S : subgroupoid G) : Prop :=
  ( c, (𝟙 c)  (S.arrws c c))   -- S is "wide": all vertices of G are covered
  ( {c d} (p : c  d) (γ : c  c) (hs : γ  S.arrws c c), ((G.inv p)  γ  p)  (S.arrws d d))


end subgroupoid


section quotient

-- The vertices of the quotient of G by S
def quot_v [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :=
  (quot (λ (c d : C), (S.arrws c d).nonempty))


def quot_v.mk [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) (c : C) : quot_v S Sn:=
  (quot.mk (λ (c d : C), (S.arrws c d).nonempty) c)

def conj  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :
  (Σ (a b : C), a  b)  (Σ (a b : C), a  b)  Prop :=
begin
  rintros a,b,f c,d,g⟩,
  exact  (α  S.arrws a c) (β  S.arrws d b), f = α  g  β
end

@[refl]
lemma conj.refl [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :  F, conj S Sn F F :=
begin
  rintro a,b,f⟩,
  use [(𝟙 a), Sn.left a, (𝟙 b), Sn.left b],
  simp only [category.comp_id, category.id_comp],
end

@[symm]
lemma conj.symm [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :  F G, conj S Sn F G  conj S Sn G F :=
begin
  rintros a,b,f c,d,g α,,β,,rfl⟩,
  use [G.inv α, S.inv' , G.inv β, S.inv' ],
  simp only [category.assoc, comp_inv, category.comp_id],
  rw category.assoc,
  simp only [inv_comp, category.id_comp],
end

@[trans]
lemma conj.trans [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :
   F G H, conj S Sn F G  conj S Sn G H  conj S Sn F H :=
begin
  rintros a₀,b₀,f₀ a₁,b₁,f₁ a₂,b₂,f₂ α₀,hα₀,β₀,hβ₀,rfl  α₁,hα₁,β₁,hβ₁,rfl⟩,
  use [α₀  α₁, S.mul' hα₀ hα₁, β₁  β₀, S.mul' hβ₁ hβ₀],
  simp only [category.assoc],
end

def quot_start [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : (quot $ conj S Sn)  (quot_v S Sn) :=
begin
  refine quot.lift _ _,
  { rintro a,b,f⟩, apply quot_v.mk, exact a,},
  { rintro a₀,b₀,f₀ a₁,b₁,f₁ α,,β,,rfl⟩,simp,dsimp [quot_v.mk], apply quot.sound, exact α,⟩,}
end

def quot_end [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : (quot $ conj S Sn)  (quot_v S Sn) :=
begin
  refine quot.lift _ _,
  { rintro a,b,f⟩, apply quot_v.mk, exact b,},
  { rintro a₀,b₀,f₀ a₁,b₁,f₁ α,,β,,rfl⟩,simp,dsimp [quot_v.mk], apply quot.sound, exact G.inv β,S.inv' ⟩,}
end

@[instance]
def quotient_quiver [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :
  quiver (quot_v S Sn) := λc d, { F | quot_start S Sn F = c  quot_end S Sn F = d }⟩

def quot_id'  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : Π (c : quot_v S Sn),  (quot $ conj S Sn) :=
begin
  apply quot.lift, rotate,
  { rintro c,
    exact quot.mk (conj S Sn) c,c,𝟙 c },
  { rintros c d f,fS⟩,
    apply quot.sound,
    use [f,fS,G.inv f, S.inv' fS],
    simp only [category.id_comp, comp_inv], }
end

def quotient_id  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : Π (c : quot_v S Sn),  c  c :=
λ c,  quot_id' S Sn c, by {dsimp only [quot_id',quot_start,quot_end,quot_v.mk], induction c, simp, simp,}⟩


def quot_id''  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : Π (c : quot_v S Sn),  c  c :=
begin
  refine λ c, c.rec_on _ _,
  { rintro c, dsimp only [quotient_quiver,quot_start,quot_end,quot_v.mk],
    use quot.mk (conj S Sn) c,c,𝟙 c⟩, split, simp only, simp only, },
  { rintros c d f,fS⟩,
    have : quot.mk (λ (c d : C), (S.arrws c d).nonempty) c = quot.mk (λ (c d : C), (S.arrws c d).nonempty) d, by
    { apply quot.sound, constructor, use fS,},
    simp,
    sorry,
    }
end


def quot_comp'  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : Π (c d e : quot_v S Sn), (c  d)  (d  e)  (quot $ conj S Sn) :=
begin
  sorry
end


end quotient


end groupoid
end category_theory

Junyan Xu (Sep 24 2022 at 04:00):

Several comments:

  • Since you've shown that conj is reflexive, symmetric and transitive, you may package them into a docs#setoid instance, and then you can use quotient instead of quot, which allows you access to theorems like docs#quotient.exact that isn't true if the relation you quotient by is not an equivalence relation.
  • When defining data, we usually don't destruct an input; instead we use its projections. For example, conj should be defined as λ f g, ∃ (α ∈ S.arrws f.1 g.1) (β ∈ S.arrws g.2.1 f.2.1), f.2.2 = α ≫ g.2.2 ≫ β, and the same applies to quot_start and quot_end; in proofs we don't care though.
  • I think the way you construct quot_id and quotient_id is perfectly fine. Not sure why you want to try the approach in quot_id''. The use of quot.rec_on seems exactly what introduces eq.rec that's hard to deal with.
  • In order to define quot_comp', I would take the following approach: first convert (c ⟶ d) and (d ⟶ e) which are subtypes of quotient types into quotient types of subtypes using docs#equiv.subtype_quotient_equiv_quotient_subtype, then use quotient.lift₂. You would still need to use choice to pick an arrow from (S.arrws _ _).nonempty to connect the two lifts of d, but this is the best solution I can think of.

Junyan Xu (Sep 24 2022 at 04:22):

I think it may be easier to simply define the types of arrows in the quotient groupoid as quotients rather than subtypes of quotients; I believe the following is also a valid definition:

def conj' [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) (a b : quot_v S Sn)
  (f g : Σ (c : {c // quot.mk _ c = a}) (d : {d // quot.mk _ d = b}), c.1  d.1) : Prop :=
 (α  S.arrws f.1.1 g.1.1) (β  S.arrws g.2.1.1 f.2.1.1), f.2.2 = α  g.2.2  β

def quotient_quiver [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :
  quiver (quot_v S Sn) := λ a b, quot (conj' S Sn a b)⟩

Rémi Bottinelli (Sep 24 2022 at 10:25):

Thanks for the feedback.
As for your third bullet: It's mostly because I felt that I'd have to deal with this problem of quot.rec_on/eq.rec with quot_comp anyway, and since id is easier than comp, it would help me figure out how to deal with that.
As for your proposal, I thought about something along these lines but couldn't tell if it was useful. Do we agree that your proposal takes care of the conversion mentioned in bullet 4 already?

Rémi Bottinelli (Sep 24 2022 at 11:02):

But as far as I understand, I can't simply do quotient.lift₂, because the lift needs to have a dependent codomain, so only quot.rec works here.

Kyle Miller (Sep 24 2022 at 15:46):

@Rémi Bottinelli I haven't dealt with the composition problem, but I have some suggestions for handling the groupoid structure and how to organize taking the vertex quotient

import category_theory.groupoid

open set

namespace category_theory

universes u v

variables (C : Type u)

namespace groupoid

section subgroupoid

variable [groupoid C]

@[ext]
structure subgroupoid (C : Type u) [groupoid C] :=
(arrws :  (c d : C), set (c  d))
(inv' :  {c d} {p : c  d} (hp : p  arrws c d),
          groupoid.inv p  arrws d c)
(mul' :  {c d e} {p} (hp : p  arrws c d) {q} (hq : q  arrws d e),
          p  q  arrws c e)

variable {C}

namespace subgroupoid

structure is_normal (S : subgroupoid C) : Prop :=
(wide :  c, 𝟙 c  S.arrws c c)  -- S is "wide": all vertices of G are covered
(conj {c d} (p : c  d) (γ : c  c) (hs : γ  S.arrws c c) :
  groupoid.inv p  γ  p  S.arrws d d)

lemma is_normal.arrws_nonempty_refl {S : subgroupoid C} (Sn : S.is_normal) (c : C) :
  (S.arrws c c).nonempty :=
𝟙 c, Sn.wide c

lemma is_normal.arrws_nonempty_symm {S : subgroupoid C} (Sn : S.is_normal)
  {c d : C} : (S.arrws c d).nonempty  (S.arrws d c).nonempty :=
by { rintro f, hf⟩, exact groupoid.inv f, S.inv' hf }

lemma is_normal.arrws_nonempty_trans {S : subgroupoid C} (Sn : S.is_normal)
  {c d e : C} : (S.arrws c d).nonempty  (S.arrws d e).nonempty  (S.arrws c e).nonempty :=
by { rintro f, hf g, hg⟩, exact f  g, S.mul' hf hg }

def is_normal.arrws_nonempty_setoid {S : subgroupoid C} (Sn : S.is_normal) : setoid C :=
{ r := λ c d, (S.arrws c d).nonempty,
  iseqv := Sn.arrws_nonempty_refl,
            λ c d, Sn.arrws_nonempty_symm,
            λ c d e, Sn.arrws_nonempty_trans }

end subgroupoid

end subgroupoid

section quotient
variables {C} [groupoid C] (S : subgroupoid C) (Sn : S.is_normal)

-- The vertices of the quotient of G by S
@[reducible] def subgroupoid.quot_v := quotient Sn.arrws_nonempty_setoid

def subgroupoid.quot_v_mk (c : C) : S.quot_v Sn := quotient.mk' c

namespace subgroupoid

/-- We don't need Sn in the definition, but it makes it inferrable where it is needed. -/
def conj (Sn : S.is_normal) : (Σ (a b : C), a  b)  (Σ (a b : C), a  b)  Prop
| a, b, f c, d, g :=  (α  S.arrws a c) (β  S.arrws d b), f = α  g  β

@[refl]
lemma conj.refl :  F, S.conj Sn F F :=
begin
  rintro a,b,f⟩,
  use [𝟙 a, Sn.wide a, 𝟙 b, Sn.wide b],
  simp only [category.comp_id, category.id_comp],
end

@[symm]
lemma conj.symm :  F G, S.conj Sn F G  S.conj Sn G F :=
begin
  rintros a,b,f c,d,g α,,β,,rfl⟩,
  use [groupoid.inv α, S.inv' , groupoid.inv β, S.inv' ],
  simp only [category.assoc, comp_inv, category.comp_id],
  rw category.assoc,
  simp only [inv_comp, category.id_comp],
end

@[trans]
lemma conj.trans :  F G H, conj S Sn F G  conj S Sn G H  conj S Sn F H :=
begin
  rintros a₀,b₀,f₀ a₁,b₁,f₁ a₂,b₂,f₂ α₀,hα₀,β₀,hβ₀,rfl  α₁,hα₁,β₁,hβ₁,rfl⟩,
  use [α₀  α₁, S.mul' hα₀ hα₁, β₁  β₀, S.mul' hβ₁ hβ₀],
  simp only [category.assoc],
end

def conj_setoid : setoid (Σ (a b : C), a  b) :=
{ r := S.conj Sn,
  iseqv := conj.refl _ _, λ _ _, conj.symm _ _ _ _, λ _ _ _, conj.trans _ _ _ _ _ }

@[reducible] def quot_conj := quotient (S.conj_setoid Sn)

def quot_conj_mk {a b : C} (f : a  b) : S.quot_conj Sn := quotient.mk' a, b, f

namespace quot_conj
variables {S} {Sn}

protected def start : S.quot_conj Sn  S.quot_v Sn :=
quotient.map' (λ f, f.1) begin
  rintro a₀,b₀,f₀ a₁,b₁,f₁ α,,β,,rfl⟩,
  exact α, ⟩,
end

protected def «end»  : S.quot_conj Sn  S.quot_v Sn :=
quotient.map' (λ f, f.2.1) begin
  rintro a₀,b₀,f₀ a₁,b₁,f₁ α,,β,,rfl⟩,
  exact groupoid.inv β, S.inv' ⟩,
end

end quot_conj

@[simp]
lemma start_mk_eq {a b : C} (f : a  b) : (S.quot_conj_mk Sn f).start = S.quot_v_mk Sn a := rfl

@[simp]
lemma end_mk_eq {a b : C} (f : a  b) : (S.quot_conj_mk Sn f).end = S.quot_v_mk Sn b := rfl

instance quot_quiver : quiver (S.quot_v Sn) :=
λ c d, { F : S.quot_conj Sn | F.start = c  F.end = d }⟩

def quot_id (c : quot_v S Sn) : c  c :=
quotient.lift_on' c (λ c', S.quot_conj_mk Sn (𝟙 c')) begin
  rintro a b f, hf⟩,
  apply quotient.sound',
  use [f, hf, groupoid.inv f, S.inv' hf],
  simp only [category.id_comp, comp_inv],
end, by exact quotient.ind' (λ _, rfl, rfl⟩) c

def quot_comp {c d e : quot_v S Sn} : (c  d)  (d  e)  (c  e) :=
begin
  -- should do in a different way
  letI := Sn.arrws_nonempty_setoid,
  refine quotient.rec (λ c', _) _ c,
  refine quotient.rec (λ d', _) _ d,
  refine quotient.rec (λ e', _) _ e,
  rintro f, hf g, hg⟩,
  sorry
end


end subgroupoid
end quotient

end groupoid
end category_theory

Kyle Miller (Sep 24 2022 at 15:50):

I think Junyan's correct about how the main difficulty is in subtypes of quotients vs quotients of subtypes. It might help to make custom lift functions to deal with dependent types from the objects.

Rémi Bottinelli (Sep 24 2022 at 17:05):

Thanks for the cleaned-up code. I tried commuting quotients and subtype here but as far as I can tell, it doesn't help with the fact that I need a dependent function.

Junyan Xu (Sep 25 2022 at 03:22):

@Rémi Bottinelli Here's a full construction of the composition, which should be inserted after

def subgroupoid.quot_v_mk
namespace subgroupoid

in Kyle's code (thanks!). I use my own definition of quotient_quiver to be able to apply quot.lift₂ directly. Surely the resulting type c ⟶ e depends on c and e, but it's still the same type for different choice of elements of the input types c ⟶ d and d ⟶ e, so quot.lift works without problem. (With your original definition of quotient_quiver, the situation is in some sense better, since you're constructing an element in a subtype of a type that doesn't even depend on c and e, however needing to convert from subtype of quotient to quotient of subtype makes it unpleasant to work with.) I might open a PR to put everything about inv into category_theory.groupoid.

def conj {a b c d : C} (f : a  b) (g : c  d) : Prop :=
 (α  S.arrws a c) (β  S.arrws d b), f = α  g  β

attribute [reassoc] inv_comp comp_inv -- groupoid

lemma conj.refl {a b : C} (f : a  b) : S.conj f f := _, Sn.wide _, _, Sn.wide _, by simp

lemma conj.symm {a b c d : C} (f : a  b) (g : c  d) : S.conj f g  S.conj g f :=
λ α, , β, , he⟩, _, S.inv' , _, S.inv' , by simp [he]⟩

lemma conj_comm {a b c d : C} (f : a  b) (g : c  d) : S.conj f g  S.conj g f :=
conj.symm S f g, conj.symm S g f

lemma conj.trans {a b c d e f : C} (g : a  b) (h : c  d) (i : e  f) :
  S.conj g h  S.conj h i  S.conj g i :=
λ α₁, hα₁, β₁, hβ₁, he₁ α₂, hα₂, β₂, hβ₂, he₂⟩,
  _, S.mul' hα₁ hα₂, _, S.mul' hβ₂ hβ₁, by simp [he₁, he₂]⟩

def conj_setoid (a b : quot_v S Sn) :
  setoid (Σ (c : {c // quot.mk _ c = a}) (d : {d // quot.mk _ d = b}), c.1  d.1) :=
{ r := λ f g, S.conj f.2.2 g.2.2,
  iseqv := λ _, conj.refl _ Sn _, λ _ _, conj.symm _ _ _, λ _ _ _, conj.trans _ _ _ _ }

lemma conj_comp {a b c d e : C} (f : a  b) (g : c  d) {h : d  e} (hS : h  S.arrws d e) :
  S.conj f (g  h)  S.conj f g :=
λ α, , β, , he⟩, α, , h  β, S.mul' hS , by simp [he]⟩,
 λ α, , β, , he⟩, α, , inv h  β, S.mul' (S.inv' hS) , by simp [he]⟩⟩

lemma conj_comp' {a b c d e : C} (f : a  b) (g : c  d) {h : e  c} (hS : h  S.arrws e c) :
  S.conj f (h  g)  S.conj f g :=
λ α, , β, , he⟩, α  h, S.mul'  hS, β, , by simp [he]⟩,
 λ α, , β, , he⟩, α  inv h, S.mul'  (S.inv' hS), β, , by simp [he]⟩⟩

@[simp] lemma inv_inv {a b : C} (f : a  b) : inv (inv f) = f :=
by rw [ category.comp_id (inv (inv f)),  inv_comp f, inv_comp_assoc]

lemma conj_congr_left {a b c d : C} (f₁ : a  c) (f₂ : b  c) (g : c  d) (h : S.conj f₁ f₂) :
  S.conj (f₁  g) (f₂  g) :=
let α, , β, , he := h in α, , _, Sn.conj g _ , by simp [he]⟩

lemma conj_congr_right {a b c d : C} (f : a  b) (g₁ : b  c) (g₂ : b  d) (h : S.conj g₁ g₂) :
  S.conj (f  g₁) (f  g₂) :=
let α, , β, , he := h in _, Sn.conj (groupoid.inv f) _ , β, , by simp [he]⟩

@[instance]
def quotient_quiver : quiver (quot_v S Sn) := λ a b, quotient (conj_setoid S Sn a b)⟩

noncomputable def quot_comp {c d e : quot_v S Sn} : (c  d)  (d  e)  (c  e) :=
begin
  let sm := @nonempty.some_mem,
  refine quot.lift₂ (λ f g, quot.mk _ _) (λ f g₁ g₂ h, _) (λ f₁ f₂ g h, _),
  { letI := Sn.arrws_nonempty_setoid,
    exact _, _, f.2.2  (quotient.exact $ f.2.1.2.trans g.1.2.symm).some  g.2.2 },
  all_goals { apply quot.sound, dsimp only [conj_setoid] },
  { apply S.conj_congr_right Sn,
    rw [S.conj_comp' _ _ (sm _), conj_comm, S.conj_comp' _ _ (sm _), conj_comm],
    exact h },
  { simp only [ category.assoc],
    apply S.conj_congr_left Sn,
    rw [S.conj_comp _ _ (sm _), conj_comm, S.conj_comp _ _ (sm _), conj_comm],
    exact h },
end

Junyan Xu (Sep 25 2022 at 03:57):

Oh I see you actually added four lemmas about groupoids in the free groupoid PR. I think the best thing to do is to first show that groupoid.inv = docs#category_theory.inv, and use the latter everywhere (we already has the is_iso instance), to avoid duplicating the API (docs#category_theory.is_iso.inv_comp etc. already exist). So we should probably open category_theory but not open groupoid (or hide groupoid.inv) to be able to simply write inv.

Junyan Xu (Sep 25 2022 at 05:47):

see PR #16624

Rémi Bottinelli (Sep 25 2022 at 05:55):

Thanks a lot! Looking forward to see what I was misunderstanding exactly.

Rémi Bottinelli (Sep 27 2022 at 14:26):

I think I'm being stupid, but actually, following your approach to the quotient, I feel like now defining id becomes problematic. How would you do it?

Junyan Xu (Sep 27 2022 at 18:19):

The easy way is to use choice:

noncomputable def quot_id (c : quot_v S Sn) : c  c :=
quot.mk _ ⟨⟨_, quot.out_eq c⟩, _, quot.out_eq c⟩, 𝟙 _

or you could also do it computably (albeit more complicated, and I have to adjust the sigma type to a subtype in order to use docs#subtype_quotient_equiv_quotient_subtype):

def sigma_conj_setoid (a b : quot_v S Sn) : setoid (Σ c d : C, c  d) :=
{ r := λ f g, S.conj f.2.2 g.2.2,
  iseqv := λ _, conj.refl _ Sn _, λ _ _, conj.symm _ _ _, λ _ _ _, conj.trans _ _ _ _ }

def conj_setoid' (a b : quot_v S Sn) :
  setoid {f : Σ c d : C, c  d // quot.mk _ f.1 = a  quot.mk _ f.2.1 = b} :=
{ r := λ f g, S.conj f.1.2.2 g.1.2.2,
  iseqv := λ _, conj.refl _ Sn _, λ _ _, conj.symm _ _ _, λ _ _ _, conj.trans _ _ _ _ }
-- setoid.comap coe (sigma_conj_setoid S Sn a b) -- need import data.setoid.basic

@[instance]
def quotient_quiver : quiver (quot_v S Sn) := λ a b, quotient (conj_setoid' S Sn a b)⟩

def quot_id (c : quot_v S Sn) : c  c :=
begin
  refine @equiv.subtype_quotient_equiv_quotient_subtype _ _ (sigma_conj_setoid S Sn c c)
    (conj_setoid' S Sn c c) (quot.lift _ $ λ f g h, _) (λ _, iff.rfl) (λ f g, iff.rfl) _,
  { obtain a, ha, b, hb, - := h, congr' 2; apply quot.sound, exacts [⟨a, ha⟩, _, S.inv' hb⟩] },
  { refine quot.lift (λ c, quot.mk _ _) (λ d e h, _) c, _⟩, { exact c, c, 𝟙 c },
    { obtain a, ha := h, refine quot.sound a, ha, _, S.inv' ha, by simp },
    { rcases c, exacts rfl, rfl } },
end

/- and you get nice defeq: -/
lemma quot_id_eq (c : C) : quot_id S Sn (quot_v_mk S Sn c) = quot.mk _ ⟨⟨c, c, 𝟙 c⟩, rfl, rfl := rfl

Junyan Xu (Sep 27 2022 at 18:21):

Sorry I haven't got a chance to look at your new free groupoid PR carefully yet, but I agree with Joël's comment there.

Rémi Bottinelli (Sep 28 2022 at 09:37):

Junyan Xu said:

Sorry I haven't got a chance to look at your new free groupoid PR carefully yet, but I agree with Joël's comment there.

No worry, I'm trying to finish the quotient construction in the meantime. It's at the edge of my lean abilities, so I'm advancing very slowly!

Rémi Bottinelli (Oct 02 2022 at 07:56):

Actually, I think I found a probably easier way to deal with the quotient:
If N is a normal subgroupoid, one should be able to decompose it into V * G where V consists only of the vertex groups of N, and G has at most one arrow per pair of vertices. One can then quotient first by N and then by G:

  • Quotienting by N preserves the vertices, so we only need to quotient edges.
  • Quotienting then by G preserves arrows: we're just bunching groups together corresponding to squashing vertices.

So, both definitions should be relatively transparent, and they're actually useful by their own I believe.


Last updated: Dec 20 2023 at 11:08 UTC