Fixed-target arrow extension through compatible right projections #
An ambient functor's fixed-target arrow extension passes to its restriction between right-adjoint components given an inclusion comparison, a projector comparison, and their counit mate equation. These are explicit premises of the transfer theorem. No geometric pullback or projector commutation is constructed here.
theorem
CategoryTheory.ObjectProperty.RightProjectionData.fixedTargetArrowExtension_of_ambient
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{P : ObjectProperty C}
{Q : ObjectProperty D}
(p : P.RightProjectionData)
(q : Q.RightProjectionData)
(F : Functor C D)
(G : Functor P.FullSubcategory Q.FullSubcategory)
(inclusionIso : G.comp Q.ι ≅ P.ι.comp F)
(projectionIso : F.comp q.projection ≅ p.projection.comp G)
(counit_compat :
∀ (Y : C),
q.counitApp (F.obj Y) = CategoryStruct.comp (Q.ι.map (projectionIso.app Y).hom)
(CategoryStruct.comp (inclusionIso.app (p.project Y)).hom (F.map (p.counitApp Y))))
(X : P.FullSubcategory)
(hExt : Subobject.FixedTargetArrowExtension F (P.ι.obj X))
:
Ambient all-arrow extension into an included component target transfers to the restricted functor when the inclusion and projection comparisons are mate-compatible. The projector comparison and counit equation are independent premises; an inclusion comparison alone does not imply them.