instIsIsoOverAsOverHom — Mathlib

English

If e: X ≅ Y is an isomorphism and HomIsOver e.hom S, then HomIsOver e.inv S, i.e., isomorphisms preserve the over structure on morphisms.

Русский

Если e: X ≅ Y — изоморфизм и HomIsOver e.hom S, то HomIsOver e.inv S, то есть изоморфизмы сохраняют структуру над S для морфизмов.

LaTeX

$$$[HomIsOver e.hom S] \Rightarrow HomIsOver e.inv S$$$

Lean4

instance (f : X ⟶ Y) [IsIso f] [HomIsOver f S] : IsIso (asOverHom S f) :=
  have : IsIso ((Over.forget S).map (asOverHom S f)) := ‹_›
  isIso_of_reflects_iso _ (Over.forget _)

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