Documentation Verification Report

ProdStdSimplex

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

Statistics

Metric	Count
Definitions `isoNerve`, `objEquiv`, `orderHomOfSimplex`	3
Theorems `instFiniteTensorObjObjSimplexCategoryStdSimplexMk`, `instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat`, `nonDegenerate_iff_injective_objEquiv`, `nonDegenerate_iff_strictMono_objEquiv`, `objEquiv_apply_fst`, `objEquiv_apply_snd`, `objEquiv_map_apply`, `objEquiv_naturality`, `objEquiv_δ_apply`, `orderHomOfSimplex_coe`, `strictMono_orderHomOfSimplex_iff`	11
Total	14

SSet.prodStdSimplex

Definitions

Name	Category	Theorems
`isoNerve` 📖	CompOp	—
`objEquiv` 📖	CompOp	8 math math: `objEquiv_apply_fst`, `strictMono_orderHomOfSimplex_iff`, `objEquiv_δ_apply`, `objEquiv_naturality`, `objEquiv_apply_snd`, `objEquiv_map_apply`, `nonDegenerate_iff_injective_objEquiv`, `nonDegenerate_iff_strictMono_objEquiv`
`orderHomOfSimplex` 📖	CompOp	2 math math: `orderHomOfSimplex_coe`, `strictMono_orderHomOfSimplex_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteTensorObjObjSimplexCategoryStdSimplexMk` 📖	mathematical	—	`SSet.Finite` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex`	—	`SSet.finite_of_hasDimensionLT` `instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat` `Subtype.finite` `SSet.instFiniteObjOppositeSimplexCategoryTensorObj` `SSet.stdSimplex.instFiniteObjOppositeSimplexCategory`
`instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat` 📖	mathematical	—	`SSet.HasDimensionLE` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex`	—	`Set.ext` `Fintype.card_le_of_injective` `StrictMono.injective` `strictMono_orderHomOfSimplex_iff` `nonDegenerate_iff_strictMono_objEquiv` `SSet.mem_nonDegenerate_iff_notMem_degenerate` `Fintype.card_fin` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`nonDegenerate_iff_injective_objEquiv` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `OrderHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv`	—	`SSet.nonDegenerate_iff_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `PartialOrder.mem_nerve_nonDegenerate_iff_injective` `Function.Injective.of_comp_iff` `ULift.down_injective`
`nonDegenerate_iff_strictMono_objEquiv` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate` `StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv`	—	`SSet.nonDegenerate_iff_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `PartialOrder.mem_nerve_nonDegenerate_iff_strictMono`
`objEquiv_apply_fst` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `OrderHom.instFunLike` `Equiv` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat`	—	—
`objEquiv_apply_snd` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `OrderHom.instFunLike` `Equiv` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat`	—	—
`objEquiv_map_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `OrderHom.instFunLike` `Equiv` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.len` `SimplexCategory.Hom.toOrderHom`	—	—
`objEquiv_naturality` 📖	mathematical	—	`OrderHom.comp` `SimplexCategory.len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `DFunLike.coe` `Equiv` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `OrderHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `SimplexCategory.Hom.toOrderHom` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`objEquiv_δ_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `OrderHom.instFunLike` `Equiv` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `CategoryTheory.SimplicialObject.δ` `Fin.succAbove`	—	—
`orderHomOfSimplex_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `orderHomOfSimplex` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `Opposite.op` `SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat`	—	—
`strictMono_orderHomOfSimplex_iff` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `orderHomOfSimplex` `Prod.instPreorder` `Equiv` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `SSet.largeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SSet.instCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv`	—	`Prod.lt_iff` `OrderHom.monotone` `Fin.castSucc_le_succ`

---

← Back to Index