functoriality_full — Mathlib

English

A bilimit for the binary bicone corresponds exactly to a bilimit for the original bicone.

Русский

Билимит для бинарного бикона точно соответствует билимиту исходного бикона.

LaTeX

$$$$ \text{IsLimit}(b.toBinaryBicone.toCone) \simeq \text{IsLimit}(b.toCone) $$$$

Lean4

instance functoriality_full [F.Full] [F.Faithful] : (functoriality P Q F).Full where
  map_surjective
    t :=
    ⟨{  hom := F.preimage t.hom
        winl := F.map_injective (by simpa using t.winl)
        winr := F.map_injective (by simpa using t.winr)
        wfst := F.map_injective (by simpa using t.wfst)
        wsnd := F.map_injective (by simpa using t.wsnd) }, by cat_disch⟩

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