Internal

📁 Source: Mathlib/CategoryTheory/Preadditive/Projective/Internal.lean

Statistics

Metric	Count
Definitions isInternallyProjective	1
Theorems ofRetract, preserves_epi, instIsStableUnderRetractsIsInternallyProjective	3
Total	4

CategoryTheory

Definitions

Name	Category	Theorems
isInternallyProjective 📖	CompOp	1 math math: instIsStableUnderRetractsIsInternallyProjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStableUnderRetractsIsInternallyProjective 📖	mathematical	—	ObjectProperty.IsStableUnderRetracts isInternallyProjective	—	Functor.preservesEpimorphisms.ofRetract InternallyProjective.preserves_epi

CategoryTheory.InternallyProjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofRetract 📖	mathematical	—	CategoryTheory.InternallyProjective	—	CategoryTheory.ObjectProperty.prop_of_retract CategoryTheory.instIsStableUnderRetractsIsInternallyProjective CategoryTheory.ObjectProperty.prop_of_is
preserves_epi 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed	—	CategoryTheory.ObjectProperty.prop_of_is

---

← Back to Index