Documentation Verification Report

Explicit

📁 Source: Mathlib/Condensed/Light/Explicit.lean

Statistics

Metric	Count
Definitions `ofSheafLightProfinite`, `ofSheafLightProfinite`, `ofSheafLightProfinite`, `ofSheafForgetLightProfinite`, `ofSheafLightProfinite`	5
Theorems `equalizerCondition`, `instPreservesFiniteProductsOppositeLightProfiniteObjFunctorIsSheafCoherentTopology`, `ofSheafForgetLightProfinite_obj`, `ofSheafLightProfinite_obj`	4
Total	9

LightCondAb

Definitions

Name	Category	Theorems
`ofSheafLightProfinite` 📖	CompOp	—

LightCondMod

Definitions

Name	Category	Theorems
`ofSheafLightProfinite` 📖	CompOp	—

LightCondSet

Definitions

Name	Category	Theorems
`ofSheafLightProfinite` 📖	CompOp	—

LightCondensed

Definitions

Name	Category	Theorems
`ofSheafForgetLightProfinite` 📖	CompOp	1 math math: `ofSheafForgetLightProfinite_obj`
`ofSheafLightProfinite` 📖	CompOp	1 math math: `ofSheafLightProfinite_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equalizerCondition` 📖	mathematical	—	`CategoryTheory.regularTopology.EqualizerCondition` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `LightProfinite.instPreregular` `CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` `CompHausLike.instHasLimitWalkingCospanCospan` `LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `Subtype.totallyDisconnectedSpace` `Prod.totallyDisconnectedSpace` `LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology` `TopologicalSpace.Subtype.secondCountableTopology` `TopologicalSpace.instSecondCountableTopologyProd` `LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace` `CategoryTheory.ObjectProperty.FullSubcategory.property`
`instPreservesFiniteProductsOppositeLightProfiniteObjFunctorIsSheafCoherentTopology` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteProducts` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `LightProfinite.instPreregular` `CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` `CompHausLike.instHasLimitWalkingCospanCospan` `LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `Subtype.totallyDisconnectedSpace` `Prod.totallyDisconnectedSpace` `LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology` `TopologicalSpace.Subtype.secondCountableTopology` `TopologicalSpace.instSecondCountableTopologyProd` `LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace` `CategoryTheory.ObjectProperty.FullSubcategory.property`
`ofSheafForgetLightProfinite_obj` 📖	mathematical	`CategoryTheory.regularTopology.EqualizerCondition` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.types` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.forget`	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `ofSheafForgetLightProfinite`	—	—
`ofSheafLightProfinite_obj` 📖	mathematical	`CategoryTheory.regularTopology.EqualizerCondition` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology`	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `ofSheafLightProfinite`	—	—

---

← Back to Index