Русский
Если H' : D' ⥤ V является точечным левым Кан-расширением вдоль L: D ⥤ D' в точке d и тензорование слева с K.obj e сохраняет колимиты, то K ⊠ H является точочным левым Кан-расширением вдоль Id_E × L в точке (e,d) для каждого e.
LaTeX
$$$\\text{isPointwiseLeftKanExtensionAtExtensionUnitRight}: (d: D') \\to (P: (H' \\alpha).IsPointwiseLeftKanExtensionAt d) \\to (e: E) \\to (K \\boxtimes H) \\text{ is pointwise along } (Id_E \\times L)$$$
Lean4
/-- If `H' : D' ⥤ V` is a pointwise left Kan extension along `L : D ⥤ D'` at `d : D'` and
if tensoring left with an object preserves colimits in `V`,
then `K ⊠ H' : D' × E ⥤ V` is a pointwise left Kan extension along `(𝟭 E) × L` at `(e, d)` for
every `e`. -/
def isPointwiseLeftKanExtensionAtExtensionUnitRight (d : D')
(P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d) (e : E)
[Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft <| K.obj e)] :
(Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).IsPointwiseLeftKanExtensionAt (e, d) :=
by
set cone := Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K) |>.coconeAt (e, d)
let equiv := CostructuredArrow.prodEquivalence (𝟭 E) L e d |>.symm
apply Limits.IsColimit.ofWhiskerEquivalence equiv
let I : CostructuredArrow L d ⥤ CostructuredArrow (𝟭 E) e × CostructuredArrow L d :=
-- this definition makes it easier to prove finality of I
(prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse ⋙ (Functor.fromPUnit.{0} <| .mk <| 𝟙 _).prod (𝟭 _)
letI : I.Final :=
by
letI : Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.Final :=
Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e)
apply
Iff.mp <|
Functor.final_iff_final_comp (F := (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse) (G :=
Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.prod <| 𝟭 _)
infer_instance
apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone) |>.toFun
let diag_iso :
(CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e) ≅
I ⋙ equiv.functor ⋙ CostructuredArrow.proj (𝟭 E |>.prod L) (e, d) ⋙ K ⊠ H :=
NatIso.ofComponents (fun _ ↦ Iso.refl _)
apply
Limits.IsColimit.equivOfNatIsoOfIso diag_iso (d :=
Limits.Cocone.whisker I <| Limits.Cocone.whisker equiv.functor cone) (c :=
(tensorLeft <| K.obj e).mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d)
(Limits.Cocones.ext <| .refl _) |>.toFun
exact Limits.PreservesColimit.preserves (F := tensorLeft <| K.obj e) P |>.some
