bijective_respectsIso — Mathlib

English

The surjective property is stable under isomorphisms: if a morphism is surjective, its isomorphic image remains surjective via forgetful functors.

Русский

Сюръективность сохраняется под изоморфизмами: образ через изоморфизм остается сюръективным через забывающий функтор.

LaTeX

$$$ (\\text{MorphismProperty.surjective } C).RespectsIso$.$$

Lean4

instance bijective_respectsIso : (MorphismProperty.bijective C).RespectsIso :=
  respectsIso_of_isStableUnderComposition (fun _ _ f (_ : IsIso f) => ((forget C).mapIso (asIso f)).toEquiv.bijective)

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