Documentation Verification Report

Free

📁 Source: Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

Statistics

Metric	Count
Definitions `free`, `freeCofan`, `freeFunctor`, `freeHomEquiv`, `freeMap`, `freeSection`, `isColimitFreeCofan`, `mapFree`, `ιFree`	9
Theorems `freeCofan_inj`, `freeFunctor_map`, `freeFunctor_obj`, `freeHomEquiv_comp_apply`, `freeHomEquiv_freeMap`, `freeHomEquiv_symm_comp`, `map_ιFree_mapFree_hom`, `map_ιFree_mapFree_hom_assoc`, `sectionMap_freeMap_freeSection`, `unitHomEquiv_symm_freeHomEquiv_apply`, `ιFree_freeMap`, `ιFree_freeMap_assoc`, `ιFree_mapFree_inv`, `ιFree_mapFree_inv_assoc`	14
Total	23

SheafOfModules

Definitions

Name	Category	Theorems
`free` 📖	CompOp	25 math math: `freeHomEquiv_freeMap`, `unitHomEquiv_symm_freeHomEquiv_apply`, `GeneratingSections.epi`, `ιFree_mapFree_inv_assoc`, `pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc`, `freeHomEquiv_symm_comp`, `sectionMap_freeMap_freeSection`, `pullbackObjFreeIso_hom_naturality_assoc`, `freeHomEquiv_comp_apply`, `ιFree_freeMap`, `freeFunctor_obj`, `ιFree_freeMap_assoc`, `Presentation.map_relations_I`, `ιFree_mapFree_inv`, `Presentation.mapRelations_mapGenerators`, `Presentation.of_isIso_relations`, `Presentation.mapRelations_mapGenerators_assoc`, `GeneratingSections.ofEpi_π`, `map_ιFree_mapFree_hom`, `pullbackObjFreeIso_hom_naturality`, `pullback_map_ιFree_comp_pullbackObjFreeIso_hom`, `map_ιFree_mapFree_hom_assoc`, `Presentation.IsFinite.finite_relations`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`, `Presentation.map_π_eq`
`freeCofan` 📖	CompOp	1 math math: `freeCofan_inj`
`freeFunctor` 📖	CompOp	2 math math: `freeFunctor_obj`, `freeFunctor_map`
`freeHomEquiv` 📖	CompOp	8 math math: `freeHomEquiv_freeMap`, `unitHomEquiv_symm_freeHomEquiv_apply`, `GeneratingSections.epi`, `freeHomEquiv_symm_comp`, `freeHomEquiv_comp_apply`, `Presentation.map_relations_I`, `relationsOfIsCokernelFree_s`, `generatorsOfIsCokernelFree_s`
`freeMap` 📖	CompOp	7 math math: `freeHomEquiv_freeMap`, `sectionMap_freeMap_freeSection`, `pullbackObjFreeIso_hom_naturality_assoc`, `ιFree_freeMap`, `freeFunctor_map`, `ιFree_freeMap_assoc`, `pullbackObjFreeIso_hom_naturality`
`freeSection` 📖	CompOp	2 math math: `freeHomEquiv_freeMap`, `sectionMap_freeMap_freeSection`
`isColimitFreeCofan` 📖	CompOp	—
`mapFree` 📖	CompOp	6 math math: `ιFree_mapFree_inv_assoc`, `Presentation.map_relations_I`, `ιFree_mapFree_inv`, `map_ιFree_mapFree_hom`, `map_ιFree_mapFree_hom_assoc`, `Presentation.map_π_eq`
`ιFree` 📖	CompOp	10 math math: `unitHomEquiv_symm_freeHomEquiv_apply`, `ιFree_mapFree_inv_assoc`, `pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc`, `ιFree_freeMap`, `ιFree_freeMap_assoc`, `ιFree_mapFree_inv`, `map_ιFree_mapFree_hom`, `pullback_map_ιFree_comp_pullbackObjFreeIso_hom`, `map_ιFree_mapFree_hom_assoc`, `freeCofan_inj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`freeCofan_inj` 📖	mathematical	—	`SheafOfModules` `instCategory` `unit` `freeCofan` `ιFree`	—	—
`freeFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.types` `SheafOfModules` `instCategory` `freeFunctor` `freeMap`	—	—
`freeFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.types` `SheafOfModules` `instCategory` `freeFunctor` `free`	—	—
`freeHomEquiv_comp_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `SheafOfModules` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `free` `EquivLike.toFunLike` `Equiv.instEquivLike` `freeHomEquiv` `CategoryTheory.CategoryStruct.comp` `sectionsMap`	—	—
`freeHomEquiv_freeMap` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `SheafOfModules` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `free` `EquivLike.toFunLike` `Equiv.instEquivLike` `freeHomEquiv` `freeMap` `sections` `freeSection`	—	`Equiv.injective` `Equiv.symm_apply_apply`
`freeHomEquiv_symm_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `free` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `freeHomEquiv` `sectionsMap`	—	`Equiv.injective` `PresheafOfModules.sections_ext` `Equiv.apply_symm_apply`
`map_ιFree_mapFree_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `unit` `free` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Functor.map` `ιFree` `CategoryTheory.Iso.hom` `mapFree`	—	`CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.hom_inv_id_assoc`
`map_ιFree_mapFree_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `unit` `free` `CategoryTheory.Functor.map` `ιFree` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Iso.hom` `mapFree`	—	`CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_ιFree_mapFree_hom`
`sectionMap_freeMap_freeSection` 📖	mathematical	—	`sectionsMap` `free` `freeMap` `freeSection`	—	`CategoryTheory.Category.id_comp` `freeHomEquiv_freeMap`
`unitHomEquiv_symm_freeHomEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `sections` `Quiver.Hom` `SheafOfModules` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `unit` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `unitHomEquiv` `free` `freeHomEquiv` `CategoryTheory.CategoryStruct.comp` `ιFree`	—	`Equiv.symm_apply_apply`
`ιFree_freeMap` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `unit` `free` `ιFree` `freeMap`	—	`unitHomEquiv_symm_freeHomEquiv_apply` `freeHomEquiv_freeMap` `CategoryTheory.Category.comp_id`
`ιFree_freeMap_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `unit` `free` `ιFree` `freeMap`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ιFree_freeMap`
`ιFree_mapFree_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `unit` `free` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Functor.obj` `ιFree` `CategoryTheory.Iso.inv` `mapFree` `CategoryTheory.Functor.map`	—	`CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.Category.assoc` `CategoryTheory.Equivalence.invFunIdAssoc_inv_app` `CategoryTheory.Discrete.functor_map_id` `CategoryTheory.Category.id_comp`
`ιFree_mapFree_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `unit` `free` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `AddCommGrpCat` `AddCommGrpCat.instCategory` `ιFree` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.inv` `mapFree` `CategoryTheory.Functor.map`	—	`CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ιFree_mapFree_inv`

---

← Back to Index