preservesSheafification_of_adjunction

English

A variant of preservesSheafification asserting the same property in a broader setting of adjunctions in sheaf contexts.

Русский

Вариант утверждения о сохранении шейфикации в более широком контексте сопряжений в шейфовых контекстах.

LaTeX

$$$J.PreservesSheafification\\,G$ (variant)$$

Lean4

theorem preservesSheafification_of_adjunction (adj : G ⊣ F) : J.PreservesSheafification G where
  le P Q f
    hf := by
    have := adj.isRightAdjoint
    rw [MorphismProperty.inverseImage_iff]
    dsimp
    intro R hR
    rw [← ((adj.whiskerRight Cᵒᵖ).homEquiv P R).comp_bijective]
    convert
      (((adj.whiskerRight Cᵒᵖ).homEquiv Q R).trans
          (hf.homEquiv (R ⋙ F) ((sheafCompose J F).obj ⟨R, hR⟩).cond)).bijective
    ext g X
    dsimp
    rw [← NatTrans.comp_app]
    congr
    exact Adjunction.homEquiv_naturality_left _ _ _

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