preservesFiniteLimits_of_preservesFiniteLimitsOfSize

English

If F ≅ G and F preserves finite limits, then G preserves finite limits.

Русский

Если F и G естественно изоморфны и F сохраняет конечные пределы, то G сохраняет конечные пределы.

LaTeX

$$PreservesFiniteLimits(F) ⇒ PreservesFiniteLimits(G) given F ≅ G$$

Lean4

/-- We can always derive `PreservesFiniteLimits C` by showing that we are preserving limits at an
arbitrary universe. -/
theorem preservesFiniteLimits_of_preservesFiniteLimitsOfSize (F : C ⥤ D)
    (h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), PreservesLimitsOfShape J F) :
    PreservesFiniteLimits F where
  preservesFiniteLimits J (_ : SmallCategory J)
    _ := by
    haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
    exact preservesLimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

Похожие утверждения