guitartExact_of_isLeftDerivabilityStructure'

English

There is a dual version stating that Right Derivability is equivalent to Left Derivability after appropriate constructions.

Русский

Существует дуальная версия: правая деривируемость эквивалентна левой деривируемости после соответствующих конструций.

LaTeX

$$$\Phi.IsRightDerivabilityStructure \iff \Phi'.IsLeftDerivabilityStructure$$$

Lean4

theorem guitartExact_of_isLeftDerivabilityStructure' [h : Φ.IsLeftDerivabilityStructure] (e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F) :
    TwoSquare.GuitartExact e.inv := by simpa only [Φ.isLeftDerivabilityStructure_iff L₁ L₂ F e] using h

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