isLeftDerivabilityStructure_iff_op

English

There is a symmetry: Φ.IsLeftDerivabilityStructure is equivalent to Φ.op.IsRightDerivabilityStructure.

Русский

Существует симметрия: Φ.IsLeftDerivabilityStructure эквивалентна Φ.op.IsRightDerivabilityStructure.

LaTeX

$$$\Phi.IsLeftDerivabilityStructure \iff \Phi^{\mathrm{op}}.IsRightDerivabilityStructure$$$

Lean4

theorem isLeftDerivabilityStructure_iff_op : Φ.IsLeftDerivabilityStructure ↔ Φ.op.IsRightDerivabilityStructure :=
  by
  let F := Φ.localizedFunctor W₁.Q W₂.Q
  let e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := (Φ.catCommSq W₁.Q W₂.Q).iso
  let e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
  have eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv := TwoSquare.guitartExact_op_iff _
  constructor
  · rintro ⟨_, _⟩
    rwa [Φ.op.isRightDerivabilityStructure_iff _ _ _ e', eq]
  · intro
    have : Φ.HasLeftResolutions := by
      rw [hasLeftResolutions_iff_op]
      infer_instance
    refine ⟨inferInstance, ?_⟩
    rw [← eq]
    exact Φ.op.guitartExact_of_isRightDerivabilityStructure' _ _ _ e'

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