Documentation

Mathlib.CategoryTheory.MorphismProperty.Concrete

Morphism properties defined in concrete categories #

In this file, we define the class of morphisms MorphismProperty.injective, MorphismProperty.surjective, MorphismProperty.bijective in concrete categories, and show that it is stable under composition and respect isomorphisms.

We introduce type-classes HasSurjectiveInjectiveFactorization and HasFunctorialSurjectiveInjectiveFactorization expressing that in a concrete category C, all morphisms can be factored (resp. factored functorially) as a surjective map followed by an injective map.

@[reducible, inline]

The property that any morphism in a concrete category can be factored as a surjective map followed by an injective map.

Equations
@[reducible, inline]

The property that any morphism in a concrete category can be functorially factored as a surjective map followed by an injective map.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

The structure containing the data of a functorial factorization of morphisms as a surjective map followed by an injective map in a concrete category.

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

In the category of types, any map can be functorially factored as a surjective map followed by an injective map.

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