The triangle of H⁰ attached to a closed dg natural transformation #
HomogeneousNatTrans.ConeData chooses a dg cone of every component of a closed
degree-zero dg natural transformation α : F ⟶ G. Each choice gives a
distinguished triangle of H⁰ D,
F X ⟶ G X ⟶ Cone(α) X ⟶ (F X)⟦1⟧,
and this file says those triangles are functorial in X.
Why this is not automatic #
The three vertices are functorial separately: F.h0, G.h0 and
ConeData.functor.h0 are ordinary functors H⁰ C ⥤ H⁰ D. What has to be
supplied is that a morphism of H⁰ C induces a morphism of triangles, and
the third square of a triangle morphism involves the connecting map and the
chosen shift of H⁰ D. That square is the one IsConeOf.Morphism was built
to carry, so the work here is to produce a cone morphism from a cocycle of C
and hand it to IsConeOf.Morphism.toTriangleMorphism.
Producing it needs three naturality statements that already exist and no new computation:
- the square on the first two vertices is graded naturality of
αat degree zero, where the Koszul sign is+1, so the square is strict and the homotopy is zero; - the square on the cone inclusions is naturality of
ConeData.inr; - the square on the cone projections is naturality of
ConeData.fst, whose degree-one sign(-1)^(1 * 0)is also+1.
The homotopy class, not the representative #
A morphism of H⁰ C is a homotopy class and a cone morphism needs an actual
cocycle, so different representatives give different cone morphisms. The
triangle morphism they produce is nevertheless the same, because its three
components are F.h0.map f, G.h0.map f and ConeData.functor.h0.map f,
all of which depend only on the class. That is why the functor below is
defined with those three components and only its three commuting squares are
proved by choosing a representative.
Naturality in the transformation, and its hypothesis #
A strictly commuting square of closed degree-zero dg natural transformations
between two cone situations induces a natural transformation of triangle
functors (triangleNatTrans). Strictness is the hypothesis that makes this
work and it is not cosmetic: with a zero homotopy every cone map in sight is a
strict lift, so homogeneousLift_strict_comp collapses each composite to a
single lift and the two agree because u and v are natural at degree zero.
The cone lifts are therefore natural on the nose, not merely up to
homotopy, which is functor_map_comp_lift.
When both endpoint maps are isomorphisms in the closed degree-zero dg-functor
category, triangleIsoOfStrictSquare upgrades this natural transformation to
a natural isomorphism. Its first two components are the H⁰ images of the
endpoint isomorphisms, and its third is the H⁰ image of the canonical dg
cone-functor isomorphism ConeData.isoOfStrictSquare.
The homotopy-coherent version is open. With a nonzero homotopy the two composite lifts carry different homotopies, and identifying them needs uniqueness of the lift up to homotopy, which this repository does not have.
The cone choices do not matter #
ConeData is a choice of cone at every object, and compareIso says the
triangle functor does not depend on it: two choices give canonically
isomorphic functors. The comparison is the identity case of the naturality
above, since two ConeData for the same α are related by the identity
square, and compareNatTrans_self and compareNatTrans_comp are what make it
an isomorphism rather than merely a map.
What this does not give #
No comparison is made from a merely homotopy-commuting square, and no statement
says that triangleFunctor is triangulated or exact in any sense. The generic
strict-square interface is specialized to object twists in H0/ObjectTwist;
autoequivalence and sphericality remain separate questions.
The dg cone morphism a degree-zero cocycle of C induces.
The homotopy is zero: graded naturality of α at degree zero carries the sign
(-1)^(0 * 0) = +1, so the square on the first two vertices commutes on the
nose. The other two squares are naturality of ConeData.inr and of
ConeData.fst.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The distinguished triangle of H⁰ D at one object.
Equations
Instances For
The triangle morphism a cocycle of C induces between the cone triangles.
The two cocycles are passed explicitly. toTriangleMorphism takes them as
implicit arguments constrained only through IsConeOf, so leaving them to
unification asks Lean to solve ?f.val =?= app α X for a subtype element, and
it does not terminate.
Equations
- K.coneTriangleMorphism hα f = CategoryTheory.IsConeOf.Morphism.toTriangleMorphism (K.isCone X) (K.isCone Y) (K.coneMorphism f)
Instances For
The cone triangles are functorial.
The three components are the three induced functors on H⁰, so functoriality
is theirs; only the three commuting squares need a representative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every value of the triangle functor is a distinguished triangle.
Naturality in the transformation #
A strictly commuting square of closed degree-zero dg natural transformations, read at one object. The homotopy is zero, which is what makes the whole naturality statement below strict rather than up to homotopy.
Equations
Instances For
The cone morphism the square induces at one object: the standard dg lift, with zero homotopy.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triangle morphism the square induces at one object.
The two cocycles are passed explicitly for the same reason as in
coneTriangleMorphism: left to unification they do not resolve.
Equations
- K.squareTriangleMorphism hα K' hα' hu hv hsq X = CategoryTheory.IsConeOf.Morphism.toTriangleMorphism (K.isCone X) (K'.isCone X) (K.squareConeMorphism K' hu hv hsq X)
Instances For
The cone lifts are natural, on the nose.
Both composites are a composite of two strict lifts, so
homogeneousLift_strict_comp rewrites each to a single strict lift, and the
two agree because u and v are natural at degree zero, where the Koszul
sign is +1. Nothing here is up to homotopy: that is what the square being
strict buys.
The triangle functors are natural in the transformation.
A strictly commuting square of closed degree-zero dg natural transformations
induces a natural transformation of triangle functors. The first two
components are naturality of u and v on H⁰; the third is
functor_map_comp_lift.
Every step goes through the component lemmas rather than through exact on
the assembled triangle morphisms. The assembled terms unfold to the chosen
cones and the chosen shift, and the defeq check does not terminate.
Equations
- K.triangleNatTrans hα K' hα' hu hv hsq = { app := fun (X : CategoryTheory.H0 C) => K.squareTriangleMorphism hα K' hα' hu hv hsq (CategoryTheory.H0.of C X), naturality := ⋯ }
Instances For
Isomorphisms induced by strict isomorphism squares #
A strict square of closed dg natural transformations whose two endpoint
maps are isomorphisms induces a natural isomorphism of their cone triangle
functors. Its third component is the H⁰ image of the dg cone-functor
isomorphism ConeData.isoOfStrictSquare.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Independence of the chosen cones #
The comparison map between two chosen cones of the same component: the strict lift of the two identities.
Equations
- L.compareCone M X = (L.isCone X).homogeneousLift (M.isCone X) 0 (CategoryTheory.DGCategoryStruct.dgId (F.obj X)) (CategoryTheory.DGCategoryStruct.dgId (G.obj X)) 0
Instances For
The comparison maps compose. Both sides are strict lifts, so
homogeneousLift_strict_comp applies and the two identities compose to one.
The identity square relating a cone situation to itself. Both composites
are α, by the two unit laws of the dg category of dg functors.
The triangle functor does not depend on the chosen cones.
Two ConeData for the same transformation are related by the identity square,
so triangleNatTrans applies with u and v the identities. The
transformation it produces is the objectwise comparison of cones.
Equations
- CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.compareNatTrans hα L M = L.triangleNatTrans hα M hα ⋯ ⋯ ⋯
Instances For
Comparing a cone choice with itself is the identity.
The comparisons compose.
The triangle functors of two cone choices are canonically isomorphic.
Equations
- One or more equations did not get rendered due to their size.