mapIso — Mathlib

English

If two maps f and g are equal, then the induced functors map f and map g are isomorphic.

Русский

Если два отображения f и g равны, индуцированные функторы map f и map g изоморфны.

LaTeX

$$$\\text{If } f=g, \\; map(f) \\cong map(g)$$$

Lean4

/-- If two continuous maps `f g : X ⟶ Y` are equal,
then the functors `Opens Y ⥤ Opens X` they induce are isomorphic.
-/
def mapIso (f g : X ⟶ Y) (h : f = g) : map f ≅ map g :=
  NatIso.ofComponents fun U => eqToIso (by rw [congr_arg map h])

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