isIso_iff_of_hasLeftResolutions — Mathlib

English

If Φ.HasRightResolutions, α : F ⟶ G is an isomorphism in D₂-functors iff all components at L₂.obj(Φ.functor.obj X₁) are isomorphisms.

Русский

Если Φ имеет правые разрешения, то изоморфизм α между функторными отображениями F ⟶ G является изоморфизмом тогда и только тогда, когда каждый компонент αapp на L₂.obj(Φ.functor.obj X₁) является изоморфизмом.

LaTeX

$$$\text{IsIso}(\alpha) \iff \forall X_1, \text{IsIso}(\alpha_{\!\mathrm{obj}(L_2(\Phi.map X_1))}).$$$

Lean4

theorem isIso_iff_of_hasLeftResolutions [Φ.HasLeftResolutions] {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_hasLeftResolutions L₂
      rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]
      apply hα
    exact NatIso.isIso_of_isIso_app α

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