ofConeOfConeUncurry — Mathlib

English

If D.obj j are limit cones and c is a cone on uncurry.obj F, and P is IsLimit c, then P.lift yields an IsLimit structure for cone S built from D and c, giving c as a limit via S.

Русский

Если D.obj j — предел-конусы, и c является конусом над uncurry.obj F, а P является IsLimit c, то P.lift порождает структуру IsLimit для конуса S, построенного из D и c, тем самым задавая предел для c через S.

LaTeX

$$$\text{IsLimit} \ c \Rightarrow \text{IsLimit} \ (\text{coneOfConeUncurry } Q c).$$$

Lean4

/-- If `coneOfConeUncurry Q c` is a limit cone then `c` is in fact a limit cone.
-/
def ofConeOfConeUncurry {D : DiagramOfCones F} (Q : ∀ j, IsLimit (D.obj j)) {c : Cone (uncurry.obj F)}
    (P : IsLimit (coneOfConeUncurry Q c)) : IsLimit c :=
  -- These constructions are used in various fields of the proof so we abstract them here.

  letI E (j : J) : Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j := NatIso.ofComponents (fun _ ↦ Iso.refl _)
  letI S (s : Cone (uncurry.obj F)) : Cone D.conePoints :=
    { pt := s.pt
      π :=
        { app j := (Q j).lift <| (Cones.postcompose (E j).hom).obj <| s.whisker (Prod.sectR j K)
          naturality {j' j} f := (Q j).hom_ext <| fun k ↦ by simpa [E] using s.π.naturality ((Prod.sectL J k).map f) } }
  { lift s := P.lift (S s)
    fac s
      p := by
      have h1 := (Q p.1).fac ((Cones.postcompose (E p.1).hom).obj <| s.whisker (Prod.sectR p.1 K)) p.2
      simp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj, Cones.postcompose_obj_pt, Cone.whisker_pt,
        Cones.postcompose_obj_π, Cone.whisker_π, NatTrans.comp_app, Functor.const_obj_obj, whiskerLeft_app,
        NatIso.ofComponents_hom_app, Iso.refl_hom, Category.comp_id, E] at h1
      have h2 := (P.fac (S s) p.1)
      dsimp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj, NatTrans.id_app, Functor.const_obj_obj,
        DiagramOfCones.conePoints_obj, DiagramOfCones.conePoints_map, Functor.const_obj_map, id_eq,
        Cones.postcompose_obj_pt, Cone.whisker_pt, Cones.postcompose_obj_π, Cone.whisker_π, NatTrans.comp_app,
        whiskerLeft_app, NatIso.ofComponents_hom_app, Iso.refl_hom, Prod.sectL_obj, Prod.sectL_map, eq_mp_eq_cast,
        eq_mpr_eq_cast, coneOfConeUncurry_pt, coneOfConeUncurry_π_app, S, E] at h2 ⊢
      simp [← h1, ← h2]
    uniq s f hf := P.uniq (s := S s) _ <| fun j ↦ (Q j).hom_ext <| fun k ↦ by simpa [S, E] using hf (j, k) }

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