Documentation Verification Report

Equivalence

📁 Source: Mathlib/Condensed/Equivalence.lean

Statistics

Metric	Count
Definitions `equivalence`, `equivalence`, `equivalence`, `stoneanToProfiniteEffectivePresentation`	4
Theorems `instEffectivelyEnoughStoneanProfiniteToProfinite`, `instPreservesEffectiveEpisStoneanProfiniteToProfinite`, `instReflectsEffectiveEpisStoneanProfiniteToProfinite`, `isSheafProfinite`, `isSheafStonean`	5
Total	9

Condensed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheafProfinite` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.StructuredArrow` `Opposite` `Profinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CompHaus` `CategoryTheory.Functor.op` `profiniteToCompHaus` `CategoryTheory.instCategoryStructuredArrow`	`CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier` `Profinite.instPreregular` `CategoryTheory.Functor.comp` `CategoryTheory.Sheaf.val`	—	`CategoryTheory.Sheaf.cond` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier` `Profinite.instPreregular`
`isSheafStonean` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.StructuredArrow` `Opposite` `Stonean` `CategoryTheory.Category.opposite` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `CompHaus` `CategoryTheory.Functor.op` `Stonean.toCompHaus` `CategoryTheory.instCategoryStructuredArrow`	`CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier` `Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier` `Stonean.instPreregular` `CategoryTheory.Functor.comp` `CategoryTheory.Sheaf.val`	—	`CategoryTheory.Sheaf.cond` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier` `Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier` `Stonean.instPreregular`

Condensed.ProfiniteCompHaus

Definitions

Name	Category	Theorems
`equivalence` 📖	CompOp	2 math math: `CondensedMod.isDiscrete_tfae`, `CondensedSet.isDiscrete_tfae`

Condensed.StoneanCompHaus

Definitions

Name	Category	Theorems
`equivalence` 📖	CompOp	—

Condensed.StoneanProfinite

Definitions

Name	Category	Theorems
`equivalence` 📖	CompOp	—
`stoneanToProfiniteEffectivePresentation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEffectivelyEnoughStoneanProfiniteToProfinite` 📖	mathematical	—	`CategoryTheory.Functor.EffectivelyEnough` `Stonean` `Profinite` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `TotallyDisconnectedSpace` `Stonean.toProfinite`	—	—
`instPreservesEffectiveEpisStoneanProfiniteToProfinite` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEffectiveEpis` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `Profinite` `TotallyDisconnectedSpace` `Stonean.toProfinite`	—	`List.TFAE.out` `Profinite.effectiveEpi_tfae` `Stonean.effectiveEpi_tfae`
`instReflectsEffectiveEpisStoneanProfiniteToProfinite` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsEffectiveEpis` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `Profinite` `TotallyDisconnectedSpace` `Stonean.toProfinite`	—	`List.TFAE.out` `Stonean.effectiveEpi_tfae` `Profinite.effectiveEpi_tfae`

---

← Back to Index