Mathlib Map

Structures · Category theory

CategoryTheory.ExtremalEpi

An extremal epimorphism f : X ⟶ Y is an epimorphism which does not factor through any proper subobject of Y.

Defined in
Mathlib.CategoryTheory.ExtremalEpi
Shape
One type argument · adds isIso

Extends1

Extended by0

Nothing extends this class yet.

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by5

Ancestors1