A cone functor preserves shifts #
DGFunctor.PreservesShifts and PreservesChosenCones are the two dg-level
capabilities from which H⁰ F is triangulated. Both are now available for
every dg functor. This file retains the more structured cone-functor proofs:
they compute the witnesses from the two endpoints and expose the block-matrix
argument used by adjunction-cone consumers.
The retained coordinate calculation for cone functors shows directly how
Cone(α) acts on a supplied shift when α : F ⟶ G is closed of degree
zero. The public preservation witness itself delegates to the generic
DGFunctor.preservesShifts theorem; the calculation remains useful for its
explicit coordinates.
The proof is the splitting, not a computation #
A morphism into a cone splits uniquely along inl and inr
(IsConeOf.bijective), and right composition with the cone lift respects that
splitting: inl picks up (-1)^p times the F-component
(inl_comp_homogeneousLift_strict) and inr picks up the G-component
(inr_comp_homogeneousLift). So right composition with Cone(α).map (-n) s.hom
is, through the splitting, the product of right composition with
F.map (-n) s.hom and with G.map (-n) s.hom, up to a sign on the first
factor. Both of those are bijective because F and G preserve shifts, and a
sign is a unit, so the product is bijective.
No property of α beyond being a closed degree-zero transformation is used, and
the argument never touches the differential.
Both halves #
preservesChosenCones is the other one: the 3-by-3 lemma, in the strict form
the capability asks for. Its proof has the same shape with four factors instead
of two, and the point is that in those coordinates the map is block diagonal
rather than merely triangular.
With both, H⁰ (Cone α) is a triangulated functor. For the twist candidate of
a dg adjunction that is exactness, and it is what the word "twist" is supposed
to mean once the twist/cotwist conditions make it an equivalence.
What this does not give #
Nothing about sphericality. Exactness and invertibility of the twist are two of Anno--Logvinenko's conditions, not all four, and the implication from the recorded pair to the rest needs Morita quasi-functors.
Right composition with the cone lift, read through the splitting.
A morphism into Cone(α) X of degree p is a ≫ inl + b ≫ inr; composing on
the right with Cone(α).map (-n) s.hom sends it to the same expression built
from a ≫ F.map (-n) s.hom and b ≫ G.map (-n) s.hom, with the sign
(-1)^(-n) on the first. That sign is inl_comp_homogeneousLift_strict's and
nothing more.
A cone functor preserves shifts.
Kept for the name and for dot notation on ConeData; the content is
DGFunctor.preservesShifts, which holds for every dg functor because a shift
element is a closed two-sided invertible element and functors preserve
invertibility. The cone splitting plays no part, and the two PreservesShifts
arguments this used to take are gone -- there is nothing for a caller to
supply.
preservesChosenCones below retains its two endpoint arguments as a structured
constructor, although DGFunctor.preservesChosenCones K.functor supplies the
same capability without them.
Equations
Instances For
Cones #
The second capability. A cone of f in the source goes to a cone of
Cone(α)(f), so a cone functor preserves chosen cones when its two ends do.
The argument is the same shape as for shifts, with four factors instead of
two. A morphism into Cone(α) Z splits along the Z-cone of α into an
F Z part and a G Z part, and each of those splits again along the image
under F or G of the cone of f. A pair of morphisms into Cone(α) X and
Cone(α) Y splits along the X- and Y-cones of α into the same four
groups, in a different order. In those coordinates the map is block
diagonal, not merely triangular: the F block is the cone splitting F
supplies and the G block is the one G supplies, with a single sign on one
factor coming from inl_comp_homogeneousLift_strict.
The cone splitting of Cone(α), in coordinates.
Both inclusions of the cone of Cone(α)(f) are computed on a morphism already
split along the X- and Y-cones of α. The result is split along the
Z-cone of α, and each component is the corresponding cone splitting of F
or of G.
A cone functor preserves chosen cones.
The 3-by-3 lemma, in the strict dg form the capability asks for. Both
inclusions of the image cone are the images of the inclusions, and the
splitting is coneSplit_functor_map: in the four coordinates the map is block
diagonal, with the F block and the G block the cone splittings that F and
G supply.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The twist candidate preserves shifts.
Unconditional, because every dg functor does. The adjacent 3-by-3 constructor retains the endpoint witnesses in order to expose how the cone functor acts in split coordinates; the generic dg-functor constructor makes them optional to later exactness consumers.
Equations
Instances For
The twist candidate preserves chosen cones. The 3-by-3 lemma applied
to the counit's cone: with preservesShifts this is full dg-level exactness
data for the twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit cone preserves chosen cones too.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit cone preserves shifts too, and equally unconditionally.