instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact

English

The square built from identities has Guitart exactness.

Русский

Квадрат, построенный из тождественных функторов, является точным по Гитхарту.

LaTeX

$$$\mathrm{GuitartExact}(\mathrm{TwoSquare.mk}(\mathrm{id}, F, F, \mathrm{id}, \mathrm{Id}(F)))$$$

Lean4

instance [hw : w.GuitartExact] {X₂ : C₂} (g : StructuredArrow (R.obj X₂) B) :
    IsConnected (CostructuredArrow (w.structuredArrowDownwards X₂) g) :=
  by
  rw [guitartExact_iff_isConnected_downwards] at hw
  apply hw

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