Limits

📁 Source: Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Statistics

Metric	Count
Definitions HasPullbacks, HasPullbacksAlong, HasPushouts, HasPushoutsAlong, IsStableUnderBaseChange, IsStableUnderBaseChangeAlong, IsStableUnderCobaseChange, IsStableUnderCobaseChangeAlong, IsStableUnderColimitsOfShape, IsStableUnderCoproducts, IsStableUnderCoproductsOfShape, IsStableUnderFilteredColimits, IsStableUnderFiniteCoproducts, IsStableUnderFiniteProducts, IsStableUnderLimitsOfShape, IsStableUnderProductsOfShape, colimitsOfShape, coproducts, diagonal, limitsOfShape, pullbacks, pushouts, universally	23
Theorems hasPullback, hasPullback, hasPushout, hasPushout, diagonal, hasOfPostcompProperty_monomorphisms, inf, isomorphisms, mk', monomorphisms, of_forall_exists_isPullback, of_isPullback, op, respectsIso, universally_eq, unop, of_isPullback, epimorphisms, hasOfPrecompProperty_epimorphisms, inf, isomorphisms, mk', of_forall_exists_isPullback, of_isPushout, op, respectsIso, unop, of_isPushout, condition, isomorphisms, universally, isStableUnderCoproductsOfShape, mk, isStableUnderColimitsOfShape, isStableUnderCoproductsOfShape, isStableUnderProductsOfShape, condition, mk, diagonal, baseChange_map, baseChange_map', baseChange_obj, colimMap, mk', of_isColimit, colimitsOfShape_colimMap, colimitsOfShape_eq_of_equivalence, colimitsOfShape_le, colimitsOfShape_le_coproducts, colimitsOfShape_le_of_final, colimitsOfShape_monotone, coproducts_eq_self, coproducts_iff, coproducts_le, coproducts_le_iff, coproducts_monotone, coproducts_of_small, diagonal_iff, diagonal_isStableUnderComposition, diagonal_isomorphisms, hasOfPostcompProperty_iff_le_diagonal, hasPullback, hasPushout, instContainsIdentitiesDiagonalOfRespectsIso, instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong, instHasPullbacksAlongOfHasPullbacks, instHasPullbacksOfHasPullbacks, instHasPushoutsAlongCompOfIsStableUnderCobaseChangeAlong, instHasPushoutsAlongOfHasPushouts, instHasPushoutsOfHasPushouts, instIsMultiplicativeDiagonalOfIsStableUnderBaseChange, instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong, instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange, instIsStableUnderBaseChangePullbacks, instIsStableUnderBaseChangeTop, instIsStableUnderCobaseChangeAlongCompOfHasPushoutsAlong, instIsStableUnderCobaseChangeAlongOfIsStableUnderCobaseChange, instIsStableUnderCobaseChangePushouts, instIsStableUnderCobaseChangeTop, instIsStableUnderFilteredColimitsIsomorphisms, instRespectsIsoColimitsOfShape, instRespectsIsoLimitsOfShape, instRespectsIsoPullbacks, instRespectsIsoPushouts, isStableUnderBaseChange_iff_pullbacks_le, isStableUnderCobaseChange_iff_pushouts_le, isStableUnderColimitsOfShape_iff_colimitsOfShape_le, isStableUnderLimitsOfShape_iff_limitsOfShape_le, isomorphisms_le_pushouts, le_colimitsOfShape_punit, le_coproducts, le_pullbacks, le_pushouts, limMap, mk', limitsOfShape_le, limitsOfShape_limMap, limitsOfShape_monotone, of_isPullback, of_isPushout, overPullbackMap, pullbackLift_fst_snd, pullbackMap, pullback_fst, pullback_map, pullback_snd, pullbacks_le, pullbacks_mk, pullbacks_monotone, pushoutDesc_inl_inr, pushoutMap, pushout_inl, pushout_inr, pushouts_le, pushouts_le_iff, pushouts_mk, pushouts_monotone, underPushoutMap, universally_eq_iff, universally_inf, universally_isStableUnderBaseChange, universally_le, universally_mk', universally_mono, universally_respectsIso	125
Total	148

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
HasPullbacks 📖	CompData	2 math math: instHasPullbacksOfHasPullbacks, AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion
HasPullbacksAlong 📖	CompData	2 math math: instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong, instHasPullbacksAlongOfHasPullbacks
HasPushouts 📖	CompData	1 math math: instHasPushoutsOfHasPushouts
HasPushoutsAlong 📖	CompData	2 math math: instHasPushoutsAlongCompOfIsStableUnderCobaseChangeAlong, instHasPushoutsAlongOfHasPushouts
IsStableUnderBaseChange 📖	CompData	64 math math: AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyIrreducible, AlgebraicGeometry.IsImmersion.isStableUnderBaseChange, AlgebraicGeometry.IsSeparated.isStableUnderBaseChange, IsStableUnderCobaseChange.op, AlgebraicGeometry.UniversallyOpen.instIsStableUnderBaseChangeScheme, relative_isStableUnderBaseChange, AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange, AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange, AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange, IsStableUnderBaseChange.isomorphisms, AlgebraicGeometry.isSmooth_isStableUnderBaseChange, CategoryTheory.Functor.relativelyRepresentable.isStableUnderBaseChange, AlgebraicGeometry.WeaklyEtale.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeLocallyQuasiFinite, AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.IsProper.isStableUnderBaseChange, rlp_isStableUnderBaseChange, IsStableUnderBaseChange.inf, AlgebraicGeometry.quasiCompact_isStableUnderBaseChange, CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeMonoModSerre, AlgebraicGeometry.ValuativeCriterion.Existence.stableUnderBaseChange, CategoryTheory.Types.instIsStableUnderBaseChangeEpimorphismsType, AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange, CategoryTheory.Abelian.instIsStableUnderBaseChangeEpimorphisms, CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeIsoModSerre, AlgebraicGeometry.universallyClosed_isStableUnderBaseChange, AlgebraicGeometry.smooth_isStableUnderBaseChange, CategoryTheory.Regular.regularEpiIsStableUnderBaseChange, AlgebraicGeometry.IsLocalIso.instIsStableUnderBaseChangeScheme, IsStableUnderBaseChange.mk', universally_isStableUnderBaseChange, AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyIntegral, instIsStableUnderBaseChangeTop, AlgebraicGeometry.isAffineHom_isStableUnderBaseChange, HomotopicalAlgebra.instIsStableUnderBaseChangeTrivialFibrations, instIsStableUnderBaseChangeFunctorFunctorCategoryOfHasPullbacks, CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeEpiModSerre, AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange, AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange, instIsStableUnderBaseChangePullbacks, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometrically, HomotopicalAlgebra.instIsStableUnderBaseChangeFibrations, AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.Etale.etale_isStableUnderBaseChange, AlgebraicGeometry.sourceLocalClosure.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget, AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange, IsStableUnderBaseChange.monomorphisms, AlgebraicGeometry.IsPreimmersion.instIsStableUnderBaseChangeScheme, TopCat.instIsStableUnderBaseChangeIsOpenEmbedding, AlgebraicGeometry.SurjectiveOnStalks.stableUnderBaseChange, AlgebraicGeometry.Flat.isStableUnderBaseChange, universally_eq_iff, IsStableUnderCobaseChange.unop, AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange, AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyReduced, isStableUnderBaseChange_iff_pullbacks_le, AlgebraicGeometry.quasiSeparated_isStableUnderBaseChange, AlgebraicGeometry.isSmoothOfRelativeDimension_isStableUnderBaseChange, IsStableUnderBaseChange.diagonal, IsStableUnderBaseChange.of_forall_exists_isPullback
IsStableUnderBaseChangeAlong 📖	CompData	2 math math: instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange, instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong
IsStableUnderCobaseChange 📖	CompData	22 math math: RingHom.isStableUnderCobaseChange_toMorphismProperty_iff, instIsStableUnderCobaseChangePushouts, IsStableUnderCobaseChange.isomorphisms, CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeEpiModSerre, CategoryTheory.Types.instIsStableUnderCobaseChangeMonomorphismsType, HomotopicalAlgebra.instIsStableUnderCobaseChangeTrivialCofibrations, llp_isStableUnderCobaseChange, isStableUnderCobaseChange_iff_pushouts_le, IsStableUnderBaseChange.unop, instIsStableUnderCobaseChangeTop, IsStableUnderBaseChange.op, SSet.instIsStableUnderCobaseChangeMonomorphisms, IsStableUnderCobaseChange.mk', IsStableUnderCobaseChange.of_forall_exists_isPullback, CategoryTheory.Abelian.instIsStableUnderCobaseChangeMonomorphisms, CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeMonoModSerre, HomotopicalAlgebra.instIsStableUnderCobaseChangeCofibrations, CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeIsoModSerre, IsStableUnderCobaseChange.epimorphisms, instIsStableUnderCobaseChangeIndOfHasPushouts, IsStableUnderCobaseChange.inf, instIsStableUnderCobaseChangeFunctorFunctorCategoryOfHasPushouts
IsStableUnderCobaseChangeAlong 📖	CompData	2 math math: instIsStableUnderCobaseChangeAlongOfIsStableUnderCobaseChange, instIsStableUnderCobaseChangeAlongCompOfHasPushoutsAlong
IsStableUnderColimitsOfShape 📖	CompData	5 math math: IsStableUnderColimitsOfShape.functorCategory, isStableUnderColimitsOfShape_monomorphisms, IsStableUnderColimitsOfShape.isomorphisms, IsStableUnderFilteredColimits.isStableUnderColimitsOfShape, isStableUnderColimitsOfShape_iff_colimitsOfShape_le
IsStableUnderCoproducts 📖	CompData	4 math math: instIsStableUnderCoproductsMonomorphismsOfAB4OfSize, SSet.instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType, instIsStableUnderCoproductsFunctorMonomorphismsOfHasCoproductsOfHasPullbacks, CategoryTheory.Types.instIsStableUnderCoproductsMonomorphismsType
IsStableUnderCoproductsOfShape 📖	MathDef	8 math math: IsStableUnderCoproductsOfShape.mk, HomotopicalAlgebra.isStableUnderCoproductsOfShape_trivialCofibrations, IsStableUnderFiniteCoproducts.isStableUnderCoproductsOfShape, llp_isStableUnderCoproductsOfShape, instIsStableUnderCoproductsOfShapeFunctorMonomorphismsOfHasCoproductsOfShapeOfHasPullbacks, CategoryTheory.Types.instIsStableUnderCoproductsOfShapeMonomorphismsType, IsStableUnderCoproducts.isStableUnderCoproductsOfShape, HomotopicalAlgebra.isStableUnderCoproductsOfShape_cofibrations
IsStableUnderFilteredColimits 📖	CompData	4 math math: SSet.instIsStableUnderFilteredColimitsMonomorphisms, CategoryTheory.Types.instIsStableUnderFilteredColimitsMonomorphismsType, instIsStableUnderFilteredColimitsIsomorphisms, instIsStableUnderFilteredColimitsMonomorphismsOfAB5OfSize
IsStableUnderFiniteCoproducts 📖	CompData	—
IsStableUnderFiniteProducts 📖	CompData	1 math math: CategoryTheory.ObjectProperty.instIsStableUnderFiniteProductsTrWOfIsTriangulated
IsStableUnderLimitsOfShape 📖	CompData	2 math math: isStableUnderLimitsOfShape_iff_limitsOfShape_le, IsStableUnderLimitsOfShape.functorCategory
IsStableUnderProductsOfShape 📖	MathDef	5 math math: HomotopicalAlgebra.isStableUnderProductsOfShape_trivialFibrations, rlp_isStableUnderProductsOfShape, HomotopicalAlgebra.isStableUnderProductsOfShape_fibrations, IsStableUnderProductsOfShape.mk, IsStableUnderFiniteProducts.isStableUnderProductsOfShape
colimitsOfShape 📖	CompData	13 math math: colimitsOfShape_eq_of_equivalence, colimitsOfShape_le_coproducts, colimitsOfShape_le, colimitsOfShape_discrete_le_llp_rlp, colimitsOfShape.of_isColimit, colimitsOfShape_monotone, instRespectsIsoColimitsOfShape, colimitsOfShape_colimMap, coproducts_iff, colimitsOfShape_le_of_final, colimitsOfShape.mk', isStableUnderColimitsOfShape_iff_colimitsOfShape_le, le_colimitsOfShape_punit
coproducts 📖	CompOp	22 math math: rlp_coproducts, coproducts_of_small, colimitsOfShape_le_coproducts, transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, coproducts_monotone, llp_rlp_of_hasSmallObjectArgument, coproducts_le_iff, retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp, HomotopicalAlgebra.AttachCells.pushouts_coproducts, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument, le_coproducts, coproducts_le, coproducts_le_llp_rlp, coproducts_iff, llp_rlp_of_hasSmallObjectArgument', retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, HomotopicalAlgebra.nonempty_attachCells_iff, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument', transfiniteCompositions_pushouts_coproducts_le_llp_rlp, CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObj, coproducts_eq_self, HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape_toTransfiniteCompositionOfShape
diagonal 📖	CompOp	19 math math: AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat, hasOfPostcompProperty_iff_le_diagonal, AlgebraicGeometry.instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion, instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange, instIsMultiplicativeDiagonalOfIsStableUnderBaseChange, AlgebraicGeometry.HasAffineProperty.diagonal_iff, AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion, AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact, RespectsIso.diagonal, instContainsIdentitiesDiagonalOfRespectsIso, AlgebraicGeometry.universallyInjective_eq_diagonal, diagonal_isStableUnderComposition, diagonal_iff, AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover_diagonal, diagonal_isomorphisms, AlgebraicGeometry.instIsZariskiLocalAtTargetDiagonalScheme, AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover, IsStableUnderBaseChange.diagonal, AlgebraicGeometry.instHasAffinePropertyDiagonalSchemeDiagonal
limitsOfShape 📖	CompData	6 math math: isStableUnderLimitsOfShape_iff_limitsOfShape_le, limitsOfShape_monotone, limitsOfShape_le, limitsOfShape.mk', instRespectsIsoLimitsOfShape, limitsOfShape_limMap
pullbacks 📖	CompOp	7 math math: instRespectsIsoPullbacks, le_pullbacks, instIsStableUnderBaseChangePullbacks, pullbacks_mk, pullbacks_monotone, isStableUnderBaseChange_iff_pullbacks_le, pullbacks_le
pushouts 📖	CompOp	28 math math: instIsStableUnderCobaseChangePushouts, pushouts_le, CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms, transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, isStableUnderCobaseChange_iff_pushouts_le, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, pushouts_mk, le_pushouts, llp_rlp_of_hasSmallObjectArgument, retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp, HomotopicalAlgebra.AttachCells.pushouts_coproducts, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument, rlp_pushouts, llp_rlp_of_hasSmallObjectArgument', CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_pushouts, retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, isomorphisms_le_pushouts, HomotopicalAlgebra.nonempty_attachCells_iff, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_transfiniteCompositionOfShape, instRespectsIsoPushouts, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument', transfiniteCompositions_pushouts_coproducts_le_llp_rlp, pushouts_le_llp_rlp, CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObj, pushouts_le_iff, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobject, HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape_toTransfiniteCompositionOfShape, pushouts_monotone
universally 📖	CompOp	27 math math: universally_inf, universally_mk', IsStableUnderBaseChange.universally_eq, AlgebraicGeometry.UniversallyOpen.out, AlgebraicGeometry.geometrically_eq_universally, AlgebraicGeometry.universallyInjective_iff, AlgebraicGeometry.ValuativeCriterion.Existence.eq, universally_le, AlgebraicGeometry.universallyInjective_eq, AlgebraicGeometry.UniversallyClosed.out, AlgebraicGeometry.universally_isLocalAtTarget, universally_isStableUnderBaseChange, AlgebraicGeometry.UniversallyOpen.eq, AlgebraicGeometry.UniversallyOpen.universally_isOpenMap, AlgebraicGeometry.universallyOpen_iff, AlgebraicGeometry.UniversallyClosed.universally_isClosedMap, AlgebraicGeometry.universallyClosed_eq_universallySpecializing, universally_respectsIso, AlgebraicGeometry.universally_isZariskiLocalAtSource, AlgebraicGeometry.universally_isZariskiLocalAtTarget, AlgebraicGeometry.universally_isLocalAtSource, IsStableUnderComposition.universally, universally_eq_iff, AlgebraicGeometry.universallyClosed_iff, universally_mono, AlgebraicGeometry.universallyClosed_eq, AlgebraicGeometry.UniversallyInjective.universally_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_map 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback CategoryTheory.CommaMorphism.left CategoryTheory.Functor.map	—	overPullbackMap
baseChange_map' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	pullbackLift_fst_snd
baseChange_obj 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	pullback_snd
colimMap 📖	mathematical	functorCategory	CategoryTheory.Limits.colimit CategoryTheory.Limits.colimMap	—	colimitsOfShape_le colimitsOfShape_colimMap
colimitsOfShape_colimMap 📖	mathematical	functorCategory	colimitsOfShape CategoryTheory.Limits.colimit CategoryTheory.Limits.colimMap	—	—
colimitsOfShape_eq_of_equivalence 📖	mathematical	—	colimitsOfShape	—	le_antisymm colimitsOfShape_le_of_final CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Equivalence.isEquivalence_functor
colimitsOfShape_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra colimitsOfShape	—	isStableUnderColimitsOfShape_iff_colimitsOfShape_le
colimitsOfShape_le_coproducts 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra colimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory coproducts	—	le_iSup
colimitsOfShape_le_of_final 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra colimitsOfShape	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.fac
colimitsOfShape_monotone 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra colimitsOfShape	—	—
coproducts_eq_self 📖	mathematical	—	coproducts	—	le_antisymm coproducts_le le_coproducts
coproducts_iff 📖	mathematical	—	coproducts colimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—
coproducts_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra coproducts	—	coproducts_iff colimitsOfShape_le IsStableUnderCoproducts.isStableUnderCoproductsOfShape
coproducts_le_iff 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra coproducts	—	le_trans le_coproducts coproducts_monotone coproducts_le
coproducts_monotone 📖	mathematical	—	Monotone CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra coproducts	—	coproducts_iff colimitsOfShape_le_coproducts colimitsOfShape_monotone
coproducts_of_small 📖	mathematical	colimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	coproducts	—	coproducts_iff colimitsOfShape_eq_of_equivalence
diagonal_iff 📖	mathematical	—	diagonal CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.diagonal	—	—
diagonal_isStableUnderComposition 📖	mathematical	—	IsStableUnderComposition diagonal	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape diagonal_iff CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback.diagonal_comp comp_mem CategoryTheory.Iso.isIso_inv pullback_snd instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange
diagonal_isomorphisms 📖	mathematical	—	diagonal isomorphisms monomorphisms	—	ext CategoryTheory.Limits.pullback.isIso_diagonal_iff
hasOfPostcompProperty_iff_le_diagonal 📖	mathematical	—	HasOfPostcompProperty CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra diagonal	—	HasOfPostcompProperty.of_postcomp pullback_fst instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.Limits.pullback.diagonal_fst id_mem IsMultiplicative.toContainsIdentities CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.id_comp CategoryTheory.Limits.limit.lift_π comp_mem IsMultiplicative.toIsStableUnderComposition of_isPullback CategoryTheory.Limits.pullback_lift_diagonal_isPullback pullback_snd
hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	HasPullbacks.hasPullback
hasPushout 📖	mathematical	—	CategoryTheory.Limits.HasPushout	—	HasPushouts.hasPushout
instContainsIdentitiesDiagonalOfRespectsIso 📖	mathematical	—	ContainsIdentities diagonal	—	of_isIso CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono CategoryTheory.instMonoId
instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong 📖	mathematical	—	HasPullbacksAlong CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	HasPullbacksAlong.hasPullback pullback_snd CategoryTheory.IsPullback.hasPullback CategoryTheory.IsPullback.paste_horiz CategoryTheory.IsPullback.of_hasPullback
instHasPullbacksAlongOfHasPullbacks 📖	mathematical	—	HasPullbacksAlong	—	hasPullback
instHasPullbacksOfHasPullbacks 📖	mathematical	—	HasPullbacks	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instHasPushoutsAlongCompOfIsStableUnderCobaseChangeAlong 📖	mathematical	—	HasPushoutsAlong CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	HasPushoutsAlong.hasPushout pushout_inr CategoryTheory.IsPushout.hasPushout CategoryTheory.IsPushout.paste_vert CategoryTheory.IsPushout.of_hasPushout
instHasPushoutsAlongOfHasPushouts 📖	mathematical	—	HasPushoutsAlong	—	hasPushout
instHasPushoutsOfHasPushouts 📖	mathematical	—	HasPushouts	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instIsMultiplicativeDiagonalOfIsStableUnderBaseChange 📖	mathematical	—	IsMultiplicative diagonal	—	instContainsIdentitiesDiagonalOfRespectsIso IsMultiplicative.toContainsIdentities instRespectsOfRespectsLeftOfRespectsRight Respects.toRespectsLeft IsStableUnderBaseChange.respectsIso Respects.toRespectsRight diagonal_isStableUnderComposition IsMultiplicative.toIsStableUnderComposition
instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong 📖	mathematical	—	IsStableUnderBaseChangeAlong CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	HasPullbacksAlong.hasPullback CategoryTheory.IsPullback.of_hasPullback IsStableUnderBaseChangeAlong.of_isPullback CategoryTheory.IsPullback.of_right'
instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange 📖	mathematical	—	IsStableUnderBaseChangeAlong	—	IsStableUnderBaseChange.of_isPullback
instIsStableUnderBaseChangePullbacks 📖	mathematical	—	IsStableUnderBaseChange pullbacks	—	CategoryTheory.IsPullback.paste_horiz
instIsStableUnderBaseChangeTop 📖	mathematical	—	IsStableUnderBaseChange Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	—
instIsStableUnderCobaseChangeAlongCompOfHasPushoutsAlong 📖	mathematical	—	IsStableUnderCobaseChangeAlong CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	HasPushoutsAlong.hasPushout CategoryTheory.IsPushout.of_hasPushout IsStableUnderCobaseChangeAlong.of_isPushout CategoryTheory.IsPushout.flip CategoryTheory.IsPushout.of_left'
instIsStableUnderCobaseChangeAlongOfIsStableUnderCobaseChange 📖	mathematical	—	IsStableUnderCobaseChangeAlong	—	IsStableUnderCobaseChange.of_isPushout
instIsStableUnderCobaseChangePushouts 📖	mathematical	—	IsStableUnderCobaseChange pushouts	—	CategoryTheory.IsPushout.paste_horiz
instIsStableUnderCobaseChangeTop 📖	mathematical	—	IsStableUnderCobaseChange Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	—
instIsStableUnderFilteredColimitsIsomorphisms 📖	mathematical	—	IsStableUnderFilteredColimits isomorphisms	—	IsStableUnderColimitsOfShape.isomorphisms
instRespectsIsoColimitsOfShape 📖	mathematical	—	RespectsIso colimitsOfShape	—	RespectsIso.of_respects_arrow_iso CategoryTheory.CommaMorphism.w CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.fac CategoryTheory.Category.assoc CategoryTheory.Limits.IsColimit.fac_assoc
instRespectsIsoLimitsOfShape 📖	mathematical	—	RespectsIso limitsOfShape	—	RespectsIso.of_respects_arrow_iso CategoryTheory.CommaMorphism.w CategoryTheory.Arrow.hom_inv_id_left_assoc CategoryTheory.Arrow.hom_inv_id_right_assoc CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Limits.IsLimit.fac CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
instRespectsIsoPullbacks 📖	mathematical	—	RespectsIso pullbacks	—	RespectsIso.of_respects_arrow_iso CategoryTheory.IsPullback.paste_horiz CategoryTheory.IsPullback.of_horiz_isIso CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_inv CategoryTheory.Arrow.isIso_right CategoryTheory.CommaMorphism.w
instRespectsIsoPushouts 📖	mathematical	—	RespectsIso pushouts	—	RespectsIso.of_respects_arrow_iso CategoryTheory.IsPushout.paste_horiz CategoryTheory.IsPushout.of_horiz_isIso CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_hom CategoryTheory.Arrow.isIso_right CategoryTheory.CommaMorphism.w
isStableUnderBaseChange_iff_pullbacks_le 📖	mathematical	—	IsStableUnderBaseChange CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pullbacks	—	of_isPullback
isStableUnderCobaseChange_iff_pushouts_le 📖	mathematical	—	IsStableUnderCobaseChange CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pushouts	—	of_isPushout
isStableUnderColimitsOfShape_iff_colimitsOfShape_le 📖	mathematical	—	IsStableUnderColimitsOfShape CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra colimitsOfShape	—	IsStableUnderColimitsOfShape.condition CategoryTheory.Limits.IsColimit.fac colimitsOfShape.mk'
isStableUnderLimitsOfShape_iff_limitsOfShape_le 📖	mathematical	—	IsStableUnderLimitsOfShape CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra limitsOfShape	—	IsStableUnderLimitsOfShape.condition CategoryTheory.Limits.IsLimit.fac limitsOfShape.mk'
isomorphisms_le_pushouts 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.IsIso	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra isomorphisms pushouts	—	CategoryTheory.IsPushout.of_iso CategoryTheory.IsPushout.of_id_snd CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc
le_colimitsOfShape_punit 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra colimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	CategoryTheory.Limits.HasZeroObject.hasInitial CategoryTheory.Limits.hasZeroObject_pUnit CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.fac CategoryTheory.Limits.IsInitial.to_self CategoryTheory.Discrete.functor_map_id CategoryTheory.inv.congr_simp CategoryTheory.IsIso.inv_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Discrete.ext
le_coproducts 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra coproducts	—	LE.le.trans le_colimitsOfShape_punit colimitsOfShape_le_coproducts
le_pullbacks 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pullbacks	—	CategoryTheory.IsPullback.of_id_fst
le_pushouts 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pushouts	—	CategoryTheory.IsPushout.of_id_fst
limMap 📖	mathematical	functorCategory	CategoryTheory.Limits.limit CategoryTheory.Limits.limMap	—	limitsOfShape_le limitsOfShape_limMap
limitsOfShape_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra limitsOfShape	—	isStableUnderLimitsOfShape_iff_limitsOfShape_le
limitsOfShape_limMap 📖	mathematical	functorCategory	limitsOfShape CategoryTheory.Limits.limit CategoryTheory.Limits.limMap	—	—
limitsOfShape_monotone 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra limitsOfShape	—	—
of_isPullback 📖	—	CategoryTheory.IsPullback	—	—	IsStableUnderBaseChange.of_isPullback
of_isPushout 📖	—	CategoryTheory.IsPushout	—	—	IsStableUnderCobaseChange.of_isPushout
overPullbackMap 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback CategoryTheory.CommaMorphism.left CategoryTheory.Functor.map	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.comp_id pullbackLift_fst_snd
pullbackLift_fst_snd 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	of_isPullback CategoryTheory.IsPullback.of_bot CategoryTheory.Limits.limit.lift_π CategoryTheory.IsPullback.of_hasPullback
pullbackMap 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasPullback_symmetry_of_hasPullbacksAlong CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CategoryStruct.comp CategoryTheory.Category.comp_id	—	CategoryTheory.Limits.hasPullback_symmetry_of_hasPullbacksAlong CategoryTheory.Category.comp_id CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd comp_mem cancel_left_of_respectsIso IsStableUnderBaseChange.respectsIso CategoryTheory.Iso.isIso_hom overPullbackMap
pullback_fst 📖	mathematical	—	CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst	—	IsStableUnderBaseChangeAlong.of_isPullback CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_hasPullback
pullback_map 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasPullback_symmetry_of_hasPullbacksAlong CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CategoryStruct.comp CategoryTheory.Category.comp_id	—	pullbackMap
pullback_snd 📖	mathematical	—	CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.snd	—	IsStableUnderBaseChangeAlong.of_isPullback CategoryTheory.IsPullback.of_hasPullback
pullbacks_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pullbacks	—	isStableUnderBaseChange_iff_pullbacks_le
pullbacks_mk 📖	mathematical	CategoryTheory.IsPullback	pullbacks	—	—
pullbacks_monotone 📖	mathematical	—	Monotone CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pullbacks	—	—
pushoutDesc_inl_inr 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.desc CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr	—	IsStableUnderCobaseChangeAlong.of_isPushout instIsStableUnderCobaseChangeAlongOfIsStableUnderCobaseChange CategoryTheory.IsPushout.of_top CategoryTheory.Limits.colimit.ι_desc CategoryTheory.IsPushout.flip CategoryTheory.IsPushout.of_hasPushout
pushoutMap 📖	mathematical	CategoryTheory.Limits.HasPushoutsAlong CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pushout CategoryTheory.Limits.hasPushouts_symmetry_of_hasPushoutsAlong CategoryTheory.Limits.pushout.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasPushouts_symmetry_of_hasPushoutsAlong CategoryTheory.Category.id_comp CategoryTheory.Limits.hasPushout_symmetry CategoryTheory.Limits.pushout.hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.assoc CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc comp_mem cancel_left_of_respectsIso IsStableUnderCobaseChange.respectsIso CategoryTheory.Iso.isIso_hom underPushoutMap
pushout_inl 📖	mathematical	—	CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inl	—	IsStableUnderCobaseChangeAlong.of_isPushout CategoryTheory.IsPushout.of_hasPushout
pushout_inr 📖	mathematical	—	CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr	—	IsStableUnderCobaseChangeAlong.of_isPushout CategoryTheory.IsPushout.flip CategoryTheory.IsPushout.of_hasPushout
pushouts_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pushouts	—	isStableUnderCobaseChange_iff_pushouts_le
pushouts_le_iff 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pushouts	—	le_trans le_pushouts pushouts_monotone pushouts_le
pushouts_mk 📖	mathematical	CategoryTheory.IsPushout	pushouts	—	—
pushouts_monotone 📖	mathematical	—	Monotone CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra pushouts	—	—
underPushoutMap 📖	mathematical	CategoryTheory.Limits.HasPushoutsAlong CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.pushout CategoryTheory.CommaMorphism.right CategoryTheory.Functor.map	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.id_comp pushoutDesc_inl_inr
universally_eq_iff 📖	mathematical	—	universally IsStableUnderBaseChange	—	universally_isStableUnderBaseChange LE.le.antisymm universally_le IsStableUnderBaseChange.of_isPullback CategoryTheory.IsPullback.flip
universally_inf 📖	mathematical	—	universally CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	—	ext
universally_isStableUnderBaseChange 📖	mathematical	—	IsStableUnderBaseChange universally	—	CategoryTheory.IsPullback.paste_vert CategoryTheory.IsPullback.flip
universally_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra universally	—	CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
universally_mk' 📖	mathematical	CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst	universally	—	CategoryTheory.IsPullback.hasPullback CategoryTheory.IsPullback.isoPullback_hom_fst cancel_left_of_respectsIso CategoryTheory.Iso.isIso_hom
universally_mono 📖	mathematical	—	Monotone CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra universally	—	—
universally_respectsIso 📖	mathematical	—	RespectsIso universally	—	CategoryTheory.IsPullback.of_horiz_isIso CategoryTheory.IsIso.id CategoryTheory.Iso.isIso_inv CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.IsPullback.paste_horiz

CategoryTheory.MorphismProperty.HasPullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	—

CategoryTheory.MorphismProperty.HasPullbacksAlong

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	—

CategoryTheory.MorphismProperty.HasPushouts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPushout 📖	mathematical	—	CategoryTheory.Limits.HasPushout	—	—

CategoryTheory.MorphismProperty.HasPushoutsAlong

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPushout 📖	mathematical	—	CategoryTheory.Limits.HasPushout	—	—

CategoryTheory.MorphismProperty.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagonal 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty.diagonal	—	mk' CategoryTheory.MorphismProperty.RespectsIso.diagonal CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.MorphismProperty.diagonal_iff CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.diagonal_pullback_fst CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_hom CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.Iso.isIso_inv CategoryTheory.MorphismProperty.overPullbackMap
hasOfPostcompProperty_monomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.Limits.hasPullback_of_left_factors_mono CategoryTheory.Limits.pullback_snd_iso_of_left_factors_mono CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition CategoryTheory.MorphismProperty.cancel_left_of_respectsIso respectsIso CategoryTheory.Iso.isIso_inv CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange
inf 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	of_isPullback
isomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.IsPullback.isIso_snd_of_isIso
mk' 📖	mathematical	CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst	CategoryTheory.MorphismProperty.IsStableUnderBaseChange	—	CategoryTheory.IsPullback.hasPullback CategoryTheory.IsPullback.flip CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_inv CategoryTheory.IsPullback.isoPullback_inv_fst
monomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.IsPullback.mono_snd_of_mono
of_forall_exists_isPullback 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.IsPullback	CategoryTheory.MorphismProperty.IsStableUnderBaseChange	—	mk' CategoryTheory.IsPullback.isoPullback_inv_fst CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_inv
of_isPullback 📖	—	CategoryTheory.IsPullback	—	—	—
op 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPushout.unop
respectsIso 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso	—	CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso of_isPullback CategoryTheory.IsPullback.of_horiz_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_inv CategoryTheory.Arrow.isIso_right CategoryTheory.CommaMorphism.w
universally_eq 📖	mathematical	—	CategoryTheory.MorphismProperty.universally	—	CategoryTheory.MorphismProperty.universally_eq_iff
unop 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPushout.op

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isPullback 📖	—	CategoryTheory.IsPullback	—	—	—

CategoryTheory.MorphismProperty.IsStableUnderCobaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epimorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange CategoryTheory.MorphismProperty.epimorphisms	—	CategoryTheory.IsPushout.epi_inl_of_epi
hasOfPrecompProperty_epimorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPrecompProperty CategoryTheory.MorphismProperty.epimorphisms	—	CategoryTheory.Limits.hasPushout_of_left_factors_epi CategoryTheory.Limits.pushout_inl_iso_of_left_factors_epi CategoryTheory.asIso_inv CategoryTheory.IsIso.eq_comp_inv CategoryTheory.cancel_epi CategoryTheory.Limits.pushout.condition CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.cancel_right_of_respectsIso respectsIso CategoryTheory.Iso.isIso_inv CategoryTheory.MorphismProperty.pushout_inr CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeAlongOfIsStableUnderCobaseChange
inf 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	of_isPushout
isomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.IsPushout.isIso_inl_of_isIso
mk' 📖	mathematical	CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange	—	CategoryTheory.IsPushout.hasPushout CategoryTheory.IsPushout.flip CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.Iso.isIso_hom CategoryTheory.IsPushout.inr_isoPushout_hom
of_forall_exists_isPullback 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.IsPushout	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange	—	mk' CategoryTheory.IsPushout.inr_isoPushout_hom CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.Iso.isIso_hom
of_isPushout 📖	—	CategoryTheory.IsPushout	—	—	—
op 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPullback.unop
respectsIso 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso	—	CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso of_isPushout CategoryTheory.IsPushout.of_horiz_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_hom CategoryTheory.Arrow.isIso_right CategoryTheory.CommaMorphism.w
unop 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPullback.op

CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isPushout 📖	—	CategoryTheory.IsPushout	—	—	—

CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	CategoryTheory.MorphismProperty.functorCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	CategoryTheory.Limits.Cocone.pt	—	—
isomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.NatIso.isIso_of_isIso_app CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Limits.IsColimit.fac CategoryTheory.NatIso.isIso_inv_app CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.Category.comp_id CategoryTheory.Limits.IsColimit.fac_assoc CategoryTheory.IsIso.inv_hom_id_assoc

CategoryTheory.MorphismProperty.IsStableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
universally 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition CategoryTheory.MorphismProperty.universally	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.lift_fst CategoryTheory.MorphismProperty.comp_mem CategoryTheory.IsPullback.of_right CategoryTheory.Limits.pullback.lift_snd CategoryTheory.IsPullback.of_hasPullback

CategoryTheory.MorphismProperty.IsStableUnderCoproducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStableUnderCoproductsOfShape 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape	—	—

CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk 📖	mathematical	CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.Sigma.map	CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape	—	CategoryTheory.Limits.hasColimit_of_iso CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.Sigma.ι_isoColimit_hom_assoc CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc CategoryTheory.Limits.Sigma.ι_map_assoc CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom

CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStableUnderColimitsOfShape 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape	—	—

CategoryTheory.MorphismProperty.IsStableUnderFiniteCoproducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStableUnderCoproductsOfShape 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape	—	—

CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStableUnderProductsOfShape 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape	—	—

CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	CategoryTheory.MorphismProperty.functorCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	CategoryTheory.Limits.Cone.pt	—	—

CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk 📖	mathematical	CategoryTheory.Limits.piObj CategoryTheory.Limits.Pi.map	CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape	—	CategoryTheory.Limits.hasLimit_of_iso CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.Limits.limit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.Pi.map_π CategoryTheory.Limits.Pi.isoLimit_inv_π_assoc CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc CategoryTheory.Limits.Pi.isoLimit_inv_π CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp

CategoryTheory.MorphismProperty.RespectsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagonal 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso CategoryTheory.MorphismProperty.diagonal	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.MorphismProperty.diagonal_iff CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback.diagonal_comp CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.Limits.pullback.map_isIso CategoryTheory.IsIso.id CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.pullback_fst_iso_of_right_iso CategoryTheory.IsIso.comp_isIso CategoryTheory.Limits.pullback_snd_iso_of_left_iso

CategoryTheory.MorphismProperty.colimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	CategoryTheory.MorphismProperty.functorCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	CategoryTheory.MorphismProperty.colimitsOfShape CategoryTheory.Limits.Cocone.pt	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.fac
of_isColimit 📖	mathematical	CategoryTheory.Functor.obj Preorder.smallCategory Bot.bot OrderBot.toBot Preorder.toLE CategoryTheory.Functor.map CategoryTheory.homOfLE bot_le	CategoryTheory.MorphismProperty.colimitsOfShape Preorder.smallCategory CategoryTheory.Functor.obj Bot.bot OrderBot.toBot Preorder.toLE CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	bot_le mk' CategoryTheory.IsCofiltered.isConnected CategoryTheory.isCofiltered_of_directed_ge_nonempty OrderBot.instIsCodirectedOrder bot_nonempty CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Limits.Cocone.w

CategoryTheory.MorphismProperty.limitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	CategoryTheory.MorphismProperty.functorCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	CategoryTheory.MorphismProperty.limitsOfShape CategoryTheory.Limits.Cone.pt	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Limits.IsLimit.fac

---

← Back to Index