Documentation Verification Report

EnoughInjectives

📁 Source: Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

Statistics

Metric	Count
Definitions `EnoughInjectives`, `generatingMonomorphisms`, `functor`, `functorToMonoOver`, `largerSubobject`, `transfiniteCompositionOfShapeMapFromBot`, `transfiniteCompositionOfShapeOfEqTop`, `monoMapFactorizationDataRlp`	8
Theorems `enoughInjectives`, `exists_larger_subobject`, `exists_ordinal`, `exists_pushouts`, `exists_transfiniteCompositionOfShape`, `functorToMonoOver_map`, `functorToMonoOver_obj`, `instIsWellOrderContinuousFunctor`, `largerSubobject_top`, `le_largerSubobject`, `lt_largerSubobject`, `pushouts_ofLE_le_largerSubobject`, `top_mem_range`, `generatingMonomorphisms_le_monomorphisms`, `generatingMonomorphisms_rlp`, `instHasFunctorialFactorizationMonomorphismsRlp`, `instHasSmallObjectArgumentGeneratingMonomorphisms`, `instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom`, `instIsSmallGeneratingMonomorphismsOfSmallSubobject`, `instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp`, `isomorphisms_le_pushouts_generatingMonomorphisms`, `llp_rlp_monomorphisms`	22
Total	30

CategoryTheory

Definitions

Name	Category	Theorems
`EnoughInjectives` 📖	CompData	12 math math: `Equivalence.enoughInjectives_iff`, `Injective.enoughInjectives_of_enoughProjectives_op`, `EnoughInjectives.of_equivalence`, `IsGrothendieckAbelian.enoughInjectives`, `instEnoughInjectivesModuleCatOfSmall`, `AddCommGrpCat.enoughInjectives`, `Injective.Type.enoughInjectives`, `CommGrpCat.enoughInjectives`, `Injective.instEnoughInjectivesOppositeOfEnoughProjectives`, `EnoughInjectives.of_adjunction`, `ModuleCat.enoughInjectives`, `instEnoughInjectivesModuleCatInt`

CategoryTheory.IsGrothendieckAbelian

Definitions

Name	Category	Theorems
`generatingMonomorphisms` 📖	CompOp	8 math math: `isomorphisms_le_pushouts_generatingMonomorphisms`, `generatingMonomorphisms_le_monomorphisms`, `generatingMonomorphisms.exists_larger_subobject`, `generatingMonomorphisms.exists_transfiniteCompositionOfShape`, `generatingMonomorphisms_rlp`, `instIsSmallGeneratingMonomorphismsOfSmallSubobject`, `generatingMonomorphisms.pushouts_ofLE_le_largerSubobject`, `instHasSmallObjectArgumentGeneratingMonomorphisms`
`monoMapFactorizationDataRlp` 📖	CompOp	2 math math: `instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp`, `instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`enoughInjectives` 📖	mathematical	—	`CategoryTheory.EnoughInjectives`	—	`CategoryTheory.Abelian.hasZeroObject` `instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom` `instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp`
`generatingMonomorphisms_le_monomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `generatingMonomorphisms` `CategoryTheory.MorphismProperty.monomorphisms`	—	`CategoryTheory.Subobject.arrow_mono`
`generatingMonomorphisms_rlp` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.MorphismProperty.rlp` `generatingMonomorphisms` `CategoryTheory.MorphismProperty.monomorphisms`	—	`le_antisymm` `generatingMonomorphisms.exists_transfiniteCompositionOfShape` `CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_llp_rlp` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem` `CategoryTheory.MorphismProperty.rlp_pushouts` `CategoryTheory.MorphismProperty.antitone_rlp` `generatingMonomorphisms_le_monomorphisms`
`instHasFunctorialFactorizationMonomorphismsRlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasFunctorialFactorization` `CategoryTheory.MorphismProperty.monomorphisms` `CategoryTheory.MorphismProperty.rlp`	—	`hasSeparator` `CategoryTheory.isSeparator_separator` `generatingMonomorphisms_rlp` `llp_rlp_monomorphisms` `CategoryTheory.MorphismProperty.instHasFunctorialFactorizationLlpRlp` `instHasSmallObjectArgumentGeneratingMonomorphisms`
`instHasSmallObjectArgumentGeneratingMonomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasSmallObjectArgument` `generatingMonomorphisms`	—	`HasCardinalLT.exists_regular_cardinal` `CategoryTheory.small_subobject` `locallySmall` `wellPowered` `Cardinal.IsRegular.ne_zero` `instIsSmallGeneratingMonomorphismsOfSmallSubobject` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Abelian.hasFiniteColimits` `CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `hasColimits` `CategoryTheory.Limits.instHasIterationOfShapeOfHasColimitsOfSize` `wellFoundedLT_toType` `Order.le_succ` `HomotopicalAlgebra.AttachCells.pushouts_coproducts` `CategoryTheory.Abelian.instIsStableUnderCobaseChangeMonomorphisms` `CategoryTheory.MorphismProperty.instIsStableUnderCoproductsMonomorphismsOfAB4OfSize` `ab4OfSize` `generatingMonomorphisms_le_monomorphisms` `CategoryTheory.MorphismProperty.ofHoms_homFamily` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem_map` `instIsStableUnderTransfiniteCompositionMonomorphisms` `preservesColimit_coyoneda_obj_of_mono` `CategoryTheory.instIsCardinalFilteredToTypeOrd` `CategoryTheory.Subobject.hasCardinalLT_of_mono` `CategoryTheory.Subobject.arrow_mono`
`instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom` 📖	mathematical	—	`CategoryTheory.Injective` `CategoryTheory.MorphismProperty.MapFactorizationData.Z` `CategoryTheory.MorphismProperty.monomorphisms` `CategoryTheory.MorphismProperty.rlp` `CategoryTheory.Limits.HasZeroObject.zero'` `CategoryTheory.Abelian.hasZeroObject` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `monoMapFactorizationDataRlp`	—	`CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Limits.IsZero.eq_of_tgt` `CategoryTheory.Limits.isZero_zero` `CategoryTheory.MorphismProperty.MapFactorizationData.hp`
`instIsSmallGeneratingMonomorphismsOfSmallSubobject` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsSmall` `generatingMonomorphisms`	—	`CategoryTheory.MorphismProperty.isSmall_ofHoms`
`instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.MorphismProperty.MapFactorizationData.Z` `CategoryTheory.MorphismProperty.monomorphisms` `CategoryTheory.MorphismProperty.rlp` `monoMapFactorizationDataRlp` `CategoryTheory.MorphismProperty.MapFactorizationData.i`	—	`CategoryTheory.MorphismProperty.MapFactorizationData.hi`
`isomorphisms_le_pushouts_generatingMonomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.isomorphisms` `CategoryTheory.MorphismProperty.pushouts` `generatingMonomorphisms`	—	`CategoryTheory.MorphismProperty.isomorphisms_le_pushouts` `CategoryTheory.Subobject.isIso_top_arrow`
`llp_rlp_monomorphisms` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.MorphismProperty.llp` `CategoryTheory.MorphismProperty.rlp` `CategoryTheory.MorphismProperty.monomorphisms`	—	`le_antisymm` `generatingMonomorphisms_rlp` `CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument` `instHasSmallObjectArgumentGeneratingMonomorphisms` `CategoryTheory.MorphismProperty.retracts_monotone` `CategoryTheory.MorphismProperty.transfiniteCompositions_monotone` `CategoryTheory.MorphismProperty.pushouts_monotone` `CategoryTheory.MorphismProperty.coproducts_monotone` `generatingMonomorphisms_le_monomorphisms` `CategoryTheory.MorphismProperty.coproducts_eq_self` `CategoryTheory.MorphismProperty.instIsStableUnderCoproductsMonomorphismsOfAB4OfSize` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `hasColimits` `ab4OfSize` `CategoryTheory.MorphismProperty.IsStableUnderRetracts.monomorphisms` `instIsStableUnderTransfiniteCompositionMonomorphisms` `CategoryTheory.Abelian.instIsStableUnderCobaseChangeMonomorphisms` `CategoryTheory.MorphismProperty.le_llp_rlp`

CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms

Definitions

Name	Category	Theorems
`functor` 📖	CompOp	1 math math: `instIsWellOrderContinuousFunctor`
`functorToMonoOver` 📖	CompOp	2 math math: `functorToMonoOver_map`, `functorToMonoOver_obj`
`largerSubobject` 📖	CompOp	8 math math: `exists_ordinal`, `lt_largerSubobject`, `functorToMonoOver_map`, `top_mem_range`, `functorToMonoOver_obj`, `largerSubobject_top`, `pushouts_ofLE_le_largerSubobject`, `le_largerSubobject`
`transfiniteCompositionOfShapeMapFromBot` 📖	CompOp	—
`transfiniteCompositionOfShapeOfEqTop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_larger_subobject` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.MorphismProperty.pushouts` `CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `CategoryTheory.Subobject.ofLE` `LT.lt.le`	—	`CategoryTheory.Subobject.ind` `LT.lt.le` `exists_pushouts` `CategoryTheory.Subobject.mk_lt_mk_of_comm` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.instRespectsIsoPushouts` `CategoryTheory.cancel_mono` `CategoryTheory.Category.assoc` `CategoryTheory.Subobject.ofLE_arrow`
`exists_ordinal` 📖	mathematical	`CategoryTheory.IsSeparator`	`transfiniteIterate` `CategoryTheory.Subobject` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Subobject.instCompleteLattice` `CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.Limits.WidePullbackShape` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.IsGrothendieckAbelian.hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `largerSubobject` `Ordinal.ToType` `linearOrder_toType` `Ordinal.instSuccOrderToType` `wellFoundedLT_toType` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.orderTop`	—	`CategoryTheory.small_subobject` `CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered` `Cardinal.succ_ne_zero` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.IsGrothendieckAbelian.hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `wellFoundedLT_toType` `top_mem_range` `lt_of_lt_of_le` `Order.lt_succ` `Cardinal.instNoMaxOrder` `Cardinal.mk_toType` `Cardinal.card_ord` `Cardinal.lift_succ` `Cardinal.lift_mk_shrink'`
`exists_pushouts` 📖	mathematical	`CategoryTheory.IsSeparator` `CategoryTheory.IsIso`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.ObjectProperty.IsDetecting.isIso_iff_of_mono` `CategoryTheory.IsSeparator.isDetector` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Abelian.hasFiniteColimits` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.Limits.pullback.snd_of_mono` `CategoryTheory.IsPushout.of_iso` `CategoryTheory.IsPushout.of_hasPushout` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Subobject.underlyingIso_arrow` `CategoryTheory.Category.id_comp` `CategoryTheory.isIso_iff_yoneda_map_bijective` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.eq_whisker` `CategoryTheory.IsPushout.mono_of_isPullback_of_mono` `CategoryTheory.IsPullback.of_hasPullback`
`exists_transfiniteCompositionOfShape` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape` `CategoryTheory.MorphismProperty.pushouts` `CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms`	—	`CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.IsGrothendieckAbelian.hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `wellFoundedLT_toType` `exists_ordinal` `Set.ordConnected_Iic` `Subtype.wellFoundedLT`
`functorToMonoOver_map` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.Functor.map` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `functorToMonoOver` `CategoryTheory.MonoOver.homMk` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `transfiniteIterate` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Subobject.instCompleteLattice` `CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered` `largerSubobject` `CategoryTheory.Subobject.arrow` `CategoryTheory.Subobject.ofLE`	—	`CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered`
`functorToMonoOver_obj` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.MonoOver` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.isMono` `functorToMonoOver` `CategoryTheory.Subobject` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `transfiniteIterate` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Subobject.instCompleteLattice` `CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered` `largerSubobject` `CategoryTheory.Subobject.arrow`	—	—
`instIsWellOrderContinuousFunctor` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.Functor.IsWellOrderContinuous` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `functor`	—	`PrincipalSeg.monotone` `Set.Nonempty.to_subtype` `Order.IsSuccLimit.nonempty_Iio` `CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered` `CategoryTheory.Subobject.arrow_mono` `CategoryTheory.isFiltered_of_directed_le_nonempty` `SemilatticeSup.instIsDirectedOrder` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.IsGrothendieckAbelian.hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.MonoOver.mono` `CategoryTheory.Subobject.mk_arrow` `transfiniteIterate_limit`
`largerSubobject_top` 📖	mathematical	`CategoryTheory.IsSeparator`	`largerSubobject` `Top.top` `CategoryTheory.Subobject` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.orderTop`	—	`exists_larger_subobject`
`le_largerSubobject` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.Subobject` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `largerSubobject`	—	`largerSubobject_top` `LT.lt.le` `lt_largerSubobject`
`lt_largerSubobject` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.Subobject` `Preorder.toLT` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `largerSubobject`	—	`exists_larger_subobject` `LT.lt.le`
`pushouts_ofLE_le_largerSubobject` 📖	mathematical	`CategoryTheory.IsSeparator`	`CategoryTheory.MorphismProperty.pushouts` `CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `largerSubobject` `CategoryTheory.Subobject.ofLE` `le_largerSubobject`	—	`le_largerSubobject` `CategoryTheory.Subobject.isIso_arrow_iff_eq_top` `largerSubobject_top` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.instRespectsIsoPushouts` `CategoryTheory.Subobject.isIso_top_arrow` `CategoryTheory.Category.comp_id` `CategoryTheory.Subobject.ofLE_arrow` `CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms` `CategoryTheory.MorphismProperty.isomorphisms.infer_property` `CategoryTheory.IsIso.id` `LT.lt.le` `exists_larger_subobject` `LE.le.trans` `CategoryTheory.Category.id_comp` `CategoryTheory.Subobject.ofLE_comp_ofLE`
`top_mem_range` 📖	mathematical	`CategoryTheory.IsSeparator` `HasCardinalLT` `CategoryTheory.Subobject`	`transfiniteIterate` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Subobject.instCompleteLattice` `CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.Limits.WidePullbackShape` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.IsGrothendieckAbelian.hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `largerSubobject` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.orderTop`	—	`top_mem_range_transfiniteIterate` `CategoryTheory.IsGrothendieckAbelian.locallySmall` `CategoryTheory.IsGrothendieckAbelian.wellPowered` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.IsGrothendieckAbelian.hasLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.IsGrothendieckAbelian.hasColimits` `CategoryTheory.Limits.HasZeroObject.initialMonoClass` `CategoryTheory.Abelian.hasZeroObject` `lt_largerSubobject` `largerSubobject_top` `HasCardinalLT.of_injective`

---

← Back to Index