Documentation Verification Report

Flasque

📁 Source: Mathlib/Topology/Sheaves/Flasque.lean

Statistics

Metric	Count
Definitions `IsFlasque`, `IsFlasque`, `Under`	3
Theorems `epi`, `pushforward_isFlasque`, `epi_of_shortExact`, `of_shortExact_of_isFlasque₁₂`, `pushforward_isFlasque`, `structured_arrows_elements_sheaf_chains_bounded`	6
Total	9

TopCat.Presheaf

Definitions

Name	Category	Theorems
`IsFlasque` 📖	CompData	1 math math: `IsFlasque.pushforward_isFlasque`

TopCat.Presheaf.IsFlasque

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.map`	—	—
`pushforward_isFlasque` 📖	mathematical	—	`TopCat.Presheaf.IsFlasque` `CategoryTheory.Functor.obj` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward`	—	`epi`

TopCat.Sheaf

Definitions

Name	Category	Theorems
`IsFlasque` 📖	MathDef	2 math math: `IsFlasque.pushforward_isFlasque`, `IsFlasque.of_shortExact_of_isFlasque₁₂`

TopCat.Sheaf.IsFlasque

Definitions

Name	Category	Theorems
`Under` 📖	CompOp	1 math math: `structured_arrows_elements_sheaf_chains_bounded`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_of_shortExact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `TopCat.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `TopCat.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `TopCat.Sheaf.instAbelian` `CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opens.grothendieckTopology` `AddCommGrpCat.hasLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `AddCommGrpCat.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf` `CategoryTheory.GrothendieckTopology.Cover.instInhabited` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `AddCommGrpCat.hasLimits` `AddCommGrpCat.instAbelian`	`CategoryTheory.Epi` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `Opens.grothendieckTopology` `CategoryTheory.ShortComplex.X₂` `TopCat.Sheaf` `TopCat.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `TopCat.Sheaf.instAbelian` `CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `AddCommGrpCat.hasLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `small_subtype` `small_Pi` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `AddCommGrpCat.hasColimitsOfShape` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf` `CategoryTheory.GrothendieckTopology.Cover.instInhabited` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `AddCommGrpCat.hasLimits` `AddCommGrpCat.instAbelian` `Opposite.op` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.NatTrans.app` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ShortComplex.g`	—	`CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `AddCommGrpCat.hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `univLE_of_max` `UnivLE.self` `AddCommGrpCat.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `AddCommGrpCat.hasLimits` `AddCommGrpCat.epi_iff_surjective` `exists_maximal_of_chains_bounded` `structured_arrows_elements_sheaf_chains_bounded` `CategoryTheory.leOfHom` `CategoryTheory.CategoryOfElements.map_snd` `TopCat.Sheaf.isLocallySurjective_iff_epi` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Functor.corepresentable_preservesLimit` `AddCommGrpCat.forget_isCorepresentable` `CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms` `AddCommGrpCat.hasLimitsOfShape` `CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `AddCommGrpCat.forget_commGrp_preserves_mono` `AddCommGrpCat.forget_commGrp_preserves_epi` `CategoryTheory.ShortComplex.ShortExact.epi_g` `TopCat.Presheaf.isLocallySurjective_iff` `inf_le_left` `inf_le_right` `map_sub` `AddMonoidHom.instAddMonoidHomClass` `TopCat.Presheaf.map_restrict` `TopCat.Presheaf.restrictOpen.congr_simp` `TopCat.Presheaf.restrict_restrict` `sub_self` `TopCat.Sheaf.sections_exact_of_left_exact` `CategoryTheory.ShortComplex.ShortExact.exact` `CategoryTheory.ShortComplex.ShortExact.mono_f` `TopCat.Presheaf.IsFlasque.epi` `TopCat.Presheaf.restrict_sum` `add_sub_cancel` `TopCat.Sheaf.existsUnique_gluing` `le_of_eq` `inf_comm` `iSup_le_iff` `TopCat.Sheaf.eq_app_of_locally_eq` `map_add` `AddMonoidHomClass.toAddHomClass` `CategoryTheory.NatTrans.comp_app` `CategoryTheory.ObjectProperty.FullSubcategory.comp_hom` `CategoryTheory.ShortComplex.zero` `add_zero` `le_iSup` `TopCat.Presheaf.restrict_self`
`of_shortExact_of_isFlasque₁₂` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `TopCat.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `TopCat.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `TopCat.Sheaf.instAbelian` `CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opens.grothendieckTopology` `AddCommGrpCat.hasLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `AddCommGrpCat.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf` `CategoryTheory.GrothendieckTopology.Cover.instInhabited` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `AddCommGrpCat.hasLimits` `AddCommGrpCat.instAbelian`	`TopCat.Sheaf.IsFlasque` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.ShortComplex.X₃` `TopCat.Sheaf` `TopCat.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `TopCat.Sheaf.instAbelian` `CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opens.grothendieckTopology` `AddCommGrpCat.hasLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `AddCommGrpCat.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf` `CategoryTheory.GrothendieckTopology.Cover.instInhabited` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `AddCommGrpCat.hasLimits` `AddCommGrpCat.instAbelian`	—	`CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `AddCommGrpCat.hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `univLE_of_max` `UnivLE.self` `AddCommGrpCat.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `AddCommGrpCat.hasLimits` `CategoryTheory.NatTrans.naturality` `CategoryTheory.epi_comp'` `TopCat.Presheaf.IsFlasque.epi` `epi_of_shortExact` `CategoryTheory.epi_of_epi`
`pushforward_isFlasque` 📖	mathematical	—	`TopCat.Sheaf.IsFlasque` `CategoryTheory.Functor.obj` `TopCat.Sheaf` `TopCat.instCategorySheaf` `TopCat.Sheaf.pushforward`	—	`TopCat.Presheaf.IsFlasque.pushforward_isFlasque`
`structured_arrows_elements_sheaf_chains_bounded` 📖	mathematical	`IsChain` `Under` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.Elements` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.comp` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `Opens.grothendieckTopology` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.categoryOfElements` `CategoryTheory.Functor.obj` `Opposite.op` `CategoryTheory.NatTrans.mapElements` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	`Under` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.Elements` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.comp` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `Opens.grothendieckTopology` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.categoryOfElements` `CategoryTheory.Functor.obj` `Opposite.op` `CategoryTheory.NatTrans.mapElements` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	`TopCat.Sheaf.existsUnique_gluing` `AddCommGrpCat.hasLimits` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.CategoryOfElements.map_snd` `iSup_le` `CategoryTheory.leOfHom` `le_iSup` `TopCat.Sheaf.eq_app_of_locally_eq`

---

← Back to Index