mk' — Mathlib

English

If Φ.IsLeftDerivabilityStructure, then ((Φ.catCommSq L₁ L₂).iso).inv gives a guitart exactness for the inverted direction.

Русский

Если Φ обладает левой деривируемостью, то соответствующий инверсный изоморфизм даёт точность Гитурата.

LaTeX

$$$[\Phi.IsLeftDerivabilityStructure] \Rightarrow TwoSquare.GuitartExact\big((\Phi.catCommSq L_1 L_2).iso\!\big).inv$$$

Lean4

/-- If a localizer morphism `Φ` is a localized equivalence, then it is a right
derivability structure if the categories of right resolutions are connected and the
categories of right resolutions of arrows are nonempty. -/
theorem mk' [Φ.IsLocalizedEquivalence] : Φ.IsRightDerivabilityStructure :=
  by
  rw [Φ.isRightDerivabilityStructure_iff (Φ.functor ⋙ W₂.Q) W₂.Q (𝟭 _) (Functor.rightUnitor _).symm,
    TwoSquare.guitartExact_iff_isConnected_downwards]
  intro X₂ X₃ g
  apply Constructor.isConnected

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