Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/SmallObject/Basic.lean

Statistics

Metric	Count
Definitions `HasSmallObjectArgument`, `instOrderBotToTypeOrdSmallObjectκ`, `smallObjectκ`	3
Theorems `exists_cardinal`, `instHasFunctorialFactorizationLlpRlp`, `isCardinalForSmallObjectArgument_smallObjectκ`, `llp_rlp_of_hasSmallObjectArgument`, `llp_rlp_of_hasSmallObjectArgument'`, `smallObjectκ_isRegular`	6
Total	9

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`HasSmallObjectArgument` 📖	CompData	1 math math: `CategoryTheory.IsGrothendieckAbelian.instHasSmallObjectArgumentGeneratingMonomorphisms`
`instOrderBotToTypeOrdSmallObjectκ` 📖	CompOp	2 math math: `isCardinalForSmallObjectArgument_smallObjectκ`, `llp_rlp_of_hasSmallObjectArgument'`
`smallObjectκ` 📖	CompOp	3 math math: `smallObjectκ_isRegular`, `isCardinalForSmallObjectArgument_smallObjectκ`, `llp_rlp_of_hasSmallObjectArgument'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasFunctorialFactorizationLlpRlp` 📖	mathematical	—	`HasFunctorialFactorization` `llp` `rlp`	—	`CategoryTheory.SmallObject.hasFunctorialFactorization` `smallObjectκ_isRegular` `isCardinalForSmallObjectArgument_smallObjectκ`
`isCardinalForSmallObjectArgument_smallObjectκ` 📖	mathematical	—	`IsCardinalForSmallObjectArgument` `smallObjectκ` `smallObjectκ_isRegular` `instOrderBotToTypeOrdSmallObjectκ`	—	`HasSmallObjectArgument.exists_cardinal`
`llp_rlp_of_hasSmallObjectArgument` 📖	mathematical	—	`llp` `rlp` `retracts` `transfiniteCompositions` `pushouts` `coproducts`	—	`CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument` `smallObjectκ_isRegular` `isCardinalForSmallObjectArgument_smallObjectκ`
`llp_rlp_of_hasSmallObjectArgument'` 📖	mathematical	—	`llp` `rlp` `retracts` `transfiniteCompositionsOfShape` `pushouts` `coproducts` `Ordinal.ToType` `Cardinal.ord` `smallObjectκ` `linearOrder_toType` `Ordinal.instSuccOrderToType` `instOrderBotToTypeOrdSmallObjectκ` `wellFoundedLT_toType`	—	`CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'` `smallObjectκ_isRegular` `isCardinalForSmallObjectArgument_smallObjectκ`
`smallObjectκ_isRegular` 📖	mathematical	—	`Fact` `Cardinal.IsRegular` `smallObjectκ`	—	`HasSmallObjectArgument.exists_cardinal`

CategoryTheory.MorphismProperty.HasSmallObjectArgument

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_cardinal` 📖	mathematical	—	`Cardinal` `Fact` `Cardinal.IsRegular` `OrderBot` `Ordinal.ToType` `Cardinal.ord` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `linearOrder_toType` `CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument`	—	—

---

← Back to Index