Documentation Verification Report

Functors

📁 Source: Mathlib/Condensed/Functors.lean

Statistics

Metric	Count
Definitions `toCondensed`, `ulift`, `toCondensed`, `toCondensed`, `compHausToCondensed`, `compHausToCondensed'`, `profiniteToCondensed`, `stoneanToCondensed`	8
Theorems `instFaithfulCompHausCondensedSetCompHausToCondensed`, `instFaithfulCompHausCondensedTypeCompHausToCondensed'`, `instFaithfulCondensedTypeCondensedSetUlift`, `instFullCompHausCondensedSetCompHausToCondensed`, `instFullCompHausCondensedTypeCompHausToCondensed'`, `instFullCondensedTypeCondensedSetUlift`	6
Total	14

CompHaus

Definitions

Name	Category	Theorems
`toCondensed` 📖	CompOp	—

Condensed

Definitions

Name	Category	Theorems
`ulift` 📖	CompOp	2 math math: `instFaithfulCondensedTypeCondensedSetUlift`, `instFullCondensedTypeCondensedSetUlift`

Profinite

Definitions

Name	Category	Theorems
`toCondensed` 📖	CompOp	—

Stonean

Definitions

Name	Category	Theorems
`toCondensed` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`compHausToCondensed` 📖	CompOp	3 math math: `instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed`, `instFullCompHausCondensedSetCompHausToCondensed`, `instFaithfulCompHausCondensedSetCompHausToCondensed`
`compHausToCondensed'` 📖	CompOp	2 math math: `instFullCompHausCondensedTypeCompHausToCondensed'`, `instFaithfulCompHausCondensedTypeCompHausToCondensed'`
`profiniteToCondensed` 📖	CompOp	—
`stoneanToCondensed` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulCompHausCondensedSetCompHausToCondensed` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CompHaus` `CompHausLike.category` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `compHausToCondensed`	—	`CategoryTheory.Functor.Faithful.comp` `instFaithfulCompHausCondensedTypeCompHausToCondensed'` `instFaithfulCondensedTypeCondensedSetUlift`
`instFaithfulCompHausCondensedTypeCompHausToCondensed'` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CompHaus` `CompHausLike.category` `Condensed` `CategoryTheory.types` `instCategoryCondensed` `compHausToCondensed'`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular` `CategoryTheory.coherentTopology.subcanonical` `CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda`
`instFaithfulCondensedTypeCondensedSetUlift` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Condensed` `CategoryTheory.types` `instCategoryCondensed` `CondensedSet` `Condensed.ulift`	—	`CategoryTheory.instFaithfulSheafSheafCompose` `CategoryTheory.uliftFunctor_faithful`
`instFullCompHausCondensedSetCompHausToCondensed` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CompHaus` `CompHausLike.category` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `compHausToCondensed`	—	`CategoryTheory.Functor.Full.comp` `instFullCompHausCondensedTypeCompHausToCondensed'` `instFullCondensedTypeCondensedSetUlift`
`instFullCompHausCondensedTypeCompHausToCondensed'` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CompHaus` `CompHausLike.category` `Condensed` `CategoryTheory.types` `instCategoryCondensed` `compHausToCondensed'`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular` `CategoryTheory.coherentTopology.subcanonical` `CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda`
`instFullCondensedTypeCondensedSetUlift` 📖	mathematical	—	`CategoryTheory.Functor.Full` `Condensed` `CategoryTheory.types` `instCategoryCondensed` `CondensedSet` `Condensed.ulift`	—	`CategoryTheory.instFullSheafSheafComposeOfFaithful` `CategoryTheory.uliftFunctor_full` `CategoryTheory.uliftFunctor_faithful`

---

← Back to Index