Documentation Verification Report

PreservesSheafification

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

Statistics

Metric	Count
Definitions `composeAndSheafify`, `instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify`, `presheafToSheafCompComposeAndSheafifyIso`, `sheafComposeNatIso`, `sheafComposeNatTrans`, `sheafifyComposeIso`, `toPresheafToSheafCompComposeAndSheafify`	7
Theorems `le`, `W_isInvertedBy_whiskeringRight_presheafToSheaf`, `W_of_preservesSheafification`, `instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction`, `instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction`, `instPreservesSheafification`, `instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms`, `preservesSheafification_iff_of_adjunctions`, `preservesSheafification_iff_of_adjunctions_of_hasSheafCompose`, `sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv`, `instIsIsoFunctorOppositeSheafSheafComposeNatTrans`, `instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify`, `presheafToSheafCompComposeAndSheafifyIso_inv_app`, `sheafComposeIso_hom_fac`, `sheafComposeIso_hom_fac_assoc`, `sheafComposeIso_inv_fac`, `sheafComposeIso_inv_fac_assoc`, `sheafComposeNatTrans_app_uniq`, `sheafComposeNatTrans_fac`, `toPresheafToSheafCompComposeAndSheafify_app`	20
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
`instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify` 📖	CompOp	—
`presheafToSheafCompComposeAndSheafifyIso` 📖	CompOp	1 math math: `presheafToSheafCompComposeAndSheafifyIso_inv_app`
`sheafComposeNatIso` 📖	CompOp	—
`sheafComposeNatTrans` 📖	CompOp	7 math math: `instIsIsoFunctorOppositeSheafSheafComposeNatTrans`, `GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction`, `GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv`, `sheafComposeNatTrans_app_uniq`, `GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose`, `GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction`, `sheafComposeNatTrans_fac`
`sheafifyComposeIso` 📖	CompOp	6 math math: `constantCommuteCompose_hom_app_val`, `sheafComposeIso_hom_fac`, `sheafComposeIso_inv_fac_assoc`, `constantCommuteCompose_hom_app_hom`, `sheafComposeIso_hom_fac_assoc`, `sheafComposeIso_inv_fac`
`toPresheafToSheafCompComposeAndSheafify` 📖	CompOp	2 math math: `toPresheafToSheafCompComposeAndSheafify_app`, `instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoFunctorOppositeSheafSheafComposeNatTrans` 📖	mathematical	—	`IsIso` `Functor` `Opposite` `Category.opposite` `Functor.category` `Sheaf` `ObjectProperty.FullSubcategory.category` `Presheaf.IsSheaf` `Functor.comp` `Functor.obj` `Functor.whiskeringRight` `sheafCompose` `sheafComposeNatTrans`	—	`GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose`
`instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify` 📖	mathematical	—	`IsIso` `Functor` `Opposite` `Category.opposite` `Functor.category` `Sheaf` `ObjectProperty.FullSubcategory.category` `Presheaf.IsSheaf` `Functor.comp` `Functor.obj` `Functor.whiskeringRight` `presheafToSheaf` `Sheaf.composeAndSheafify` `toPresheafToSheafCompComposeAndSheafify`	—	`NatTrans.isIso_iff_isIso_app` `GrothendieckTopology.W_iff` `GrothendieckTopology.W_of_preservesSheafification` `GrothendieckTopology.W_toSheafify`
`presheafToSheafCompComposeAndSheafifyIso_inv_app` 📖	mathematical	—	`NatTrans.app` `Functor` `Opposite` `Category.opposite` `Functor.category` `Sheaf` `ObjectProperty.FullSubcategory.category` `Presheaf.IsSheaf` `Functor.comp` `Functor.obj` `Functor.whiskeringRight` `presheafToSheaf` `Sheaf.composeAndSheafify` `Iso.inv` `presheafToSheafCompComposeAndSheafifyIso` `Functor.map` `ObjectProperty.FullSubcategory.obj` `Functor.whiskerRight` `toSheafify`	—	—
`sheafComposeIso_hom_fac` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Opposite` `Category.opposite` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `sheafify` `toSheafify` `Iso.hom` `sheafifyComposeIso` `Functor.whiskerRight`	—	`sheafComposeNatTrans_fac`
`sheafComposeIso_hom_fac_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Opposite` `Category.opposite` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `sheafify` `toSheafify` `Iso.hom` `sheafifyComposeIso` `Functor.whiskerRight`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `sheafComposeIso_hom_fac`
`sheafComposeIso_inv_fac` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Opposite` `Category.opposite` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `sheafify` `Functor.whiskerRight` `toSheafify` `Iso.inv` `sheafifyComposeIso`	—	`sheafComposeIso_hom_fac` `Category.assoc` `Iso.hom_inv_id` `Category.comp_id`
`sheafComposeIso_inv_fac_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Opposite` `Category.opposite` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `sheafify` `Functor.whiskerRight` `toSheafify` `Iso.inv` `sheafifyComposeIso`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `sheafComposeIso_inv_fac`
`sheafComposeNatTrans_app_uniq` 📖	mathematical	`CategoryStruct.comp` `Functor` `Opposite` `Category.opposite` `Category.toCategoryStruct` `Functor.category` `Functor.obj` `Functor.id` `Functor.comp` `Sheaf` `ObjectProperty.FullSubcategory.category` `Presheaf.IsSheaf` `sheafToPresheaf` `sheafCompose` `NatTrans.app` `Adjunction.unit` `Functor.map` `Functor.whiskerRight`	`NatTrans.app` `Functor` `Opposite` `Category.opposite` `Functor.category` `Sheaf` `ObjectProperty.FullSubcategory.category` `Presheaf.IsSheaf` `Functor.comp` `Functor.obj` `Functor.whiskeringRight` `sheafCompose` `sheafComposeNatTrans`	—	`Equiv.injective` `Equiv.apply_symm_apply` `Adjunction.homEquiv_unit`
`sheafComposeNatTrans_fac` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Opposite` `Category.opposite` `Category.toCategoryStruct` `Functor.category` `Functor.obj` `Functor.id` `Functor.comp` `Sheaf` `ObjectProperty.FullSubcategory.category` `Presheaf.IsSheaf` `sheafToPresheaf` `sheafCompose` `NatTrans.app` `Adjunction.unit` `Functor.map` `Functor.whiskeringRight` `sheafComposeNatTrans` `Functor.whiskerRight`	—	`Adjunction.homEquiv_counit` `Functor.map_comp` `Adjunction.unit_naturality_assoc` `Adjunction.right_triangle_components` `Category.comp_id`
`toPresheafToSheafCompComposeAndSheafify_app` 📖	mathematical	—	`NatTrans.app` `Functor` `Opposite` `Category.opposite` `Functor.category` `Sheaf` `ObjectProperty.FullSubcategory.category` `Presheaf.IsSheaf` `Functor.comp` `Functor.obj` `Functor.whiskeringRight` `presheafToSheaf` `Sheaf.composeAndSheafify` `toPresheafToSheafCompComposeAndSheafify` `Functor.map` `ObjectProperty.FullSubcategory.obj` `Functor.whiskerRight` `toSheafify`	—	—

CategoryTheory.GrothendieckTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`W_isInvertedBy_whiskeringRight_presheafToSheaf` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Presheaf.IsSheaf` `W` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.presheafToSheaf`	—	`W_iff` `W_of_preservesSheafification`
`W_of_preservesSheafification` 📖	mathematical	`W`	`W` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.whiskerRight`	—	`PreservesSheafification.le`
`instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.HasColimitsOfShape` `Opposite` `Cover` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `instPreorderCover` `CategoryTheory.Limits.PreservesColimitsOfShape` `CategoryTheory.Limits.PreservesLimit` `Cover.shape` `CategoryTheory.Limits.MulticospanIndex.multicospan` `Cover.index` `CategoryTheory.types` `CategoryTheory.forget`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.plusPlusSheaf` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.types` `CategoryTheory.forget` `CategoryTheory.Limits.WalkingMulticospan` `Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.MulticospanIndex.multicospan` `Cover.index` `CategoryTheory.sheafCompose` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.sheafComposeNatTrans` `CategoryTheory.plusPlusAdjunction`	—	`CategoryTheory.NatIso.isIso_of_isIso_app` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction`
`instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.HasColimitsOfShape` `Opposite` `Cover` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `instPreorderCover` `CategoryTheory.Limits.PreservesColimitsOfShape` `CategoryTheory.Limits.PreservesLimit` `Cover.shape` `CategoryTheory.Limits.MulticospanIndex.multicospan` `Cover.index` `CategoryTheory.types` `CategoryTheory.forget`	`CategoryTheory.IsIso` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.plusPlusSheaf` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.types` `CategoryTheory.forget` `CategoryTheory.Limits.WalkingMulticospan` `Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.MulticospanIndex.multicospan` `Cover.index` `CategoryTheory.sheafCompose` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.NatTrans.app` `CategoryTheory.sheafComposeNatTrans` `CategoryTheory.plusPlusAdjunction`	—	`CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.isIso_iff_of_reflects_iso` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.ObjectProperty.full_ι` `CategoryTheory.ObjectProperty.faithful_ι` `sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv` `CategoryTheory.Iso.isIso_inv`
`instPreservesSheafification` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.HasColimitsOfShape` `Opposite` `Cover` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `instPreorderCover` `CategoryTheory.Limits.PreservesColimitsOfShape` `CategoryTheory.Limits.PreservesLimit` `Cover.shape` `CategoryTheory.Limits.MulticospanIndex.multicospan` `Cover.index` `CategoryTheory.types` `CategoryTheory.forget`	`PreservesSheafification`	—	`CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `preservesSheafification_iff_of_adjunctions_of_hasSheafCompose` `instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction`
`instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms` 📖	mathematical	`CategoryTheory.Limits.HasColimitsOfShape` `Opposite` `Cover` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `instPreorderCover` `CategoryTheory.Limits.PreservesColimitsOfShape` `CategoryTheory.types` `CategoryTheory.forget` `CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory`	`PreservesSheafification` `CategoryTheory.types` `CategoryTheory.forget`	—	`instPreservesSheafification` `CategoryTheory.Limits.Types.hasLimitsOfShape` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.Types.instFullForgetTypeHom` `CategoryTheory.instFaithfulForget`
`preservesSheafification_iff_of_adjunctions` 📖	mathematical	—	`PreservesSheafification` `CategoryTheory.IsIso` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Functor.map` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit`	—	`W_iff_isIso_map_of_adjunction` `W_of_preservesSheafification` `CategoryTheory.Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull` `CategoryTheory.ObjectProperty.faithful_ι` `CategoryTheory.ObjectProperty.full_ι` `CategoryTheory.MorphismProperty.postcomp_iff` `CategoryTheory.MorphismProperty.Respects.toRespectsRight` `CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition` `CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsLocal` `CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPostcompProperty` `CategoryTheory.Functor.whiskerRight_comp` `CategoryTheory.NatTrans.naturality` `CategoryTheory.MorphismProperty.precomp_iff` `CategoryTheory.MorphismProperty.Respects.toRespectsLeft` `CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPrecompProperty` `CategoryTheory.ObjectProperty.isLocal_of_isIso` `CategoryTheory.Functor.isIso_whiskerRight` `CategoryTheory.Functor.map_isIso`
`preservesSheafification_iff_of_adjunctions_of_hasSheafCompose` 📖	mathematical	—	`PreservesSheafification` `CategoryTheory.IsIso` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.sheafCompose` `CategoryTheory.sheafComposeNatTrans`	—	`preservesSheafification_iff_of_adjunctions` `CategoryTheory.NatTrans.isIso_iff_isIso_app` `W_iff_isIso_map_of_adjunction` `W_sheafToPresheaf_map_iff_isIso` `CategoryTheory.sheafComposeNatTrans_fac` `CategoryTheory.MorphismProperty.precomp_iff` `CategoryTheory.MorphismProperty.Respects.toRespectsLeft` `CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition` `CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsLocal` `CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPrecompProperty` `W_adj_unit_app`
`sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.HasColimitsOfShape` `Opposite` `Cover` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `instPreorderCover` `CategoryTheory.Limits.PreservesColimitsOfShape` `CategoryTheory.Limits.PreservesLimit` `Cover.shape` `CategoryTheory.Limits.MulticospanIndex.multicospan` `Cover.index` `CategoryTheory.types` `CategoryTheory.forget`	`CategoryTheory.Functor.map` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.plusPlusSheaf` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.types` `CategoryTheory.forget` `CategoryTheory.Limits.WalkingMulticospan` `Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.MulticospanIndex.multicospan` `Cover.index` `CategoryTheory.sheafCompose` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.NatTrans.app` `CategoryTheory.sheafComposeNatTrans` `CategoryTheory.plusPlusAdjunction` `CategoryTheory.Iso.inv` `sheafify` `sheafifyCompIso`	—	`CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `Equiv.injective` `HasSheafCompose.isSheaf` `sheafify_isSheaf` `CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv` `sheafifyCompIso_inv_eq_sheafifyLift` `toSheafify_sheafifyLift` `CategoryTheory.Category.comp_id` `CategoryTheory.sheafComposeNatTrans_fac`

CategoryTheory.GrothendieckTopology.PreservesSheafification

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.GrothendieckTopology.W` `CategoryTheory.MorphismProperty.inverseImage` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight`	—	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`composeAndSheafify` 📖	CompOp	8 math math: `adjunction_unit_app_hom`, `CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app`, `adjunction_counit_app_val`, `adjunction_unit_app_val`, `CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app`, `instIsLeftAdjointComposeAndSheafify`, `CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify`, `adjunction_counit_app_hom`

---

← Back to Index