isLeftDerivabilityStructure_iff — Mathlib

English

There is an equivalence between Φ.IsLeftDerivabilityStructure and TwoSquare.GuitartExact e.inv for a suitable isomorphism e, when Φ HasLeftResolutions.

Русский

Существует эквивалентность между Φ.IsLeftDerivabilityStructure и TwoSquare.GuitartExact e.inv для подходящего изоморфизма e, если у Φ есть левый набор резолюций.

LaTeX

$$$[\Phi.HasLeftResolutions] \;\Rightarrow\; (\Phi.IsLeftDerivabilityStructure \iff TwoSquare.GuitartExact(e.inv))$$$

Lean4

theorem isLeftDerivabilityStructure_iff [Φ.HasLeftResolutions] (e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F) :
    Φ.IsLeftDerivabilityStructure ↔ TwoSquare.GuitartExact e.inv :=
  by
  rw [isLeftDerivabilityStructure_iff_op, Φ.op.isRightDerivabilityStructure_iff L₁.op L₂.op F.op (NatIso.op e.symm), ←
    TwoSquare.guitartExact_op_iff e.inv]
  rfl

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