Documentation Verification Report

Module

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

Statistics

Metric	Count
Definitions `LightCondAb`, `LightCondMod`, `forget`, `free`, `freeForgetAdjunction`, `instAbelianLightCondMod`	6
Theorems `hom_naturality_apply`, `forget_map_val_app`, `forget_obj_val_map`	3
Total	9

LightCondMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_naturality_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `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`

LightCondensed

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	8 math math: `ihomPoints_apply`, `forget_obj_val_map`, `LightCondMod.instPreservesEpimorphismsLightCondSetForget`, `forget_map_val_app`, `LightCondMod.instReflectsEpimorphismsLightCondSetForget`, `LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `ihomPoints_symm_apply`, `LightCondMod.isDiscrete_iff_isDiscrete_forget`
`free` 📖	CompOp	10 math math: `free_internallyProjective_iff_tensor_condition`, `ihomPoints_apply`, `ihomPoints_symm_comp`, `free_lightProfinite_internallyProjective_iff_tensor_condition`, `internallyProjective_iff_tensor_condition`, `free_lightProfinite_internallyProjective_iff_tensor_condition'`, `free_internallyProjective_iff_tensor_condition'`, `ihomPoints_symm_apply`, `ihom_map_val_app`, `internallyProjective_iff_tensor_condition'`
`freeForgetAdjunction` 📖	CompOp	2 math math: `ihomPoints_apply`, `ihomPoints_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_map_val_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.types` `CategoryTheory.Functor.comp` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.forget` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map` `LightCondMod` `instCategoryLightCondensed` `LightCondSet` `forget` `DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.ConcreteCategory.hom`	—	—
`forget_obj_val_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.Functor.obj` `LightCondMod` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `LightCondSet` `forget` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `CategoryTheory.ConcreteCategory.hom` `ModuleCat.instConcreteCategoryLinearMapIdCarrier`	—	—

(root)

Definitions

Name	Category	Theorems
`LightCondAb` 📖	CompOp	—
`LightCondMod` 📖	CompOp	26 math math: `LightCondensed.free_internallyProjective_iff_tensor_condition`, `LightCondensed.ihomPoints_apply`, `LightCondensed.forget_obj_val_map`, `LightCondensed.ihomPoints_symm_comp`, `LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition`, `LightCondMod.instPreservesEpimorphismsLightCondSetForget`, `LightCondMod.isDiscrete_tfae`, `LightCondensed.internallyProjective_iff_tensor_condition`, `LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim`, `LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition'`, `LightCondensed.forget_map_val_app`, `LightCondMod.instReflectsEpimorphismsLightCondSetForget`, `LightCondensed.free_internallyProjective_iff_tensor_condition'`, `LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `instHasLimitsOfSizeLightCondMod_1`, `LightCondMod.LocallyConstant.instFaithfulModuleCatFunctor`, `LightCondensed.ihomPoints_symm_apply`, `LightCondMod.LocallyConstant.instFullModuleCatFunctor`, `LightCondMod.epi_iff_locallySurjective_on_lightProfinite`, `LightCondensed.ihom_map_val_app`, `instHasFiniteLimitsLightCondMod`, `instHasLimitsOfSizeLightCondMod`, `LightCondensed.instCountableAB4StarLightCondMod`, `LightCondensed.internallyProjective_iff_tensor_condition'`, `LightCondensed.instIsGrothendieckAbelianLightCondMod`, `LightCondMod.isDiscrete_iff_isDiscrete_forget`
`instAbelianLightCondMod` 📖	CompOp	1 math math: `LightCondensed.instIsGrothendieckAbelianLightCondMod`

---

← Back to Index