Kernels from torsor squares of group objects #
If the kernel pair of q : G ⟶ Q is G × N, with its two maps given by
(g, n) ↦ g and (g, n) ↦ g i(n), then i : N ⟶ G is the categorical
kernel of q. This criterion applies in any cartesian monoidal category, in particular
to group objects in sheaves, without assuming that quotient sections lift globally.
theorem
CategoryTheory.Grp.comp_eq_zero_of_commSq
{C : Type u_1}
[Category.{u_2, u_1} C]
[CartesianMonoidalCategory C]
{N G Q : Grp C}
(i : N ⟶ G)
(q : G ⟶ Q)
(h :
CommSq (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)
:
Commutativity of a torsor square forces the subgroup map to have trivial composite with the projection.
noncomputable def
CategoryTheory.Grp.isLimitKernelForkOfIsPullback
{C : Type u_1}
[Category.{u_2, u_1} C]
[CartesianMonoidalCategory C]
{N G Q : Grp C}
(i : N ⟶ G)
(q : G ⟶ Q)
(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)
:
The subgroup in a torsor kernel-pair square is the categorical kernel of the projection.
Equations
- One or more equations did not get rendered due to their size.