Documentation Verification Report

CompStruct

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/CompStruct.lean

Statistics

Metric	Count
Definitions `Edge`, `CompStruct`, `compId`, `idComp`, `map`, `mk`, `ofTruncated`, `simplex`, `toTruncated`, `edge`, `id`, `map`, `mk`, `mk'`, `ofTruncated`, `toTruncated`, `CompStruct`	17
Theorems `compId_simplex`, `d₀`, `d₁`, `d₂`, `exists_of_simplex`, `ext`, `ext_iff`, `idComp_simplex`, `map_simplex`, `mk_simplex`, `exists_of_simplex`, `ext`, `ext_iff`, `id_edge`, `map_edge`, `map_id`, `mk'_edge`, `mk_edge`, `ofTruncated_edge`, `src_eq`, `tgt_eq`, `toTruncated_edge`, `toTruncated_id`	23
Total	40

SSet

Definitions

Name	Category	Theorems
`Edge` 📖	CompOp	10 math math: `CategoryTheory.nerve.functorOfNerveMap_map`, `CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMap`, `CategoryTheory.nerve.homEquiv_apply`, `CategoryTheory.nerve.homEquiv_edgeMk`, `CategoryTheory.nerve.homEquiv_comp`, `CategoryTheory.nerve.mk₁_homEquiv_apply`, `CategoryTheory.nerve.homEquiv_id`, `Truncated.HomotopyCategory.descOfTruncation_map_homMk`, `CategoryTheory.nerve.edgeMk_surjective`, `CategoryTheory.nerve.homEquiv_symm_apply`

SSet.Edge

Definitions

Name	Category	Theorems
`CompStruct` 📖	CompOp	1 math math: `CategoryTheory.nerve.nonempty_compStruct_iff`
`edge` 📖	CompOp	20 math math: `CategoryTheory.nerve.edgeMk_edge`, `CompStruct.d₀`, `tgt_eq`, `CategoryTheory.nerve.homEquiv_apply`, `ofTruncated_edge`, `CategoryTheory.nerve.right_edge`, `mk_edge`, `ext_iff`, `CategoryTheory.nerve.left_edge`, `CategoryTheory.nerve.mk₁_homEquiv_apply`, `exists_of_simplex`, `mk'_edge`, `CompStruct.idComp_simplex`, `CompStruct.d₂`, `CompStruct.d₁`, `map_edge`, `CompStruct.compId_simplex`, `toTruncated_edge`, `id_edge`, `src_eq`
`id` 📖	CompOp	7 math math: `map_id`, `CategoryTheory.nerve.edgeMk_id`, `CompStruct.idComp_simplex`, `CategoryTheory.nerve.homEquiv_id`, `CompStruct.compId_simplex`, `toTruncated_id`, `id_edge`
`map` 📖	CompOp	4 math math: `map_id`, `CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMap`, `map_edge`, `CompStruct.map_simplex`
`mk` 📖	CompOp	—
`mk'` 📖	CompOp	1 math math: `mk'_edge`
`ofTruncated` 📖	CompOp	1 math math: `ofTruncated_edge`
`toTruncated` 📖	CompOp	3 math math: `CategoryTheory.nerve.functorOfNerveMap_map`, `toTruncated_id`, `toTruncated_edge`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_simplex` 📖	mathematical	—	`edge`	—	—
`ext` 📖	—	`edge`	—	—	`SSet.Truncated.Edge.ext`
`ext_iff` 📖	mathematical	—	`edge`	—	`ext`
`id_edge` 📖	mathematical	—	`edge` `id` `CategoryTheory.SimplicialObject.σ` `CategoryTheory.types`	—	—
`map_edge` 📖	mathematical	—	`edge` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `map`	—	—
`map_id` 📖	mathematical	—	`map` `id` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op`	—	`SSet.Truncated.Edge.map_id`
`mk'_edge` 📖	mathematical	—	`edge` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `mk'`	—	—
`mk_edge` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `CategoryTheory.SimplicialObject.δ`	`edge`	—	—
`ofTruncated_edge` 📖	mathematical	—	`edge` `ofTruncated` `SSet.Truncated.Edge.edge` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation`	—	—
`src_eq` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `edge`	—	`SSet.Truncated.Edge.src_eq`
`tgt_eq` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `edge`	—	`SSet.Truncated.Edge.tgt_eq`
`toTruncated_edge` 📖	mathematical	—	`SSet.Truncated.Edge.edge` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation` `toTruncated` `edge`	—	—
`toTruncated_id` 📖	mathematical	—	`toTruncated` `id` `SSet.Truncated.Edge.id` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation`	—	—

SSet.Edge.CompStruct

Definitions

Name	Category	Theorems
`compId` 📖	CompOp	1 math math: `compId_simplex`
`idComp` 📖	CompOp	1 math math: `idComp_simplex`
`map` 📖	CompOp	1 math math: `map_simplex`
`mk` 📖	CompOp	—
`ofTruncated` 📖	CompOp	—
`simplex` 📖	CompOp	9 math math: `d₀`, `exists_of_simplex`, `ext_iff`, `idComp_simplex`, `d₂`, `d₁`, `map_simplex`, `compId_simplex`, `mk_simplex`
`toTruncated` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compId_simplex` 📖	mathematical	—	`simplex` `SSet.Edge.id` `compId` `CategoryTheory.SimplicialObject.σ` `CategoryTheory.types` `SSet.Edge.edge`	—	—
`d₀` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `simplex` `SSet.Edge.edge`	—	`SSet.Truncated.Edge.CompStruct.d₀`
`d₁` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `simplex` `SSet.Edge.edge`	—	`SSet.Truncated.Edge.CompStruct.d₁`
`d₂` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `simplex` `SSet.Edge.edge`	—	`SSet.Truncated.Edge.CompStruct.d₂`
`exists_of_simplex` 📖	mathematical	—	`simplex`	—	`SSet.Truncated.Edge.CompStruct.exists_of_simplex`
`ext` 📖	—	`simplex`	—	—	`SSet.Truncated.Edge.CompStruct.ext`
`ext_iff` 📖	mathematical	—	`simplex`	—	`ext`
`idComp_simplex` 📖	mathematical	—	`simplex` `SSet.Edge.id` `idComp` `CategoryTheory.SimplicialObject.σ` `CategoryTheory.types` `SSet.Edge.edge`	—	—
`map_simplex` 📖	mathematical	—	`simplex` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `SSet.Edge.map` `map`	—	—
`mk_simplex` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `CategoryTheory.SimplicialObject.δ` `SSet.Edge.edge`	`simplex`	—	—

SSet.Truncated.Edge

Definitions

Name	Category	Theorems
`CompStruct` 📖	CompData	4 math math: `SSet.Truncated.Quasicategory₂.fill32`, `SSet.Truncated.Quasicategory₂.fill21`, `CompStruct.nonempty_iff`, `SSet.Truncated.Quasicategory₂.fill31`

---

← Back to Index