Dg functors obtained from objectwise cones

A closed degree-zero dg natural transformation α : F ⟶ G has a cone dg functor once a cone of every component α.app X has been chosen. This file separates those two concerns:

• ConeData α is the minimal objectwise representability data;
• ConeData.functor supplies every homogeneous map by the signed cone lift;
• ConeData.inr and ConeData.inl are the canonical degree 0 and degree -1 homogeneous natural transformations of the cone sequence.

The construction is dg-level. It does not choose ordinary triangulated cones or quotient morphisms in H⁰, and it does not depend on Fourier--Mukai kernels. Those are downstream realizations of this canonical root.

structure CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} (α : ↥(F.HomogeneousNatTrans G 0)) : Type (max (max u u') v)

The minimal choices needed to turn componentwise cones of α into a dg functor. No compatibility fields are necessary: graded naturality of α and the universal all-degree cone lift force the map laws.

• obj : C → D

  The chosen cone object of each component.

• isCone (X : C) : IsConeOf (app α X) (self.obj X)

  The chosen dg cone presentation of each component.

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.chosenConeData {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} [IsPretriangulated D] (α : ↥(F.HomogeneousNatTrans G 0)) (hα : IsClosed α) : ConeData α

A pretriangulated target supplies objectwise cone data for every closed degree-zero dg natural transformation.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.chosenConeData α hα = { obj := fun (X : C) => ⋯.choose, isCone := fun (X : C) => ⋯.some }

@[reducible, inline]

noncomputable abbrev CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.functor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : DGFunctor C D

The dg functor obtained by taking the chosen cone of every component of α. Its action on a degree-p morphism is the signed strict homogeneous cone lift of F.map p f and G.map p f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.functor_obj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) (X : C) : K.functor.obj X = K.obj X

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.functor_map {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : (K.functor.map p) f = (K.isCone X).homogeneousLift (K.isCone Y) p ((F.map p) f) ((G.map p) f) 0

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inr {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : ↥(G.HomogeneousNatTrans K.functor 0)

The target inclusions form the canonical closed degree-zero dg natural transformation G ⟶ Cone(α).

Equations

• K.inr = ⟨fun (X : C) => (K.isCone X).inr, ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inr_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) (X : C) : app K.inr X = (K.isCone X).inr

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inr_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : IsClosed K.inr

The canonical target inclusion is closed in the dg functor category.

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inl {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : ↥(F.HomogeneousNatTrans K.functor (-1))

The shifted source inclusions form the canonical degree--1 homogeneous dg natural transformation F ⟶ Cone(α).

Equations

• K.inl = ⟨fun (X : C) => (K.isCone X).inl, ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inl_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) (X : C) : app K.inl X = (K.isCone X).inl

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.differential_inl {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : differential K.inl = comp α K.inr

The boundary of the shifted source inclusion is the component map followed by the target inclusion. This is the dg-functor-level cone equation.

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.fst {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : ↥(K.functor.HomogeneousNatTrans F 1)

The cone projections to the source form a degree-one homogeneous dg natural transformation Cone(α) ⟶ F.

Graded naturality at degree one is exactly homogeneousLift_comp_fst: the sign (-1)^p that lemma produces is the Koszul sign (-1)^(1 * p) the naturality convention asks for, which is why the cone projection is natural on the nose and not only up to homotopy.

Equations

• K.fst = ⟨fun (X : C) => (K.isCone X).fst, ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.fst_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) (X : C) : app K.fst X = (K.isCone X).fst

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.fst_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : IsClosed K.fst

The degree-one projection from a functorial cone to its source is closed in the dg functor category.

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.snd {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : ↥(K.functor.HomogeneousNatTrans G 0)

The cone projections to the target form a closed degree-zero homogeneous dg natural transformation Cone(α) ⟶ G.

Equations

• K.snd = ⟨fun (X : C) => (K.isCone X).snd, ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.snd_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) (X : C) : app K.snd X = (K.isCone X).snd

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.isConeOf {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : IsConeOf α K.functor

The objectwise cones assemble into a cone in the dg category of dg functors.

This is what upgrades ConeData from a family of cones to a cone: the two inclusions are the transformations already built, and a homogeneous transformation into the cone splits along them objectwise. The splitting is natural because fst and snd are, which is the content of the two constructions above.

Anno--Logvinenko's triangles are triangles of functors; this is the statement that the repository's objectwise construction produces one.

Why every step is a show

Composition and the differential of the dg category DGFunctor C D are HomogeneousNatTrans.composition and the pointwise differential by definition, so a goal stated with dgComp is definitionally a goal about components — but not syntactically, and rw matches syntactically. Each show below is that definitional step, made explicit so the rest of the proof can be an ordinary calculation in D.

Equations

• K.isConeOf = { inr := K.inr, inr_closed := ⋯, inl := K.inl, δ_inl := ⋯, bijective := ⋯ }

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.isConeOf_fst {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : K.isConeOf.fst = K.fst

The projection selected from the assembled cone in the dg-functor category is the explicit pointwise source projection transformation.

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.isConeOf_snd {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : K.isConeOf.snd = K.snd

The projection selected from the assembled cone in the dg-functor category is the explicit pointwise target projection transformation.

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.isoOfStrictSquare {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) {F' G' : DGFunctor C D} {α' : ↥(F'.HomogeneousNatTrans G' 0)} (K' : ConeData α') (eF : (have this := F; this) ≅ have this := F'; this) (eG : (have this := G; this) ≅ have this := G'; this) (hsq : ((composition F G G' 0 0 0 ⋯) α) ↑eG.hom = ((composition F F' G' 0 0 0 ⋯) ↑eF.hom) α') : (have this := K.functor; this) ≅ have this := K'.functor; this

A strict isomorphism square between two dg natural transformations lifts to an isomorphism between their chosen cone dg functors.

Equations

• K.isoOfStrictSquare K' eF eG hsq = K.isConeOf.isoOfStrictSquare K'.isConeOf eF eG hsq

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.isoOfStrictSquare_hom_val {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) {F' G' : DGFunctor C D} {α' : ↥(F'.HomogeneousNatTrans G' 0)} (K' : ConeData α') (eF : (have this := F; this) ≅ have this := F'; this) (eG : (have this := G; this) ≅ have this := G'; this) (hsq : ((composition F G G' 0 0 0 ⋯) α) ↑eG.hom = ((composition F F' G' 0 0 0 ⋯) ↑eF.hom) α') : ↑(K.isoOfStrictSquare K' eF eG hsq).hom = K.isConeOf.lift K'.isConeOf (↑eF.hom) (↑eG.hom) 0

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.isoOfStrictSquare_inv_val {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) {F' G' : DGFunctor C D} {α' : ↥(F'.HomogeneousNatTrans G' 0)} (K' : ConeData α') (eF : (have this := F; this) ≅ have this := F'; this) (eG : (have this := G; this) ≅ have this := G'; this) (hsq : ((composition F G G' 0 0 0 ⋯) α) ↑eG.hom = ((composition F F' G' 0 0 0 ⋯) ↑eF.hom) α') : ↑(K.isoOfStrictSquare K' eF eG hsq).inv = K'.isConeOf.lift K.isConeOf (↑eF.inv) (↑eG.inv) 0

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.isoOfStrictSquare_hom_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) {F' G' : DGFunctor C D} {α' : ↥(F'.HomogeneousNatTrans G' 0)} (K' : ConeData α') (eF : (have this := F; this) ≅ have this := F'; this) (eG : (have this := G; this) ≅ have this := G'; this) (hsq : ((composition F G G' 0 0 0 ⋯) α) ↑eG.hom = ((composition F F' G' 0 0 0 ⋯) ↑eF.hom) α') (X : C) : app (↑(K.isoOfStrictSquare K' eF eG hsq).hom) X = (K.isCone X).lift (K'.isCone X) (app (↑eF.hom) X) (app (↑eG.hom) X) 0

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.isoOfStrictSquare_inv_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) {F' G' : DGFunctor C D} {α' : ↥(F'.HomogeneousNatTrans G' 0)} (K' : ConeData α') (eF : (have this := F; this) ≅ have this := F'; this) (eG : (have this := G; this) ≅ have this := G'; this) (hsq : ((composition F G G' 0 0 0 ⋯) α) ↑eG.hom = ((composition F F' G' 0 0 0 ⋯) ↑eF.hom) α') (X : C) : app (↑(K.isoOfStrictSquare K' eF eG hsq).inv) X = (K'.isCone X).lift (K.isCone X) (app (↑eF.inv) X) (app (↑eG.inv) X) 0

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inr_comp_isoOfStrictSquare_hom {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) {F' G' : DGFunctor C D} {α' : ↥(F'.HomogeneousNatTrans G' 0)} (K' : ConeData α') (eF : (have this := F; this) ≅ have this := F'; this) (eG : (have this := G; this) ≅ have this := G'; this) (hsq : ((composition F G G' 0 0 0 ⋯) α) ↑eG.hom = ((composition F F' G' 0 0 0 ⋯) ↑eF.hom) α') : ((composition G K.functor K'.functor 0 0 0 ⋯) K.inr) ↑(K.isoOfStrictSquare K' eF eG hsq).hom = ((composition G G' K'.functor 0 0 0 ⋯) ↑eG.hom) K'.inr

The lifted dg-functor isomorphism strictly commutes with the canonical target inclusions of the two cone sequences.