Documentation

Mathlib.CategoryTheory.Functor.EpiMono

Preservation and reflection of monomorphisms and epimorphisms #

We provide typeclasses that state that a functor preserves or reflects monomorphisms or epimorphisms.

A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.

Instances

    A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.

    Instances

      A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves monomorphisms.

      Instances
        • reflects : ∀ {X Y : C} (f : X Y), CategoryTheory.Epi (F.map f)CategoryTheory.Epi f

          A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.

        A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.

        Instances

          If F is a fully faithful functor, split epimorphisms are preserved and reflected by F.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            If F is a fully faithful functor, split monomorphisms are preserved and reflected by F.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For