Documentation Verification Report

LimitsOver

📁 Source: Mathlib/AlgebraicGeometry/LimitsOver.lean

Statistics

Metric	Count
Definitions `instCreatesColimitOverSchemeTopMorphismPropertyOverForget`, `instCreatesColimitsOfShapeOverSchemeTopMorphismPropertyOverDiscreteForgetOfSmall`	2
Theorems `instHasColimitOverScheme`, `instHasColimitOverSchemeTopMorphismProperty`, `instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall`, `instHasFiniteCoproductsOverSchemeTopMorphismProperty`, `instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget`, `instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan`, `instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty`, `instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget`, `instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit`, `instPreservesColimitOverSchemeTopMorphismPropertyOverForget`	10
Total	12

AlgebraicGeometry

Definitions

Name	Category	Theorems
`instCreatesColimitOverSchemeTopMorphismPropertyOverForget` 📖	CompOp	—
`instCreatesColimitsOfShapeOverSchemeTopMorphismPropertyOverDiscreteForgetOfSmall` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasColimitOverScheme` 📖	mathematical	`IsOpenImmersion` `CategoryTheory.Comma.left` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.map` `Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Limits.HasColimit`	—	`CategoryTheory.hasColimit_of_created` `Scheme.IsLocallyDirected.instHasColimit`
`instHasColimitOverSchemeTopMorphismProperty` 📖	mathematical	`IsOpenImmersion` `CategoryTheory.Comma.left` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Functor.map` `Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver`	`CategoryTheory.Limits.HasColimit`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.hasColimit_of_created` `CategoryTheory.Over.hasColimit_of_hasColimit_comp_forget` `Scheme.IsLocallyDirected.instHasColimit` `instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget` `instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget`
`instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall` 📖	mathematical	—	`CategoryTheory.Limits.HasCoproductsOfShape` `CategoryTheory.MorphismProperty.Over` `Scheme` `Scheme.instCategory` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `instHasColimitOverSchemeTopMorphismProperty` `IsOpenImmersion.of_isIso` `CategoryTheory.Comma.instIsIsoLeft` `CategoryTheory.MorphismProperty.Comma.instIsIsoCommaHom` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete`
`instHasFiniteCoproductsOverSchemeTopMorphismProperty` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteCoproducts` `CategoryTheory.MorphismProperty.Over` `Scheme` `Scheme.instCategory` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget` 📖	mathematical	—	`CategoryTheory.Functor.IsLocallyDirected` `CategoryTheory.Functor.comp` `Scheme` `Scheme.instCategory` `CategoryTheory.types` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.Over` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Over.forget` `CategoryTheory.Over.forget` `Scheme.forget`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan` 📖	mathematical	—	`IsOpenImmersion` `CategoryTheory.Comma.left` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Limits.span` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Functor.map`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Functor.map_id` `IsOpenImmersion.of_isIso` `CategoryTheory.Comma.instIsIsoLeft` `CategoryTheory.MorphismProperty.Comma.instIsIsoCommaHom` `CategoryTheory.IsIso.id`
`instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty` 📖	mathematical	`IsOpenImmersion` `CategoryTheory.Comma.left` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Functor.map` `Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver`	`CategoryTheory.Limits.colimit` `instHasColimitOverSchemeTopMorphismProperty` `CategoryTheory.Limits.colimit.ι`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `instHasColimitOverSchemeTopMorphismProperty` `CategoryTheory.MorphismProperty.Over.forget_comp_forget_map` `CategoryTheory.Limits.instHasColimitCompOfPreservesColimit` `CategoryTheory.Limits.comp_preservesColimit` `instPreservesColimitOverSchemeTopMorphismPropertyOverForget` `CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit` `Scheme.IsLocallyDirected.instHasColimit` `instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget` `instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `isOpenImmersion_respectsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.ι_preservesColimitIso_hom` `Scheme.IsLocallyDirected.instIsOpenImmersionι`
`instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget` 📖	mathematical	`IsOpenImmersion` `CategoryTheory.Comma.left` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Functor.map`	`CategoryTheory.Functor.comp` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.Over.forget` `CategoryTheory.Over.forget`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Over` `Scheme` `Scheme.instCategory` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Limits.span` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.Over.forget` `CategoryTheory.Over.forget` `Scheme.forget` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WidePushoutShape.Hom.init`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.mono_iff_injective` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding` `Scheme.Hom.isOpenEmbedding`
`instPreservesColimitOverSchemeTopMorphismPropertyOverForget` 📖	mathematical	`IsOpenImmersion` `CategoryTheory.Comma.left` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Functor.map` `Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver`	`CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.Over.forget`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit` `CategoryTheory.Over.hasColimit_of_hasColimit_comp_forget` `Scheme.IsLocallyDirected.instHasColimit` `instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget` `instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget`

---

← Back to Index