instReflectsIsomorphismsBasedFunctorFunctorObjForgetful

English

The forgetful functor from BasedNatTrans to the underlying functor category reflects isomorphisms: if its image of α is an isomorphism, then α is an isomorphism.

Русский

Забывающий функтор из BasedNatTrans в базовую категорию отражает изоморфизмы: если образ α является изоморфизмом, то сам α также изоморфизм.

LaTeX

$$$\\text{forgetful } (𝒳, 𝒴):\\; (F,G) \\mapsto F\\to G\\text{ reflects isomorphisms}$$$

Lean4

instance : (forgetful 𝒳 𝒴).ReflectsIsomorphisms where
  reflects {F G} α
    _ := by
    constructor
    use {
        toNatTrans := inv ((forgetful 𝒳 𝒴).map α)
        isHomLift' := fun a ↦ by simp [lift_id_inv_isIso] }
    aesop

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