Documentation Verification Report

Horn

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

Statistics

Metric	Count
Definitions `horn`, `const`, `edge`, `edge₃`, `face`, `faceι`, `primitiveEdge`, `primitiveTriangle`, `ι`, `«termΛ[_,_]»`	10
Theorems `face_le_horn`, `const_val_apply`, `edge_coe`, `edge₃_coe_down`, `faceSingletonComplIso_inv_ι`, `faceSingletonComplIso_inv_ι_assoc`, `faceι_ι`, `faceι_ι_assoc`, `hom_ext`, `primitiveEdge_coe_down`, `primitiveTriangle_coe`, `yonedaEquiv_ι`, `ι_ι`, `ι_ι_assoc`, `horn_eq_iSup`, `horn_obj`, `horn_obj_zero`	17
Total	27

SSet

Definitions

Name	Category	Theorems
`horn` 📖	CompOp	59 math math: `horn₃₁.desc.multicofork_π_two`, `horn.faceSingletonComplIso_inv_ι_assoc`, `horn₃₁.exists_desc`, `horn.yonedaEquiv_ι`, `horn₃₂.desc.multicofork_π_one`, `horn₃₂.ι₁_desc`, `horn₂₂.sq`, `horn₃₁.ι₂_desc_assoc`, `horn₃₁.desc.multicofork_pt`, `horn.faceSingletonComplIso_inv_ι`, `horn₃₁.ι₃_desc_assoc`, `modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration`, `horn₃₁.desc.multicofork_π_two_assoc`, `horn.spineId_map_hornInclusion`, `horn₃₁.desc.multicofork_π_zero_assoc`, `horn_obj`, `modelCategoryQuillen.horn_ι_mem_J`, `horn₂₀.sq`, `horn₃₂.exists_desc`, `horn.edge_coe`, `horn₃₁.ι₂_desc`, `horn₃₂.ι₃_desc`, `horn₃₂.ι₀_desc`, `face_le_horn`, `horn.faceι_ι`, `horn.edge₃_coe_down`, `horn₂₁.isPushout`, `horn_eq_iSup`, `horn₃₂.ι₁_desc_assoc`, `horn₃₂.desc.multicofork_π_zero_assoc`, `horn.faceι_ι_assoc`, `horn_obj_zero`, `horn.spineId_vertex_coe`, `horn.multicoequalizerDiagram`, `horn.spineId_arrow_coe`, `horn₃₁.desc.multicofork_π_three_assoc`, `horn₃₁.desc.multicofork_π_zero`, `horn₂₀.isPushout`, `Quasicategory.hornFilling`, `horn₃₂.desc.multicofork_π_three`, `horn₃₁.ι₀_desc_assoc`, `horn₃₂.desc.multicofork_pt`, `horn₂₂.isPushout`, `Quasicategory.hornFilling'`, `horn.primitiveEdge_coe_down`, `horn₃₁.ι₃_desc`, `horn.ι_ι_assoc`, `horn₃₂.desc.multicofork_π_zero`, `horn₃₂.desc.multicofork_π_three_assoc`, `horn₃₂.desc.multicofork_π_one_assoc`, `KanComplex.hornFilling`, `horn.ι_ι`, `horn₃₁.ι₀_desc`, `horn.const_val_apply`, `horn₃₁.desc.multicofork_π_three`, `horn₃₂.ι₃_desc_assoc`, `horn₂₁.sq`, `horn.primitiveTriangle_coe`, `horn₃₂.ι₀_desc_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`face_le_horn` 📖	mathematical	—	`Subcomplex` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `largeCategory` `stdSimplex` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `CategoryTheory.Category.opposite` `stdSimplex.face` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `horn`	—	`horn_eq_iSup` `le_iSup`
`horn_eq_iSup` 📖	mathematical	—	`horn` `iSup` `Subcomplex` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `largeCategory` `stdSimplex` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `Opposite` `CategoryTheory.Category.opposite` `stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Set.instMembership`	—	`CategoryTheory.Subfunctor.ext` `Set.ext` `Set.union_singleton` `CategoryTheory.Subfunctor.iSup_obj` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop`
`horn_obj` 📖	mathematical	—	`CategoryTheory.Subfunctor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.Functor.obj` `SSet` `largeCategory` `stdSimplex` `horn` `setOf` `CategoryTheory.types` `Set` `Set.instUnion` `Set.range` `SimplexCategory.len` `Opposite.unop` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `stdSimplex.asOrderHom` `Set.instSingletonSet` `Set.univ`	—	—
`horn_obj_zero` 📖	mathematical	—	`CategoryTheory.Subfunctor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.Functor.obj` `SSet` `largeCategory` `stdSimplex` `horn` `Opposite.op` `Top.top` `Set` `CategoryTheory.types` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	`Set.ext` `horn_eq_iSup` `CategoryTheory.Subfunctor.iSup_obj` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `Finset.card_le_card` `Eq.le` `LE.le.trans` `Fintype.card_fin` `Finset.card_le_two` `Finset.eq_univ_iff_forall` `Fintype.complete`

SSet.horn

Definitions

Name	Category	Theorems
`const` 📖	CompOp	1 math math: `const_val_apply`
`edge` 📖	CompOp	1 math math: `edge_coe`
`edge₃` 📖	CompOp	1 math math: `edge₃_coe_down`
`face` 📖	CompOp	1 math math: `yonedaEquiv_ι`
`faceι` 📖	CompOp	4 math math: `faceSingletonComplIso_inv_ι_assoc`, `faceSingletonComplIso_inv_ι`, `faceι_ι`, `faceι_ι_assoc`
`primitiveEdge` 📖	CompOp	1 math math: `primitiveEdge_coe_down`
`primitiveTriangle` 📖	CompOp	1 math math: `primitiveTriangle_coe`
`ι` 📖	CompOp	5 math math: `faceSingletonComplIso_inv_ι_assoc`, `yonedaEquiv_ι`, `faceSingletonComplIso_inv_ι`, `ι_ι_assoc`, `ι_ι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_val_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `Opposite.op` `SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.horn` `const`	—	—
`edge_coe` 📖	mathematical	`Finset.card` `Finset` `Finset.instInsert` `Finset.instSingleton`	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.horn` `edge` `SSet.stdSimplex.edge`	—	—
`edge₃_coe_down` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `Opposite.op` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.horn` `edge₃` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`faceSingletonComplIso_inv_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex` `SSet.stdSimplex.face` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `SSet.horn` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso` `ι` `faceι`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.hom_inv_id_assoc`
`faceSingletonComplIso_inv_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex` `SSet.stdSimplex.face` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso` `SSet.horn` `ι` `faceι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `faceSingletonComplIso_inv_ι`
`faceι_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex` `SSet.stdSimplex.face` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `SSet.horn` `faceι` `SSet.Subcomplex.ι`	—	—
`faceι_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex` `SSet.stdSimplex.face` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `SSet.horn` `faceι` `SSet.Subcomplex.ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `faceι_ι`
`hom_ext` 📖	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `SSet.horn` `Opposite.op` `face`	—	—	`CategoryTheory.Subfunctor.equalizer_eq_iff` `le_antisymm` `CategoryTheory.Subfunctor.equalizer_le` `SSet.horn_eq_iSup` `CategoryTheory.Subfunctor.mem_equalizer_iff`
`primitiveEdge_coe_down` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `Opposite.op` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.horn` `primitiveEdge` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`primitiveTriangle_coe` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.horn` `primitiveTriangle` `SSet.stdSimplex.triangle`	—	—
`yonedaEquiv_ι` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `SSet` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `SSet.yonedaEquiv` `ι` `face`	—	`ι.eq_1` `Equiv.apply_symm_apply`
`ι_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι` `SSet.Subcomplex.ι` `CategoryTheory.CosimplicialObject.δ`	—	`ι.eq_1` `face.eq_1` `Equiv.symm_apply_apply` `CategoryTheory.Subfunctor.lift_ι`
`ι_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι` `SSet.Subcomplex.ι` `CategoryTheory.CosimplicialObject.δ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_ι`

Simplicial

Definitions

Name	Category	Theorems
`«termΛ[_,_]»` 📖	CompOp	—

---

← Back to Index