IsCardinalForSmallObjectArgument

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

Statistics

Metric	Count
Definitions IsCardinalForSmallObjectArgument, attachCellsOfSuccStructProp, functorialFactorizationData, iteration, iterationFunctor, iterationFunctorMapSuccAppArrowIso, iterationFunctorObjObjRightIso, iterationObjRightIso, obj, objMap, propArrow, relativeCellComplexιObj, relativeCellComplexιObjFObjSuccIso, succStruct, transfiniteCompositionOfShapeSuccStructPropιIteration, transfiniteCompositionOfShapeιIterationAppRight, ιIteration, ιObj, πObj	19
Theorems hasCoproducts, hasIterationOfShape, hasPushouts, isSmall, locallySmall, preservesColimit, functorialFactorizationData_Z_map, functorialFactorizationData_Z_obj, functorialFactorizationData_i_app, functorialFactorizationData_p_app, hasColimitsOfShape_discrete, hasCoproducts, hasFunctorialFactorization, hasIterationOfShape, hasPushouts, hasRightLiftingProperty_πObj, instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor, instIsIsoRightAppArrowιIteration, isSmall, iterationFunctorMapSuccAppArrowIso_hom_left, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, iterationFunctorObjObjRightIso_ιIteration_app_right, iterationFunctorObjObjRightIso_ιIteration_app_right_assoc, iterationObjRightIso_hom, llp_rlp_of_isCardinalForSmallObjectArgument, llp_rlp_of_isCardinalForSmallObjectArgument', llp_rlp_ιObj, locallySmall, objMap_comp, objMap_comp_assoc, objMap_id, preservesColimit, prop_iterationFunctor_map_succ, rlp_πObj, succStruct_prop_le_propArrow, transfiniteCompositionOfShapeSuccStructPropιIteration_F, transfiniteCompositionsOfShape_ιObj, ιFunctorObj_eq, ιObj_naturality, ιObj_naturality_assoc, ιObj_πObj, ιObj_πObj_assoc, πFunctorObj_eq, πObj_naturality, πObj_naturality_assoc, πObj_ιIteration_app_right, πObj_ιIteration_app_right_assoc	48
Total	67

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
IsCardinalForSmallObjectArgument 📖	CompData	2 math math: isCardinalForSmallObjectArgument_smallObjectκ, HasSmallObjectArgument.exists_cardinal

CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCoproducts 📖	mathematical	—	CategoryTheory.Limits.HasCoproducts	—	—
hasIterationOfShape 📖	mathematical	—	CategoryTheory.Limits.HasIterationOfShape Ordinal.ToType Cardinal.ord linearOrder_toType	—	—
hasPushouts 📖	mathematical	—	CategoryTheory.Limits.HasPushouts	—	—
isSmall 📖	mathematical	—	CategoryTheory.MorphismProperty.IsSmall	—	—
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall	—	—
preservesColimit 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.types Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.TransfiniteCompositionOfShape.F Ordinal.instSuccOrderToType wellFoundedLT_toType HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape Set.Elem CategoryTheory.Arrow CategoryTheory.MorphismProperty.toSet CategoryTheory.Comma.left CategoryTheory.Functor.id Set Set.instMembership CategoryTheory.Comma.right CategoryTheory.MorphismProperty.homFamily CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op	—	—

CategoryTheory.SmallObject

Definitions

Name	Category	Theorems
attachCellsOfSuccStructProp 📖	CompOp	—
functorialFactorizationData 📖	CompOp	4 math math: functorialFactorizationData_i_app, functorialFactorizationData_Z_obj, functorialFactorizationData_Z_map, functorialFactorizationData_p_app
iteration 📖	CompOp	7 math math: πObj_ιIteration_app_right, iterationObjRightIso_hom, πObj_ιIteration_app_right_assoc, iterationFunctorObjObjRightIso_ιIteration_app_right, transfiniteCompositionOfShapeSuccStructPropιIteration_F, iterationFunctorObjObjRightIso_ιIteration_app_right_assoc, instIsIsoRightAppArrowιIteration
iterationFunctor 📖	CompOp	10 math math: ιFunctorObj_eq, instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, iterationFunctorMapSuccAppArrowIso_hom_left, πFunctorObj_eq, iterationFunctorObjObjRightIso_ιIteration_app_right, transfiniteCompositionOfShapeSuccStructPropιIteration_F, prop_iterationFunctor_map_succ, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, iterationFunctorObjObjRightIso_ιIteration_app_right_assoc
iterationFunctorMapSuccAppArrowIso 📖	CompOp	3 math math: iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, iterationFunctorMapSuccAppArrowIso_hom_left, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp
iterationFunctorObjObjRightIso 📖	CompOp	3 math math: πFunctorObj_eq, iterationFunctorObjObjRightIso_ιIteration_app_right, iterationFunctorObjObjRightIso_ιIteration_app_right_assoc
iterationObjRightIso 📖	CompOp	1 math math: iterationObjRightIso_hom
obj 📖	CompOp	20 math math: πObj_ιIteration_app_right, functorialFactorizationData_i_app, objMap_comp_assoc, functorialFactorizationData_Z_obj, llp_rlp_ιObj, objMap_id, ιObj_naturality, ιFunctorObj_eq, πObj_ιIteration_app_right_assoc, πObj_naturality_assoc, hasRightLiftingProperty_πObj, πFunctorObj_eq, objMap_comp, rlp_πObj, ιObj_πObj, ιObj_πObj_assoc, ιObj_naturality_assoc, functorialFactorizationData_p_app, transfiniteCompositionsOfShape_ιObj, πObj_naturality
objMap 📖	CompOp	10 math math: functorialFactorizationData_i_app, objMap_comp_assoc, objMap_id, ιObj_naturality, πObj_naturality_assoc, functorialFactorizationData_Z_map, objMap_comp, ιObj_naturality_assoc, functorialFactorizationData_p_app, πObj_naturality
propArrow 📖	CompOp	1 math math: succStruct_prop_le_propArrow
relativeCellComplexιObj 📖	CompOp	2 math math: ιFunctorObj_eq, πFunctorObj_eq
relativeCellComplexιObjFObjSuccIso 📖	CompOp	2 math math: ιFunctorObj_eq, πFunctorObj_eq
succStruct 📖	CompOp	3 math math: succStruct_prop_le_propArrow, transfiniteCompositionOfShapeSuccStructPropιIteration_F, prop_iterationFunctor_map_succ
transfiniteCompositionOfShapeSuccStructPropιIteration 📖	CompOp	1 math math: transfiniteCompositionOfShapeSuccStructPropιIteration_F
transfiniteCompositionOfShapeιIterationAppRight 📖	CompOp	2 math math: iterationFunctorObjObjRightIso_ιIteration_app_right, iterationFunctorObjObjRightIso_ιIteration_app_right_assoc
ιIteration 📖	CompOp	7 math math: πObj_ιIteration_app_right, iterationObjRightIso_hom, πObj_ιIteration_app_right_assoc, iterationFunctorObjObjRightIso_ιIteration_app_right, transfiniteCompositionOfShapeSuccStructPropιIteration_F, iterationFunctorObjObjRightIso_ιIteration_app_right_assoc, instIsIsoRightAppArrowιIteration
ιObj 📖	CompOp	9 math math: functorialFactorizationData_i_app, llp_rlp_ιObj, ιObj_naturality, ιFunctorObj_eq, πFunctorObj_eq, ιObj_πObj, ιObj_πObj_assoc, ιObj_naturality_assoc, transfiniteCompositionsOfShape_ιObj
πObj 📖	CompOp	10 math math: πObj_ιIteration_app_right, πObj_ιIteration_app_right_assoc, πObj_naturality_assoc, hasRightLiftingProperty_πObj, πFunctorObj_eq, rlp_πObj, ιObj_πObj, ιObj_πObj_assoc, functorialFactorizationData_p_app, πObj_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorialFactorizationData_Z_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z CategoryTheory.MorphismProperty.llp CategoryTheory.MorphismProperty.rlp functorialFactorizationData objMap	—	—
functorialFactorizationData_Z_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z CategoryTheory.MorphismProperty.llp CategoryTheory.MorphismProperty.rlp functorialFactorizationData obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
functorialFactorizationData_i_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Arrow.leftFunc obj CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom objMap CategoryTheory.MorphismProperty.FunctorialFactorizationData.i CategoryTheory.MorphismProperty.llp CategoryTheory.MorphismProperty.rlp functorialFactorizationData ιObj	—	—
functorialFactorizationData_p_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow obj CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom objMap CategoryTheory.Arrow.rightFunc CategoryTheory.MorphismProperty.FunctorialFactorizationData.p CategoryTheory.MorphismProperty.llp CategoryTheory.MorphismProperty.rlp functorialFactorizationData πObj	—	—
hasColimitsOfShape_discrete 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Discrete FunctorObjIndex Set.Elem CategoryTheory.Arrow CategoryTheory.MorphismProperty.toSet CategoryTheory.Comma.left CategoryTheory.Functor.id Set Set.instMembership CategoryTheory.Comma.right CategoryTheory.MorphismProperty.homFamily CategoryTheory.discreteCategory	—	CategoryTheory.Limits.hasColimitsOfShape_of_equivalence instSmallFunctorObjIndex locallySmall CategoryTheory.MorphismProperty.IsSmall.small_toSet isSmall hasCoproducts
hasCoproducts 📖	mathematical	—	CategoryTheory.Limits.HasCoproducts	—	CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasCoproducts
hasFunctorialFactorization 📖	mathematical	—	CategoryTheory.MorphismProperty.HasFunctorialFactorization CategoryTheory.MorphismProperty.llp CategoryTheory.MorphismProperty.rlp	—	—
hasIterationOfShape 📖	mathematical	—	CategoryTheory.Limits.HasIterationOfShape Ordinal.ToType Cardinal.ord linearOrder_toType	—	CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasIterationOfShape
hasPushouts 📖	mathematical	—	CategoryTheory.Limits.HasPushouts	—	CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasPushouts
hasRightLiftingProperty_πObj 📖	mathematical	—	CategoryTheory.HasLiftingProperty obj πObj	—	wellFoundedLT_toType CategoryTheory.Limits.Types.jointly_surjective preservesColimit Order.le_succ ιFunctorObj_extension' hasColimitsOfShape_discrete CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hasPushouts CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Category.id_comp ιFunctorObj_eq πFunctorObj_eq CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.CommSq.w CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id
instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.Functor CategoryTheory.Functor.category iterationFunctor CategoryTheory.CommaMorphism.right CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	wellFoundedLT_toType CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoMapF
instIsIsoRightAppArrowιIteration 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow iteration CategoryTheory.CommaMorphism.right CategoryTheory.NatTrans.app ιIteration	—	CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.isIso wellFoundedLT_toType
isSmall 📖	mathematical	—	CategoryTheory.MorphismProperty.IsSmall	—	CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.isSmall
iterationFunctorMapSuccAppArrowIso_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.id CategoryTheory.Functor.obj Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.Functor CategoryTheory.Functor.category iterationFunctor Order.succ Ordinal.instSuccOrderToType CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.homOfLE Order.le_succ functor Set.Elem CategoryTheory.MorphismProperty.toSet CategoryTheory.Comma.left Set Set.instMembership CategoryTheory.Comma.right CategoryTheory.MorphismProperty.homFamily hasPushouts hasColimitsOfShape_discrete ε CategoryTheory.Iso.hom iterationFunctorMapSuccAppArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	Order.le_succ hasPushouts hasColimitsOfShape_discrete
iterationFunctorMapSuccAppArrowIso_hom_right_right_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.Functor CategoryTheory.Functor.category iterationFunctor Order.succ Ordinal.instSuccOrderToType CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.homOfLE Order.le_succ functor Set.Elem CategoryTheory.MorphismProperty.toSet CategoryTheory.Comma.left Set Set.instMembership CategoryTheory.MorphismProperty.homFamily hasPushouts hasColimitsOfShape_discrete ε CategoryTheory.CommaMorphism.right CategoryTheory.Iso.hom iterationFunctorMapSuccAppArrowIso CategoryTheory.CategoryStruct.id	—	Order.le_succ hasPushouts hasColimitsOfShape_discrete CategoryTheory.Functor.congr_map CategoryTheory.CommaMorphism.w CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.Functor CategoryTheory.Functor.category iterationFunctor Order.succ Ordinal.instSuccOrderToType CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.homOfLE Order.le_succ functor Set.Elem CategoryTheory.MorphismProperty.toSet CategoryTheory.Comma.left Set Set.instMembership CategoryTheory.MorphismProperty.homFamily hasPushouts hasColimitsOfShape_discrete ε CategoryTheory.CommaMorphism.right CategoryTheory.Iso.hom iterationFunctorMapSuccAppArrowIso	—	Order.le_succ hasPushouts hasColimitsOfShape_discrete CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' iterationFunctorMapSuccAppArrowIso_hom_right_right_comp
iterationFunctorObjObjRightIso_ιIteration_app_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.Functor CategoryTheory.Functor.category iterationFunctor iteration CategoryTheory.Iso.hom iterationFunctorObjObjRightIso CategoryTheory.CommaMorphism.right CategoryTheory.NatTrans.app ιIteration CategoryTheory.TransfiniteCompositionOfShape.F Ordinal.instSuccOrderToType wellFoundedLT_toType CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape CategoryTheory.MorphismProperty.isomorphisms transfiniteCompositionOfShapeιIterationAppRight CategoryTheory.Functor.const CategoryTheory.TransfiniteCompositionOfShape.incl	—	wellFoundedLT_toType instIsIsoRightAppArrowιIteration CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id
iterationFunctorObjObjRightIso_ιIteration_app_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.Functor CategoryTheory.Functor.category iterationFunctor CategoryTheory.Iso.hom iterationFunctorObjObjRightIso iteration CategoryTheory.CommaMorphism.right CategoryTheory.NatTrans.app ιIteration CategoryTheory.TransfiniteCompositionOfShape.F Ordinal.instSuccOrderToType wellFoundedLT_toType CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape CategoryTheory.MorphismProperty.isomorphisms transfiniteCompositionOfShapeιIterationAppRight CategoryTheory.Functor.const CategoryTheory.TransfiniteCompositionOfShape.incl	—	wellFoundedLT_toType CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iterationFunctorObjObjRightIso_ιIteration_app_right
iterationObjRightIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow iteration iterationObjRightIso CategoryTheory.CommaMorphism.right CategoryTheory.NatTrans.app ιIteration	—	—
llp_rlp_of_isCardinalForSmallObjectArgument 📖	mathematical	—	CategoryTheory.MorphismProperty.llp CategoryTheory.MorphismProperty.rlp CategoryTheory.MorphismProperty.retracts CategoryTheory.MorphismProperty.transfiniteCompositions CategoryTheory.MorphismProperty.pushouts CategoryTheory.MorphismProperty.coproducts	—	le_antisymm wellFoundedLT_toType llp_rlp_of_isCardinalForSmallObjectArgument' CategoryTheory.MorphismProperty.retracts_monotone CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions CategoryTheory.MorphismProperty.retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp
llp_rlp_of_isCardinalForSmallObjectArgument' 📖	mathematical	—	CategoryTheory.MorphismProperty.llp CategoryTheory.MorphismProperty.rlp CategoryTheory.MorphismProperty.retracts CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape CategoryTheory.MorphismProperty.pushouts CategoryTheory.MorphismProperty.coproducts Ordinal.ToType Cardinal.ord linearOrder_toType Ordinal.instSuccOrderToType wellFoundedLT_toType	—	le_antisymm wellFoundedLT_toType ιObj_πObj CategoryTheory.Category.comp_id rlp_πObj CategoryTheory.sq_hasLift_of_hasLiftingProperty CategoryTheory.Category.id_comp CategoryTheory.CommSq.fac_left CategoryTheory.Arrow.hom_ext CategoryTheory.CommSq.fac_right transfiniteCompositionsOfShape_ιObj CategoryTheory.MorphismProperty.retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp
llp_rlp_ιObj 📖	mathematical	—	CategoryTheory.MorphismProperty.llp CategoryTheory.MorphismProperty.rlp obj ιObj	—	CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp wellFoundedLT_toType transfiniteCompositionsOfShape_ιObj
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall	—	CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.locallySmall
objMap_comp 📖	mathematical	—	objMap CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow obj CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Functor.map_comp
objMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom objMap CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' objMap_comp
objMap_id 📖	mathematical	—	objMap CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow obj CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Functor.map_id
preservesColimit 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.types Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.TransfiniteCompositionOfShape.F Ordinal.instSuccOrderToType wellFoundedLT_toType HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape Set.Elem CategoryTheory.Arrow CategoryTheory.MorphismProperty.toSet CategoryTheory.Comma.left CategoryTheory.Functor.id Set Set.instMembership CategoryTheory.Comma.right CategoryTheory.MorphismProperty.homFamily CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op	—	wellFoundedLT_toType CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit
prop_iterationFunctor_map_succ 📖	mathematical	—	SuccStruct.prop CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.category succStruct CategoryTheory.Functor.obj Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType iterationFunctor Order.succ Ordinal.instSuccOrderToType CategoryTheory.Functor.map CategoryTheory.homOfLE Order.le_succ	—	hasIterationOfShape Cardinal.noMaxOrder Cardinal.IsRegular.aleph0_le Fact.elim SuccStruct.prop_iterationFunctor_map_succ wellFoundedLT_toType CategoryTheory.Limits.instHasIterationOfShapeFunctor CategoryTheory.Limits.instHasIterationOfShapeArrow not_isMax
rlp_πObj 📖	mathematical	—	CategoryTheory.MorphismProperty.rlp obj πObj	—	hasRightLiftingProperty_πObj
succStruct_prop_le_propArrow 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra SuccStruct.prop succStruct CategoryTheory.MorphismProperty.functorCategory propArrow	—	CategoryTheory.MorphismProperty.ofHoms_homFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hasColimitsOfShape_discrete hasPushouts functorObj_isPushout CategoryTheory.MorphismProperty.coproducts_of_small CategoryTheory.MorphismProperty.colimitsOfShape_colimMap instSmallFunctorObjIndex locallySmall CategoryTheory.MorphismProperty.IsSmall.small_toSet isSmall CategoryTheory.MorphismProperty.isomorphisms.iff CategoryTheory.IsIso.id
transfiniteCompositionOfShapeSuccStructPropιIteration_F 📖	mathematical	—	CategoryTheory.TransfiniteCompositionOfShape.F CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.category Ordinal.ToType Cardinal.ord linearOrder_toType CategoryTheory.Functor.id iteration ιIteration Ordinal.instSuccOrderToType wellFoundedLT_toType CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape SuccStruct.prop succStruct transfiniteCompositionOfShapeSuccStructPropιIteration iterationFunctor	—	wellFoundedLT_toType
transfiniteCompositionsOfShape_ιObj 📖	mathematical	—	CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape CategoryTheory.MorphismProperty.pushouts CategoryTheory.MorphismProperty.coproducts Ordinal.ToType Cardinal.ord linearOrder_toType Ordinal.instSuccOrderToType wellFoundedLT_toType obj ιObj	—	wellFoundedLT_toType CategoryTheory.MorphismProperty.ofHoms_homFamily
ιFunctorObj_eq 📖	mathematical	—	ιFunctorObj Set.Elem CategoryTheory.Arrow CategoryTheory.MorphismProperty.toSet CategoryTheory.Comma.left CategoryTheory.Functor.id Set Set.instMembership CategoryTheory.Comma.right CategoryTheory.MorphismProperty.homFamily CategoryTheory.Functor.obj CategoryTheory.instCategoryArrow Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.Functor CategoryTheory.Functor.category iterationFunctor CategoryTheory.Comma.hom hasColimitsOfShape_discrete CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair hasPushouts CategoryTheory.Limits.span CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjSrcFamily CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorObjTgtFamily functorObjTop functorObjLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.TransfiniteCompositionOfShape.F obj ιObj Ordinal.instSuccOrderToType wellFoundedLT_toType HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape relativeCellComplexιObj Order.succ functorObj CategoryTheory.Functor.map CategoryTheory.homOfLE Order.le_succ CategoryTheory.Iso.hom relativeCellComplexιObjFObjSuccIso	—	hasColimitsOfShape_discrete CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hasPushouts wellFoundedLT_toType Order.le_succ CategoryTheory.Category.id_comp CategoryTheory.Functor.congr_map CategoryTheory.CommaMorphism.w
ιObj_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left obj CategoryTheory.Comma.right CategoryTheory.Comma.hom ιObj objMap CategoryTheory.CommaMorphism.left	—	CategoryTheory.Functor.congr_map CategoryTheory.NatTrans.naturality
ιObj_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id obj CategoryTheory.Comma.right CategoryTheory.Comma.hom ιObj objMap CategoryTheory.CommaMorphism.left	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιObj_naturality
ιObj_πObj 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj ιObj πObj	—	CategoryTheory.Arrow.w_mk_right_assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id
ιObj_πObj_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj ιObj πObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιObj_πObj
πFunctorObj_eq 📖	mathematical	—	πFunctorObj Set.Elem CategoryTheory.Arrow CategoryTheory.MorphismProperty.toSet CategoryTheory.Comma.left CategoryTheory.Functor.id Set Set.instMembership CategoryTheory.Comma.right CategoryTheory.MorphismProperty.homFamily CategoryTheory.Functor.obj CategoryTheory.instCategoryArrow Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType CategoryTheory.Functor CategoryTheory.Functor.category iterationFunctor CategoryTheory.Comma.hom hasColimitsOfShape_discrete CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair hasPushouts CategoryTheory.Limits.span CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjSrcFamily CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorObjTgtFamily functorObjTop functorObjLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj CategoryTheory.TransfiniteCompositionOfShape.F obj ιObj Ordinal.instSuccOrderToType wellFoundedLT_toType HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape relativeCellComplexιObj Order.succ CategoryTheory.Iso.inv relativeCellComplexιObjFObjSuccIso CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.TransfiniteCompositionOfShape.incl πObj iterationFunctorObjObjRightIso	—	Order.le_succ hasPushouts hasColimitsOfShape_discrete CategoryTheory.CommaMorphism.w wellFoundedLT_toType CategoryTheory.NatTrans.naturality CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom instIsIsoRightAppArrowιIteration CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc πObj_ιIteration_app_right iterationFunctorObjObjRightIso_ιIteration_app_right CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Category.comp_id Mathlib.Tactic.Reassoc.eq_whisker' iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc CategoryTheory.Arrow.w_mk_right
πObj_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom objMap πObj CategoryTheory.CommaMorphism.right	—	instIsIsoRightAppArrowιIteration CategoryTheory.eq_whisker CategoryTheory.CommaMorphism.w CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.inv_hom_id CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Category.comp_id
πObj_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom objMap πObj CategoryTheory.CommaMorphism.right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πObj_naturality
πObj_ιIteration_app_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow iteration πObj CategoryTheory.CommaMorphism.right CategoryTheory.NatTrans.app ιIteration CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id
πObj_ιIteration_app_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj πObj CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow iteration CategoryTheory.CommaMorphism.right CategoryTheory.NatTrans.app ιIteration CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πObj_ιIteration_app_right

---

← Back to Index