sheafComposeNatTrans_app_uniq — Mathlib

English

The equivalence between preservesSheafification and isIso of the sheafComposeNatTrans holds under HasSheafCompose assumptions.

Русский

Эквивалентность сохраняет шарообразование и изоморфизм SheafComposeNatTrans сохраняется при наличии HasSheafCompose.

LaTeX

$$$J.PreservesSheafification F \iff IsIso (\text{sheafComposeNatTrans } J F adj_1 adj_2)$$$

Lean4

theorem sheafComposeNatTrans_app_uniq (P : Cᵒᵖ ⥤ A) (α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
    (hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F) :
    α = (sheafComposeNatTrans J F adj₁ adj₂).app P :=
  by
  apply (adj₂.homEquiv _ _).injective
  dsimp [sheafComposeNatTrans]
  erw [Equiv.apply_symm_apply]
  rw [← hα]
  apply adj₂.homEquiv_unit

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