of_binaryCofan — Mathlib

English

Given a binary cofan c with a colimit, and mono legs, there is a canonical construction of a BinaryCoproductDisjoint X Y.

Русский

При наличии бинарного кофана с колимитом и моно-ножками строится дисjoint копродукт.

LaTeX

$$$\\text{BinaryCoproductDisjoint}\\ X\\ Y$$$

Lean4

theorem of_binaryCofan {c : BinaryCofan X Y} (hc : IsColimit c) [Mono c.inl] [Mono c.inr] {s : PullbackCone c.inl c.inr}
    (hs : IsLimit s) (H : IsInitial s.pt) : BinaryCoproductDisjoint X Y :=
  by
  have (i : WalkingPair) : Mono (Cofan.inj c i) := by
    cases i
    · exact inferInstanceAs <| Mono c.inl
    · exact inferInstanceAs <| Mono c.inr
  refine .of_cofan hc (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_)
  ·
    match i, j with
    | .left, .right => exact s
    | .right, .left => exact s.flip
  · dsimp
    split
    · exact hs
    · exact PullbackCone.flipIsLimit hs
  · dsimp; split <;> exact H

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