mk' — Mathlib

English

Given morphisms and cones in a functor category with a shape J, the limitsOfShape construction yields a morphism property that respects the given data, under a limit IsLimit structure.

Русский

Задаётся свойство пределов формы mk' в категории функций, сохраняемое под IsLimit.

LaTeX

$$Theorem: given X₁, X₂ : J ⥤ C, c₁, c₂ IsLimit cones, f, hf, φ with compatibility, then W.limitsOfShape J φ holds.$$

Lean4

theorem mk' (X₁ X₂ : J ⥤ C) (c₁ : Cone X₁) (c₂ : Cone X₂) (h₁ : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂)
    (hf : W.functorCategory J f) (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ j, φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) :
    W.limitsOfShape J φ :=
  by
  obtain rfl : φ = h₂.lift (Cone.mk _ (c₁.π ≫ f)) := h₂.hom_ext (fun j ↦ by simp [hφ])
  exact ⟨_, _, _, _, h₁, _, _, hf⟩

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