base_isIso_of_iso — Mathlib

English

If a morphism f between PresheafedSpace objects is an isomorphism, then the underlying base map on the underlying topological spaces is also an isomorphism.

Русский

Если морфизм f между объектами PresheafedSpace является изоморфизмом, то базовый отображение f.base на базовых топологических пространствах также является изоморфизмом.

LaTeX

$$$\forall f:\ X \to Y \text{ in } \mathsf{PresheafedSpace}(C),\; [\text{IsIso}(f) \Rightarrow \text{IsIso}(f.{\rm base})].$$$

Lean4

instance base_isIso_of_iso (f : X ⟶ Y) [IsIso f] : IsIso f.base :=
  ((forget _).mapIso (asIso f)).isIso_hom

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