Documentation Verification Report

Module

📁 Source: Mathlib/Condensed/Module.lean

Statistics

Metric	Count
Definitions `abForget`, `forget`, `free`, `freeAb`, `freeForgetAdjunction`, `setAbAdjunction`, `CondensedAb`, `CondensedMod`, `instAbelianCondensedMod`	9
Theorems `hom_naturality_apply`	1
Total	10

Condensed

Definitions

Name	Category	Theorems
`abForget` 📖	CompOp	—
`forget` 📖	CompOp	2 math math: `CondensedMod.isDiscrete_iff_isDiscrete_forget`, `CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`
`free` 📖	CompOp	—
`freeAb` 📖	CompOp	—
`freeForgetAdjunction` 📖	CompOp	—
`setAbAdjunction` 📖	CompOp	—

CondensedMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_naturality_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map`	—	`CategoryTheory.NatTrans.naturality_apply`

(root)

Definitions

Name	Category	Theorems
`CondensedAb` 📖	CompOp	—
`CondensedMod` 📖	CompOp	15 math math: `Condensed.instAB4StarCondensedMod`, `CondensedMod.IsSolid.isIso_solidification_map`, `Condensed.instAB5CondensedMod`, `CondensedMod.isDiscrete_tfae`, `CondensedMod.LocallyConstant.instFullModuleCatFunctor`, `CondensedMod.isDiscrete_iff_isDiscrete_forget`, `CondensedMod.epi_iff_surjective_on_stonean`, `instHasLimitsCondensedMod`, `Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit`, `instHasLimitsOfSizeCondensedMod`, `CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `CondensedMod.epi_iff_locallySurjective_on_compHaus`, `instHasColimitsCondensedMod`, `CondensedMod.LocallyConstant.instFaithfulModuleCatFunctor`, `Condensed.instAB4CondensedMod`
`instAbelianCondensedMod` 📖	CompOp	—

---

← Back to Index