of_equiv_comp — Mathlib

English

If G is an equivalence and HasConicalLimitsOfShape for G ⋙ F, then F has conical limits of the same shape.

Русский

Если G эквивалентно и HasConicalLimitsOfShape для G ⋙ F, то F имеет конусные пределы той же формы.

LaTeX

$$$\forall F: J \to C,\; \forall G: J' \to J, [G.IsEquivalence] \Rightarrow HasConicalLimitsOfShape J V C \text{ if } HasConicalLimitsOfShape J' V C \text{ for } G \odot F.$$$

Lean4

/-- If a `G ⋙ F` has a limit, and `G` is an equivalence, we can construct a limit of `F`. -/
theorem of_equiv_comp (F : J ⥤ C) (G : J' ⥤ J) [G.IsEquivalence] [HasConicalLimit V (G ⋙ F)] : HasConicalLimit V F :=
  have e : G.inv ⋙ G ⋙ F ≅ F := G.asEquivalence.invFunIdAssoc F
  HasConicalLimit.of_iso V e

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