Mathlib Map

Structures · Category theory

CategoryTheory.Functor.PreservesProjectiveObjects

A functor preserves projective objects if it maps projective objects to projective objects.

Defined in
Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Shape
One type argument · adds projective_obj

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances2

  • ModuleCat
  • Rep

How is a type an instance?

Loading the hierarchy index…

Assumed by9

Ancestors0

No ancestors.