Documentation Verification Report

LocallyBijective

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

Statistics

Metric	Count
Definitions `WEqualsLocallyBijective`	1
Theorems `isLocallyInjective`, `isLocallySurjective`, `iff`, `mk'`, `W_iff_isLocallyBijective`, `W_of_isLocallyBijective`, `instIsLocallyInjectiveToSheafify`, `instIsLocallySurjectiveToSheafify`, `instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget`, `instWEqualsLocallyBijectiveTypeHom`, `isLocallyInjective_presheafToSheaf_map_iff`, `isLocallySurjective_presheafToSheaf_map_iff`, `isLocallyBijective_iff_isIso`	13
Total	14

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`WEqualsLocallyBijective` 📖	CompData	6 math math: `instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget`, `WEqualsLocallyBijective.ofEssentiallySmall`, `WEqualsLocallyBijective.mk'`, `LightProfinite.instWEqualsLocallyBijectiveCoherentTopology`, `WEqualsLocallyBijective.transport`, `instWEqualsLocallyBijectiveTypeHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`W_iff_isLocallyBijective` 📖	mathematical	—	`W` `CategoryTheory.Presheaf.IsLocallyInjective` `CategoryTheory.Presheaf.IsLocallySurjective`	—	`WEqualsLocallyBijective.iff`
`W_of_isLocallyBijective` 📖	mathematical	—	`W`	—	`W_iff_isLocallyBijective`
`instIsLocallyInjectiveToSheafify` 📖	mathematical	—	`CategoryTheory.Presheaf.IsLocallyInjective` `CategoryTheory.sheafify` `CategoryTheory.toSheafify`	—	`W.isLocallyInjective` `W_toSheafify`
`instIsLocallySurjectiveToSheafify` 📖	mathematical	—	`CategoryTheory.Presheaf.IsLocallySurjective` `CategoryTheory.sheafify` `CategoryTheory.toSheafify`	—	`W.isLocallySurjective` `W_toSheafify`
`instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget` 📖	mathematical	—	`WEqualsLocallyBijective`	—	`WEqualsLocallyBijective.mk'` `CategoryTheory.Presheaf.isLocallyInjective_toSheafify'` `CategoryTheory.Presheaf.isLocallySurjective_toSheafify'`
`instWEqualsLocallyBijectiveTypeHom` 📖	mathematical	—	`WEqualsLocallyBijective` `CategoryTheory.types` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory`	—	`instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.instHasSheafifyType` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Functor.corepresentable_preservesLimit` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms` `CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `UnivLE.small` `UnivLE.self` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.Limits.Types.hasLimitsOfShape` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.Types.instFullForgetTypeHom` `CategoryTheory.instFaithfulForget`

CategoryTheory.GrothendieckTopology.W

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocallyInjective` 📖	mathematical	`CategoryTheory.GrothendieckTopology.W`	`CategoryTheory.Presheaf.IsLocallyInjective`	—	`CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective`
`isLocallySurjective` 📖	mathematical	`CategoryTheory.GrothendieckTopology.W`	`CategoryTheory.Presheaf.IsLocallySurjective`	—	`CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective`

CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.W` `CategoryTheory.Presheaf.IsLocallyInjective` `CategoryTheory.Presheaf.IsLocallySurjective`	—	—
`mk'` 📖	mathematical	`CategoryTheory.Presheaf.IsLocallyInjective` `CategoryTheory.sheafify` `CategoryTheory.toSheafify` `CategoryTheory.Presheaf.IsLocallySurjective`	`CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective`	—	`CategoryTheory.GrothendieckTopology.W_iff` `CategoryTheory.Sheaf.isLocallyBijective_iff_isIso` `CategoryTheory.Presheaf.isLocallyInjective_comp_iff` `CategoryTheory.Presheaf.isLocallySurjective_comp_iff` `CategoryTheory.toSheafify_naturality` `CategoryTheory.Presheaf.comp_isLocallyInjective_iff` `CategoryTheory.Presheaf.comp_isLocallySurjective_iff`

CategoryTheory.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocallyInjective_presheafToSheaf_map_iff` 📖	mathematical	—	`CategoryTheory.Sheaf.IsLocallyInjective` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.presheafToSheaf` `CategoryTheory.Functor.map` `IsLocallyInjective`	—	`CategoryTheory.Sheaf.isLocallyInjective_sheafToPresheaf_map_iff` `isLocallyInjective_comp_iff` `CategoryTheory.GrothendieckTopology.instIsLocallyInjectiveToSheafify` `comp_isLocallyInjective_iff` `CategoryTheory.GrothendieckTopology.instIsLocallySurjectiveToSheafify` `CategoryTheory.toSheafify_naturality` `CategoryTheory.sheafToPresheaf_map`
`isLocallySurjective_presheafToSheaf_map_iff` 📖	mathematical	—	`CategoryTheory.Sheaf.IsLocallySurjective` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.presheafToSheaf` `CategoryTheory.Functor.map` `IsLocallySurjective`	—	`CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_map_iff` `isLocallySurjective_comp_iff` `CategoryTheory.GrothendieckTopology.instIsLocallyInjectiveToSheafify` `CategoryTheory.GrothendieckTopology.instIsLocallySurjectiveToSheafify` `comp_isLocallySurjective_iff` `CategoryTheory.toSheafify_naturality` `CategoryTheory.sheafToPresheaf_map`

CategoryTheory.Sheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocallyBijective_iff_isIso` 📖	mathematical	—	`IsLocallyInjective` `IsLocallySurjective` `CategoryTheory.IsIso` `CategoryTheory.Sheaf` `instCategorySheaf`	—	`CategoryTheory.isIso_iff_of_reflects_iso` `CategoryTheory.instReflectsIsomorphismsSheafSheafCompose` `isLocallyInjective_forget` `instIsLocallySurjectiveHomMapTypeSheafComposeForget` `isLocallyInjective_of_iso` `isLocallySurjective_of_iso`

---

← Back to Index