forget_reflects_isos — Mathlib

English

The forgetful functor forgets isomorphisms: if the underlying morphism is an isomorphism, the original morphism is an isomorphism in the domain category.

Русский

Функтор забывания отражает изоморфизмы: если базовый морфизм является изоморфизмом, то исходный морфизм является изоморфизмом в исходной категории.

LaTeX

$$(forget (BialgCat R)).ReflectsIsomorphisms$$

Lean4

instance forget_reflects_isos : (forget (BialgCat.{v} R)).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget (BialgCat.{v} R)).map f)
    let e : X ≃ₐc[R] Y := { f.toBialgHom, i.toEquiv with }
    exact ⟨e.toBialgIso.isIso_hom.1⟩

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