preserves limits

Stream: Infinity-Cosmos

[Jon Eugster]

Is this, or some modified similar version of this true?

import Mathlib

open CategoryTheory Limits

-- TODO: hyps are too strong and just copy-pasted over, some can be dropped, e.g. `V` & `EnrichedOrdinaryCategory`
theorem helper {J : Type u₁} [Category.{v₁, u₁} J]
    {K : Type u₂} [Category.{v₂, u₂} K]
    (V : Type u') [Category.{v', u'} V] [MonoidalCategory V]
    {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C]
    (F : J ⥤ C) (e : K ≌ J) (G : C ⥤ V)
    (h : PreservesLimit F G) : PreservesLimit (e.functor ⋙ F) G := by
  constructor
  intro c hc
  apply Nonempty.intro
  sorry

[Markus Himmel]

Here is a quick-and-dirty proof:

import Mathlib

open CategoryTheory Limits

-- TODO: hyps are too strong and just copy-pasted over, some can be dropped, e.g. `V` & `EnrichedOrdinaryCategory`
theorem helper {J : Type u₁} [Category.{v₁, u₁} J]
    {K : Type u₂} [Category.{v₂, u₂} K]
    (V : Type u') [Category.{v', u'} V] [MonoidalCategory V]
    {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C]
    (F : J ⥤ C) (e : K ≌ J) (G : C ⥤ V)
    (h : PreservesLimit F G) : PreservesLimit (e.functor ⋙ F) G := by
  constructor
  intro c hc
  apply Nonempty.intro
  have := hc.whiskerEquivalence e.symm
  let equ := e.invFunIdAssoc F
  have := (IsLimit.postcomposeHomEquiv equ _).symm this
  have := (isLimitOfPreserves G this)
  refine IsLimit.ofIsoLimit (this.whiskerEquivalence e) ?_
  refine Cones.ext (Iso.refl _) fun j => ?_
  simp [equ, ← Functor.map_comp]
  have := c.w (e.unit.app j)
  simp at this
  simp [← this, ← Functor.map_comp]

[Jon Eugster]

thank you :)