isIso_iff_of_hasRightResolutions — Mathlib

English

If Φ.HasLeftResolutions, then Φ.op.HasRightResolutions.

Русский

Если у Φ есть левые разрешения, то у Φ.op есть правые разрешения.

LaTeX

$$$[\Phi.HasLeftResolutions] \Rightarrow [\Phi^{op}.HasRightResolutions].$$$

Lean4

theorem isIso_iff_of_hasRightResolutions [Φ.HasRightResolutions] {F G : D₂ ⥤ H} (α : F ⟶ G) :
    IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁))) :=
  by
  constructor
  · intros
    infer_instance
  · intro hα
    have : ∀ (X₂ : D₂), IsIso (α.app X₂) := fun X₂ =>
      by
      have := Φ.essSurj_of_hasRightResolutions L₂
      rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]
      apply hα
    exact NatIso.isIso_of_isIso_app α

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