isIso_of_toNatTrans_isIso — Mathlib

English

If α is a natural transformation between endofunctors with an isomorphism of its underlying natural transformation, then α is an isomorphism in the category of BasedNatTrans.

Русский

Если натуральная трансформация α между функторaми имеет изоморфизм своей основы, то α является изоморфизмом в категории BasedNatTrans.

LaTeX

$$$\\text{IsIso }\\alpha$ given [IsIso α^{toNatTrans}].$$

Lean4

theorem isIso_of_toNatTrans_isIso (α : F ⟶ G) [IsIso (X := F.toFunctor) α.toNatTrans] : IsIso α :=
  have : IsIso ((forgetful 𝒳 𝒴).map α) := by simp_all
  Functor.ReflectsIsomorphisms.reflects (forgetful 𝒳 𝒴) α

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