Documentation Verification Report

Equivalence

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

Statistics

Metric	Count
Definitions `sheafCongr`, `counitIso`, `functor`, `inverse`, `unitIso`, `transportAndSheafify`, `transportIsoSheafToPresheaf`, `transportSheafificationAdjunction`, `smallSheafificationAdjunction`, `smallSheafify`	10
Theorems `eq_inducedTopology_of_isDenseSubsite`, `hasSheafCompose`, `hasSheafify`, `instIsCoverDenseOfIsEquivalence`, `instIsDenseSubsiteFunctor`, `instIsDenseSubsiteInducedTopologyInverseFunctor`, `instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify`, `isDenseSubsite_functor_of_isCocontinuous`, `isDenseSubsite_inverse_of_isCocontinuous`, `counitIso_hom_app_hom_app`, `counitIso_inv_app_hom_app`, `functor_map_hom_app`, `functor_obj_obj_map`, `functor_obj_obj_obj`, `inverse_map_hom_app`, `inverse_obj_obj_map`, `inverse_obj_obj_obj`, `unitIso_hom_app_hom_app`, `unitIso_inv_app_hom_app`, `sheafCongr_counitIso`, `sheafCongr_functor`, `sheafCongr_inverse`, `sheafCongr_unitIso`, `transport`, `ofEssentiallySmall`, `transport`, `W_inverseImage_whiskeringLeft`, `W_whiskerLeft_iff`, `instPreservesSheafification_1`, `hasColimitsEssentiallySmallSite`, `hasLimitsEssentiallySmallSite`, `hasSheafComposeEssentiallySmallSite`, `hasSheafifyEssentiallySmallSite`	33
Total	43

CategoryTheory

Definitions

Name	Category	Theorems
`smallSheafificationAdjunction` 📖	CompOp	—
`smallSheafify` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimitsEssentiallySmallSite` 📖	mathematical	—	`Limits.HasColimitsOfSize` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf`	—	`Functor.locallyCoverDense_of_isCoverDense` `Functor.IsLocallyFull.of_full` `Equivalence.full_inverse` `Equivalence.instIsCoverDenseOfIsEquivalence` `Equivalence.isEquivalence_inverse` `Functor.IsLocallyFaithful.of_faithful` `Equivalence.faithful_inverse` `Adjunction.has_colimits_of_equivalence` `Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense` `Equivalence.isEquivalence_functor`
`hasLimitsEssentiallySmallSite` 📖	mathematical	—	`Limits.HasLimitsOfSize` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf`	—	`Functor.locallyCoverDense_of_isCoverDense` `Functor.IsLocallyFull.of_full` `Equivalence.full_inverse` `Equivalence.instIsCoverDenseOfIsEquivalence` `Equivalence.isEquivalence_inverse` `Functor.IsLocallyFaithful.of_faithful` `Equivalence.faithful_inverse` `Adjunction.has_limits_of_equivalence` `Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense` `Equivalence.isEquivalence_functor`
`hasSheafComposeEssentiallySmallSite` 📖	mathematical	—	`GrothendieckTopology.HasSheafCompose`	—	`Functor.locallyCoverDense_of_isCoverDense` `Functor.IsLocallyFull.of_full` `Equivalence.full_inverse` `Equivalence.instIsCoverDenseOfIsEquivalence` `Equivalence.isEquivalence_inverse` `Functor.IsLocallyFaithful.of_faithful` `Equivalence.faithful_inverse` `Equivalence.hasSheafCompose` `Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense`
`hasSheafifyEssentiallySmallSite` 📖	mathematical	—	`HasSheafify`	—	`Functor.locallyCoverDense_of_isCoverDense` `Functor.IsLocallyFull.of_full` `Equivalence.full_inverse` `Equivalence.instIsCoverDenseOfIsEquivalence` `Equivalence.isEquivalence_inverse` `Functor.IsLocallyFaithful.of_faithful` `Equivalence.faithful_inverse` `Equivalence.hasSheafify` `Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense`

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
`sheafCongr` 📖	CompOp	4 math math: `sheafCongr_functor`, `sheafCongr_counitIso`, `sheafCongr_inverse`, `sheafCongr_unitIso`
`transportAndSheafify` 📖	CompOp	1 math math: `instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify`
`transportIsoSheafToPresheaf` 📖	CompOp	—
`transportSheafificationAdjunction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_inducedTopology_of_isDenseSubsite` 📖	mathematical	—	`CategoryTheory.Functor.inducedTopology` `inverse` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `full_inverse` `instIsCoverDenseOfIsEquivalence` `isEquivalence_inverse` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `faithful_inverse`	—	`CategoryTheory.GrothendieckTopology.ext` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `full_inverse` `instIsCoverDenseOfIsEquivalence` `isEquivalence_inverse` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `faithful_inverse` `Set.ext` `CategoryTheory.Functor.functorPushforward_mem_iff`
`hasSheafCompose` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.HasSheafCompose`	—	`CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf` `CategoryTheory.Functor.op_comp_isSheaf` `CategoryTheory.Functor.IsDenseSubsite.instIsContinuous` `instIsDenseSubsiteFunctor` `CategoryTheory.Presheaf.isSheaf_of_iso_iff`
`hasSheafify` 📖	mathematical	—	`CategoryTheory.HasSheafify`	—	`CategoryTheory.HasSheafify.mk'` `instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify`
`instIsCoverDenseOfIsEquivalence` 📖	mathematical	—	`CategoryTheory.Functor.IsCoverDense`	—	`CategoryTheory.Sieve.ext` `CategoryTheory.Presieve.in_coverByImage` `CategoryTheory.Sieve.downward_closed` `unitIso_hom_inv_id_app_assoc` `CategoryTheory.GrothendieckTopology.top_mem`
`instIsDenseSubsiteFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsDenseSubsite` `functor`	—	`CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `full_inverse` `instIsCoverDenseOfIsEquivalence` `isEquivalence_inverse` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `faithful_inverse` `eq_inducedTopology_of_isDenseSubsite` `instIsDenseSubsiteInducedTopologyInverseFunctor`
`instIsDenseSubsiteInducedTopologyInverseFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsDenseSubsite` `CategoryTheory.Functor.inducedTopology` `inverse` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `full_inverse` `instIsCoverDenseOfIsEquivalence` `isEquivalence_inverse` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `faithful_inverse` `functor`	—	`CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `full_inverse` `instIsCoverDenseOfIsEquivalence` `isEquivalence_inverse` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `faithful_inverse` `full_functor` `isEquivalence_functor` `faithful_functor` `CategoryTheory.GrothendieckTopology.ext` `Set.ext` `CategoryTheory.GrothendieckTopology.pullback_mem_iff_of_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Sieve.ext` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `functor_unit_comp` `CategoryTheory.Category.comp_id` `inv_fun_map` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense`
`instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Presheaf.IsSheaf` `transportAndSheafify`	—	`CategoryTheory.Limits.comp_preservesLimitsOfShape` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `isEquivalence_functor` `CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf` `isEquivalence_inverse`
`isDenseSubsite_functor_of_isCocontinuous` 📖	mathematical	—	`CategoryTheory.Functor.IsDenseSubsite` `functor`	—	`instIsCoverDenseOfIsEquivalence` `isEquivalence_functor` `CategoryTheory.Functor.IsLocallyFull.of_full` `full_functor` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `faithful_functor` `CategoryTheory.GrothendieckTopology.superset_covering` `GaloisCoinsertion.u_l_eq` `le_refl` `CategoryTheory.Functor.cover_lift` `CategoryTheory.Functor.map_comp` `fun_inv_map` `CategoryTheory.Category.assoc` `counitInv_functor_comp` `CategoryTheory.Category.comp_id` `counitIso_inv_hom_id_app_assoc` `CategoryTheory.GrothendieckTopology.pullback_stable`
`isDenseSubsite_inverse_of_isCocontinuous` 📖	mathematical	—	`CategoryTheory.Functor.IsDenseSubsite` `inverse`	—	`isDenseSubsite_functor_of_isCocontinuous`
`sheafCongr_counitIso` 📖	mathematical	—	`counitIso` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `sheafCongr` `sheafCongr.counitIso`	—	—
`sheafCongr_functor` 📖	mathematical	—	`functor` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `sheafCongr` `sheafCongr.functor`	—	—
`sheafCongr_inverse` 📖	mathematical	—	`inverse` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `sheafCongr` `sheafCongr.inverse`	—	—
`sheafCongr_unitIso` 📖	mathematical	—	`unitIso` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `sheafCongr` `sheafCongr.unitIso`	—	—

CategoryTheory.Equivalence.sheafCongr

Definitions

Name	Category	Theorems
`counitIso` 📖	CompOp	3 math math: `CategoryTheory.Equivalence.sheafCongr_counitIso`, `counitIso_inv_app_hom_app`, `counitIso_hom_app_hom_app`
`functor` 📖	CompOp	16 math math: `CategoryTheory.Equivalence.sheafCongr_functor`, `CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app`, `unitIso_inv_app_hom_app`, `functor_obj_obj_map`, `functor_obj_obj_obj`, `CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app`, `unitIso_hom_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app`, `counitIso_inv_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app`, `functor_map_hom_app`, `CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app`, `counitIso_hom_app_hom_app`
`inverse` 📖	CompOp	16 math math: `inverse_obj_obj_map`, `CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app`, `unitIso_inv_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app`, `unitIso_hom_app_hom_app`, `inverse_obj_obj_obj`, `CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app`, `counitIso_inv_app_hom_app`, `CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app`, `CategoryTheory.Equivalence.sheafCongr_inverse`, `CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app`, `inverse_map_hom_app`, `counitIso_hom_app_hom_app`
`unitIso` 📖	CompOp	3 math math: `unitIso_inv_app_hom_app`, `unitIso_hom_app_hom_app`, `CategoryTheory.Equivalence.sheafCongr_unitIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counitIso_hom_app_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `inverse` `functor` `CategoryTheory.Functor.id` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.hom` `counitIso` `CategoryTheory.Functor.map` `Opposite.op` `CategoryTheory.Equivalence.functor` `CategoryTheory.Equivalence.inverse` `Opposite.unop` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.Equivalence.counitIso`	—	—
`counitIso_inv_app_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `inverse` `functor` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `counitIso` `CategoryTheory.Functor.map` `Opposite.op` `CategoryTheory.Equivalence.functor` `CategoryTheory.Equivalence.inverse` `Opposite.unop` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.Equivalence.counitIso`	—	—
`functor_map_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.comp` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.op` `CategoryTheory.Equivalence.inverse` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `functor` `Opposite.op` `Opposite.unop`	—	—
`functor_obj_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `functor` `Opposite.op` `CategoryTheory.Equivalence.inverse` `Opposite.unop` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom.unop`	—	—
`functor_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `functor` `Opposite.op` `CategoryTheory.Equivalence.inverse` `Opposite.unop`	—	—
`inverse_map_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.comp` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.op` `CategoryTheory.Equivalence.functor` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `inverse` `Opposite.op` `Opposite.unop`	—	—
`inverse_obj_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `inverse` `Opposite.op` `CategoryTheory.Equivalence.functor` `Opposite.unop` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom.unop`	—	—
`inverse_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `inverse` `Opposite.op` `CategoryTheory.Equivalence.functor` `Opposite.unop`	—	—
`unitIso_hom_app_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `functor` `inverse` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.hom` `unitIso` `CategoryTheory.Functor.map` `Opposite.op` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Equivalence.functor` `Opposite.unop` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.Equivalence.unitIso`	—	—
`unitIso_inv_app_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `functor` `inverse` `CategoryTheory.Functor.id` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `unitIso` `CategoryTheory.Functor.map` `Opposite.op` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Equivalence.functor` `Opposite.unop` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.Equivalence.unitIso`	—	—

CategoryTheory.GrothendieckTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`W_inverseImage_whiskeringLeft` 📖	mathematical	—	`CategoryTheory.MorphismProperty.inverseImage` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `W` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.op`	—	`CategoryTheory.MorphismProperty.ext` `W_eq_isLocal_range_sheafToPresheaf_obj` `CategoryTheory.ObjectProperty.isoClosure_isLocal` `Function.Bijective.of_comp_iff` `CategoryTheory.Functor.whiskerLeft_obj_map_bijective_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `CategoryTheory.ObjectProperty.FullSubcategory.property` `Function.Bijective.of_comp_iff'` `CategoryTheory.MorphismProperty.inverseImage_iff`
`W_whiskerLeft_iff` 📖	mathematical	—	`W` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `CategoryTheory.Functor.whiskerLeft`	—	`W_inverseImage_whiskeringLeft`
`instPreservesSheafification_1` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.StructuredArrow` `Opposite` `CategoryTheory.SmallModel` `CategoryTheory.Category.opposite` `CategoryTheory.smallCategorySmallModel` `CategoryTheory.Functor.op` `CategoryTheory.Equivalence.inverse` `CategoryTheory.equivSmallModel` `CategoryTheory.instCategoryStructuredArrow`	`PreservesSheafification`	—	`CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `CategoryTheory.Equivalence.full_inverse` `CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence` `CategoryTheory.Equivalence.isEquivalence_inverse` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `CategoryTheory.Equivalence.faithful_inverse` `PreservesSheafification.transport` `CategoryTheory.Functor.IsDenseSubsite.instIsContinuous` `CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense` `CategoryTheory.Functor.IsEquivalence.essSurj` `CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous`

CategoryTheory.GrothendieckTopology.PreservesSheafification

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`transport` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.PreservesSheafification`	—	`CategoryTheory.GrothendieckTopology.W_of_preservesSheafification` `CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff` `CategoryTheory.MorphismProperty.of_postcomp` `CategoryTheory.MorphismProperty.instHasOfPostcompPropertyIsomorphismsOfRespectsIso` `CategoryTheory.ObjectProperty.instRespectsIsoIsLocal` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.MorphismProperty.of_precomp` `CategoryTheory.MorphismProperty.instHasOfPrecompPropertyIsomorphismsOfRespectsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Functor.whiskerRight_left`

CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofEssentiallySmall` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.StructuredArrow` `Opposite` `CategoryTheory.SmallModel` `CategoryTheory.Category.opposite` `CategoryTheory.smallCategorySmallModel` `CategoryTheory.Functor.op` `CategoryTheory.Equivalence.inverse` `CategoryTheory.equivSmallModel` `CategoryTheory.instCategoryStructuredArrow`	`CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective`	—	`CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `CategoryTheory.Equivalence.full_inverse` `CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence` `CategoryTheory.Equivalence.isEquivalence_inverse` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `CategoryTheory.Equivalence.faithful_inverse` `transport` `CategoryTheory.Functor.IsDenseSubsite.instIsContinuous` `CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense` `CategoryTheory.Functor.IsEquivalence.essSurj` `CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous` `CategoryTheory.Functor.inducedTopology_isCocontinuous` `CategoryTheory.Functor.IsDenseSubsite.coverPreserving`
`transport` 📖	mathematical	`CategoryTheory.CoverPreserving`	`CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective`	—	`CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff` `CategoryTheory.Presheaf.isLocallyInjective_whisker_iff` `CategoryTheory.Presheaf.isLocallySurjective_whisker_iff` `CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective`

---

← Back to Index