isStableUnderColimitsOfShape_iff_colimitsOfShape_le

English

W is stable under colimits of shape J if and only if W.colimitsOfShape J ≤ W.

Русский

W стабилен относительно колимит по форме J тогда и только тогда, когда W.colimitsOfShape J ≤ W.

LaTeX

$$W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape J ≤ W$$

Lean4

theorem isStableUnderColimitsOfShape_iff_colimitsOfShape_le :
    W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape 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 _ (colimitsOfShape.mk' X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ)

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