Documentation Verification Report

SingularSet

📁 Source: Mathlib/AlgebraicTopology/SingularSet.lean

Statistics

Metric	Count
Definitions `toTop`, `toTopSimplex`, `«term\|_\|»`, `toSSet`, `toSSetIsoConst`, `toSSetObjEquiv`, `sSetTopAdj`	7
Theorems `instIsLeftAdjointSSetTopCatToTop`, `instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex`, `instIsRightAdjointSSetTopCatToSSet`	3
Total	10

SSet

Definitions

Name	Category	Theorems
`toTop` 📖	CompOp	7 math math: `SimplexCategory.toTopHomeo_symm_naturality`, `instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex`, `SimplexCategory.toTopHomeo_naturality_apply`, `instIsLeftAdjointSSetTopCatToTop`, `sSetTopAdj_homEquiv_stdSimplex_zero`, `SimplexCategory.toTopHomeo_symm_naturality_apply`, `SimplexCategory.toTopHomeo_naturality`
`toTopSimplex` 📖	CompOp	1 math math: `instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex`

Simplicial

Definitions

Name	Category	Theorems
`«term\|_\|»` 📖	CompOp	—

TopCat

Definitions

Name	Category	Theorems
`toSSet` 📖	CompOp	13 math math: `SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ`, `sSetTopAdj_homEquiv_stdSimplex_zero`, `SSet.stdSimplex.δ_zero_toSSetObjI`, `toSSetObj₀Equiv_symm_apply`, `SSet.stdSimplex.toSSetObj_app_const_zero`, `SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc`, `toSSetObj₀Equiv_apply`, `SSet.stdSimplex.δ_one_toSSetObjI`, `instIsRightAdjointSSetTopCatToSSet`, `toSSet_map_const`, `SSet.stdSimplex.toSSetObj_app_const_one`, `SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ`, `SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc`
`toSSetIsoConst` 📖	CompOp	—
`toSSetObjEquiv` 📖	CompOp	2 math math: `toSSetObj₀Equiv_symm_apply`, `toSSetObj₀Equiv_apply`

(root)

Definitions

Name	Category	Theorems
`sSetTopAdj` 📖	CompOp	1 math math: `sSetTopAdj_homEquiv_stdSimplex_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLeftAdjointSSetTopCatToTop` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `TopCat` `TopCat.instCategory` `SSet.toTop`	—	`CategoryTheory.Adjunction.isLeftAdjoint`
`instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftKanExtension` `SimplexCategory` `TopCat` `SSet` `SimplexCategory.smallCategory` `TopCat.instCategory` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `SSet.toTop` `SSet.stdSimplex` `SimplexCategory.toTop` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.comp` `SSet.toTopSimplex`	—	—
`instIsRightAdjointSSetTopCatToSSet` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `TopCat` `TopCat.instCategory` `TopCat.toSSet`	—	`CategoryTheory.Adjunction.isRightAdjoint`

---

← Back to Index