instIsCofilteredDiscretePUnit — Mathlib

English

In a cofiltered category, for a bowtie of morphisms f1: k1 → j1, g1: k2 → j1, f2: k1 → j2, g2: k2 → j2, there exist an object s and morphisms α: s → k1, β: s → k2 such that the two resulting squares commute.

Русский

В кофильтрованной категории существует общий подобъект s и стрелки α, β, образующие квадрат так, что две диагональные пары композиторов равны.

LaTeX

$$$$ \\exists s, \\alpha: s\\to k_1, \\beta: s\\to k_2, \\; (\\alpha \\to f_1) = (\\beta \\to g_1) \\land (\\alpha \\to f_2) = (\\beta \\to g_2). $$$$

Lean4

instance : IsCofiltered (Discrete PUnit)
    where
  cone_objs _ Y := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, ⟨⟨by subsingleton⟩⟩, trivial⟩
  cone_maps X Y f
    g :=
    ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, by
      apply ULift.ext
      subsingleton⟩

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