essSurj_of_hasRightResolutions — Mathlib

English

If Φ.HasRightResolutions and L₂ is a localization, the composite (Φ.functor ⋙ L₂) is essentially surjective.

Русский

Если Φ имеет правые разрешения и L₂ локализация, то композиция (Φ.functor ⋙ L₂) полна по образу (essSurj).

LaTeX

$$$\text{EssSurj}(\Φ.functor \circ L_2).$$$

Lean4

theorem essSurj_of_hasRightResolutions [Φ.HasRightResolutions] : (Φ.functor ⋙ L₂).EssSurj where
  mem_essImage
    X₂ := by
    have := Localization.essSurj L₂ W₂
    have R : Φ.RightResolution (L₂.objPreimage X₂) := Classical.arbitrary _
    exact ⟨R.X₁, ⟨(Localization.isoOfHom L₂ W₂ _ R.hw).symm ≪≫ L₂.objObjPreimageIso X₂⟩⟩

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