Basic

📁 Source: Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean

Statistics

Metric	Count
Definitions `IsCoverDense`, `appHom`, `appIso`, `presheafHom`, `presheafIso`, `pushforwardFamily`, `sheafIso`, `homOver`, `isoOver`, `presheafIso`, `restrictHomEquivHom`, `sheafCoyonedaHom`, `sheafHom`, `sheafIso`, `sheafYonedaHom`, `IsDenseSubsite`, `mapPreimage`, `CoverByImageStructure`, `map`, `obj`, `coverByImage`, `coverByImage`	22
Theorems `appHom_restrict`, `appHom_valid_glue`, `appIso_hom`, `appIso_inv`, `naturality`, `naturality_apply`, `naturality_assoc`, `presheafHom_app`, `presheafIso_hom_app`, `presheafIso_inv_app`, `pushforwardFamily_apply`, `pushforwardFamily_compatible`, `pushforwardFamily_def`, `sheafIso_hom_val`, `sheafIso_inv_val`, `compatiblePreserving`, `ext`, `faithful_sheafPushforwardContinuous`, `full_sheafPushforwardContinuous`, `functorPullback_pushforward_covering`, `homOver_app`, `isContinuous`, `is_cover`, `isoOver_hom_app`, `isoOver_inv_app`, `iso_of_restrict_iso`, `presheafIso_hom_app`, `presheafIso_inv`, `restrictHomEquivHom_naturality_left`, `restrictHomEquivHom_naturality_left_assoc`, `restrictHomEquivHom_naturality_left_symm`, `restrictHomEquivHom_naturality_left_symm_assoc`, `restrictHomEquivHom_naturality_right`, `restrictHomEquivHom_naturality_right_assoc`, `restrictHomEquivHom_naturality_right_symm`, `restrictHomEquivHom_naturality_right_symm_assoc`, `sheafCoyonedaHom_app`, `sheafHom_eq`, `sheafHom_restrict_eq`, `sheafIso_hom_val`, `sheafIso_inv_val`, `sheaf_eq_amalgamation`, `coverPreserving`, `equalizer_mem`, `faithful_sheafPushforwardContinuous`, `full_sheafPushforwardContinuous`, `functorPushforward_mem_iff`, `imageSieve_mem`, `instIsCocontinuous`, `instIsContinuous`, `isCoverDense`, `isCoverDense'`, `isLocallyFaithful`, `isLocallyFaithful'`, `isLocallyFull`, `isLocallyFull'`, `mapPreimage_comp`, `mapPreimage_comp_assoc`, `mapPreimage_comp_map`, `mapPreimage_comp_map_assoc`, `mapPreimage_id`, `mapPreimage_map`, `mapPreimage_map_of_fac`, `mapPreimage_of_eq`, `map_eq_of_eq`, `functorPushforward_mem_iff`, `isCoverDense_of_generate_singleton_functor_π_mem`, `is_cover_of_isCoverDense`, `whiskerLeft_obj_map_bijective_of_isCoverDense`, `fac`, `fac_assoc`, `in_coverByImage`	72
Total	94

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`IsCoverDense` 📖	CompData	9 math math: `CategoryTheory.regularTopology.instIsCoverDense`, `isCoverDense_of_generate_singleton_functor_π_mem`, `TopCat.Opens.coverDense_inducedFunctor`, `TopCat.Opens.coverDense_iff_isBasis`, `IsDenseSubsite.isCoverDense'`, `CategoryTheory.coherentTopology.instIsCoverDense`, `IsDenseSubsite.isCoverDense`, `CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence`, `AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat`
`IsDenseSubsite` 📖	CompData	12 math math: `CategoryTheory.Equivalence.isDenseSubsite_inverse_of_isCocontinuous`, `CategoryTheory.Equivalence.isDenseSubsite_functor_of_isCocontinuous`, `CategoryTheory.coherentTopology.instIsDenseSubsite`, `CategoryTheory.Equivalence.instIsDenseSubsiteInducedTopologyInverseFunctor`, `instIsDenseSubsiteInducedTopologyOfIsCoverDense`, `CategoryTheory.Equivalence.instIsDenseSubsiteRegularTopologyInverse`, `AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor`, `CategoryTheory.regularTopology.instIsDenseSubsite`, `CategoryTheory.instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv`, `CategoryTheory.Equivalence.instIsDenseSubsiteFunctor`, `CategoryTheory.Equivalence.instIsDenseSubsiteCoherentTopologyInverse`, `isDenseSubsite_of_isOneHypercoverDense`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functorPushforward_mem_iff` 📖	mathematical	—	`CategoryTheory.Sieve` `obj` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.functorPushforward`	—	`IsDenseSubsite.functorPushforward_mem_iff`
`isCoverDense_of_generate_singleton_functor_π_mem` 📖	mathematical	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.generate` `CategoryTheory.Presieve.singleton` `obj`	`IsCoverDense`	—	`CategoryTheory.GrothendieckTopology.superset_covering`
`is_cover_of_isCoverDense` 📖	mathematical	—	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.coverByImage`	—	`IsCoverDense.is_cover`
`whiskerLeft_obj_map_bijective_of_isCoverDense` 📖	mathematical	`CategoryTheory.Presheaf.IsSheaf`	`Function.Bijective` `Quiver.Hom` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `category` `obj` `whiskeringLeft` `op` `map`	—	`Equiv.bijective`

CategoryTheory.Functor.IsCoverDense

Definitions

Name	Category	Theorems
`homOver` 📖	CompOp	2 math math: `sheafCoyonedaHom_app`, `homOver_app`
`isoOver` 📖	CompOp	2 math math: `isoOver_hom_app`, `isoOver_inv_app`
`presheafIso` 📖	CompOp	4 math math: `presheafIso_hom_app`, `presheafIso_inv`, `sheafIso_inv_val`, `sheafIso_hom_val`
`restrictHomEquivHom` 📖	CompOp	8 math math: `restrictHomEquivHom_naturality_left_symm_assoc`, `restrictHomEquivHom_naturality_right_symm`, `restrictHomEquivHom_naturality_left`, `restrictHomEquivHom_naturality_left_assoc`, `restrictHomEquivHom_naturality_right_assoc`, `restrictHomEquivHom_naturality_right_symm_assoc`, `restrictHomEquivHom_naturality_right`, `restrictHomEquivHom_naturality_left_symm`
`sheafCoyonedaHom` 📖	CompOp	1 math math: `sheafCoyonedaHom_app`
`sheafHom` 📖	CompOp	3 math math: `sheafHom_eq`, `sheafHom_restrict_eq`, `presheafIso_inv`
`sheafIso` 📖	CompOp	2 math math: `sheafIso_inv_val`, `sheafIso_hom_val`
`sheafYonedaHom` 📖	CompOp	2 math math: `presheafIso_hom_app`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatiblePreserving` 📖	mathematical	—	`CategoryTheory.CompatiblePreserving`	—	`ext` `CategoryTheory.Functor.IsLocallyFull.ext` `CategoryTheory.Functor.IsLocallyFaithful.ext` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc`
`ext` 📖	—	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `Opposite.op` `CategoryTheory.Functor.obj` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—	`CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `CategoryTheory.isSheaf_iff_isSheaf_of_type` `CategoryTheory.Sheaf.cond` `CategoryTheory.Functor.is_cover_of_isCoverDense` `CategoryTheory.FunctorToTypes.map_comp_apply`
`faithful_sheafPushforwardContinuous` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Functor.sheafPushforwardContinuous`	—	`CategoryTheory.Sheaf.hom_ext` `sheafHom_eq`
`full_sheafPushforwardContinuous` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Functor.sheafPushforwardContinuous`	—	`CategoryTheory.Sheaf.Hom.ext` `sheafHom_restrict_eq`
`functorPullback_pushforward_covering` 📖	mathematical	—	`CategoryTheory.Sieve` `CategoryTheory.Functor.obj` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.functorPushforward` `CategoryTheory.Sieve.functorPullback`	—	`CategoryTheory.GrothendieckTopology.transitive` `CategoryTheory.Functor.is_cover_of_isCoverDense` `CategoryTheory.Sieve.pullback_comp` `CategoryTheory.GrothendieckTopology.pullback_stable` `CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.Category.assoc` `CategoryTheory.Sieve.downward_closed` `CategoryTheory.Functor.functorPushforward_imageSieve_mem`
`homOver_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op` `CategoryTheory.Sheaf.val` `CategoryTheory.sheafOver` `homOver` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	—
`isContinuous` 📖	mathematical	`CategoryTheory.CoverPreserving`	`CategoryTheory.Functor.IsContinuous`	—	`CategoryTheory.Functor.isContinuous_of_coverPreserving` `compatiblePreserving`
`is_cover` 📖	mathematical	—	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.coverByImage`	—	—
`isoOver_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.coyoneda` `Opposite.op` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val` `CategoryTheory.Iso.hom` `CategoryTheory.sheafOver` `isoOver` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	—
`isoOver_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.coyoneda` `Opposite.op` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val` `CategoryTheory.Iso.inv` `CategoryTheory.sheafOver` `isoOver` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	—
`iso_of_restrict_iso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf`	—	`CategoryTheory.Sheaf.hom_ext` `sheafHom_eq` `CategoryTheory.Iso.isIso_hom`
`presheafIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `presheafIso` `CategoryTheory.Functor.preimage` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.yoneda` `CategoryTheory.Yoneda.yoneda_full` `CategoryTheory.Functor.comp` `sheafYonedaHom` `CategoryTheory.Functor.op`	—	—
`presheafIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `presheafIso` `CategoryTheory.inv` `sheafHom` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op`	—	—
`restrictHomEquivHom_naturality_left` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val` `EquivLike.toFunLike` `Equiv.instEquivLike` `restrictHomEquivHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.whiskerLeft`	—	`Equiv.injective` `Equiv.symm_apply_apply` `restrictHomEquivHom_naturality_left_symm`
`restrictHomEquivHom_naturality_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `restrictHomEquivHom` `CategoryTheory.Functor.whiskerLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `restrictHomEquivHom_naturality_left`
`restrictHomEquivHom_naturality_left_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `restrictHomEquivHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.whiskerLeft`	—	—
`restrictHomEquivHom_naturality_left_symm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `restrictHomEquivHom` `CategoryTheory.Functor.whiskerLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `restrictHomEquivHom_naturality_left_symm`
`restrictHomEquivHom_naturality_right` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val` `EquivLike.toFunLike` `Equiv.instEquivLike` `restrictHomEquivHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Sheaf.Hom.val`	—	`Equiv.injective` `Equiv.symm_apply_apply` `restrictHomEquivHom_naturality_right_symm`
`restrictHomEquivHom_naturality_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `restrictHomEquivHom` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Sheaf.Hom.val`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `restrictHomEquivHom_naturality_right`
`restrictHomEquivHom_naturality_right_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `restrictHomEquivHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.whiskerLeft`	—	—
`restrictHomEquivHom_naturality_right_symm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `restrictHomEquivHom` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.whiskerLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `restrictHomEquivHom_naturality_right_symm`
`sheafCoyonedaHom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.coyoneda` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Sheaf.val` `sheafCoyonedaHom` `Types.presheafHom` `Opposite.op` `Opposite.unop` `CategoryTheory.sheafOver` `homOver`	—	—
`sheafHom_eq` 📖	mathematical	—	`sheafHom` `CategoryTheory.Functor.whiskerLeft` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.map_injective` `CategoryTheory.Yoneda.yoneda_faithful` `CategoryTheory.types_ext` `CategoryTheory.Yoneda.yoneda_full` `CategoryTheory.Functor.map_preimage` `sheaf_eq_amalgamation` `CategoryTheory.Functor.is_cover_of_isCoverDense` `Types.pushforwardFamily_compatible` `CategoryTheory.Presieve.CoverByImageStructure.fac` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality`
`sheafHom_restrict_eq` 📖	mathematical	—	`CategoryTheory.Functor.whiskerLeft` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val` `sheafHom`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.map_injective` `CategoryTheory.Yoneda.yoneda_faithful` `CategoryTheory.types_ext` `CategoryTheory.Yoneda.yoneda_full` `CategoryTheory.Functor.map_preimage` `sheaf_eq_amalgamation` `CategoryTheory.Functor.is_cover_of_isCoverDense` `Types.pushforwardFamily_compatible` `CategoryTheory.Presieve.CoverByImageStructure.fac` `CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.Category.assoc` `CategoryTheory.Presheaf.isSheaf_comp_of_isSheaf` `CategoryTheory.coyoneda_preservesLimits` `CategoryTheory.Sheaf.cond` `Types.naturality_apply` `CategoryTheory.Category.id_comp`
`sheafIso_hom_val` 📖	mathematical	—	`CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Iso.hom` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `sheafIso` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `presheafIso`	—	—
`sheafIso_inv_val` 📖	mathematical	—	`CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Iso.inv` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `sheafIso` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `presheafIso`	—	—
`sheaf_eq_amalgamation` 📖	mathematical	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Presieve.FamilyOfElements.Compatible` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op` `CategoryTheory.Sieve.arrows` `CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation`	`CategoryTheory.Presieve.IsSheafFor.amalgamate` `CategoryTheory.Sheaf.cond`	—	`CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `CategoryTheory.Sheaf.cond` `CategoryTheory.Presieve.IsSheafFor.isAmalgamation`

CategoryTheory.Functor.IsCoverDense.Types

Definitions

Name	Category	Theorems
`appHom` 📖	CompOp	7 math math: `appHom_valid_glue`, `appHom_restrict`, `appIso_inv`, `presheafIso_inv_app`, `presheafIso_hom_app`, `presheafHom_app`, `appIso_hom`
`appIso` 📖	CompOp	2 math math: `appIso_inv`, `appIso_hom`
`presheafHom` 📖	CompOp	2 math math: `CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom_app`, `presheafHom_app`
`presheafIso` 📖	CompOp	4 math math: `sheafIso_hom_val`, `presheafIso_inv_app`, `sheafIso_inv_val`, `presheafIso_hom_app`
`pushforwardFamily` 📖	CompOp	3 math math: `pushforwardFamily_def`, `pushforwardFamily_compatible`, `pushforwardFamily_apply`
`sheafIso` 📖	CompOp	2 math math: `sheafIso_hom_val`, `sheafIso_inv_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`appHom_restrict` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `Opposite.op` `CategoryTheory.Functor.obj` `appHom` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op`	—	`CategoryTheory.isSheaf_iff_isSheaf_of_type` `CategoryTheory.Sheaf.cond` `CategoryTheory.Functor.is_cover_of_isCoverDense` `pushforwardFamily_compatible` `CategoryTheory.Presieve.in_coverByImage` `CategoryTheory.Presieve.IsSheafFor.valid_glue` `pushforwardFamily_apply`
`appHom_valid_glue` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Sheaf.val` `appHom` `CategoryTheory.Functor.map` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.types_ext` `appHom_restrict`
`appIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `appIso` `appHom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op`	—	—
`appIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `appIso` `appHom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op`	—	—
`naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `Opposite.op` `CategoryTheory.Sheaf.val` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`CategoryTheory.types_ext` `naturality_apply`
`naturality_apply` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `Opposite.op` `CategoryTheory.Functor.obj` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op`	—	`CategoryTheory.NatTrans.naturality` `CategoryTheory.Functor.IsLocallyFull.ext`
`naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `Opposite.op` `CategoryTheory.Sheaf.val` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality`
`presheafHom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `presheafHom` `appHom` `Opposite.unop`	—	—
`presheafIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `presheafIso` `appHom` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `Opposite.unop`	—	—
`presheafIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `presheafIso` `appHom` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `Opposite.unop`	—	—
`pushforwardFamily_apply` 📖	mathematical	—	`pushforwardFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Presieve.in_coverByImage` `CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Sheaf.val` `Opposite.op` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Presieve.in_coverByImage` `naturality_apply`
`pushforwardFamily_compatible` 📖	mathematical	—	`CategoryTheory.Presieve.FamilyOfElements.Compatible` `CategoryTheory.Sheaf.val` `CategoryTheory.types` `CategoryTheory.Presieve.coverByImage` `pushforwardFamily`	—	`CategoryTheory.Functor.IsCoverDense.ext` `naturality_apply` `CategoryTheory.Category.assoc`
`pushforwardFamily_def` 📖	mathematical	—	`pushforwardFamily` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.op` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Presieve.CoverByImageStructure.obj` `Nonempty.some` `CategoryTheory.Presieve.CoverByImageStructure` `CategoryTheory.Presieve.CoverByImageStructure.lift` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Presieve.CoverByImageStructure.map`	—	—
`sheafIso_hom_val` 📖	mathematical	—	`CategoryTheory.Sheaf.Hom.val` `CategoryTheory.types` `CategoryTheory.Iso.hom` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `sheafIso` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `presheafIso`	—	—
`sheafIso_inv_val` 📖	mathematical	—	`CategoryTheory.Sheaf.Hom.val` `CategoryTheory.types` `CategoryTheory.Iso.inv` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `sheafIso` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf.val` `presheafIso`	—	—

CategoryTheory.Functor.IsDenseSubsite

Definitions

Name	Category	Theorems
`mapPreimage` 📖	CompOp	11 math math: `mapPreimage_map_of_fac`, `mapPreimage_id`, `mapPreimage_map`, `mapPreimage_comp_assoc`, `CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition`, `mapPreimage_comp_map`, `mapPreimage_comp_map_assoc`, `mapPreimage_comp`, `mapPreimage_of_eq`, `CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map`, `CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coverPreserving` 📖	mathematical	—	`CategoryTheory.CoverPreserving`	—	`functorPushforward_mem_iff`
`equalizer_mem` 📖	mathematical	`CategoryTheory.Functor.map`	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.equalizer`	—	`functorPushforward_mem_iff` `CategoryTheory.Functor.functorPushforward_equalizer_mem` `isLocallyFaithful`
`faithful_sheafPushforwardContinuous` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Functor.sheafPushforwardContinuous` `instIsContinuous`	—	`instIsContinuous` `CategoryTheory.Functor.IsCoverDense.faithful_sheafPushforwardContinuous` `isCoverDense` `isLocallyFull`
`full_sheafPushforwardContinuous` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Functor.sheafPushforwardContinuous` `instIsContinuous`	—	`instIsContinuous` `CategoryTheory.Functor.IsCoverDense.full_sheafPushforwardContinuous` `isCoverDense` `isLocallyFull`
`functorPushforward_mem_iff` 📖	mathematical	—	`CategoryTheory.Sieve` `CategoryTheory.Functor.obj` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.functorPushforward`	—	—
`imageSieve_mem` 📖	mathematical	—	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Functor.imageSieve`	—	`functorPushforward_mem_iff` `CategoryTheory.Functor.functorPushforward_imageSieve_mem` `isLocallyFull`
`instIsCocontinuous` 📖	mathematical	—	`CategoryTheory.Functor.IsCocontinuous`	—	`functorPushforward_mem_iff` `CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering` `isCoverDense` `isLocallyFull`
`instIsContinuous` 📖	mathematical	—	`CategoryTheory.Functor.IsContinuous`	—	`CategoryTheory.Functor.IsCoverDense.isContinuous` `isCoverDense` `isLocallyFull` `isLocallyFaithful` `coverPreserving`
`isCoverDense` 📖	mathematical	—	`CategoryTheory.Functor.IsCoverDense`	—	`isCoverDense'`
`isCoverDense'` 📖	mathematical	—	`CategoryTheory.Functor.IsCoverDense`	—	—
`isLocallyFaithful` 📖	mathematical	—	`CategoryTheory.Functor.IsLocallyFaithful`	—	`isLocallyFaithful'`
`isLocallyFaithful'` 📖	mathematical	—	`CategoryTheory.Functor.IsLocallyFaithful`	—	—
`isLocallyFull` 📖	mathematical	—	`CategoryTheory.Functor.IsLocallyFull`	—	`isLocallyFull'`
`isLocallyFull'` 📖	mathematical	—	`CategoryTheory.Functor.IsLocallyFull`	—	—
`mapPreimage_comp` 📖	mathematical	—	`mapPreimage` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op`	—	`CategoryTheory.Presheaf.IsSheaf.hom_ext` `CategoryTheory.Sheaf.cond` `imageSieve_mem` `CategoryTheory.GrothendieckTopology.pullback_stable` `CategoryTheory.Category.assoc` `mapPreimage_map_of_fac` `CategoryTheory.Functor.map_comp`
`mapPreimage_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `mapPreimage`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mapPreimage_comp`
`mapPreimage_comp_map` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `mapPreimage` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`mapPreimage_comp` `mapPreimage_map`
`mapPreimage_comp_map_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `mapPreimage` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mapPreimage_comp_map`
`mapPreimage_id` 📖	mathematical	—	`mapPreimage` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op`	—	`CategoryTheory.Functor.map_id` `mapPreimage_map` `CategoryTheory.op_id`
`mapPreimage_map` 📖	mathematical	—	`mapPreimage` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`mapPreimage_of_eq`
`mapPreimage_map_of_fac` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `mapPreimage` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`CategoryTheory.Presheaf.IsSheaf.hom_ext` `CategoryTheory.Sheaf.cond` `CategoryTheory.GrothendieckTopology.pullback_stable` `imageSieve_mem` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.op_comp` `mapPreimage.eq_1` `CategoryTheory.Presheaf.IsSheaf.amalgamate_map` `map_eq_of_eq` `CategoryTheory.Functor.map_comp_assoc`
`mapPreimage_of_eq` 📖	mathematical	`CategoryTheory.Functor.map`	`mapPreimage` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `mapPreimage_map_of_fac` `CategoryTheory.Category.id_comp`
`map_eq_of_eq` 📖	mathematical	`CategoryTheory.Functor.map`	`Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Presheaf.IsSheaf.hom_ext` `CategoryTheory.Sheaf.cond` `equalizer_mem`

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
`CoverByImageStructure` 📖	CompData	1 math math: `CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def`
`coverByImage` 📖	CompOp	2 math math: `CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible`, `in_coverByImage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`in_coverByImage` 📖	mathematical	—	`coverByImage` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Category.id_comp`

CategoryTheory.Presieve.CoverByImageStructure

Definitions

Name	Category	Theorems
`map` 📖	CompOp	3 math math: `fac`, `CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def`, `fac_assoc`
`obj` 📖	CompOp	3 math math: `fac`, `CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def`, `fac_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `obj` `lift` `map`	—	—
`fac_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `obj` `lift` `map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`

CategoryTheory.Sieve

Definitions

Name	Category	Theorems
`coverByImage` 📖	CompOp	2 math math: `CategoryTheory.Functor.is_cover_of_isCoverDense`, `CategoryTheory.Functor.IsCoverDense.is_cover`

---

← Back to Index