Creates

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

Statistics

Metric	Count
Definitions `CreatesColimit`, `lifts`, `CreatesColimits`, `CreatesColimitsOfShape`, `CreatesColimit`, `CreatesColimitsOfSize`, `CreatesColimitsOfShape`, `CreatesLimit`, `lifts`, `CreatesLimits`, `CreatesLimitsOfShape`, `CreatesLimit`, `CreatesLimitsOfSize`, `CreatesLimitsOfShape`, `LiftableCocone`, `liftedCocone`, `validLift`, `LiftableCone`, `liftedCone`, `validLift`, `LiftsToColimit`, `makesColimit`, `toLiftableCocone`, `LiftsToLimit`, `makesLimit`, `toLiftableCone`, `compCreatesColimit`, `compCreatesColimits`, `compCreatesColimitsOfShape`, `compCreatesLimit`, `compCreatesLimits`, `compCreatesLimitsOfShape`, `createsColimitOfFullyFaithfulOfIso`, `createsColimitOfFullyFaithfulOfIso'`, `createsColimitOfFullyFaithfulOfLift`, `createsColimitOfFullyFaithfulOfLift'`, `createsColimitOfIsoDiagram`, `createsColimitOfNatIso`, `createsColimitOfReflectsIso`, `createsColimitOfReflectsIso'`, `createsColimitOfReflectsIsomorphismsOfPreserves`, `createsColimitsOfNatIso`, `createsColimitsOfShapeOfEquiv`, `createsColimitsOfShapeOfNatIso`, `createsLimitOfFullyFaithfulOfIso`, `createsLimitOfFullyFaithfulOfIso'`, `createsLimitOfFullyFaithfulOfLift`, `createsLimitOfFullyFaithfulOfLift'`, `createsLimitOfFullyFaithfulOfPreserves`, `createsLimitOfIsoDiagram`, `createsLimitOfNatIso`, `createsLimitOfReflectsIso`, `createsLimitOfReflectsIso'`, `createsLimitOfReflectsIsomorphismsOfPreserves`, `createsLimitsOfNatIso`, `createsLimitsOfShapeOfEquiv`, `createsLimitsOfShapeOfNatIso`, `idCreatesColimits`, `idCreatesLimits`, `idLiftsCocone`, `idLiftsCone`, `inhabitedLiftableCocone`, `inhabitedLiftableCone`, `inhabitedLiftsToColimit`, `inhabitedLiftsToLimit`, `liftColimit`, `liftLimit`, `liftedColimitIsColimit`, `liftedColimitMapsToOriginal`, `liftedLimitIsLimit`, `liftedLimitMapsToOriginal`, `liftsToColimitOfCreates`, `liftsToLimitOfCreates`	73
Theorems `toReflectsColimit`, `toReflectsLimit`, `hasColimit_of_created`, `hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape`, `hasColimits_of_hasColimits_createsColimits`, `hasLimit_of_created`, `hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape`, `hasLimits_of_hasLimits_createsLimits`, `liftedLimitMapsToOriginal_hom_π`, `liftedLimitMapsToOriginal_inv_map_π`, `preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape`, `preservesColimit_comp_of_createsColimit`, `preservesColimit_of_createsColimit_and_hasColimit`, `preservesColimits_of_createsColimits_and_hasColimits`, `preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape`, `preservesLimit_comp_of_createsLimit`, `preservesLimit_of_createsLimit_and_hasLimit`, `preservesLimits_of_createsLimits_and_hasLimits`, `reflectsColimitsOfCreatesColimits`, `reflectsColimitsOfShapeOfCreatesColimitsOfShape`, `reflectsLimitsOfCreatesLimits`, `reflectsLimitsOfShapeOfCreatesLimitsOfShape`	22
Total	95

CategoryTheory

Definitions

Name	Category	Theorems
`CreatesColimit` 📖	CompData	—
`CreatesColimits` 📖	CompOp	—
`CreatesColimitsOfShape` 📖	CompData	—
`CreatesColimitsOfSize` 📖	CompData	—
`CreatesLimit` 📖	CompData	—
`CreatesLimits` 📖	CompOp	—
`CreatesLimitsOfShape` 📖	CompData	—
`CreatesLimitsOfSize` 📖	CompData	—
`LiftableCocone` 📖	CompData	—
`LiftableCone` 📖	CompData	—
`LiftsToColimit` 📖	CompData	—
`LiftsToLimit` 📖	CompData	—
`compCreatesColimit` 📖	CompOp	—
`compCreatesColimits` 📖	CompOp	—
`compCreatesColimitsOfShape` 📖	CompOp	—
`compCreatesLimit` 📖	CompOp	—
`compCreatesLimits` 📖	CompOp	—
`compCreatesLimitsOfShape` 📖	CompOp	—
`createsColimitOfFullyFaithfulOfIso` 📖	CompOp	—
`createsColimitOfFullyFaithfulOfIso'` 📖	CompOp	—
`createsColimitOfFullyFaithfulOfLift` 📖	CompOp	—
`createsColimitOfFullyFaithfulOfLift'` 📖	CompOp	—
`createsColimitOfIsoDiagram` 📖	CompOp	—
`createsColimitOfNatIso` 📖	CompOp	—
`createsColimitOfReflectsIso` 📖	CompOp	—
`createsColimitOfReflectsIso'` 📖	CompOp	—
`createsColimitOfReflectsIsomorphismsOfPreserves` 📖	CompOp	—
`createsColimitsOfNatIso` 📖	CompOp	—
`createsColimitsOfShapeOfEquiv` 📖	CompOp	—
`createsColimitsOfShapeOfNatIso` 📖	CompOp	—
`createsLimitOfFullyFaithfulOfIso` 📖	CompOp	—
`createsLimitOfFullyFaithfulOfIso'` 📖	CompOp	—
`createsLimitOfFullyFaithfulOfLift` 📖	CompOp	—
`createsLimitOfFullyFaithfulOfLift'` 📖	CompOp	—
`createsLimitOfFullyFaithfulOfPreserves` 📖	CompOp	—
`createsLimitOfIsoDiagram` 📖	CompOp	—
`createsLimitOfNatIso` 📖	CompOp	—
`createsLimitOfReflectsIso` 📖	CompOp	—
`createsLimitOfReflectsIso'` 📖	CompOp	—
`createsLimitOfReflectsIsomorphismsOfPreserves` 📖	CompOp	—
`createsLimitsOfNatIso` 📖	CompOp	—
`createsLimitsOfShapeOfEquiv` 📖	CompOp	—
`createsLimitsOfShapeOfNatIso` 📖	CompOp	—
`idCreatesColimits` 📖	CompOp	—
`idCreatesLimits` 📖	CompOp	2 math math: `CartesianMonoidalCategory.prodComparisonIso_id`, `CartesianMonoidalCategory.preservesTerminalIso_id`
`idLiftsCocone` 📖	CompOp	—
`idLiftsCone` 📖	CompOp	—
`inhabitedLiftableCocone` 📖	CompOp	—
`inhabitedLiftableCone` 📖	CompOp	—
`inhabitedLiftsToColimit` 📖	CompOp	—
`inhabitedLiftsToLimit` 📖	CompOp	—
`liftColimit` 📖	CompOp	—
`liftLimit` 📖	CompOp	2 math math: `liftedLimitMapsToOriginal_inv_map_π`, `liftedLimitMapsToOriginal_hom_π`
`liftedColimitIsColimit` 📖	CompOp	—
`liftedColimitMapsToOriginal` 📖	CompOp	—
`liftedLimitIsLimit` 📖	CompOp	—
`liftedLimitMapsToOriginal` 📖	CompOp	2 math math: `liftedLimitMapsToOriginal_inv_map_π`, `liftedLimitMapsToOriginal_hom_π`
`liftsToColimitOfCreates` 📖	CompOp	—
`liftsToLimitOfCreates` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimit_of_created` 📖	mathematical	—	`Limits.HasColimit`	—	—
`hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape` 📖	mathematical	—	`Limits.HasColimitsOfShape`	—	`hasColimit_of_created` `Limits.hasColimitOfHasColimitsOfShape`
`hasColimits_of_hasColimits_createsColimits` 📖	mathematical	—	`Limits.HasColimitsOfSize`	—	`hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape` `Limits.hasColimitsOfShapeOfHasColimitsOfSize`
`hasLimit_of_created` 📖	mathematical	—	`Limits.HasLimit`	—	—
`hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape` 📖	mathematical	—	`Limits.HasLimitsOfShape`	—	`hasLimit_of_created` `Limits.hasLimitOfHasLimitsOfShape`
`hasLimits_of_hasLimits_createsLimits` 📖	mathematical	—	`Limits.HasLimitsOfSize`	—	`hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape` `Limits.hasLimitsOfShapeOfHasLimits`
`liftedLimitMapsToOriginal_hom_π` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Limits.Cone.pt` `Functor.comp` `Functor.mapCone` `liftLimit` `Functor.obj` `Limits.ConeMorphism.hom` `Iso.hom` `Limits.Cone` `Limits.Cone.category` `liftedLimitMapsToOriginal` `NatTrans.app` `Functor` `Functor.category` `Functor.const` `Limits.Cone.π` `Functor.map`	—	`liftedLimitMapsToOriginal_inv_map_π` `Iso.hom_inv_id` `Category.id_comp`
`liftedLimitMapsToOriginal_inv_map_π` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Limits.Cone.pt` `Functor.comp` `Functor.mapCone` `liftLimit` `Functor.obj` `Limits.ConeMorphism.hom` `Iso.inv` `Limits.Cone` `Limits.Cone.category` `liftedLimitMapsToOriginal` `Functor.map` `NatTrans.app` `Functor` `Functor.category` `Functor.const` `Limits.Cone.π`	—	`Limits.ConeMorphism.w` `Category.assoc` `Limits.Cone.category_comp_hom` `Iso.inv_hom_id` `Category.id_comp`
`preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape` 📖	mathematical	—	`Limits.PreservesColimitsOfShape`	—	`preservesColimit_of_createsColimit_and_hasColimit` `Limits.hasColimitOfHasColimitsOfShape`
`preservesColimit_comp_of_createsColimit` 📖	mathematical	—	`Limits.PreservesColimit` `Functor.comp`	—	—
`preservesColimit_of_createsColimit_and_hasColimit` 📖	mathematical	—	`Limits.PreservesColimit`	—	—
`preservesColimits_of_createsColimits_and_hasColimits` 📖	mathematical	—	`Limits.PreservesColimitsOfSize`	—	`preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape` `Limits.hasColimitsOfShapeOfHasColimitsOfSize`
`preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape` 📖	mathematical	—	`Limits.PreservesLimitsOfShape`	—	`preservesLimit_of_createsLimit_and_hasLimit` `Limits.hasLimitOfHasLimitsOfShape`
`preservesLimit_comp_of_createsLimit` 📖	mathematical	—	`Limits.PreservesLimit` `Functor.comp`	—	—
`preservesLimit_of_createsLimit_and_hasLimit` 📖	mathematical	—	`Limits.PreservesLimit`	—	—
`preservesLimits_of_createsLimits_and_hasLimits` 📖	mathematical	—	`Limits.PreservesLimitsOfSize`	—	`preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape` `Limits.hasLimitsOfShapeOfHasLimits`
`reflectsColimitsOfCreatesColimits` 📖	mathematical	—	`Limits.ReflectsColimitsOfSize`	—	`reflectsColimitsOfShapeOfCreatesColimitsOfShape`
`reflectsColimitsOfShapeOfCreatesColimitsOfShape` 📖	mathematical	—	`Limits.ReflectsColimitsOfShape`	—	`CreatesColimit.toReflectsColimit`
`reflectsLimitsOfCreatesLimits` 📖	mathematical	—	`Limits.ReflectsLimitsOfSize`	—	`reflectsLimitsOfShapeOfCreatesLimitsOfShape`
`reflectsLimitsOfShapeOfCreatesLimitsOfShape` 📖	mathematical	—	`Limits.ReflectsLimitsOfShape`	—	`CreatesLimit.toReflectsLimit`

CategoryTheory.CreatesColimit

Definitions

Name	Category	Theorems
`lifts` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toReflectsColimit` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsColimit`	—	—

CategoryTheory.CreatesColimitsOfShape

Definitions

Name	Category	Theorems
`CreatesColimit` 📖	CompOp	1 math math: `AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty`

CategoryTheory.CreatesColimitsOfSize

Definitions

Name	Category	Theorems
`CreatesColimitsOfShape` 📖	CompOp	—

CategoryTheory.CreatesLimit

Definitions

Name	Category	Theorems
`lifts` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toReflectsLimit` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsLimit`	—	—

CategoryTheory.CreatesLimitsOfShape

Definitions

Name	Category	Theorems
`CreatesLimit` 📖	CompOp	2 math math: `CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_id`, `CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_id`

CategoryTheory.CreatesLimitsOfSize

Definitions

Name	Category	Theorems
`CreatesLimitsOfShape` 📖	CompOp	2 math math: `CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_id`, `CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_id`

CategoryTheory.LiftableCocone

Definitions

Name	Category	Theorems
`liftedCocone` 📖	CompOp	—
`validLift` 📖	CompOp	—

CategoryTheory.LiftableCone

Definitions

Name	Category	Theorems
`liftedCone` 📖	CompOp	—
`validLift` 📖	CompOp	—

CategoryTheory.LiftsToColimit

Definitions

Name	Category	Theorems
`makesColimit` 📖	CompOp	—
`toLiftableCocone` 📖	CompOp	—

CategoryTheory.LiftsToLimit

Definitions

Name	Category	Theorems
`makesLimit` 📖	CompOp	—
`toLiftableCone` 📖	CompOp	—

---

← Back to Index