Documentation Verification Report

EqualizerSheafCondition

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

Statistics

Metric	Count
Definitions `FirstObj`, `FirstObj`, `SecondObj`, `firstMap`, `forkMap`, `secondMap`, `SecondObj`, `firstMap`, `instInhabitedSecondObjBotPresieve`, `secondMap`, `SecondObj`, `firstMap`, `instInhabitedSecondObjBotSieve`, `secondMap`, `firstObjEqFamily`, `forkMap`, `instInhabitedFirstObjArrowsBotSieve`, `instInhabitedFirstObjBotPresieve`	18
Theorems `ext`, `ext_iff`, `ext`, `ext_iff`, `ext`, `ext_iff`, `compatible_iff`, `compatible_iff_of_small`, `sheaf_condition`, `w`, `compatible_iff`, `isSheafFor_singleton_iff`, `isSheafFor_singleton_iff_of_hasPullback`, `sheaf_condition`, `w`, `ext`, `ext_iff`, `compatible_iff`, `equalizer_sheaf_condition`, `w`, `firstObjEqFamily_hom`, `firstObjEqFamily_inv`	22
Total	40

CategoryTheory.Equalizer

Definitions

Name	Category	Theorems
`FirstObj` 📖	CompOp	8 math math: `Sieve.equalizer_sheaf_condition`, `firstObjEqFamily_inv`, `firstObjEqFamily_hom`, `Sieve.w`, `Presieve.compatible_iff`, `Presieve.sheaf_condition`, `Presieve.w`, `Sieve.compatible_iff`
`firstObjEqFamily` 📖	CompOp	4 math math: `firstObjEqFamily_inv`, `firstObjEqFamily_hom`, `Presieve.compatible_iff`, `Sieve.compatible_iff`
`forkMap` 📖	CompOp	4 math math: `Sieve.equalizer_sheaf_condition`, `Sieve.w`, `Presieve.sheaf_condition`, `Presieve.w`
`instInhabitedFirstObjArrowsBotSieve` 📖	CompOp	—
`instInhabitedFirstObjBotPresieve` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`firstObjEqFamily_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.types` `FirstObj` `CategoryTheory.Presieve.FamilyOfElements` `firstObjEqFamily` `CategoryTheory.Limits.Pi.π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	—
`firstObjEqFamily_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.types` `FirstObj` `CategoryTheory.Presieve.FamilyOfElements` `firstObjEqFamily` `CategoryTheory.Limits.Pi.lift` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	—

CategoryTheory.Equalizer.FirstObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.Limits.Pi.π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	—	`CategoryTheory.Limits.Types.limit_ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.Limits.Pi.π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	`ext`

CategoryTheory.Equalizer.Presieve

Definitions

Name	Category	Theorems
`SecondObj` 📖	CompOp	2 math math: `sheaf_condition`, `w`
`firstMap` 📖	CompOp	3 math math: `compatible_iff`, `sheaf_condition`, `w`
`instInhabitedSecondObjBotPresieve` 📖	CompOp	—
`secondMap` 📖	CompOp	3 math math: `compatible_iff`, `sheaf_condition`, `w`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatible_iff` 📖	mathematical	—	`CategoryTheory.Presieve.FamilyOfElements.Compatible` `CategoryTheory.Iso.hom` `CategoryTheory.types` `CategoryTheory.Equalizer.FirstObj` `CategoryTheory.Presieve.FamilyOfElements` `CategoryTheory.Equalizer.firstObjEqFamily` `firstMap` `secondMap`	—	`CategoryTheory.Presieve.pullbackCompatible_iff` `CategoryTheory.Limits.Types.limit_ext` `CategoryTheory.Limits.Types.pi_lift_π_apply` `small_prod` `small_sigma` `UnivLE.small` `univLE_of_max` `UnivLE.self` `small_subtype` `CategoryTheory.instSmallHomOfLocallySmall` `CategoryTheory.locallySmall_of_univLE` `CategoryTheory.Presieve.HasPairwisePullbacks.has_pullbacks` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.Limits.Types.limit_ext_iff'`
`isSheafFor_singleton_iff` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Presieve.singleton` `CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.types` `CategoryTheory.Limits.parallelPair` `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.Category.toCategoryStruct` `CategoryTheory.Limits.PullbackCone.fst` `CategoryTheory.Limits.PullbackCone.snd` `CategoryTheory.Limits.Fork.ofι`	—	`CategoryTheory.Limits.PullbackCone.condition` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst` `CategoryTheory.op_comp` `CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd` `CategoryTheory.Limits.Types.type_equalizer_iff_unique` `CategoryTheory.Presieve.isSheafFor_singleton`
`isSheafFor_singleton_iff_of_hasPullback` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Presieve.singleton` `CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.types` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `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.Fork.ofι`	—	`isSheafFor_singleton_iff`
`sheaf_condition` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.types` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Equalizer.FirstObj` `SecondObj` `firstMap` `secondMap` `CategoryTheory.Limits.Fork.ofι` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Equalizer.forkMap` `w`	—	`w` `CategoryTheory.Limits.Types.type_equalizer_iff_unique` `Equiv.forall_congr_right` `Equiv.apply_symm_apply` `existsUnique_congr` `Equiv.eq_symm_apply` `CategoryTheory.Limits.Types.pi_lift_π_apply` `small_sigma` `UnivLE.small` `univLE_of_max` `UnivLE.self` `small_subtype` `CategoryTheory.instSmallHomOfLocallySmall` `CategoryTheory.locallySmall_of_univLE`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Equalizer.FirstObj` `SecondObj` `CategoryTheory.Equalizer.forkMap` `firstMap` `secondMap`	—	`CategoryTheory.Limits.Pi.hom_ext` `CategoryTheory.types_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.limit.lift_π_assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.op_comp` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.FunctorToTypes.map_comp_apply`

CategoryTheory.Equalizer.Presieve.Arrows

Definitions

Name	Category	Theorems
`FirstObj` 📖	CompOp	3 math math: `sheaf_condition`, `CategoryTheory.Presieve.piComparison_fac`, `w`
`SecondObj` 📖	CompOp	2 math math: `sheaf_condition`, `w`
`firstMap` 📖	CompOp	5 math math: `CategoryTheory.Presieve.firstMap_eq_secondMap`, `compatible_iff`, `sheaf_condition`, `compatible_iff_of_small`, `w`
`forkMap` 📖	CompOp	3 math math: `sheaf_condition`, `CategoryTheory.Presieve.piComparison_fac`, `w`
`secondMap` 📖	CompOp	5 math math: `CategoryTheory.Presieve.firstMap_eq_secondMap`, `compatible_iff`, `sheaf_condition`, `compatible_iff_of_small`, `w`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatible_iff` 📖	mathematical	—	`CategoryTheory.Presieve.Arrows.Compatible` `CategoryTheory.Iso.hom` `CategoryTheory.types` `CategoryTheory.Limits.piObj` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Discrete.functor` `CategoryTheory.Limits.Types.productIso` `firstMap` `secondMap`	—	`UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `univLE_of_max` `CategoryTheory.Presieve.Arrows.pullbackCompatible_iff` `SecondObj.ext` `CategoryTheory.Limits.Types.pi_lift_π_apply` `small_prod` `CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows` `CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply`
`compatible_iff_of_small` 📖	mathematical	—	`CategoryTheory.Presieve.Arrows.Compatible` `DFunLike.coe` `Equiv` `Shrink` `small_Pi` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op` `UnivLE.small` `UnivLE.self` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `CategoryTheory.Iso.hom` `CategoryTheory.Limits.piObj` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Discrete.functor` `CategoryTheory.Limits.Types.Small.productIso` `firstMap` `secondMap`	—	`small_Pi` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Presieve.Arrows.pullbackCompatible_iff` `SecondObj.ext` `CategoryTheory.Limits.Types.pi_lift_π_apply` `small_prod` `CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows` `CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply`
`sheaf_condition` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Presieve.ofArrows` `CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.types` `CategoryTheory.Limits.parallelPair` `FirstObj` `SecondObj` `firstMap` `secondMap` `CategoryTheory.Limits.Fork.ofι` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `forkMap` `w`	—	`w` `CategoryTheory.Limits.Types.type_equalizer_iff_unique` `CategoryTheory.Presieve.isSheafFor_arrows_iff` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `small_Pi` `UnivLE.small` `UnivLE.self` `Equiv.forall_congr_right` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply` `existsUnique_congr` `Equiv.eq_symm_apply` `Equiv.symm_apply_eq` `CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply` `CategoryTheory.Limits.Types.pi_lift_π_apply`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `FirstObj` `SecondObj` `forkMap` `firstMap` `secondMap`	—	`CategoryTheory.types_ext` `SecondObj.ext` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `small_prod` `CategoryTheory.Limits.Types.pi_lift_π_apply` `CategoryTheory.Limits.pullback.condition`

CategoryTheory.Equalizer.Presieve.Arrows.FirstObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.Limits.Pi.π` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	—	`CategoryTheory.Limits.Types.limit_ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.Limits.Pi.π` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	`ext`

CategoryTheory.Equalizer.Presieve.Arrows.SecondObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.Limits.Pi.π` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Limits.pullback`	—	—	`CategoryTheory.Limits.Types.limit_ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.Limits.Pi.π` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Limits.pullback`	—	`ext`

CategoryTheory.Equalizer.Sieve

Definitions

Name	Category	Theorems
`SecondObj` 📖	CompOp	2 math math: `equalizer_sheaf_condition`, `w`
`firstMap` 📖	CompOp	3 math math: `equalizer_sheaf_condition`, `w`, `compatible_iff`
`instInhabitedSecondObjBotSieve` 📖	CompOp	—
`secondMap` 📖	CompOp	3 math math: `equalizer_sheaf_condition`, `w`, `compatible_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatible_iff` 📖	mathematical	—	`CategoryTheory.Presieve.FamilyOfElements.Compatible` `CategoryTheory.Sieve.arrows` `CategoryTheory.Iso.hom` `CategoryTheory.types` `CategoryTheory.Equalizer.FirstObj` `CategoryTheory.Presieve.FamilyOfElements` `CategoryTheory.Equalizer.firstObjEqFamily` `firstMap` `secondMap`	—	`CategoryTheory.Presieve.compatible_iff_sieveCompatible` `SecondObj.ext` `CategoryTheory.Limits.Types.pi_lift_π_apply` `small_sigma` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.instSmallHomOfLocallySmall` `CategoryTheory.locallySmall_of_univLE` `small_subtype` `CategoryTheory.Sieve.downward_closed` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.Limits.Types.limit_ext_iff'`
`equalizer_sheaf_condition` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Sieve.arrows` `CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.types` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Equalizer.FirstObj` `SecondObj` `firstMap` `secondMap` `CategoryTheory.Limits.Fork.ofι` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Equalizer.forkMap` `w`	—	`w` `CategoryTheory.Limits.Types.type_equalizer_iff_unique` `Equiv.forall_congr_right` `CategoryTheory.inv_hom_id_apply` `existsUnique_congr` `CategoryTheory.Iso.toEquiv_symm_fun` `Equiv.eq_symm_apply` `CategoryTheory.Limits.Types.pi_lift_π_apply` `small_sigma` `UnivLE.small` `univLE_of_max` `UnivLE.self` `small_subtype` `CategoryTheory.instSmallHomOfLocallySmall` `CategoryTheory.locallySmall_of_univLE`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Equalizer.FirstObj` `CategoryTheory.Sieve.arrows` `SecondObj` `CategoryTheory.Equalizer.forkMap` `firstMap` `secondMap`	—	`CategoryTheory.types_ext` `SecondObj.ext` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `small_sigma` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.instSmallHomOfLocallySmall` `CategoryTheory.locallySmall_of_univLE` `small_subtype` `CategoryTheory.Limits.Types.pi_lift_π_apply` `CategoryTheory.FunctorToTypes.map_comp_apply`

CategoryTheory.Equalizer.Sieve.SecondObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.Limits.Pi.π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Sieve.arrows` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	—	`CategoryTheory.Limits.Types.limit_ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.Limits.Pi.π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Sieve.arrows` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	`ext`

---

← Back to Index