c_isIso_of_iso — Mathlib

English

If a morphism f: X ⟶ Y in PresheafedSpace C is an isomorphism, then the induced map on the structure sheaf component c is also an isomorphism.

Русский

Если морфизм f: X ⟶ Y в PresheafedSpace C является изоморфизмом, то индукциированная карта на компоненте оболочки c тоже изоморфизм.

LaTeX

$$$\forall f:\ X \to Y,\ [\mathrm{IsIso}(f) \Rightarrow \mathrm{IsIso}(f.c)].$$$

Lean4

instance c_isIso_of_iso (f : X ⟶ Y) [IsIso f] : IsIso f.c :=
  (sheafIsoOfIso (asIso f)).isIso_hom

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