ExtraDegeneracy

📁 Source: Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

Statistics

Metric	Count
Definitions s, extraDegeneracy, const, homotopyEquiv, map, ofIso, s, s', section_, splitEpi, extraDegeneracy, shift, shiftFun	13
Theorems s_comp_base, s_comp_base_assoc, s_comp_π_0, s_comp_π_0_assoc, s_comp_π_succ, s_comp_π_succ_assoc, const_s, const_s', ext, ext_iff, s'_comp_ε, s'_comp_ε_assoc, s_comp_δ, s_comp_δ_assoc, s_comp_δ₀, s_comp_δ₀_assoc, s_comp_σ, s_comp_σ_assoc, section_app_comp_hom_app, section_app_comp_hom_app_assoc, section_app_op_mk_zero, section_comp_hom, s₀_comp_δ₁, s₀_comp_δ₁_assoc, nonempty_extraDegeneracy_stdSimplex, shiftFun_succ, shiftFun_zero	27
Total	40

CategoryTheory.Arrow.AugmentedCechNerve

Definitions

Name	Category	Theorems
extraDegeneracy 📖	CompOp	—

CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy

Definitions

Name	Category	Theorems
s 📖	CompOp	6 math math: s_comp_base, s_comp_π_0_assoc, s_comp_π_succ_assoc, s_comp_base_assoc, s_comp_π_0, s_comp_π_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
s_comp_base 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom Opposite.op SimplexCategory s CategoryTheory.Limits.WidePullback.base	—	CategoryTheory.Limits.WidePullback.lift_base
s_comp_base_assoc 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom Opposite.op SimplexCategory s CategoryTheory.Limits.WidePullback.base	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' s_comp_base
s_comp_π_0 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom Opposite.op SimplexCategory s CategoryTheory.Limits.WidePullback.π SimplexCategory.len Opposite.unop SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat CategoryTheory.Limits.WidePullback.base CategoryTheory.SplitEpi.section_	—	CategoryTheory.Limits.limit.lift_π
s_comp_π_0_assoc 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom Opposite.op SimplexCategory s CategoryTheory.Limits.WidePullback.π SimplexCategory.len Opposite.unop SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat CategoryTheory.Limits.WidePullback.base CategoryTheory.SplitEpi.section_	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' s_comp_π_0
s_comp_π_succ 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom Opposite.op SimplexCategory s CategoryTheory.Limits.WidePullback.π	—	CategoryTheory.Limits.limit.lift_π
s_comp_π_succ_assoc 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom Opposite.op SimplexCategory s CategoryTheory.Limits.WidePullback.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' s_comp_π_succ

CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy

Definitions

Name	Category	Theorems
const 📖	CompOp	2 math math: const_s', const_s
homotopyEquiv 📖	CompOp	—
map 📖	CompOp	—
ofIso 📖	CompOp	—
s 📖	CompOp	10 math math: s_comp_δ₀_assoc, s_comp_δ, ext_iff, s₀_comp_δ₁_assoc, s_comp_σ, s₀_comp_δ₁, s_comp_δ_assoc, s_comp_σ_assoc, s_comp_δ₀, const_s
s' 📖	CompOp	7 math math: s'_comp_ε, const_s', ext_iff, s₀_comp_δ₁_assoc, s₀_comp_δ₁, s'_comp_ε_assoc, section_app_op_mk_zero
section_ 📖	CompOp	4 math math: section_app_comp_hom_app, section_app_comp_hom_app_assoc, section_app_op_mk_zero, section_comp_hom
splitEpi 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_s 📖	mathematical	—	s CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject.Augmented.const const CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op	—	—
const_s' 📖	mathematical	—	s' CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject.Augmented.const const CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const	—	—
ext 📖	—	s' s	—	—	—
ext_iff 📖	mathematical	—	s' s	—	ext
s'_comp_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.Comma.left Opposite.op s' CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
s'_comp_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.Comma.left Opposite.op s' CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' s'_comp_ε
s_comp_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op s CategoryTheory.SimplicialObject.δ	—	—
s_comp_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op s CategoryTheory.SimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' s_comp_δ
s_comp_δ₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op s CategoryTheory.SimplicialObject.δ CategoryTheory.CategoryStruct.id	—	—
s_comp_δ₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op s CategoryTheory.SimplicialObject.δ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' s_comp_δ₀
s_comp_σ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op s CategoryTheory.SimplicialObject.σ	—	—
s_comp_σ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op s CategoryTheory.SimplicialObject.σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' s_comp_σ
section_app_comp_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.NatTrans.app section_ CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id s'_comp_ε
section_app_comp_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.NatTrans.app section_ CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' section_app_comp_hom_app
section_app_op_mk_zero 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left section_ Opposite.op s'	—	CategoryTheory.Limits.IsTerminal.from_self CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
section_comp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.SimplicialObject CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left section_ CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.SimplicialObject.hom_ext section_app_comp_hom_app
s₀_comp_δ₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op s CategoryTheory.SimplicialObject.δ CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom s'	—	—
s₀_comp_δ₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const Opposite.op s CategoryTheory.SimplicialObject.δ CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom s'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' s₀_comp_δ₁

SSet.Augmented.StandardSimplex

Definitions

Name	Category	Theorems
extraDegeneracy 📖	CompOp	—
shift 📖	CompOp	—
shiftFun 📖	CompOp	2 math math: shiftFun_succ, shiftFun_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_extraDegeneracy_stdSimplex 📖	mathematical	—	CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy CategoryTheory.types CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented SSet.Augmented.stdSimplex	—	—
shiftFun_succ 📖	mathematical	—	shiftFun	—	—
shiftFun_zero 📖	mathematical	—	shiftFun	—	—

---

← Back to Index