of_equiv — Mathlib

English

If a composition G ⋙ F has conical limits of size κ and G is an equivalence, then F has conical limits of size κ.

Русский

Если композиция G ⋙ F имеет пределы конуса соответствующего размера κ и G является эквивалентностью, то F имеет пределы конуса размера κ.

LaTeX

$$$\forall F, G, [HasConicalLimit^{\text{size}}(V, G \circ F)] \wedge [G.IsEquivalence] \Rightarrow HasConicalLimit^{\text{size}}(V, F).$$$

Lean4

/-- We can transport conical limits of shape `J'` along an equivalence `J' ≌ J`. -/
theorem of_equiv [HasConicalLimitsOfShape J' V C] (G : J' ⥤ J) [G.IsEquivalence] : HasConicalLimitsOfShape J V C where
  hasConicalLimit F := HasConicalLimit.of_equiv_comp V F G

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