Limits

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

Statistics

Metric	Count
Definitions HasPullbacks, HasPullbacksAlong, IsStableUnderBaseChange, IsStableUnderBaseChangeAlong, IsStableUnderCobaseChange, IsStableUnderColimitsOfShape, IsStableUnderCoproducts, IsStableUnderCoproductsOfShape, IsStableUnderFilteredColimits, IsStableUnderFiniteCoproducts, IsStableUnderFiniteProducts, IsStableUnderLimitsOfShape, IsStableUnderProductsOfShape, colimitsOfShape, coproducts, diagonal, limitsOfShape, pullbacks, pushouts, universally	20
Theorems hasPullback, hasPullback, 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, 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, instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong, instHasPullbacksAlongOfHasPullbacks, instHasPullbacksOfHasPullbacks, instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong, instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange, instIsStableUnderBaseChangePullbacks, instIsStableUnderBaseChangeTop, 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, pullback_fst, pullback_map, pullback_snd, pullbacks_le, pullbacks_mk, pullbacks_monotone, pushout_inl, pushout_inr, pushouts_le, pushouts_le_iff, pushouts_mk, pushouts_monotone, universally_eq_iff, universally_inf, universally_isStableUnderBaseChange, universally_le, universally_mk', universally_mono, universally_respectsIso	108
Total	128

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
HasPullbacks 📖	CompData	2 math math: instHasPullbacksOfHasPullbacks, AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion
HasPullbacksAlong 📖	CompData	2 math math: instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong, instHasPullbacksAlongOfHasPullbacks
IsStableUnderBaseChange 📖	CompData	62 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.instIsStableUnderBaseChangeSchemeLocallyQuasiFinite, AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.IsProper.isStableUnderBaseChange, rlp_isStableUnderBaseChange, IsStableUnderBaseChange.inf, AlgebraicGeometry.quasiCompact_isStableUnderBaseChange, CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeMonoModSerre, AlgebraicGeometry.ValuativeCriterion.Existence.stableUnderBaseChange, 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
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	16 math math: hasOfPostcompProperty_iff_le_diagonal, AlgebraicGeometry.instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion, instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange, AlgebraicGeometry.HasAffineProperty.diagonal_iff, AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion, AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact, RespectsIso.diagonal, 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	27 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', 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.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback CategoryTheory.Functor.map	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.comp_id baseChange_map'
baseChange_map' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	of_isPullback CategoryTheory.IsPullback.of_bot CategoryTheory.Limits.limit.lift_π CategoryTheory.IsPullback.of_hasPullback
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.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback	—	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	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
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
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	—	—
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	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	limitsOfShape	—	—
of_isPullback 📖	—	CategoryTheory.IsPullback	—	—	IsStableUnderBaseChange.of_isPullback
of_isPushout 📖	—	CategoryTheory.IsPushout	—	—	IsStableUnderCobaseChange.of_isPushout
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 Quiver.Hom CategoryTheory.CategoryStruct.toQuiver 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 baseChange_map
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	—	—
pushout_inl 📖	mathematical	—	CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inl	—	of_isPushout CategoryTheory.IsPushout.of_hasPushout
pushout_inr 📖	mathematical	—	CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr	—	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	—	—
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.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.baseChange_map
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.Limits.hasPullback_of_left_iso CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsPullback.isoPullback_hom_snd
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.Limits.PullbackCone.IsLimit.hom_ext CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq Mathlib.Tactic.Reassoc.eq_whisker'
of_forall_exists_isPullback 📖	mathematical	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.Limits.PushoutCocone.IsColimit.hom_ext CategoryTheory.cancel_epi CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.CommSq.w CategoryTheory.IsPushout.toCommSq
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
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.Limits.hasPushout_of_right_iso CategoryTheory.IsIso.comp_isIso CategoryTheory.Limits.pushout_inl_iso_of_right_iso CategoryTheory.Iso.isIso_inv CategoryTheory.IsPushout.inl_isoPushout_inv
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	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.IsStableUnderColimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	—	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.ι	—	—	—
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 📖	—	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.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.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 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.NatTrans.naturality CategoryTheory.Category.comp_id

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.IsLimit.hom_ext CategoryTheory.Limits.IsLimit.fac

---

← Back to Index