surjective_respectsIso — Mathlib

English

The property of being injective is compatible with isomorphisms: if a morphism has the injective property, then its isomorphic image under forgetful or associated functors preserves injectivity.

Русский

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

LaTeX

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

Lean4

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

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