Recognising colimits and limits of shape SingleObj G #
A functor J : SingleObj G ⥤ C is an object of C with an action of the monoid G, and its
colimit, when it exists, is the object of coinvariants of that action, and its limit the object of
invariants. This file gives two criteria for a given cocone to be that colimit, and, in the
preadditive setting, the dual criterion for a given cone to be that limit.
In types, for a group G, Mathlib computes the colimit as the quotient by the action
(CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient). Correspondingly, a cocone over
J : SingleObj G ⥤ Type u is a colimit exactly when its leg is surjective and its fibres are the
orbits of the action (CategoryTheory.Limits.SingleObj.Types.nonempty_isColimit_iff).
In a preadditive category, for a finite monoid G, suppose a cocone π : J.obj * ⟶ c.pt has a
transfer: a morphism t : c.pt ⟶ J.obj * back, with t ≫ π = |G| • 𝟙 and
π ≫ t = ∑_{g ∈ G} J.map g. If multiplication by |G| is invertible on both objects, then c is
a colimit (CategoryTheory.Limits.SingleObj.isColimitOfTransfer): the averaged transfer
|G|⁻¹ • t is a section of π whose composite with π is the averaging idempotent. The
hypotheses are equations between morphisms, so every additive functor preserves them and hence
preserves this colimit (CategoryTheory.Limits.SingleObj.isColimitMapCoconeOfTransfer). This is
the formal reason why, for a finite covering with deck group G and coefficients in which |G|
is invertible, the homology of the base is the coinvariants of the homology of the total space.
For the infinite cyclic group, the coinvariants are a cokernel: if ℤ acts on an object of a
preadditive category with generator acting by t, a colimit cocone over the action is a cokernel
of 𝟙 - t (CategoryTheory.Limits.SingleObj.isColimitCokernelCoforkOfIsColimit). For an
infinite cyclic covering, this presents the chains of the base as a cokernel.
Dually, a cone over the action whose leg t : c.pt ⟶ J.obj * has a morphism p : J.obj * ⟶ c.pt
back, with t ≫ p = |G| • 𝟙 and p ≫ t = ∑_{g ∈ G} J.map g, is a limit cone when |G| is
invertible on both objects (CategoryTheory.Limits.SingleObj.isLimitOfTransfer), and every
additive functor preserves this limit (CategoryTheory.Limits.SingleObj.isLimitMapConeOfTransfer).
This is why the transfer identifies the homology of the base with the invariants of the homology of
the total space.
References #
- A. Hatcher, Algebraic Topology, Section 3.G, Proposition 3G.1, for the averaging argument with the transfer.
A cocone over J : SingleObj G ⥤ Type u is a colimit if and only if its leg is surjective
and identifies two elements exactly when they lie in the same orbit of the action of G.
A cocone over J : SingleObj G ⥤ Type u whose leg is surjective, and identifies two elements
only when they lie in the same orbit of the action of G, is a colimit.
Instances For
Let G be a finite monoid acting on an object of a preadditive category, and let c be a
cocone over the action whose leg π has a transfer t: t ≫ π = |G| • 𝟙 and
π ≫ t = ∑_{g ∈ G} J.map g. If multiplication by |G| is invertible on the acted-on object and on
the cocone point, then c is a colimit cocone: the cocone point is the object of coinvariants.
Instances For
The colimit of CategoryTheory.Limits.SingleObj.isColimitOfTransfer is preserved by every
additive functor: under the same hypotheses, every additive functor sends c to a colimit
cocone.
Instances For
A morphism out of an object with an action of ℤ that is invariant under the generator is
invariant under the whole action.
Coinvariants of an action of ℤ are a cokernel. For an action of ℤ on an object of a
preadditive category, whose generator acts by t, a colimit cocone is a cokernel of 𝟙 - t.
Instances For
Let G be a finite monoid acting on an object of a preadditive category, and let c be a
cone over the action whose leg t has a projection p back with t ≫ p = |G| • 𝟙 and
p ≫ t = ∑_{g ∈ G} J.map g. If multiplication by |G| is invertible on the acted-on object and on
the cone point, then c is a limit cone: the cone point is the object of invariants.
Instances For
The limit of CategoryTheory.Limits.SingleObj.isLimitOfTransfer is preserved by every
additive functor: if c and p satisfy its transfer identities, then every additive functor F
for which multiplication by |G| is invertible on the images of the acted-on object and of the
cone point sends c to a limit cone.