Extensions of twisted objects #
Let P and Q be twisted objects of the additive closure of a differential graded category E,
and let g : Q ⟶ P be a closed morphism of degree one of twisted objects. The extension
TauCeti.DGTwistedObject.extension P Q g is the twisted object (P ⊕ Q, δ) whose underlying
object is the direct sum P ⊕ Q in the additive closure and whose twisting matrix δ has the
twists δ_P and δ_Q on the diagonal blocks, g in the block from Q to P, and zero in the
block from P to Q. Blockwise, the Maurer–Cartan equation d δ = dgComp δ δ is the
Maurer–Cartan equations of δ_P and δ_Q together with d g = dgComp δ_Q g + dgComp g δ_P, and
the last equation says exactly that g is closed for the twisted differential
(TauCeti.DGTwistedObject.dgDifferential_extensionTwist).
The extension comes with inclusions TauCeti.DGTwistedObject.extensionInl,
TauCeti.DGTwistedObject.extensionInr and projections TauCeti.DGTwistedObject.extensionFst,
TauCeti.DGTwistedObject.extensionSnd of degree zero satisfying the biproduct equations. The
inclusion of P and the projection onto Q are closed, so P ⟶ extension P Q g ⟶ Q is a
sequence of closed degree-zero morphisms with zero composite, split as graded objects. The
splitting need not be closed: the differential of the inclusion of Q is g followed by the
inclusion of P, and the differential of the projection onto P is minus the projection onto Q
followed by g.
If g is invertible, with inverse g' : P ⟶ Q of degree -1, the extension is contractible:
minus the projection onto P, followed by g' and the inclusion of Q, is a degree -1
endomorphism whose differential is the identity, so the extension is a zero object of the
homotopy category.
The extension depends only on the homotopy class of g, up to isomorphism in the homotopy
category. If g - g' = d k for a degree-zero morphism k : Q ⟶ P, then the identity on the
summands together with k in the block from Q to P is a closed morphism
extension P Q g ⟶ extension P Q g', with inverse the same construction for -k.
The extension is functorial in the second summand: a closed degree-zero morphism φ : Q ⟶ Q'
with φ followed by g' equal to g induces a closed morphism
extension P Q g ⟶ extension P Q' g', the identity on P and φ on Q, and an isomorphism φ
induces an isomorphism in the homotopy category.
With Q the shift P'⟦1⟧ of a twisted object P' and g the degree-one morphism
P'⟦1⟧ ⟶ P' ⟶ P underlying a closed degree-zero morphism u : P' ⟶ P, the extension is the
cone of u, the basic construction of the pretriangulated envelope of Bondal and Kapranov; see
TauCeti/CategoryTheory/DG/Twisted/Cone.lean.
A DG functor G : E ⥤ E' preserves extensions: the image under the induced DG functor of
extension P Q g is isomorphic in the homotopy category to the extension of the images of P
and Q along the image of g, through the closed morphisms built from the images of the
projections and inclusions of one extension and the inclusions and projections of the other.
Main definitions #
TauCeti.DGTwistedObject.extensionTwist: the block twisting matrix of an extension.TauCeti.DGTwistedObject.extension: the extension ofQbyPalongg.TauCeti.DGTwistedObject.extensionInl,TauCeti.DGTwistedObject.extensionInr,TauCeti.DGTwistedObject.extensionFst,TauCeti.DGTwistedObject.extensionSnd: the inclusions of and projections to the two summands.TauCeti.DGTwistedObject.extensionHomOfHomotopy: the morphism of extensions induced by a degree-zero morphismk : Q ⟶ P.TauCeti.DGTwistedObject.extensionIsoOfHomotopy: the isomorphism in the homotopy category between extensions along homotopic morphisms.TauCeti.DGTwistedObject.extensionMap: the morphism of extensions induced by a morphism of second summands.TauCeti.DGTwistedObject.extensionIsoOfIso: the isomorphism in the homotopy category between extensions along isomorphic second summands.CategoryTheory.EnrichedFunctor.mapExtensionIso: the isomorphism in the homotopy category between the image of an extension under a DG functor and the extension of the images.
Main results #
TauCeti.DGTwistedObject.dgDifferential_extensionTwist: the Maurer–Cartan equation.TauCeti.DGTwistedObject.dgDifferential_extensionInl,TauCeti.DGTwistedObject.dgDifferential_extensionSnd: the inclusion ofPand the projection ontoQare closed.TauCeti.DGTwistedObject.dgDifferential_extensionInr,TauCeti.DGTwistedObject.dgDifferential_extensionFst: the differentials of the other two structure maps.TauCeti.DGTwistedObject.dgComp_extensionInl_extensionSndand the other biproduct equations: the compositeP ⟶ extension P Q g ⟶ Qvanishes, and the inclusions and projections exhibit the extension as the direct sum ofPandQas a graded object.TauCeti.DGTwistedObject.extension_dgHom_ext: morphisms out of an extension are determined by their composites with the two inclusions.TauCeti.DGTwistedObject.dgDifferential_neg_dgComp_extensionFst_extensionInrandTauCeti.DGTwistedObject.isZero_extension_of_dgComp_eq_dgId: an extension along an invertible morphism is contractible.TauCeti.DGTwistedObject.isZero_of_isEmpty: a twisted object with no summands is a zero object of the homotopy category; in particular the homotopy category has a zero object.TauCeti.DGTwistedObject.extensionHomOfHomotopy_zero: the zero morphism induces the identity.TauCeti.DGTwistedObject.dgComp_extensionInl_extensionHomOfHomotopy,TauCeti.DGTwistedObject.dgComp_extensionHomOfHomotopy_extensionSndand their formsTauCeti.DGTwistedObject.homOf_extensionInl_comp_extensionIsoOfHomotopy_hom,TauCeti.DGTwistedObject.extensionIsoOfHomotopy_hom_comp_homOf_extensionSndin the homotopy category: the morphism induced bykcommutes with the inclusion ofPand the projection ontoQ.TauCeti.DGTwistedObject.dgDifferential_extensionHomOfHomotopyandTauCeti.DGTwistedObject.dgComp_extensionHomOfHomotopy_neg: the morphism induced by a homotopykfromgtog'is closed, and the morphisms induced bykand-kare mutually inverse.TauCeti.DGTwistedObject.dgDifferential_extensionMapandTauCeti.DGTwistedObject.dgComp_extensionMap: the morphism of extensions induced by a closed morphism compatible with the gluing morphisms is closed, and these morphisms compose.CategoryTheory.EnrichedFunctor.dgComp_dgMap_extensionInl_mapExtensionHom,CategoryTheory.EnrichedFunctor.dgComp_mapExtensionHom_extensionSndand their companions: the comparison of the image of an extension with the extension of the images commutes with the structure maps.
References #
- A. I. Bondal and M. M. Kapranov, Enhanced triangulated categories, Section 1.
- V. Drinfeld, DG quotients of DG categories, Section 2.4.
Matrix entries of morphisms of twisted objects of the additive closure #
The twisted differential of a morphism of twisted objects of the additive closure, entrywise.
Composition of twisted objects of the additive closure, entrywise.
The twisted differential of a degree-zero morphism of twisted objects of the additive closure, entrywise.
The twisting matrix of an extension #
The twisting matrix of an extension of Q by P along a degree-one morphism
g : Q ⟶ P: the degree-one endomorphism of P ⊕ Q with the twists of P and Q on the
diagonal blocks, g in the block from Q to P, and zero in the block from P to Q.
Instances For
The block of the twisting matrix of an extension on the summands of P is the twist of
P.
The block of the twisting matrix of an extension from the summands of P to those of Q
vanishes.
The block of the twisting matrix of an extension from the summands of Q to those of P is
g.
The block of the twisting matrix of an extension on the summands of Q is the twist of
Q.
The twisting matrix of an extension along a closed morphism satisfies the Maurer–Cartan equation.
The extension #
The extension of Q by P along a closed degree-one morphism g : Q ⟶ P of twisted
objects of the additive closure: the twisted object (P ⊕ Q, δ) whose twisting matrix has the
twists of P and Q on the diagonal and g in the block from Q to P. Its Maurer–Cartan
equation is TauCeti.DGTwistedObject.dgDifferential_extensionTwist.
Instances For
The structure maps of an extension #
The inclusion P ⟶ extension P Q g of the first summand, a closed morphism of degree
zero.
Instances For
The inclusion Q ⟶ extension P Q g of the second summand, a morphism of degree zero which
need not be closed: its differential is g followed by the inclusion of P.
Instances For
The projection extension P Q g ⟶ P onto the first summand, a morphism of degree zero
which need not be closed: its differential is minus the projection onto Q followed by g.
Instances For
The projection extension P Q g ⟶ Q onto the second summand, a closed morphism of degree
zero.
Instances For
The block of the inclusion of P into an extension on the summands of P is the
identity.
The block of the inclusion of P into an extension to the summands of Q vanishes.
The block of the inclusion of Q into an extension to the summands of P vanishes.
The block of the inclusion of Q into an extension on the summands of Q is the
identity.
The block of the projection of an extension onto P on the summands of P is the
identity.
The block of the projection of an extension onto P from the summands of Q vanishes.
The block of the projection of an extension onto Q from the summands of P vanishes.
The block of the projection of an extension onto Q on the summands of Q is the
identity.
Differentials of the structure maps #
The inclusion of P into an extension is closed.
The projection of an extension onto Q is closed.
The differential of the inclusion of Q into an extension along g is g followed by the
inclusion of P.
The differential of the projection of an extension along g onto P is minus the
projection onto Q followed by g.
The biproduct equations #
The inclusion of P into an extension followed by the projection onto P is the
identity.
The inclusion of P into an extension followed by the projection onto Q vanishes.
The inclusion of Q into an extension followed by the projection onto P vanishes.
The inclusion of Q into an extension followed by the projection onto Q is the
identity.
An extension is the direct sum of P and Q as a graded object: the projections
followed by the inclusions sum to the identity.
Morphisms out of an extension are determined by their restrictions to the summands: two
morphisms out of an extension agree once they agree after the inclusions of P and of Q.
The inclusion of P followed by the projection onto P and then x is x.
The inclusion of P followed by the projection onto Q and then x vanishes.
The inclusion of Q followed by the projection onto P and then x vanishes.
The inclusion of Q followed by the projection onto Q and then x is x.
Extensions along invertible morphisms are contractible #
The contracting homotopy of an extension along an invertible morphism: if the closed
degree-one morphism g : Q ⟶ P has an inverse g' : P ⟶ Q of degree -1, then the differential
of minus the projection onto P, followed by g' and the inclusion of Q, is the identity of the
extension.
An extension along an invertible morphism is contractible: if the closed degree-one
morphism g : Q ⟶ P has an inverse of degree -1, then the extension of Q by P along g is
a zero object of the homotopy category.
The zero object #
A twisted object with no summands is a zero object of the homotopy category: its identity is the empty matrix, which is the differential of the zero morphism.
The homotopy category of twisted objects of an additive closure has a zero object: the empty direct sum with the zero twist.
Extensions along homotopic morphisms are isomorphic #
The degree-zero morphism extension P Q g ⟶ extension P Q g' induced by a degree-zero
morphism k : Q ⟶ P: the identity on the summands P and Q, together with k in the block
from Q to P. It is closed when d k = g - g'
(TauCeti.DGTwistedObject.dgDifferential_extensionHomOfHomotopy).
Instances For
The morphism of extensions induced by the zero morphism is the identity.
The morphism of extensions induced by a homotopy is closed: if d k = g - g', then the
differential of TauCeti.DGTwistedObject.extensionHomOfHomotopy vanishes.
The inclusion of P followed by the morphism of extensions induced by k is the inclusion
of P.
The inclusion of Q followed by the morphism of extensions induced by k is the inclusion
of Q plus k followed by the inclusion of P.
The morphism of extensions induced by k followed by the projection onto Q is the
projection onto Q.
The morphism of extensions induced by k followed by the projection onto P is the
projection onto P plus the projection onto Q followed by k.
The morphisms of extensions induced by k and -k are mutually inverse.
Extensions along homotopic morphisms are isomorphic: if g - g' = d k for a degree-zero
morphism k : Q ⟶ P, then extension P Q g and extension P Q g' are isomorphic in the
homotopy category, through the morphisms induced by k and -k.
Instances For
In the homotopy category, the inclusion of P followed by the isomorphism of extensions
along homotopic morphisms is the inclusion of P.
In the homotopy category, the isomorphism of extensions along homotopic morphisms followed by
the projection onto Q is the projection onto Q.
Extensions along isomorphic second summands are isomorphic #
The degree-zero morphism extension P Q g ⟶ extension P Q' g' induced by a degree-zero
morphism φ : Q ⟶ Q': the identity on the summand P and φ on the second summand. It is
closed when φ is closed and φ followed by g' is g
(TauCeti.DGTwistedObject.dgDifferential_extensionMap).
Instances For
The morphism of extensions induced by the identity is the identity.
The morphism of extensions induced by a closed morphism compatible with the gluing morphisms
is closed: if φ : Q ⟶ Q' is closed and φ followed by g' is g, then the differential of
TauCeti.DGTwistedObject.extensionMap vanishes.
The inclusion of P followed by the morphism of extensions induced by φ is the inclusion
of P.
The inclusion of Q followed by the morphism of extensions induced by φ is φ followed by
the inclusion of Q'.
The morphism of extensions induced by φ followed by the projection onto P is the
projection onto P.
The morphism of extensions induced by φ followed by the projection onto Q' is the
projection onto Q followed by φ.
The inclusion of P, followed by the morphism of extensions induced by φ and then x, is
the inclusion of P followed by x.
The inclusion of Q, followed by the morphism of extensions induced by φ and then x, is
φ followed by the inclusion of Q' and then x.
The morphism of extensions induced by φ, followed by the projection onto P and then x,
is the projection onto P followed by x.
The morphism of extensions induced by φ, followed by the projection onto Q' and then x,
is the projection onto Q followed by φ and then x.
The morphisms of extensions compose: the morphisms induced by φ : Q ⟶ Q' and
ψ : Q' ⟶ Q'' compose to the morphism induced by φ followed by ψ.
Extensions along isomorphic second summands are isomorphic: if φ : Q ⟶ Q' is a closed
degree-zero morphism with two-sided inverse ψ and φ followed by g' is g, then
extension P Q g and extension P Q' g' are isomorphic in the homotopy category, through the
morphisms induced by φ and ψ.
Instances For
Images of extensions #
The comparison G (extension P Q g) ⟶ extension (G P) (G Q) (G g) of the image of an
extension under the DG functor induced by G with the extension of the images: the images of
the projections followed by the inclusions of the target.
Instances For
The comparison extension (G P) (G Q) (G g) ⟶ G (extension P Q g), inverse to
CategoryTheory.EnrichedFunctor.mapExtensionHom: the projections of the source followed by the
images of the inclusions.
Instances For
The comparison of the image of an extension with the extension of the images is the images of the projections followed by the inclusions.
The inverse comparison is the projections followed by the images of the inclusions.
The comparison of the image of an extension with the extension of the images is closed.
The image of the inclusion of P followed by the comparison is the inclusion of G P.
The image of the inclusion of Q followed by the comparison is the inclusion of G Q.
The comparison followed by the projection onto G Q is the image of the projection onto
Q.
The inclusion of G P followed by the inverse comparison is the image of the inclusion of
P.
The inclusion of G Q followed by the inverse comparison is the image of the inclusion of
Q.
The comparison of the image of an extension with the extension of the images, followed by its inverse, is the identity.
The inverse comparison followed by the comparison is the identity of the extension of the images.
The inverse comparison of the extension of the images with the image of an extension is closed.
A DG functor preserves extensions: the image of extension P Q g under the DG functor
induced by G is isomorphic in the homotopy category to the extension of the images along the
image of g.