CoverPreserving

📁 Source: Mathlib/CategoryTheory/Sites/CoverPreserving.lean

Statistics

Metric	Count
Definitions CompatiblePreserving, CoverPreserving	2
Theorems apply_map, compatible, comp, cover_preserve, isContinuous_of_coverPreserving, functorPushforward, compatiblePreservingOfDownwardsClosed, compatiblePreservingOfFlat, idCoverPreserving	9
Total	11

CategoryTheory

Definitions

Name	Category	Theorems
CompatiblePreserving 📖	CompData	7 math math: compatiblePreservingOfFlat, GrothendieckTopology.over_forget_compatiblePreserving, compatiblePreserving_opens_map, Functor.IsCoverDense.compatiblePreserving, compatiblePreservingOfDownwardsClosed, GrothendieckTopology.over_map_compatiblePreserving, Topology.IsOpenEmbedding.compatiblePreserving
CoverPreserving 📖	CompData	13 math math: CoverPreserving.comp, GrothendieckTopology.over_map_coverPreserving, Functor.inducedTopology_coverPreserving, GrothendieckTopology.coverPreserving_over_star, Functor.IsDenseSubsite.coverPreserving, IsOpenMap.coverPreserving, regularTopology.coverPreserving, Adjunction.isCocontinuous_iff_coverPreserving, coherentTopology.coverPreserving, GrothendieckTopology.coverPreserving_overPullback, idCoverPreserving, coverPreserving_opens_map, GrothendieckTopology.over_forget_coverPreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compatiblePreservingOfDownwardsClosed 📖	mathematical	—	CompatiblePreserving	—	Equiv.injective Functor.mapIso_hom FunctorToTypes.map_comp_apply Functor.map_preimage Functor.map_injective Functor.map_comp Category.assoc
compatiblePreservingOfFlat 📖	mathematical	—	CompatiblePreserving	—	RepresentablyFlat.cofiltered StructuredArrow.w Category.comp_id eqToHom_op Functor.map_comp eqToHom_map NatTrans.naturality
idCoverPreserving 📖	mathematical	—	CoverPreserving Functor.id	—	Sieve.functorPushforward_id

CategoryTheory.CompatiblePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_map 📖	mathematical	CategoryTheory.CompatiblePreserving CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Presieve.FamilyOfElements.functorPushforward CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Presieve.image_mem_functorPushforward	—	CategoryTheory.Presieve.image_mem_functorPushforward CategoryTheory.FunctorToTypes.map_id_apply compatible CategoryTheory.Category.id_comp
compatible 📖	mathematical	CategoryTheory.CompatiblePreserving CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.CoverPreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	CategoryTheory.CoverPreserving	CategoryTheory.CoverPreserving CategoryTheory.Functor.comp	—	CategoryTheory.Sieve.functorPushforward_comp cover_preserve
cover_preserve 📖	mathematical	CategoryTheory.CoverPreserving CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	CategoryTheory.Sieve CategoryTheory.Functor.obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.functorPushforward	—	—

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isContinuous_of_coverPreserving 📖	mathematical	CategoryTheory.CompatiblePreserving CategoryTheory.CoverPreserving	IsContinuous	—	existsUnique_of_exists_of_unique CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.CoverPreserving.cover_preserve CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPushforward CategoryTheory.Presieve.image_mem_functorPushforward CategoryTheory.Presieve.IsSheafFor.isAmalgamation CategoryTheory.CompatiblePreserving.apply_map CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheaf.isSeparated map_comp

CategoryTheory.Presieve.FamilyOfElements.Compatible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorPushforward 📖	mathematical	CategoryTheory.CompatiblePreserving CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Presieve.functorPushforward CategoryTheory.Presieve.FamilyOfElements.functorPushforward	—	CategoryTheory.CompatiblePreserving.compatible CategoryTheory.Category.assoc CategoryTheory.FunctorToTypes.map_comp_apply

---

← Back to Index