Documentation Verification Report

Preserves

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

Statistics

Metric	Count
Definitions `isTerminal_of_isSheafFor_empty_presieve`	1
Theorems `firstMap_eq_secondMap`, `isSheafFor_iff_preservesProduct`, `isSheafFor_of_preservesProduct`, `piComparison_fac`, `preservesProduct_of_isSheafFor`, `preservesTerminal_of_isSheaf_for_empty`	6
Total	7

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
`isTerminal_of_isSheafFor_empty_presieve` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`firstMap_eq_secondMap` 📖	mathematical	`IsSheafFor` `ofArrows` `IsEmpty.elim` `Empty.instIsEmpty` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Mono` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `Pairwise` `CategoryTheory.IsPullback` `CategoryTheory.Limits.initial` `CategoryTheory.Limits.initial.to`	`CategoryTheory.Equalizer.Presieve.Arrows.firstMap` `CategoryTheory.Equalizer.Presieve.Arrows.secondMap`	—	`Empty.instIsEmpty` `CategoryTheory.types_ext` `CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext` `CategoryTheory.Limits.Types.pi_lift_π_apply` `small_prod` `CategoryTheory.Mono.right_cancellation` `CategoryTheory.Limits.pullback.condition` `preservesTerminal_of_isSheaf_for_empty` `CategoryTheory.injective_of_mono` `instHasPullbackOfHasPairwisePullbacksOfArrows` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `CategoryTheory.Limits.Types.hasLimitsOfSize` `UnivLE.self` `Finite.of_fintype` `CategoryTheory.Limits.hasTerminal_op_of_hasInitial` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Limits.Types.limit_ext`
`isSheafFor_iff_preservesProduct` 📖	mathematical	`IsSheafFor` `ofArrows` `IsEmpty.elim` `Empty.instIsEmpty` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Mono` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `Pairwise` `CategoryTheory.IsPullback` `CategoryTheory.Limits.initial` `CategoryTheory.Limits.initial.to`	`CategoryTheory.Limits.PreservesLimit` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op`	—	`Empty.instIsEmpty` `preservesProduct_of_isSheafFor` `isSheafFor_of_preservesProduct`
`isSheafFor_of_preservesProduct` 📖	mathematical	—	`IsSheafFor` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `ofArrows`	—	`CategoryTheory.Equalizer.Presieve.Arrows.w` `CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition` `CategoryTheory.Limits.Types.type_equalizer_iff_unique` `CategoryTheory.Limits.instHasProductOppositeOp` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Limits.instIsIsoPiComparison` `Function.bijective_iff_existsUnique` `CategoryTheory.isIso_iff_bijective` `piComparison_fac` `CategoryTheory.injective_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.FunctorToTypes.map_inv_map_hom_apply` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.FunctorToTypes.map_id_apply`
`piComparison_fac` 📖	mathematical	—	`CategoryTheory.Limits.piComparison` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op` `CategoryTheory.Limits.instHasProductOppositeOp` `CategoryTheory.Limits.HasColimit.mk'` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.Limits.ColimitCocone` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.piObj` `CategoryTheory.Limits.Pi.π` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Equalizer.Presieve.Arrows.FirstObj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.Limits.opCoproductIsoProduct'` `CategoryTheory.Limits.productIsProduct` `CategoryTheory.Equalizer.Presieve.Arrows.forkMap`	—	`CategoryTheory.Limits.instHasProductOppositeOp` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Limits.map_lift_piComparison` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom` `CategoryTheory.Limits.IsColimit.desc_self` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Functor.map_id`
`preservesProduct_of_isSheafFor` 📖	mathematical	`IsSheafFor` `ofArrows` `IsEmpty.elim` `Empty.instIsEmpty` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Mono` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `Pairwise` `CategoryTheory.IsPullback` `CategoryTheory.Limits.initial` `CategoryTheory.Limits.initial.to`	`CategoryTheory.Limits.PreservesLimit` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op`	—	`Empty.instIsEmpty` `CategoryTheory.Limits.PreservesProduct.of_iso_comparison` `CategoryTheory.Limits.instHasProductOppositeOp` `CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `piComparison_fac` `CategoryTheory.IsIso.comp_isIso'` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.isIso_iff_bijective` `Function.bijective_iff_existsUnique` `CategoryTheory.Equalizer.Presieve.Arrows.w` `CategoryTheory.Limits.Types.type_equalizer_iff_unique` `CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition` `firstMap_eq_secondMap`
`preservesTerminal_of_isSheaf_for_empty` 📖	mathematical	`IsSheafFor` `ofArrows` `IsEmpty.elim` `Empty.instIsEmpty` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Limits.PreservesLimit` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	—	`Empty.instIsEmpty` `CategoryTheory.Limits.IsInitial.hasInitial` `CategoryTheory.Limits.preservesTerminal_of_iso` `CategoryTheory.Limits.hasTerminal_op_of_hasInitial` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `CategoryTheory.Limits.Types.hasLimitsOfSize` `UnivLE.self` `Finite.of_fintype`

---

← Back to Index