multicofork — Mathlib

English

If c is a Colimit, then the square formed by I.fst default, I.snd default and c.πs is a pushout.

Русский

Если c является колимитом, то квадрат, образованный I.fst default, I.snd default и c.π-образами, является pushout.

LaTeX

$$$\text{IsPushout} (I.fst\ default) (I.snd\ default) (c.\pi (J.fst default)) (c.\pi (J.snd default))$$$

Lean4

/-- Given a multispan shape `J` which is essentially `.ofLinearOrder ι`
(where `ι` has exactly two elements), this is the multicofork
deduced from a pushout cocone. -/
noncomputable def multicofork : Multicofork I :=
  Multicofork.ofπ _ s.pt
    (fun k ↦
      if hk : k = J.fst default then eqToHom (by simp [hk]) ≫ s.inl
      else
        eqToHom
            (by
              obtain rfl : k = J.snd default := by
                have := h.symm.le (Set.mem_univ k)
                simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at this
                tauto
              rfl) ≫
          s.inr)
    (by
      rw [Unique.forall_iff]
      simpa [h'.symm] using s.condition)

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