instReflectsIsomorphismsSheafSheafCompose

English

If F reflects isomorphisms, then the functor (sheafCompose J F) reflects isomorphisms.

Русский

Если F отражает изоморфизмы, то (sheafCompose J F) отражает изоморфизмы.

LaTeX

$$$\mathrm{ReflectsIsomorphisms}(\mathrm{sheafCompose}\, J\, F)$$$

Lean4

instance [F.ReflectsIsomorphisms] : (sheafCompose J F).ReflectsIsomorphisms where
  reflects {G₁ G₂} f
    _ :=
    by
    rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _), ←
      isIso_iff_of_reflects_iso _ ((whiskeringRight Cᵒᵖ A B).obj F)]
    change IsIso ((sheafToPresheaf _ _).map ((sheafCompose J F).map f))
    infer_instance

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