Enhanced representatives and cones of ordinary morphisms

An enhancement e : Enhancement W presents an ordinary category W as the homotopy category of a pretriangulated dg category. Every ordinary morphism in W therefore has a closed degree-zero representative between the chosen inverse images of its endpoints, and that representative has a dg cone.

This file packages those two noncanonical choices once, independently of any Fourier--Mukai, unit, or counit interpretation. Conjugating the selected representative by the counit of the comparison equivalence recovers the original ordinary morphism. No selected representative or cone is claimed canonical, and no comparison between different selections is asserted.

noncomputable def CategoryTheory.Enhancement.liftedCocycle {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : ↥(cocycles (have this := e.equiv.inverse.obj K; this) (have this := e.equiv.inverse.obj L; this))

A noncanonical closed degree-zero representative of an ordinary morphism between the chosen inverse images of its endpoints.

Equations

• e.liftedCocycle f = (CategoryTheory.Z0.toH0 e.dgCat).preimage (e.equiv.inverse.map f)

@[simp]

theorem CategoryTheory.Enhancement.homMk_liftedCocycle {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : H0.homMk (e.liftedCocycle f) = e.equiv.inverse.map f

The selected cocycle represents the inverse image of the original ordinary morphism in H⁰ of the enhancement.

theorem CategoryTheory.Enhancement.counit_conjugate_liftedCocycle {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : CategoryStruct.comp (e.equiv.counitIso.app K).inv (CategoryStruct.comp (e.equiv.functor.map (H0.homMk (e.liftedCocycle f))) (e.equiv.counitIso.app L).hom) = f

Conjugating the selected representative by the counit of the enhancement equivalence recovers the original ordinary morphism.

noncomputable def CategoryTheory.Enhancement.conePresentation {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : DGCategory.ConePresentation e.dgCat

A noncanonically selected dg cone presentation of an ordinary morphism.

The source and target are the comparison equivalence's chosen inverse images, the arrow is liftedCocycle, and pretriangulatedness supplies the cone.

Equations

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

@[simp]

theorem CategoryTheory.Enhancement.conePresentation_source {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : (e.conePresentation f).source = H0.of e.dgCat (e.equiv.inverse.obj K)

@[simp]

theorem CategoryTheory.Enhancement.conePresentation_target {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : (e.conePresentation f).target = H0.of e.dgCat (e.equiv.inverse.obj L)

@[simp]

theorem CategoryTheory.Enhancement.conePresentation_arrow {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : (e.conePresentation f).arrow = e.liftedCocycle f

theorem CategoryTheory.Enhancement.homMk_conePresentation_arrow {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : H0.homMk (e.conePresentation f).arrow = e.equiv.inverse.map f

The arrow in the selected cone presentation represents the inverse image of the original ordinary morphism.

theorem CategoryTheory.Enhancement.counit_conjugate_conePresentation_arrow {W : Type u'} [Category.{v', u'} W] (e : Enhancement W) {K L : W} (f : K ⟶ L) : CategoryStruct.comp (e.equiv.counitIso.app K).inv (CategoryStruct.comp (e.equiv.functor.map (H0.homMk (e.conePresentation f).arrow)) (e.equiv.counitIso.app L).hom) = f

Conjugating the arrow in the selected cone presentation recovers the original ordinary morphism.