Pullback of right projections from orthogonal preservation

For fully faithful component inclusions with chosen right projections, an inclusion comparison has a canonical mate. If a triangulated functor sends the source component's right orthogonal into the target component's right orthogonal, the mate is invertible. Its inverse has the counit compatibility needed to transfer fixed-target arrow extension.

No orthogonal-preservation assertion for a geometric pullback is made here.

noncomputable def CategoryTheory.ObjectProperty.RightProjectionData.projectionMateIso {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {P : ObjectProperty C} {Q : ObjectProperty D} (p : P.RightProjectionData) (q : Q.RightProjectionData) (F : Functor C D) (G : Functor P.FullSubcategory Q.FullSubcategory) (inc : G.comp Q.ι ≅ P.ι.comp F) (hP : P.IsTriangulated) (hQ : Q.IsTriangulated) [F.CommShift ℤ] [F.IsTriangulated] (horth : P.rightOrthogonal ≤ Q.rightOrthogonal.inverseImage F) : F.comp q.projection ≅ p.projection.comp G

A triangulated functor preserving the right orthogonal commutes with the chosen right projections, by the inverse of the canonical adjunction mate.

Equations

• p.projectionMateIso q F G inc hP hQ horth = (CategoryTheory.asIso (CategoryTheory.ObjectProperty.RightProjectionData.projectionMate✝ p q F G inc)).symm

theorem CategoryTheory.ObjectProperty.RightProjectionData.projectionMateIso_counit {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {P : ObjectProperty C} {Q : ObjectProperty D} (p : P.RightProjectionData) (q : Q.RightProjectionData) (F : Functor C D) (G : Functor P.FullSubcategory Q.FullSubcategory) (inc : G.comp Q.ι ≅ P.ι.comp F) (hP : P.IsTriangulated) (hQ : Q.IsTriangulated) [F.CommShift ℤ] [F.IsTriangulated] (horth : P.rightOrthogonal ≤ Q.rightOrthogonal.inverseImage F) (Y : C) : q.counitApp (F.obj Y) = CategoryStruct.comp (Q.ι.map ((p.projectionMateIso q F G inc hP hQ horth).app Y).hom) (CategoryStruct.comp (inc.app (p.project Y)).hom (F.map (p.counitApp Y)))

The projector comparison constructed from orthogonal preservation is the mate of the inclusion comparison, hence obeys the counit equation.