ExtraDegeneracy

📁 Source: Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

Statistics

Metric	Count
Definitions s, extraDegeneracy, ExtraDegeneracy, const, homotopyEquiv, map, ofIso, s, s', extraDegeneracy, shift, shiftFun	12
Theorems s_comp_base, s_comp_π_0, s_comp_π_succ, 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, s₀_comp_δ₁, s₀_comp_δ₁_assoc, nonempty_extraDegeneracy_stdSimplex, shiftFun_succ, shiftFun_zero	20
Total	32

CategoryTheory.Arrow.AugmentedCechNerve

Definitions

Name	Category	Theorems
extraDegeneracy 📖	CompOp	—

CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy

Definitions

Name	Category	Theorems
s 📖	CompOp	3 math math: s_comp_base, 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.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Arrow.cechNerve Opposite.op s CategoryTheory.Limits.WidePullback.base SimplexCategory.len Opposite.unop	—	CategoryTheory.Limits.WidePullback.lift_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.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Arrow.cechNerve Opposite.op s CategoryTheory.Limits.WidePullback.π SimplexCategory.len Opposite.unop SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat CategoryTheory.Limits.widePullback CategoryTheory.Limits.WidePullback.base CategoryTheory.SplitEpi.section_	—	CategoryTheory.Limits.limit.lift_π
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.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Arrow.cechNerve Opposite.op s CategoryTheory.Limits.WidePullback.π	—	CategoryTheory.Limits.limit.lift_π

CategoryTheory.SimplicialObject.Augmented

Definitions

Name	Category	Theorems
ExtraDegeneracy 📖	CompData	1 math math: SSet.Augmented.StandardSimplex.nonempty_extraDegeneracy_stdSimplex

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	6 math math: s'_comp_ε, const_s', ext_iff, s₀_comp_δ₁_assoc, s₀_comp_δ₁, s'_comp_ε_assoc

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.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop 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.SimplicialObject.Augmented.point	—	—
ext 📖	—	s' s	—	—	—
ext_iff 📖	mathematical	—	s' s	—	ext
s'_comp_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject.Augmented.point Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Functor.id s' CategoryTheory.NatTrans.app CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
s'_comp_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject.Augmented.point Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op s' CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Comma.left 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.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const s CategoryTheory.SimplicialObject.δ	—	—
s_comp_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op s CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const 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.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const 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.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op s CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const 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.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const s CategoryTheory.SimplicialObject.σ	—	—
s_comp_σ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op s CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const 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.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const 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.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop Opposite.op s CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const 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