Degenerate

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

Statistics

Metric	Count
Definitions degenerate, nonDegenerate, nonDegenerateEquivOfIso	3
Theorems degenerate_eq_top_iff, eq_top_iff_contains_nonDegenerate, iSup_ofSimplex_nonDegenerate_eq_top, le_iff_contains_nonDegenerate, mem_degenerate_iff, mem_nonDegenerate_iff, degenerate_app_apply, degenerate_eq_iUnion_range_σ, degenerate_iff_of_isIso, degenerate_iff_of_mono, degenerate_le_preimage, degenerate_zero, exists_nonDegenerate, image_degenerate_le, isIso_of_nonDegenerate, mem_degenerate_iff, mem_degenerate_iff_notMem_nonDegenerate, mem_nonDegenerate_iff_notMem_degenerate, mono_of_nonDegenerate, nonDegenerateEquivOfIso_apply_coe, nonDegenerateEquivOfIso_symm_apply_coe, nonDegenerate_iff_of_isIso, nonDegenerate_iff_of_mono, nondegenerate_zero, unique_nonDegenerate_dim, unique_nonDegenerate_map, unique_nonDegenerate_simplex, σ_mem_degenerate	28
Total	31

SSet

Definitions

Name	Category	Theorems
degenerate 📖	CompOp	17 math math: degenerate_eq_top_of_hasDimensionLT, degenerate_iff_of_mono, σ_mem_degenerate, Subcomplex.degenerate_eq_top_iff, mem_degenerate_iff_notMem_nonDegenerate, PartialOrder.mem_nerve_degenerate_of_eq, hasDimensionLT_iff, degenerate_le_preimage, degenerate_zero, Subcomplex.mem_degenerate_iff, degenerate_app_apply, mem_nonDegenerate_iff_notMem_degenerate, HasDimensionLT.degenerate_eq_top, mem_degenerate_iff, image_degenerate_le, degenerate_eq_iUnion_range_σ, degenerate_iff_of_isIso
nonDegenerate 📖	CompOp	40 math math: stdSimplex.mem_nonDegenerate_iff_strictMono, nonDegenerate_iff_of_mono, prodStdSimplex.nonDegenerateEquiv₁_snd, exists_nonDegenerate, nonDegenerateEquivOfIso_symm_apply_coe, Subcomplex.eq_top_iff_of_hasDimensionLT, mem_degenerate_iff_notMem_nonDegenerate, nonDegenerate_eq_bot_of_hasDimensionLT, Subcomplex.eq_top_iff_contains_nonDegenerate, instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite, PartialOrder.mem_nerve_nonDegenerate_iff_injective, stdSimplex.nonDegenerateEquiv_apply_apply, Subcomplex.mem_nonDegenerate_iff, mem_skeleton_obj_iff_of_nonDegenerate, skeleton_succ, Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, N.mk'_surjective, Subcomplex.le_iff_of_hasDimensionLT, stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, nonDegenerate_iff_of_isIso, prodStdSimplex.nonDegenerateEquiv₁_fst, Subcomplex.PairingCore.nonDegenerate₂, prodStdSimplex.le_orderHomOfSimplex, Subcomplex.le_iff_contains_nonDegenerate, mem_nonDegenerate_iff_notMem_degenerate, Subcomplex.N.mk_surjective, mem_skeletonOfMono_obj_iff_of_nonDegenerate, prodStdSimplex.nonDegenerate_iff_injective_objEquiv, prodStdSimplex.nonDegenerate_max_dim_iff, N.mk_surjective, nonDegenerateEquivOfIso_apply_coe, stdSimplex.mem_nonDegenerate_iff_mono, prodStdSimplex.strictMono_orderHomOfSimplex, N.nonDegenerate, prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, Subcomplex.PairingCore.nonDegenerate₁, nondegenerate_zero, stdSimplex.nonDegenerateEquiv_symm_apply_coe, skeletonOfMono_succ
nonDegenerateEquivOfIso 📖	CompOp	2 math math: nonDegenerateEquivOfIso_symm_apply_coe, nonDegenerateEquivOfIso_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degenerate_app_apply 📖	mathematical	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership degenerate	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership degenerate CategoryTheory.NatTrans.app	—	CategoryTheory.FunctorToTypes.naturality
degenerate_eq_iUnion_range_σ 📖	mathematical	—	degenerate Set.iUnion CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set.range CategoryTheory.SimplicialObject.σ	—	Set.ext mem_degenerate_iff SimplexCategory.eq_σ_comp_of_not_injective SimplexCategory.le_of_mono SimplexCategory.mono_iff_injective CategoryTheory.FunctorToTypes.map_comp_apply σ_mem_degenerate
degenerate_iff_of_isIso 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership degenerate CategoryTheory.NatTrans.app	—	CategoryTheory.IsIso.hom_inv_id degenerate_app_apply
degenerate_iff_of_mono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership degenerate CategoryTheory.NatTrans.app	—	degenerate_iff_of_isIso Subcomplex.instIsIsoToRangeOfMono Subcomplex.mem_degenerate_iff
degenerate_le_preimage 📖	mathematical	—	Set CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set.instHasSubset degenerate Set.preimage CategoryTheory.NatTrans.app	—	degenerate_app_apply
degenerate_zero 📖	mathematical	—	degenerate Set CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set.instEmptyCollection	—	Set.ext Nat.instCanonicallyOrderedAdd
exists_nonDegenerate 📖	mathematical	—	Quiver.Hom SimplexCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory CategoryTheory.Epi Set.Elem CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op nonDegenerate CategoryTheory.Functor.map Quiver.Hom.op Set Set.instMembership	—	CategoryTheory.instEpiId nondegenerate_zero CategoryTheory.FunctorToTypes.map_id_apply degenerate_eq_iUnion_range_σ CategoryTheory.epi_comp SimplexCategory.instEpiσ CategoryTheory.FunctorToTypes.map_comp_apply
image_degenerate_le 📖	mathematical	—	Set CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set.instHasSubset Set.image CategoryTheory.NatTrans.app degenerate	—	degenerate_le_preimage
isIso_of_nonDegenerate 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set Set.instMembership nonDegenerate	CategoryTheory.IsIso SimplexCategory SimplexCategory.smallCategory	—	mem_nonDegenerate_iff_notMem_degenerate not_le SimplexCategory.isIso_iff_of_epi le_antisymm SimplexCategory.len_le_of_epi
mem_degenerate_iff 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership degenerate Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Epi Set.range CategoryTheory.Functor.map Quiver.Hom.op	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations SimplexCategory.len_le_of_mono CategoryTheory.Limits.instMonoι SimplexCategory.instEpiFactorThruImage CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp CategoryTheory.Limits.image.fac
mem_degenerate_iff_notMem_nonDegenerate 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership degenerate nonDegenerate	—	—
mem_nonDegenerate_iff_notMem_degenerate 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership nonDegenerate degenerate	—	—
mono_of_nonDegenerate 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set Set.instMembership nonDegenerate	CategoryTheory.Mono SimplexCategory SimplexCategory.smallCategory	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations isIso_of_nonDegenerate SimplexCategory.instEpiFactorThruImage CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp CategoryTheory.Limits.image.fac CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Limits.instMonoι
nonDegenerateEquivOfIso_apply_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership nonDegenerate DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike nonDegenerateEquivOfIso CategoryTheory.NatTrans.app CategoryTheory.Iso.hom SSet CategoryTheory.Functor.category	—	—
nonDegenerateEquivOfIso_symm_apply_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership nonDegenerate DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm nonDegenerateEquivOfIso CategoryTheory.NatTrans.app CategoryTheory.Iso.inv SSet CategoryTheory.Functor.category	—	—
nonDegenerate_iff_of_isIso 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership nonDegenerate CategoryTheory.NatTrans.app	—	—
nonDegenerate_iff_of_mono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership nonDegenerate CategoryTheory.NatTrans.app	—	—
nondegenerate_zero 📖	mathematical	—	nonDegenerate Set.univ CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op	—	degenerate_zero Set.compl_empty
unique_nonDegenerate_dim 📖	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set Set.instMembership nonDegenerate	—	—	CategoryTheory.isSplitEpi_of_epi SimplexCategory.instSplitEpiCategory le_antisymm
unique_nonDegenerate_map 📖	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set Set.instMembership nonDegenerate	—	—	SimplexCategory.Hom.ext OrderHom.ext CategoryTheory.isSplitEpi_of_epi SimplexCategory.instSplitEpiCategory SimplexCategory.congr_toOrderHom_apply CategoryTheory.SplitEpi.id OrderHom.monotone LT.lt.le
unique_nonDegenerate_simplex 📖	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set Set.instMembership nonDegenerate	—	—	CategoryTheory.isSplitEpi_of_epi SimplexCategory.instSplitEpiCategory CategoryTheory.FunctorToTypes.map_id_apply
σ_mem_degenerate 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership degenerate CategoryTheory.SimplicialObject.σ	—	Set.mem_range_self

SSet.Subcomplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degenerate_eq_top_iff 📖	mathematical	—	SSet.degenerate toSSet Top.top Set CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op BooleanAlgebra.toTop Set.instBooleanAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra CategoryTheory.Subfunctor.obj	—	Set.ext mem_degenerate_iff Subtype.prop
eq_top_iff_contains_nonDegenerate 📖	mathematical	—	Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set CategoryTheory.Functor.obj CategoryTheory.types Opposite.op Set.instHasSubset SSet.nonDegenerate CategoryTheory.Subfunctor.obj	—	le_iff_contains_nonDegenerate
iSup_ofSimplex_nonDegenerate_eq_top 📖	mathematical	—	iSup SSet.Subcomplex Set.Elem CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op SSet.nonDegenerate ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor ofSimplex Set Set.instMembership Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff_contains_nonDegenerate CategoryTheory.Subfunctor.iSup_obj mem_ofSimplex_obj
le_iff_contains_nonDegenerate 📖	mathematical	—	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj SSet.nonDegenerate	—	SSet.exists_nonDegenerate CategoryTheory.Subfunctor.map mem_nonDegenerate_iff Subtype.prop
mem_degenerate_iff 📖	mathematical	—	Set.Elem CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op CategoryTheory.Subfunctor.obj Set toSSet Set.instMembership SSet.degenerate	—	SSet.mem_degenerate_iff CategoryTheory.isSplitEpi_of_epi SimplexCategory.instSplitEpiCategory CategoryTheory.IsSplitEpi.id CategoryTheory.FunctorToTypes.map_id_apply CategoryTheory.Subfunctor.map
mem_nonDegenerate_iff 📖	mathematical	—	Set.Elem CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op CategoryTheory.Subfunctor.obj Set toSSet Set.instMembership SSet.nonDegenerate	—	SSet.mem_nonDegenerate_iff_notMem_degenerate mem_degenerate_iff

---

← Back to Index