Theorems · Definition · category theory

CategoryTheory.isInternallyProjective

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.MonoidalClosed C] → CategoryTheory.ObjectProperty C

An object P : C is internally projective if the functor P ⟶[C] - taking internal homs out of P preserves epimorphisms.

Defined in: Mathlib.CategoryTheory.Preadditive.Projective.Internal
Cited by: 2 results in Mathlib
Foundations: Depth 5 from the axioms · uses no axioms
Assumes: CategoryTheory.Category CategoryTheory.MonoidalCategory CategoryTheory.MonoidalClosed

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.MonoidalCategorystatement and proof · cited by 3,095
CategoryTheory.ObjectPropertystatement · cited by 798
CategoryTheory.ihomproof · cited by 179
CategoryTheory.MonoidalClosedstatement and proof · cited by 134
CategoryTheory.Functor.PreservesEpimorphismsproof · cited by 41

Cited by3

Results whose statement or proof uses this declaration.

CategoryTheory.InternallyProjectiveproof · cited by 8
LightCondensed.internallyProjective_iff_tensor_conditionproof · cited by 2
CategoryTheory.InternallyProjective.ofRetractproof · cited by 0