instIsIsoFunctorHom — Mathlib

English

If f: F ⟶ G is an isomorphism of single-functors, then for every n ∈ A, the component f.hom n is an isomorphism between the corresponding functor components, i.e., f.hom n is invertible.

Русский

Если f: F ⟶ G — изоморфизм однопараметрических функторов, то для каждого n ∈ A компонент f.hom n является изоморфизмом между соответствующими компонентами функторов.

LaTeX

$$$ \forall n: A, \ IsIso(f.hom(n)). $$$

Lean4

instance (f : F ⟶ G) [IsIso f] (n : A) : IsIso (f.hom n) :=
  (inferInstance : IsIso ((evaluation C D n).map f))

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