Cokernels from torsor squares #
An effective epimorphism of group objects whose kernel pair is the translation action of a subgroup is the cokernel of that subgroup's inclusion. The descent of the underlying morphism preserves multiplication when the square of the quotient map is epi. This criterion applies to group objects in sheaves, including quotients which are not representable.
The construction uses Mathlib's isColimitCoforkOfEffectiveEpi to descend morphisms of carriers.
noncomputable def
CategoryTheory.Grp.isColimitCokernelCoforkOfTorsor
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{N G Q : Grp C}
(i : N ⟶ G)
(q : G ⟶ Q)
(w : CategoryStruct.comp i q = 0)
(h :
IsPullback (SemiCartesianMonoidalCategory.fst G.X N.X)
(SemiCartesianMonoidalCategory.fst G.X N.X * CategoryStruct.comp (SemiCartesianMonoidalCategory.snd G.X N.X) i.hom.hom)
q.hom.hom q.hom.hom)
[EffectiveEpi q.hom.hom]
[Epi (MonoidalCategoryStruct.tensorHom q.hom.hom q.hom.hom)]
:
A torsor projection which is effective epi on carriers is the cokernel of its subgroup inclusion, provided its product with itself is epi.
Equations
- One or more equations did not get rendered due to their size.