isStableUnderLimitsOfShape_iff_limitsOfShape_le

English

The mk' construction in limitsOfShape provides a morphism property in the functor category given suitable IsLimit hypotheses and a compatible φ.

Русский

Конструкция mk' в limitsOfShape задаёт свойство морфизмов в категории функций, если имеются соответствующие условия IsLimit и согласование φ.

LaTeX

$$Given X₁, X₂, c₁, c₂, h₁, h₂, f, hf, φ, hφ, we have W.limitsOfShape J φ.$$

Lean4

theorem isStableUnderLimitsOfShape_iff_limitsOfShape_le : W.IsStableUnderLimitsOfShape J ↔ W.limitsOfShape J ≤ W :=
  by
  constructor
  · rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩
    exact h.condition _ _ _ _ h₁ h₂ f hf _ (by simp)
  · rintro h
    constructor
    intro X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ
    exact h _ (limitsOfShape.mk' X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ)

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