Documentation Verification Report

SheafComparison

📁 Source: Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean

Statistics

Metric	Count
Definitions `coherentExtensiveEquivalence`, `equivalence`, `equivalence'`, `equivalence`	4
Theorems `coherentExtensiveEquivalence_counitIso_hom_app_hom_app`, `coherentExtensiveEquivalence_counitIso_inv_app_hom_app`, `coherentExtensiveEquivalence_functor_map_hom`, `coherentExtensiveEquivalence_functor_obj_obj`, `coherentExtensiveEquivalence_inverse_map_hom`, `coherentExtensiveEquivalence_inverse_obj_obj`, `coherentExtensiveEquivalence_unitIso_hom_app_hom_app`, `coherentExtensiveEquivalence_unitIso_inv_app_hom_app`, `instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits`, `instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts`, `instPreservesFiniteProductsOppositeObjFunctorIsSheafCoherentTopology`, `isSheaf_coherent_iff_regular_and_extensive`, `isSheaf_coherent_of_hasPullbacks_comp`, `isSheaf_coherent_of_hasPullbacks_of_comp`, `isSheaf_coherent_of_projective_comp`, `isSheaf_coherent_of_projective_of_comp`, `isSheaf_iff_extensiveSheaf_of_projective`, `isSheaf_iff_preservesFiniteProducts_and_equalizerCondition`, `isSheaf_iff_preservesFiniteProducts_of_projective`, `coverPreserving`, `eq_induced`, `exists_effectiveEpiFamily_iff_mem_induced`, `instIsCoverDense`, `instIsDenseSubsite`, `coverPreserving`, `eq_induced`, `exists_effectiveEpi_iff_mem_induced`, `instIsCoverDense`, `instIsDenseSubsite`	29
Total	33

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
`coherentExtensiveEquivalence` 📖	CompOp	8 math math: `coherentExtensiveEquivalence_inverse_map_hom`, `coherentExtensiveEquivalence_unitIso_hom_app_hom_app`, `coherentExtensiveEquivalence_functor_obj_obj`, `coherentExtensiveEquivalence_inverse_obj_obj`, `coherentExtensiveEquivalence_functor_map_hom`, `coherentExtensiveEquivalence_unitIso_inv_app_hom_app`, `coherentExtensiveEquivalence_counitIso_inv_app_hom_app`, `coherentExtensiveEquivalence_counitIso_hom_app_hom_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coherentExtensiveEquivalence_counitIso_hom_app_hom_app` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.extensiveTopology` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `CategoryTheory.coherentTopology` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.sheafToPresheaf` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.hom` `CategoryTheory.Equivalence.counitIso` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `coherentExtensiveEquivalence` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular`
`coherentExtensiveEquivalence_counitIso_inv_app_hom_app` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.extensiveTopology` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `CategoryTheory.coherentTopology` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.sheafToPresheaf` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `CategoryTheory.Equivalence.counitIso` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `coherentExtensiveEquivalence` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular`
`coherentExtensiveEquivalence_functor_map_hom` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.extensiveTopology` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Functor.map` `CategoryTheory.Equivalence.functor` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `coherentExtensiveEquivalence`	—	`CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular`
`coherentExtensiveEquivalence_functor_obj_obj` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.extensiveTopology` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Equivalence.functor` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `coherentExtensiveEquivalence`	—	`CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular`
`coherentExtensiveEquivalence_inverse_map_hom` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.extensiveTopology` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Functor.map` `CategoryTheory.Equivalence.inverse` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `coherentExtensiveEquivalence`	—	`CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular`
`coherentExtensiveEquivalence_inverse_obj_obj` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.extensiveTopology` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Equivalence.inverse` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `coherentExtensiveEquivalence`	—	`CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular`
`coherentExtensiveEquivalence_unitIso_hom_app_hom_app` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.id` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.hom` `CategoryTheory.Equivalence.unitIso` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.extensiveTopology` `coherentExtensiveEquivalence` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`
`coherentExtensiveEquivalence_unitIso_inv_app_hom_app` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.id` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.inv` `CategoryTheory.Equivalence.unitIso` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.extensiveTopology` `coherentExtensiveEquivalence` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`
`instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits` 📖	mathematical	`CategoryTheory.Limits.HasPullback`	`CategoryTheory.GrothendieckTopology.HasSheafCompose` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_coherent_of_hasPullbacks_comp`
`instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.GrothendieckTopology.HasSheafCompose` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_coherent_of_projective_comp`
`instPreservesFiniteProductsOppositeObjFunctorIsSheafCoherentTopology` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteProducts` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_iff_preservesFiniteProducts` `isSheaf_coherent_iff_regular_and_extensive` `CategoryTheory.ObjectProperty.FullSubcategory.property`
`isSheaf_coherent_iff_regular_and_extensive` 📖	mathematical	—	`IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.extensiveTopology` `CategoryTheory.regularTopology`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.extensive_regular_generate_coherent` `isSheaf_sup`
`isSheaf_coherent_of_hasPullbacks_comp` 📖	mathematical	`CategoryTheory.Limits.HasPullback` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`	`IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` `CategoryTheory.Limits.comp_preservesFiniteProducts` `CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits` `CategoryTheory.regularTopology.equalizerCondition_w` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits`
`isSheaf_coherent_of_hasPullbacks_of_comp` 📖	mathematical	`CategoryTheory.Limits.HasPullback` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite`	`IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts` `Finite.of_fintype` `CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.regularTopology.equalizerCondition_w`
`isSheaf_coherent_of_projective_comp` 📖	mathematical	`CategoryTheory.Projective` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`	`IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_iff_preservesFiniteProducts_of_projective` `CategoryTheory.Limits.comp_preservesFiniteProducts`
`isSheaf_coherent_of_projective_of_comp` 📖	mathematical	`CategoryTheory.Projective` `IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite`	`IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_iff_preservesFiniteProducts_of_projective` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts` `Finite.of_fintype` `CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape` `CategoryTheory.Limits.instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite`
`isSheaf_iff_extensiveSheaf_of_projective` 📖	mathematical	`CategoryTheory.Projective`	`IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.extensiveTopology`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_iff_preservesFiniteProducts_of_projective` `isSheaf_iff_preservesFiniteProducts`
`isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` 📖	mathematical	`CategoryTheory.Limits.HasPullback`	`IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Limits.PreservesFiniteProducts` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.regularTopology.EqualizerCondition`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_coherent_iff_regular_and_extensive` `isSheaf_iff_preservesFiniteProducts` `CategoryTheory.regularTopology.equalizerCondition_iff_isSheaf`
`isSheaf_iff_preservesFiniteProducts_of_projective` 📖	mathematical	`CategoryTheory.Projective`	`IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CategoryTheory.Limits.PreservesFiniteProducts` `Opposite` `CategoryTheory.Category.opposite`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `isSheaf_coherent_iff_regular_and_extensive` `CategoryTheory.regularTopology.isSheaf_of_projective` `isSheaf_iff_preservesFiniteProducts`

CategoryTheory.coherentTopology

Definitions

Name	Category	Theorems
`equivalence` 📖	CompOp	—
`equivalence'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coverPreserving` 📖	mathematical	—	`CategoryTheory.CoverPreserving` `CategoryTheory.coherentTopology` `CategoryTheory.Functor.reflects_precoherent`	—	`CategoryTheory.Functor.IsDenseSubsite.coverPreserving` `CategoryTheory.Functor.reflects_precoherent` `instIsDenseSubsite`
`eq_induced` 📖	mathematical	—	`CategoryTheory.coherentTopology` `CategoryTheory.Functor.reflects_precoherent` `CategoryTheory.Functor.inducedTopology` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful`	—	`CategoryTheory.GrothendieckTopology.ext` `CategoryTheory.Functor.reflects_precoherent` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `Set.ext` `exists_effectiveEpiFamily_iff_mem_induced` `mem_sieves_iff_hasEffectiveEpiFamily`
`exists_effectiveEpiFamily_iff_mem_induced` 📖	mathematical	—	`Finite` `CategoryTheory.EffectiveEpiFamily` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Functor.inducedTopology` `CategoryTheory.coherentTopology` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful`	—	`CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `mem_sieves_iff_hasEffectiveEpiFamily` `CategoryTheory.Functor.map_finite_effectiveEpiFamily` `CategoryTheory.Sieve.image_mem_functorPushforward` `CategoryTheory.Functor.EffectivelyEnough.presentation` `CategoryTheory.precoherentEffectiveEpiFamilyCompEffectiveEpis` `CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver` `CategoryTheory.Functor.finite_effectiveEpiFamily_of_map` `CategoryTheory.Functor.map_preimage` `CategoryTheory.Functor.map_injective` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Sieve.downward_closed`
`instIsCoverDense` 📖	mathematical	—	`CategoryTheory.Functor.IsCoverDense` `CategoryTheory.coherentTopology`	—	`CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem` `CategoryTheory.Functor.EffectivelyEnough.presentation` `Finite.of_fintype` `CategoryTheory.effectiveEpi_iff_effectiveEpiFamily` `CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver`
`instIsDenseSubsite` 📖	mathematical	—	`CategoryTheory.Functor.IsDenseSubsite` `CategoryTheory.coherentTopology` `CategoryTheory.Functor.reflects_precoherent`	—	`CategoryTheory.Functor.reflects_precoherent` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `eq_induced`

CategoryTheory.regularTopology

Definitions

Name	Category	Theorems
`equivalence` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coverPreserving` 📖	mathematical	—	`CategoryTheory.CoverPreserving` `CategoryTheory.regularTopology` `CategoryTheory.Functor.reflects_preregular`	—	`CategoryTheory.Functor.IsDenseSubsite.coverPreserving` `CategoryTheory.Functor.reflects_preregular` `instIsDenseSubsite`
`eq_induced` 📖	mathematical	—	`CategoryTheory.regularTopology` `CategoryTheory.Functor.reflects_preregular` `CategoryTheory.Functor.inducedTopology` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful`	—	`CategoryTheory.GrothendieckTopology.ext` `CategoryTheory.Functor.reflects_preregular` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `Set.ext` `exists_effectiveEpi_iff_mem_induced` `mem_sieves_iff_hasEffectiveEpi`
`exists_effectiveEpi_iff_mem_induced` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.EffectiveEpi` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Functor.inducedTopology` `CategoryTheory.regularTopology` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful`	—	`CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `mem_sieves_iff_hasEffectiveEpi` `CategoryTheory.Functor.map_effectiveEpi` `CategoryTheory.Sieve.image_mem_functorPushforward` `CategoryTheory.Functor.EffectivelyEnough.presentation` `CategoryTheory.Functor.effectiveEpi_of_map` `CategoryTheory.Functor.map_preimage` `instEffectiveEpiComp` `CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver` `CategoryTheory.Functor.map_injective` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Sieve.downward_closed`
`instIsCoverDense` 📖	mathematical	—	`CategoryTheory.Functor.IsCoverDense` `CategoryTheory.regularTopology`	—	`CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem` `CategoryTheory.Functor.EffectivelyEnough.presentation` `CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver`
`instIsDenseSubsite` 📖	mathematical	—	`CategoryTheory.Functor.IsDenseSubsite` `CategoryTheory.regularTopology` `CategoryTheory.Functor.reflects_preregular`	—	`CategoryTheory.Functor.reflects_preregular` `instIsCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `eq_induced`

---

← Back to Index