Basic

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean

Statistics

Metric	Count
Definitions FreeSimplexQuiver, homRel, len, mk, quiv, δ, σ, SimplexCategoryGenRel, degeneracies, faces, generators, len, mk, rec, toSimplexCategory, δ, σ, instCategorySimplexCategoryGenRel	18
Theorems ext, ext_iff, δ, σ, hom_induction, hom_induction', mk_len, multiplicativeClosure_isGenerator_eq_top, toSimplexCategory_len, toSimplexCategory_map_δ, toSimplexCategory_map_σ, toSimplexCategory_obj_mk, δ_comp_δ, δ_comp_δ_assoc, δ_comp_δ_nat, δ_comp_σ_of_gt, δ_comp_σ_of_gt_assoc, δ_comp_σ_of_le, δ_comp_σ_of_le_assoc, δ_comp_σ_self, δ_comp_σ_self_assoc, δ_comp_σ_succ, δ_comp_σ_succ_assoc, σ_comp_σ, σ_comp_σ_assoc, σ_comp_σ_nat	26
Total	44

FreeSimplexQuiver

Definitions

Name	Category	Theorems
homRel 📖	CompData	—
len 📖	CompOp	—
mk 📖	CompOp	—
quiv 📖	CompOp	—
δ 📖	CompOp	—
σ 📖	CompOp	—

SimplexCategoryGenRel

Definitions

Name	Category	Theorems
degeneracies 📖	CompData	—
faces 📖	CompData	—
generators 📖	CompOp	3 math math: multiplicativeClosure_isGenerator_eq_top, generators.σ, generators.δ
len 📖	CompOp	4 math math: toSimplexCategory_len, mk_len, eq_or_len_le_of_P_δ, ext_iff
mk 📖	CompOp	—
rec 📖	CompOp	—
toSimplexCategory 📖	CompOp	7 math math: toSimplexCategory_len, isSplitEpi_toSimplexCategory_map_of_P_σ, toSimplexCategory_map_σ, toSimplexCategory_obj_mk, simplicialEvalσ_of_isAdmissible, toSimplexCategory_map_δ, isSplitMono_toSimplexCategory_map_of_P_δ
δ 📖	CompOp	15 math math: δ_comp_δ_nat, δ_comp_σ_of_gt_assoc, δ_comp_σ_self, δ_comp_σ_of_gt, instIsSplitMonoδ, δ_comp_σ_succ, δ_comp_σ_of_le_assoc, P_δ.δ, δ_comp_σ_of_le, generators.δ, toSimplexCategory_map_δ, δ_comp_δ_assoc, δ_comp_σ_self_assoc, δ_comp_δ, δ_comp_σ_succ_assoc
σ 📖	CompOp	18 math math: σ_comp_σ, δ_comp_σ_of_gt_assoc, standardσ_simplicialInsert, σ_comp_σ_nat, δ_comp_σ_self, δ_comp_σ_of_gt, toSimplexCategory_map_σ, δ_comp_σ_succ, δ_comp_σ_of_le_assoc, P_σ.σ, instIsSplitEpiσ, standardσ_cons, σ_comp_σ_assoc, generators.σ, δ_comp_σ_of_le, δ_comp_σ_self_assoc, standardσ_cons_assoc, δ_comp_σ_succ_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	len	—	—	—
ext_iff 📖	mathematical	—	len	—	ext
hom_induction 📖	—	CategoryTheory.CategoryStruct.id SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel CategoryTheory.CategoryStruct.comp δ σ	—	—	CategoryTheory.Category.id_comp top_le_iff multiplicativeClosure_isGenerator_eq_top CategoryTheory.MorphismProperty.top_apply
hom_induction' 📖	—	CategoryTheory.CategoryStruct.id SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel CategoryTheory.CategoryStruct.comp δ σ	—	—	CategoryTheory.Category.comp_id top_le_iff multiplicativeClosure_isGenerator_eq_top CategoryTheory.MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure' CategoryTheory.MorphismProperty.top_apply
mk_len 📖	mathematical	—	len	—	—
multiplicativeClosure_isGenerator_eq_top 📖	mathematical	—	CategoryTheory.MorphismProperty.multiplicativeClosure SimplexCategoryGenRel instCategorySimplexCategoryGenRel generators Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	le_antisymm CategoryTheory.Quotient.induction CategoryTheory.Paths.induction CategoryTheory.MorphismProperty.id_mem CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities CategoryTheory.MorphismProperty.instIsMultiplicativeMultiplicativeClosure CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition generators.δ generators.σ
toSimplexCategory_len 📖	mathematical	—	SimplexCategory.len CategoryTheory.Functor.obj SimplexCategoryGenRel instCategorySimplexCategoryGenRel SimplexCategory SimplexCategory.smallCategory toSimplexCategory len	—	—
toSimplexCategory_map_δ 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategoryGenRel instCategorySimplexCategoryGenRel SimplexCategory SimplexCategory.smallCategory toSimplexCategory δ SimplexCategory.δ	—	—
toSimplexCategory_map_σ 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategoryGenRel instCategorySimplexCategoryGenRel SimplexCategory SimplexCategory.smallCategory toSimplexCategory σ SimplexCategory.σ	—	—
toSimplexCategory_obj_mk 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategoryGenRel instCategorySimplexCategoryGenRel SimplexCategory SimplexCategory.smallCategory toSimplexCategory	—	—
δ_comp_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ	—	CategoryTheory.Quotient.sound
δ_comp_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ
δ_comp_δ_nat 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ	—	δ_comp_δ
δ_comp_σ_of_gt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ σ	—	CategoryTheory.Quotient.sound
δ_comp_σ_of_gt_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_of_gt
δ_comp_σ_of_le 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ σ	—	CategoryTheory.Quotient.sound
δ_comp_σ_of_le_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_of_le
δ_comp_σ_self 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ σ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Quotient.sound
δ_comp_σ_self_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ σ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_self
δ_comp_σ_succ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ σ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Quotient.sound
δ_comp_σ_succ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel δ σ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_succ
σ_comp_σ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel σ	—	CategoryTheory.Quotient.sound
σ_comp_σ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' σ_comp_σ
σ_comp_σ_nat 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategoryGenRel CategoryTheory.Category.toCategoryStruct instCategorySimplexCategoryGenRel σ	—	σ_comp_σ

SimplexCategoryGenRel.generators

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
δ 📖	mathematical	—	SimplexCategoryGenRel.generators SimplexCategoryGenRel.δ	—	le_sup_left
σ 📖	mathematical	—	SimplexCategoryGenRel.generators SimplexCategoryGenRel.σ	—	le_sup_right

(root)

Definitions

Name	Category	Theorems
FreeSimplexQuiver 📖	CompOp	—
SimplexCategoryGenRel 📖	CompOp	35 math math: SimplexCategoryGenRel.σ_comp_σ, SimplexCategoryGenRel.standardσ_nil, SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top, SimplexCategoryGenRel.toSimplexCategory_len, SimplexCategoryGenRel.δ_comp_δ_nat, SimplexCategoryGenRel.δ_comp_σ_of_gt_assoc, SimplexCategoryGenRel.isSplitEpi_toSimplexCategory_map_of_P_σ, SimplexCategoryGenRel.standardσ_simplicialInsert, SimplexCategoryGenRel.σ_comp_σ_nat, SimplexCategoryGenRel.δ_comp_σ_self, SimplexCategoryGenRel.δ_comp_σ_of_gt, SimplexCategoryGenRel.instIsSplitMonoδ, SimplexCategoryGenRel.standardσ_comp_standardσ_assoc, SimplexCategoryGenRel.toSimplexCategory_map_σ, SimplexCategoryGenRel.δ_comp_σ_succ, SimplexCategoryGenRel.δ_comp_σ_of_le_assoc, SimplexCategoryGenRel.exists_P_σ_P_δ_factorization, SimplexCategoryGenRel.toSimplexCategory_obj_mk, SimplexCategoryGenRel.instIsSplitEpiσ, SimplexCategoryGenRel.standardσ_cons, SimplexCategoryGenRel.σ_comp_σ_assoc, SimplexCategoryGenRel.δ_comp_σ_of_le, SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible, SimplexCategoryGenRel.eq_or_len_le_of_P_δ, SimplexCategoryGenRel.toSimplexCategory_map_δ, SimplexCategoryGenRel.δ_comp_δ_assoc, SimplexCategoryGenRel.isSplitMono_P_δ, SimplexCategoryGenRel.isSplitEpi_P_σ, SimplexCategoryGenRel.δ_comp_σ_self_assoc, SimplexCategoryGenRel.standardσ_comp_standardσ, SimplexCategoryGenRel.δ_comp_δ, SimplexCategoryGenRel.standardσ_cons_assoc, SimplexCategoryGenRel.instHasFactorizationP_σP_δ, SimplexCategoryGenRel.δ_comp_σ_succ_assoc, SimplexCategoryGenRel.isSplitMono_toSimplexCategory_map_of_P_δ
instCategorySimplexCategoryGenRel 📖	CompOp	35 math math: SimplexCategoryGenRel.σ_comp_σ, SimplexCategoryGenRel.standardσ_nil, SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top, SimplexCategoryGenRel.toSimplexCategory_len, SimplexCategoryGenRel.δ_comp_δ_nat, SimplexCategoryGenRel.δ_comp_σ_of_gt_assoc, SimplexCategoryGenRel.isSplitEpi_toSimplexCategory_map_of_P_σ, SimplexCategoryGenRel.standardσ_simplicialInsert, SimplexCategoryGenRel.σ_comp_σ_nat, SimplexCategoryGenRel.δ_comp_σ_self, SimplexCategoryGenRel.δ_comp_σ_of_gt, SimplexCategoryGenRel.instIsSplitMonoδ, SimplexCategoryGenRel.standardσ_comp_standardσ_assoc, SimplexCategoryGenRel.toSimplexCategory_map_σ, SimplexCategoryGenRel.δ_comp_σ_succ, SimplexCategoryGenRel.δ_comp_σ_of_le_assoc, SimplexCategoryGenRel.exists_P_σ_P_δ_factorization, SimplexCategoryGenRel.toSimplexCategory_obj_mk, SimplexCategoryGenRel.instIsSplitEpiσ, SimplexCategoryGenRel.standardσ_cons, SimplexCategoryGenRel.σ_comp_σ_assoc, SimplexCategoryGenRel.δ_comp_σ_of_le, SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible, SimplexCategoryGenRel.eq_or_len_le_of_P_δ, SimplexCategoryGenRel.toSimplexCategory_map_δ, SimplexCategoryGenRel.δ_comp_δ_assoc, SimplexCategoryGenRel.isSplitMono_P_δ, SimplexCategoryGenRel.isSplitEpi_P_σ, SimplexCategoryGenRel.δ_comp_σ_self_assoc, SimplexCategoryGenRel.standardσ_comp_standardσ, SimplexCategoryGenRel.δ_comp_δ, SimplexCategoryGenRel.standardσ_cons_assoc, SimplexCategoryGenRel.instHasFactorizationP_σP_δ, SimplexCategoryGenRel.δ_comp_σ_succ_assoc, SimplexCategoryGenRel.isSplitMono_toSimplexCategory_map_of_P_δ

---

← Back to Index