isoEquiv — Mathlib

English

There is a natural bijection between isomorphisms X ≅ Y in C and isomorphisms F X ≅ F Y in D provided F is fully faithful.

Русский

Существует естественная биекция между изоморфизмами X ≅ Y в C и изоморфизмами F X ≅ F Y в D при условии, что F полностью верен.

LaTeX

$$$\big(X \cong Y\big) \cong \big(F X \cong F Y\big)$, natural in X,Y, induced by $F.mapIso$ and $F$.preimageIso$$

Lean4

/-- The equivalence `(X ≅ Y) ≃ (F.obj X ≅ F.obj Y)` given by `h : F.FullyFaithful`. -/
@[simps]
def isoEquiv {X Y : C} : (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
    where
  toFun := F.mapIso
  invFun := hF.preimageIso
  left_inv := by cat_disch
  right_inv := by cat_disch

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