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