CommaSites

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

Statistics

Metric	Count
Definitions	0
Theorems exists_map_eq_of_presieve, locallyCoverDense_forget_of_le, toGrothendieck_comap_forget_eq_inducedTopology	3
Total	3

CategoryTheory.MorphismProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_map_eq_of_presieve 📖	mathematical	CategoryTheory.Precoverage Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder precoverage CategoryTheory.Presieve CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj Over Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop Over.forget Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Precoverage.comap CategoryTheory.Over.forget	CategoryTheory.Presieve Over Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop CategoryTheory.Presieve.map CategoryTheory.Over CategoryTheory.instCategoryOver Over.forget	—	IsMultiplicative.instTop CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover CategoryTheory.Over.w comp_mem CategoryTheory.Precoverage.ZeroHypercover.mem₀ Comma.prop CategoryTheory.Presieve.map_ofArrows
locallyCoverDense_forget_of_le 📖	mathematical	CategoryTheory.Precoverage Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder precoverage	CategoryTheory.Functor.LocallyCoverDense Over Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop CategoryTheory.Over CategoryTheory.instCategoryOver Over.forget CategoryTheory.GrothendieckTopology.over CategoryTheory.Precoverage.toGrothendieck	—	IsMultiplicative.instTop CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem CategoryTheory.Precoverage.instHasIsosComap CategoryTheory.Precoverage.instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected CategoryTheory.instIsConnectedWidePullbackShape CategoryTheory.Precoverage.instIsStableUnderCompositionComap CategoryTheory.Precoverage.instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan exists_map_eq_of_presieve CategoryTheory.Presieve.map_functorPullback_map
toGrothendieck_comap_forget_eq_inducedTopology 📖	mathematical	CategoryTheory.Precoverage Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder precoverage	CategoryTheory.Precoverage.toGrothendieck Over Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop CategoryTheory.Precoverage.comap CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver Over.forget CategoryTheory.Over.forget CategoryTheory.Functor.inducedTopology CategoryTheory.GrothendieckTopology.over locallyCoverDense_forget_of_le CategoryTheory.Functor.IsLocallyFull.of_full instFullOverTopOverForget CategoryTheory.Functor.IsLocallyFaithful.of_faithful instFaithfulOverTopOverForget	—	IsMultiplicative.instTop CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget locallyCoverDense_forget_of_le CategoryTheory.Functor.IsLocallyFull.of_full instFullOverTopOverForget CategoryTheory.Functor.IsLocallyFaithful.of_faithful instFaithfulOverTopOverForget CategoryTheory.Precoverage.comap_comp CategoryTheory.Functor.inducedTopology.congr_simp CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology CategoryTheory.Precoverage.instHasIsosComap CategoryTheory.Precoverage.instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected CategoryTheory.instIsConnectedWidePullbackShape CategoryTheory.Precoverage.instIsStableUnderCompositionComap CategoryTheory.Precoverage.instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan exists_map_eq_of_presieve CategoryTheory.Presieve.map_functorPullback_map

---

← Back to Index