coneOfConeUncurryIsLimit — Mathlib

English

If each D.obj j is a limit cone and c is a limit cone for uncurry.obj F, then coneOfConeUncurry Q c is a limit cone for uncurry.obj F.

Русский

Если каждый D.obj j есть предельный конус, и c является предельным конусом для uncurry.obj F, то coneOfConeUncurry Q c является предельным конусом для uncurry.obj F.

LaTeX

$$$\forall j,\ IsLimit(D.obj\,j) \quad\text{and}\quad IsLimit\; c \Rightarrow IsLimit(\text{coneOfConeUncurry } Q c).$$$

Lean4

/-- `coneOfConeUncurry Q c` is a limit cone when `c` is a limit cone.
-/
def coneOfConeUncurryIsLimit {D : DiagramOfCones F} (Q : ∀ j, IsLimit (D.obj j)) {c : Cone (uncurry.obj F)}
    (P : IsLimit c) : IsLimit (coneOfConeUncurry Q c)
    where
  lift
    s :=
    P.lift
      { pt := s.pt
        π :=
          { app := fun p => s.π.app p.1 ≫ (D.obj p.1).π.app p.2
            naturality := fun p p' f => by
              dsimp; simp only [Category.id_comp, Category.assoc]
              rcases p with ⟨j, k⟩
              rcases p' with ⟨j', k'⟩
              rcases f with ⟨fj, fk⟩
              dsimp
              slice_rhs 3 4 => rw [← NatTrans.naturality]
              slice_rhs 2 3 => rw [← (D.obj j).π.naturality]
              simp only [Functor.const_obj_map, Category.id_comp, Category.assoc]
              have w := (D.map fj).w k'
              dsimp at w
              rw [← w]
              have n := s.π.naturality fj
              dsimp at n
              simp only [Category.id_comp] at n
              rw [n]
              simp } }
  fac s
    j := by
    apply (Q j).hom_ext
    intro k
    simp
  uniq s m
    w :=
    by
    refine
      P.uniq
        { pt := s.pt
          π := _ } m ?_
    rintro ⟨j, k⟩
    dsimp
    rw [← w j]
    simp

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