Transporting H⁰ dg functors through ordinary equivalences

For a dg functor F : C ⟶ D and ordinary equivalences H⁰ C ≌ X and H⁰ D ≌ Y, this file packages the conjugate functor

X ⥤ H⁰ C ⥤ H⁰ D ⥤ Y

using Mathlib's existing CommShift, triangulated-functor, and equivalence interfaces. The source inverse shift comparison is derived from the supplied forward comparison by Equivalence.commShiftInverse; no duplicate transport or exactness structure is introduced.

The transport constructor assumes only that F.h0 is an equivalence. It does not infer one from a dg quasi-equivalence, and its exactness declarations require the endpoint equivalences to be supplied as triangulated.

Without endpoint equivalences, DGFunctor.isTriangulated_h0_asEquivalence says that H⁰ F is a triangulated equivalence whenever it is an equivalence, and DGFunctor.isTriangulated_h0Equivalence specializes it to the equivalence DGFunctor.h0Equivalence that a dg quasi-equivalence induces (which is why this file imports QuasiEquivalence.lean). Both reduce, through Mathlib's Equivalence.IsTriangulated.mk', to exactness of the forward functor, DGFunctor.h0IsTriangulated.

@[reducible, inline]

abbrev CategoryTheory.DGFunctor.transportedH0 {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] (F : DGFunctor C D) (eC : H0 C ≌ X) (eD : H0 D ≌ Y) : Functor X Y

The ordinary functor obtained by passing a dg functor to H⁰ and changing source and target along supplied category equivalences.

Equations

• F.transportedH0 eC eD = (eC.inverse.comp F.h0).comp eD.functor

theorem CategoryTheory.DGFunctor.transportedH0_isEquivalence {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] (F : DGFunctor C D) (eC : H0 C ≌ X) (eD : H0 D ≌ Y) (hF : F.h0.IsEquivalence) : (F.transportedH0 eC eD).IsEquivalence

Equivalence of F.h0 makes its ordinary transport an equivalence.

noncomputable def CategoryTheory.DGFunctor.transportedH0Equivalence {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] (F : DGFunctor C D) (eC : H0 C ≌ X) (eD : H0 D ≌ Y) (hF : F.h0.IsEquivalence) : X ≌ Y

The ordinary equivalence obtained by transporting an equivalence F.h0 through the supplied endpoint equivalences.

Equations

• F.transportedH0Equivalence eC eD hF = (eC.symm.trans F.h0.asEquivalence).trans eD

@[reducible]

noncomputable def CategoryTheory.DGFunctor.transportedH0CommShift {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] [IsPretriangulated C] [IsPretriangulated D] [HasShift X ℤ] [HasShift Y ℤ] {eC : H0 C ≌ X} {eD : H0 D ≌ Y} [eC.functor.CommShift ℤ] [eD.functor.CommShift ℤ] (F : DGFunctor C D) : (F.transportedH0 eC eD).CommShift ℤ

The coherent shift comparison on the ordinary transport of H⁰ F.

The source inverse comparison is Mathlib's mate of the supplied forward comparison. The remaining structure is inherited by functor composition.

Equations

• F.transportedH0CommShift = inferInstance

theorem CategoryTheory.DGFunctor.transportedH0IsTriangulated {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] [IsPretriangulated C] [IsPretriangulated D] [HasShift X ℤ] [HasShift Y ℤ] {eC : H0 C ≌ X} {eD : H0 D ≌ Y} [eC.functor.CommShift ℤ] [eD.functor.CommShift ℤ] [Limits.HasZeroObject X] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject Y] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [eC.functor.IsTriangulated] [eD.functor.IsTriangulated] (F : DGFunctor C D) : (F.transportedH0 eC eD).IsTriangulated

The ordinary transport of every dg functor between pretriangulated dg categories is triangulated when the endpoint equivalences are triangulated.

theorem CategoryTheory.DGFunctor.transportedH0EquivalenceIsTriangulated {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] [IsPretriangulated C] [IsPretriangulated D] [HasShift X ℤ] [HasShift Y ℤ] {eC : H0 C ≌ X} {eD : H0 D ≌ Y} [eC.functor.CommShift ℤ] [eD.functor.CommShift ℤ] [Limits.HasZeroObject X] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject Y] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [eC.functor.IsTriangulated] [eD.functor.IsTriangulated] (F : DGFunctor C D) (hF : F.h0.IsEquivalence) : (F.transportedH0Equivalence eC eD hF).IsTriangulated

The transported equivalence is a triangulated equivalence under the same endpoint hypotheses. Its inverse comparison and exactness are Mathlib's canonical mates of the forward package.

theorem CategoryTheory.DGFunctor.isTriangulated_h0_asEquivalence {C : Type uC} {D : Type uD} [DGCategory C] [DGCategory D] [IsPretriangulated C] [IsPretriangulated D] (F : DGFunctor C D) [F.h0.IsEquivalence] : F.h0.asEquivalence.IsTriangulated

A dg functor whose H⁰ is an equivalence induces a triangulated equivalence. Functor.asEquivalence of H⁰ F is a triangulated equivalence in Mathlib's sense Equivalence.IsTriangulated: the forward shift comparison is the explicit h0CommShift, and the inverse comparison and the triangulated inverse are Mathlib's canonical mates (Equivalence.commShiftInverse, Equivalence.IsTriangulated.mk'), so the only input is exactness of the forward functor, h0IsTriangulated. It is the analogue, without endpoint equivalences, of transportedH0EquivalenceIsTriangulated.

theorem CategoryTheory.DGFunctor.isTriangulated_h0Equivalence {C : Type uC} {D : Type uD} [DGCategory C] [DGCategory D] [IsPretriangulated C] [IsPretriangulated D] (F : DGFunctor C D) (hF : F.IsQuasiEquivalence) : (F.h0Equivalence hF).IsTriangulated

A quasi-equivalence of pretriangulated dg categories induces a triangulated equivalence on H⁰, in the sense of Mathlib's Equivalence.IsTriangulated.

hF only builds the equivalence h0Equivalence, whose functor is H⁰ F (h0Equivalence_functor); this is isTriangulated_h0_asEquivalence for it. The shift on H⁰ F is the explicit h0CommShift, not an instance, so callers must letI the same structure.