Documentation Verification Report

ProdStdSimplex

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

Statistics

Metric	Count
Definitions `isoNerve`, `objEquiv`, `orderHomOfSimplex`	3
Theorems `instFiniteTensorObjObjSimplexCategoryStdSimplexMk`, `instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat`, `le_orderHomOfSimplex`, `nonDegenerate_ext₁`, `nonDegenerate_ext₂`, `nonDegenerate_iff_injective_objEquiv`, `nonDegenerate_iff_strictMono_objEquiv`, `nonDegenerate_max_dim_iff`, `objEquiv_apply_fst`, `objEquiv_apply_snd`, `objEquiv_map_apply`, `objEquiv_naturality`, `objEquiv_δ_apply`, `orderHomOfSimplex_coe`, `strictMono_orderHomOfSimplex`, `strictMono_orderHomOfSimplex_iff`	16
Total	19

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	5 math math: `orderHomOfSimplex_coe`, `strictMono_orderHomOfSimplex_iff`, `le_orderHomOfSimplex`, `nonDegenerate_max_dim_iff`, `strictMono_orderHomOfSimplex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteTensorObjObjSimplexCategoryStdSimplexMk` 📖	mathematical	—	`SSet.Finite` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `SSet.stdSimplex`	—	`SSet.finite_of_hasDimensionLT` `instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat` `Subtype.finite` `SSet.instFiniteObjOppositeSimplexCategoryTensorObj` `SSet.stdSimplex.instFiniteObjOppositeSimplexCategory`
`instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat` 📖	mathematical	—	`SSet.HasDimensionLE` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `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` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le`
`le_orderHomOfSimplex` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `orderHomOfSimplex` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate`	—	`Nat.instCanonicallyOrderedAdd` `lt_of_le_of_lt` `strictMono_orderHomOfSimplex`
`nonDegenerate_ext₁` 📖	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `Set` `Set.instMembership` `SSet.nonDegenerate`	—	—	`Equiv.injective` `OrderHom.ext` `DFunLike.congr_fun` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `nonDegenerate_max_dim_iff`
`nonDegenerate_ext₂` 📖	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `Set` `Set.instMembership` `SSet.nonDegenerate`	—	—	`Equiv.injective` `nonDegenerate_ext₁`
`nonDegenerate_iff_injective_objEquiv` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `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` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `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`
`nonDegenerate_max_dim_iff` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate` `orderHomOfSimplex` `OrderHom.id` `PartialOrder.toPreorder` `Fin.instPartialOrder`	—	`OrderHom.eq_id_of_injective` `Finite.of_fintype` `StrictMono.injective` `strictMono_orderHomOfSimplex` `nonDegenerate_iff_injective_objEquiv`
`objEquiv_apply_fst` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `OrderHom.instFunLike` `Equiv` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.types` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `EquivLike.toFunLike` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `Equiv.instEquivLike` `objEquiv` `SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat`	—	—
`objEquiv_apply_snd` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Prod.instPreorder` `OrderHom.instFunLike` `Equiv` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.types` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `EquivLike.toFunLike` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `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` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `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` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `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` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `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` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat`	—	—
`strictMono_orderHomOfSimplex` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `orderHomOfSimplex` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `Set` `Set.instMembership` `SSet.nonDegenerate`	—	—
`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` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.stdSimplex` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv`	—	`Prod.lt_iff` `OrderHom.monotone` `Fin.castSucc_le_succ`

---

← Back to Index