Documentation Verification Report

RegularSheaves

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

Statistics

Metric	Count
Definitions `regular`, `EqualizerCondition`, `MapToEqualizer`, `SingleEqualizerCondition`, `isLimit_forkOfι_equiv`, `mapToEqualizer`	6
Theorems `single_epi`, `bijective_mapToEqualizer_pullback`, `bijective_mapToEqualizer_pullback'`, `mk`, `mk'`, `equalizerConditionMap_iff_nonempty_isLimit`, `equalizerCondition_iff_isIso_lift`, `equalizerCondition_iff_isSheaf`, `equalizerCondition_iff_of_equivalence`, `equalizerCondition_of_natIso`, `equalizerCondition_precomp_of_preservesPullback`, `equalizerCondition_w`, `equalizerCondition_w'`, `isSheafFor_regular_of_projective`, `isSheaf_of_projective`, `isSheaf_yoneda_obj`, `mapToEqualizer_eq_comp`, `parallelPair_pullback_initial`, `subcanonical`	19
Total	25

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
`regular` 📖	CompData	—

CategoryTheory.Presieve.regular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`single_epi` 📖	mathematical	—	`CategoryTheory.Presieve.ofArrows` `CategoryTheory.EffectiveEpi`	—	—

CategoryTheory.regularTopology

Definitions

Name	Category	Theorems
`EqualizerCondition` 📖	MathDef	10 math math: `EqualizerCondition.mk'`, `EqualizerCondition.mk`, `equalizerCondition_yonedaPresheaf`, `CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition`, `equalizerCondition_iff_isSheaf`, `equalizerCondition_iff_isIso_lift`, `LightCondensed.equalizerCondition`, `equalizerCondition_iff_of_equivalence`, `Condensed.equalizerCondition_profinite`, `Condensed.equalizerCondition`
`MapToEqualizer` 📖	CompOp	—
`SingleEqualizerCondition` 📖	MathDef	1 math math: `equalizerConditionMap_iff_nonempty_isLimit`
`isLimit_forkOfι_equiv` 📖	CompOp	—
`mapToEqualizer` 📖	CompOp	3 math math: `EqualizerCondition.bijective_mapToEqualizer_pullback'`, `mapToEqualizer_eq_comp`, `EqualizerCondition.bijective_mapToEqualizer_pullback`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equalizerConditionMap_iff_nonempty_isLimit` 📖	mathematical	—	`SingleEqualizerCondition` `CategoryTheory.Limits.IsLimit` `Opposite` `CategoryTheory.Presieve.category` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.ofArrows` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Presieve.diagram` `CategoryTheory.Functor.mapCone` `CategoryTheory.Limits.Cocone.op` `CategoryTheory.Presieve.cocone`	—	`CategoryTheory.Limits.pullback.condition` `equalizerCondition_w`
`equalizerCondition_iff_isIso_lift` 📖	mathematical	—	`EqualizerCondition` `CategoryTheory.types` `CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Limits.equalizer` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Limits.equalizer.lift` `equalizerCondition_w'`	—	`CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `univLE_of_max` `UnivLE.self` `equalizerCondition_w'` `CategoryTheory.Limits.pullback.condition` `EqualizerCondition.bijective_mapToEqualizer_pullback` `CategoryTheory.IsIso.of_isIso_comp_right` `CategoryTheory.Iso.isIso_hom` `mapToEqualizer_eq_comp` `CategoryTheory.isIso_iff_bijective` `CategoryTheory.IsIso.comp_isIso`
`equalizerCondition_iff_isSheaf` 📖	mathematical	`CategoryTheory.Limits.HasPullback`	`EqualizerCondition` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.regularTopology`	—	`CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage` `equalizerConditionMap_iff_nonempty_isLimit`
`equalizerCondition_iff_of_equivalence` 📖	mathematical	—	`EqualizerCondition` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Equivalence.op`	—	`equalizerCondition_precomp_of_preservesPullback` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_inverse` `CategoryTheory.Functor.instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies` `CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies` `CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence` `equalizerCondition_of_natIso` `CategoryTheory.Equivalence.isEquivalence_functor`
`equalizerCondition_of_natIso` 📖	—	`EqualizerCondition`	—	—	`equalizerCondition_w` `CategoryTheory.NatTrans.naturality`
`equalizerCondition_precomp_of_preservesPullback` 📖	mathematical	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `EqualizerCondition`	`CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op`	—	`equalizerCondition_w` `CategoryTheory.Limits.PullbackCone.condition` `CategoryTheory.Functor.map_effectiveEpi` `CategoryTheory.Category.id_comp`
`equalizerCondition_w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.PullbackCone.fst` `CategoryTheory.Limits.PullbackCone.snd`	—	`CategoryTheory.Limits.PullbackCone.condition`
`equalizerCondition_w'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.Limits.pullback.condition`
`isSheafFor_regular_of_projective` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheafFor`	—	`CategoryTheory.Presieve.regular.single_epi` `CategoryTheory.Presieve.isSheafFor_arrows_iff` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.FunctorToTypes.map_id_apply` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Projective.factorThru_comp` `CategoryTheory.Category.comp_id`
`isSheaf_of_projective` 📖	mathematical	`CategoryTheory.Projective`	`CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.regularTopology`	—	`CategoryTheory.Presieve.isSheaf_coverage` `isSheafFor_regular_of_projective`
`isSheaf_yoneda_obj` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheaf` `CategoryTheory.regularTopology` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda`	—	`eq_1` `CategoryTheory.Presieve.isSheaf_coverage` `CategoryTheory.Presieve.regular.single_epi` `CategoryTheory.EffectiveEpi.effectiveEpi` `CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend` `CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit` `CategoryTheory.Presieve.ofArrows_pUnit` `CategoryTheory.Sieve.generateSingleton_eq` `CategoryTheory.Sieve.le_generate` `CategoryTheory.Presieve.restrict_extend` `CategoryTheory.Presieve.isAmalgamation_restrict` `CategoryTheory.Presieve.isAmalgamation_sieveExtend`
`mapToEqualizer_eq_comp` 📖	mathematical	—	`mapToEqualizer` `CategoryTheory.Limits.pullback` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Limits.equalizer` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Limits.equalizer.lift` `equalizerCondition_w'` `CategoryTheory.Iso.hom` `CategoryTheory.Limits.Types.equalizerIso`	—	`CategoryTheory.Limits.pullback.condition` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `univLE_of_max` `UnivLE.self` `equalizerCondition_w'` `CategoryTheory.Iso.comp_inv_eq` `CategoryTheory.Limits.equalizer.hom_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι` `CategoryTheory.Limits.limit.lift_π`
`parallelPair_pullback_initial` 📖	mathematical	—	`CategoryTheory.Functor.Initial` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `Opposite` `CategoryTheory.Presieve.category` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.ofArrows` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `CategoryTheory.Limits.parallelPair` `Opposite.op` `CategoryTheory.Presieve.categoryMk` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.PullbackCone.fst` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Presieve.ofArrows` `Quiver.Hom.op` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Over.homMk` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Limits.PullbackCone.snd` `CategoryTheory.Limits.PullbackCone.condition`	—	`CategoryTheory.Limits.PullbackCone.condition` `CategoryTheory.ObjectProperty.FullSubcategory.property` `CategoryTheory.Over.w` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst_assoc` `CategoryTheory.ObjectProperty.hom_ext` `CategoryTheory.Over.OverMorphism.ext` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd`
`subcanonical` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.Subcanonical` `CategoryTheory.regularTopology`	—	`CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj` `isSheaf_yoneda_obj`

CategoryTheory.regularTopology.EqualizerCondition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_mapToEqualizer_pullback` 📖	mathematical	`CategoryTheory.regularTopology.EqualizerCondition` `CategoryTheory.types`	`Function.Bijective` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Set.Elem` `setOf` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd` `CategoryTheory.regularTopology.mapToEqualizer` `CategoryTheory.Limits.pullback.condition`	—	`bijective_mapToEqualizer_pullback'`
`bijective_mapToEqualizer_pullback'` 📖	mathematical	`CategoryTheory.regularTopology.EqualizerCondition` `CategoryTheory.types`	`Function.Bijective` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Set.Elem` `setOf` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.PullbackCone.fst` `CategoryTheory.Limits.PullbackCone.snd` `CategoryTheory.regularTopology.mapToEqualizer` `CategoryTheory.Limits.PullbackCone.condition`	—	`CategoryTheory.Limits.PullbackCone.condition` `Function.bijective_iff_existsUnique` `CategoryTheory.regularTopology.equalizerCondition_w` `CategoryTheory.Limits.Types.type_equalizer_iff_unique`
`mk` 📖	mathematical	`Function.Bijective` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op` `Set.Elem` `setOf` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd` `CategoryTheory.regularTopology.mapToEqualizer` `CategoryTheory.Limits.pullback.condition`	`CategoryTheory.regularTopology.EqualizerCondition`	—	`CategoryTheory.Limits.pullback.condition` `CategoryTheory.regularTopology.equalizerCondition_w` `CategoryTheory.Limits.Types.type_equalizer_iff_unique` `CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp` `CategoryTheory.op_comp` `CategoryTheory.FunctorToTypes.map_comp_apply` `Function.bijective_iff_existsUnique`
`mk'` 📖	mathematical	`Function.Bijective` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op` `Set.Elem` `setOf` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.PullbackCone.fst` `CategoryTheory.Limits.PullbackCone.snd` `CategoryTheory.regularTopology.mapToEqualizer` `CategoryTheory.Limits.PullbackCone.condition`	`CategoryTheory.regularTopology.EqualizerCondition`	—	`CategoryTheory.Limits.PullbackCone.condition` `CategoryTheory.regularTopology.equalizerCondition_w` `CategoryTheory.Limits.Types.type_equalizer_iff_unique` `Function.bijective_iff_existsUnique`

---

← Back to Index