lowerCone — Mathlib

English

There is a limit cone lifting property for mapCone along principalsKanExtension, i.e., the constructed cone is a limit of the diagram.

Русский

Существует предел-конус, удовлетворяющий свойству предела диаграммы для mapCone вдоль principalsKanExtension.

LaTeX

$$$\text{IsLimit}(\mathrm{mapCone}(\mathrm{principalsKanExtension}(F), \cdots))$$$

Lean4

/-- This is an auxiliary definition which is only meant to be used in `isLimit` below. -/
@[simps]
def lowerCone {α : Type v} (Us : α → Opens X)
    (S : Cone ((ObjectProperty.ι fun V => ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)) :
    Cone (generator (iSup Us) ⋙ F) where
  pt := S.pt
  π :=
    { app := fun f =>
        S.π.app ((projSup Us).obj f) ≫ limit.π (generator (principalOpen f.right) ⋙ F) ⟨.mk .unit, f.right, 𝟙 _⟩
      naturality := by
        rintro x y e
        simp only [Functor.const_obj_obj, Functor.comp_obj, Functor.const_obj_map, Functor.op_obj, ObjectProperty.ι_obj,
          Functor.pointwiseRightKanExtension_obj, Category.id_comp, Functor.comp_map, Category.assoc]
        rw [← S.w ((projSup Us).map e), Category.assoc]
        congr 1
        simp only [projSup_obj, Functor.comp_obj, Functor.op_obj, ObjectProperty.ι_obj,
          Functor.pointwiseRightKanExtension_obj, projSup_map, homOfLE_leOfHom, Functor.comp_map, Functor.op_map,
          Quiver.Hom.unop_op, Functor.pointwiseRightKanExtension_map, limit.lift_π]
        let xx : StructuredArrow (Opposite.op (principalOpen x.right)) (principals X) := ⟨.mk .unit, x.right, 𝟙 _⟩
        let yy : StructuredArrow (Opposite.op (principalOpen x.right)) (principals X) :=
          ⟨.mk .unit, y.right, .op <| LE.le.hom <| principalOpen_le e.right.le⟩
        let ee : xx ⟶ yy := { left := 𝟙 _, right := e.right }
        exact limit.w (StructuredArrow.proj (Opposite.op (principalOpen x.right)) (principals X) ⋙ F) ee |>.symm }

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