Documentation Verification Report

Subsheaf

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

Statistics

Metric	Count
Definitions `image`, `imageι`, `toImage`, `sheafify`, `sheafifyLift`, `toRangeSheafify`, `sheafify`, `sheafifyLift`, `toRangeSheafify`, `imageFactorization`, `imageMonoFactorization`	11
Theorems `image_val`, `imageι_val`, `toImage_val`, `toImage_ι`, `toImage_ι_assoc`, `eq_sheafify`, `eq_sheafify_iff`, `isSeparated`, `isSheaf_iff`, `le_sheafify`, `sheafify_isSheaf`, `sheafify_le`, `sheafify_sheafify`, `toRangeSheafify_app_coe`, `to_sheafifyLift`, `to_sheafify_lift_unique`, `eq_sheafify`, `eq_sheafify_iff`, `isSeparated`, `isSheaf_iff`, `le_sheafify`, `sheafify_isSheaf`, `sheafify_le`, `sheafify_sheafify`, `to_sheafifyLift`, `to_sheafify_lift_unique`, `instEpiSheafTypeToImage`, `instHasImagesSheafType`, `instMonoSheafTypeImageι`	29
Total	40

CategoryTheory

Definitions

Name	Category	Theorems
`imageFactorization` 📖	CompOp	—
`imageMonoFactorization` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEpiSheafTypeToImage` 📖	mathematical	—	`Epi` `Sheaf` `types` `Sheaf.instCategorySheaf` `Sheaf.image` `Sheaf.toImage`	—	`Sheaf.hom_ext` `NatTrans.ext'` `types_ext` `Presieve.IsSeparatedFor.ext` `Presieve.IsSheafFor.isSeparatedFor` `isSheaf_iff_isSheaf_of_type` `Sheaf.cond` `NatTrans.naturality`
`instHasImagesSheafType` 📖	mathematical	—	`Limits.HasImages` `Sheaf` `types` `Sheaf.instCategorySheaf`	—	—
`instMonoSheafTypeImageι` 📖	mathematical	—	`Mono` `Sheaf` `types` `Sheaf.instCategorySheaf` `Sheaf.image` `Sheaf.imageι`	—	`Functor.mono_of_mono_map` `reflectsMonomorphisms_of_reflectsLimitsOfShape` `Limits.reflectsLimitsOfShape_of_reflectsLimits` `Limits.fullyFaithful_reflectsLimits` `instFullSheafFunctorOppositeSheafToPresheaf` `instFaithfulSheafFunctorOppositeSheafToPresheaf` `Subfunctor.instMonoFunctorTypeι`

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`image` 📖	CompOp	10 math math: `instIsLocallySurjectiveHomToImage`, `toImage_ι_assoc`, `CategoryTheory.instEpiSheafTypeToImage`, `toImage_ι`, `imageι_val`, `toImage_val`, `instIsLocallyInjectiveHomImageι`, `isLocallySurjective_iff_isIso`, `CategoryTheory.instMonoSheafTypeImageι`, `image_val`
`imageι` 📖	CompOp	6 math math: `toImage_ι_assoc`, `toImage_ι`, `imageι_val`, `instIsLocallyInjectiveHomImageι`, `isLocallySurjective_iff_isIso`, `CategoryTheory.instMonoSheafTypeImageι`
`toImage` 📖	CompOp	5 math math: `instIsLocallySurjectiveHomToImage`, `toImage_ι_assoc`, `CategoryTheory.instEpiSheafTypeToImage`, `toImage_ι`, `toImage_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_val` 📖	mathematical	—	`val` `CategoryTheory.types` `image` `CategoryTheory.Subfunctor.toFunctor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Subfunctor.sheafify` `CategoryTheory.Subfunctor.range` `Hom.val`	—	—
`imageι_val` 📖	mathematical	—	`Hom.val` `CategoryTheory.types` `image` `imageι` `CategoryTheory.Subfunctor.ι` `Opposite` `CategoryTheory.Category.opposite` `val` `CategoryTheory.Subfunctor.sheafify` `CategoryTheory.Subfunctor.range`	—	—
`toImage_val` 📖	mathematical	—	`Hom.val` `CategoryTheory.types` `image` `toImage` `CategoryTheory.Subfunctor.toRangeSheafify` `val`	—	—
`toImage_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Sheaf` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `instCategorySheaf` `image` `toImage` `imageι`	—	`hom_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Subfunctor.homOfLe_ι`
`toImage_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Sheaf` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `instCategorySheaf` `image` `toImage` `imageι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `toImage_ι`

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
`sheafify` 📖	CompOp	20 math math: `sheafify_sheafify`, `sheafify_le`, `CategoryTheory.Subpresheaf.sheafify_sheafify`, `CategoryTheory.Sheaf.imageι_val`, `CategoryTheory.Subpresheaf.sheafify_le`, `le_sheafify`, `CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top`, `CategoryTheory.Subpresheaf.eq_sheafify`, `CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top'`, `sheafify_isSheaf`, `CategoryTheory.Subpresheaf.sheafify_isSheaf`, `CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify`, `toRangeSheafify_app_coe`, `CategoryTheory.Subpresheaf.eq_sheafify_iff`, `CategoryTheory.Subpresheaf.le_sheafify`, `eq_sheafify`, `to_sheafifyLift`, `CategoryTheory.Subpresheaf.to_sheafifyLift`, `eq_sheafify_iff`, `CategoryTheory.Sheaf.image_val`
`sheafifyLift` 📖	CompOp	2 math math: `to_sheafifyLift`, `CategoryTheory.Subpresheaf.to_sheafifyLift`
`toRangeSheafify` 📖	CompOp	3 math math: `CategoryTheory.Sheaf.toImage_val`, `CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify`, `toRangeSheafify_app_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_sheafify` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf` `toFunctor` `Opposite` `CategoryTheory.Category.opposite`	`sheafify`	—	`LE.le.antisymm` `le_sheafify` `family_of_elements_compatible` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `CategoryTheory.Presieve.IsSheafFor.valid_glue`
`eq_sheafify_iff` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`sheafify` `toFunctor` `Opposite` `CategoryTheory.Category.opposite`	—	`sheafify_isSheaf` `eq_sheafify`
`isSeparated` 📖	mathematical	`CategoryTheory.Presieve.IsSeparated`	`toFunctor` `Opposite` `CategoryTheory.Category.opposite`	—	`CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.map`
`isSheaf_iff` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`toFunctor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Set` `Set.instMembership` `obj`	—	`eq_sheafify_iff` `Eq.ge` `LE.le.antisymm` `le_sheafify`
`le_sheafify` 📖	mathematical	—	`CategoryTheory.Subfunctor` `Opposite` `CategoryTheory.Category.opposite` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `sheafify`	—	`eq_top_iff` `map` `CategoryTheory.GrothendieckTopology.top_mem`
`sheafify_isSheaf` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`toFunctor` `Opposite` `CategoryTheory.Category.opposite` `sheafify`	—	`CategoryTheory.Presieve.IsSeparated.isSheaf` `isSeparated` `CategoryTheory.Presieve.IsSheaf.isSeparated` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `CategoryTheory.Functor.map_comp` `CategoryTheory.op_comp` `CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.Category.assoc` `CategoryTheory.GrothendieckTopology.bind_covering` `CategoryTheory.GrothendieckTopology.superset_covering`
`sheafify_le` 📖	mathematical	`CategoryTheory.Subfunctor` `Opposite` `CategoryTheory.Category.opposite` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `CategoryTheory.Presieve.IsSheaf` `toFunctor`	`sheafify`	—	`CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `le_sheafify` `to_sheafifyLift` `nat_trans_naturality`
`sheafify_sheafify` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`sheafify`	—	`eq_sheafify_iff` `sheafify_isSheaf`
`toRangeSheafify_app_coe` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Set` `Set.instMembership` `obj` `sheafify` `range` `CategoryTheory.NatTrans.app` `toFunctor` `toRangeSheafify` `Set.range` `toRange`	—	—
`to_sheafifyLift` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `sheafify` `homOfLe` `le_sheafify` `sheafifyLift`	—	`CategoryTheory.NatTrans.ext'` `le_sheafify` `CategoryTheory.types_ext` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `Subtype.prop` `CategoryTheory.comp_apply` `Mathlib.Tactic.Elementwise.hom_elementwise` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Presieve.FamilyOfElements.Compatible.map` `family_of_elements_compatible` `CategoryTheory.Presieve.IsSheafFor.valid_glue`
`to_sheafify_lift_unique` 📖	—	`CategoryTheory.Presieve.IsSheaf` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `sheafify` `homOfLe` `le_sheafify`	—	—	`le_sheafify` `CategoryTheory.NatTrans.ext'` `CategoryTheory.types_ext` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `CategoryTheory.FunctorToTypes.naturality` `CategoryTheory.congr_app`

CategoryTheory.Subpresheaf

Definitions

Name	Category	Theorems
`sheafify` 📖	CompOp	—
`sheafifyLift` 📖	CompOp	—
`toRangeSheafify` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_sheafify` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf` `CategoryTheory.Subfunctor.toFunctor` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.Subfunctor.sheafify`	—	`CategoryTheory.Subfunctor.eq_sheafify`
`eq_sheafify_iff` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`CategoryTheory.Subfunctor.sheafify` `CategoryTheory.Subfunctor.toFunctor` `Opposite` `CategoryTheory.Category.opposite`	—	`CategoryTheory.Subfunctor.eq_sheafify_iff`
`isSeparated` 📖	mathematical	`CategoryTheory.Presieve.IsSeparated`	`CategoryTheory.Subfunctor.toFunctor` `Opposite` `CategoryTheory.Category.opposite`	—	`CategoryTheory.Subfunctor.isSeparated`
`isSheaf_iff` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`CategoryTheory.Subfunctor.toFunctor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj`	—	`CategoryTheory.Subfunctor.isSheaf_iff`
`le_sheafify` 📖	mathematical	—	`CategoryTheory.Subfunctor` `Opposite` `CategoryTheory.Category.opposite` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `CategoryTheory.Subfunctor.sheafify`	—	`CategoryTheory.Subfunctor.le_sheafify`
`sheafify_isSheaf` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`CategoryTheory.Subfunctor.toFunctor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Subfunctor.sheafify`	—	`CategoryTheory.Subfunctor.sheafify_isSheaf`
`sheafify_le` 📖	mathematical	`CategoryTheory.Subfunctor` `Opposite` `CategoryTheory.Category.opposite` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `CategoryTheory.Presieve.IsSheaf` `CategoryTheory.Subfunctor.toFunctor`	`CategoryTheory.Subfunctor.sheafify`	—	`CategoryTheory.Subfunctor.sheafify_le`
`sheafify_sheafify` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`CategoryTheory.Subfunctor.sheafify`	—	`CategoryTheory.Subfunctor.sheafify_sheafify`
`to_sheafifyLift` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Subfunctor.toFunctor` `CategoryTheory.Subfunctor.sheafify` `CategoryTheory.Subfunctor.homOfLe` `CategoryTheory.Subfunctor.le_sheafify` `CategoryTheory.Subfunctor.sheafifyLift`	—	`CategoryTheory.Subfunctor.to_sheafifyLift`
`to_sheafify_lift_unique` 📖	—	`CategoryTheory.Presieve.IsSheaf` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Subfunctor.toFunctor` `CategoryTheory.Subfunctor.sheafify` `CategoryTheory.Subfunctor.homOfLe` `CategoryTheory.Subfunctor.le_sheafify`	—	—	`CategoryTheory.Subfunctor.to_sheafify_lift_unique`

---

← Back to Index