HornColimits

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

Statistics

Metric	Count
Definitions isColimit, ι₀₁, ι₀₂, ι₀₁, ι₁₂, ι₀₂, ι₁₂, desc, multicofork, ι₀, ι₂, ι₃, desc, multicofork, ι₀, ι₁, ι₃	17
Theorems multicoequalizerDiagram, isPushout, sq, isPushout, sq, isPushout, sq, multicofork_pt, multicofork_π_three, multicofork_π_three_assoc, multicofork_π_two, multicofork_π_two_assoc, multicofork_π_zero, multicofork_π_zero_assoc, exists_desc, ι₀_desc, ι₀_desc_assoc, ι₂_desc, ι₂_desc_assoc, ι₃_desc, ι₃_desc_assoc, multicofork_pt, multicofork_π_one, multicofork_π_one_assoc, multicofork_π_three, multicofork_π_three_assoc, multicofork_π_zero, multicofork_π_zero_assoc, exists_desc, ι₀_desc, ι₀_desc_assoc, ι₁_desc, ι₁_desc_assoc, ι₃_desc, ι₃_desc_assoc	35
Total	52

SSet.horn

Definitions

Name	Category	Theorems
isColimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multicoequalizerDiagram 📖	mathematical	—	SSet.Subcomplex.MulticoequalizerDiagram CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex SSet.horn Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Set.instMembership Finset.instInsert	—	SSet.horn_eq_iSup SSet.stdSimplex.face_inter_face Finset.compl_insert Finset.ext

SSet.horn₂₀

Definitions

Name	Category	Theorems
ι₀₁ 📖	CompOp	1 math math: isPushout
ι₀₂ 📖	CompOp	1 math math: isPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPushout 📖	mathematical	—	CategoryTheory.IsPushout SSet SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet SSet.horn CategoryTheory.CosimplicialObject.δ ι₀₁ ι₀₂	—	CategoryTheory.IsPushout.of_iso' Lattice.BicartSq.le₁₂ sq Lattice.BicartSq.le₁₃ Lattice.BicartSq.le₂₄ Lattice.BicartSq.le₃₄ SSet.Subcomplex.BicartSq.isPushout
sq 📖	mathematical	—	SSet.Subcomplex.BicartSq CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex SSet.stdSimplex.face Finset Finset.instSingleton Finset.instInsert SSet.horn	—	le_antisymm sup_le_iff SSet.face_le_horn Nat.instCharZero Nat.instAtLeastTwoHAddOfNat SSet.horn_eq_iSup iSup_le_iff Fintype.complete le_sup_right le_sup_left SSet.stdSimplex.face_inter_face Finset.inter_insert_of_mem Finset.inter_singleton_of_notMem Finset.instLawfulSingleton

SSet.horn₂₁

Definitions

Name	Category	Theorems
ι₀₁ 📖	CompOp	1 math math: isPushout
ι₁₂ 📖	CompOp	1 math math: isPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPushout 📖	mathematical	—	CategoryTheory.IsPushout SSet SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet SSet.horn CategoryTheory.CosimplicialObject.δ ι₀₁ ι₁₂	—	CategoryTheory.IsPushout.of_iso' Lattice.BicartSq.le₁₂ sq Lattice.BicartSq.le₁₃ Lattice.BicartSq.le₂₄ Lattice.BicartSq.le₃₄ SSet.Subcomplex.BicartSq.isPushout
sq 📖	mathematical	—	SSet.Subcomplex.BicartSq CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex SSet.stdSimplex.face Finset Finset.instSingleton Finset.instInsert SSet.horn	—	le_antisymm sup_le_iff SSet.face_le_horn Nat.instCharZero Nat.instAtLeastTwoHAddOfNat SSet.horn_eq_iSup iSup_le_iff Fintype.complete le_sup_right le_sup_left SSet.stdSimplex.face_inter_face Finset.inter_insert_of_mem Finset.inter_singleton_of_notMem Finset.instLawfulSingleton

SSet.horn₂₂

Definitions

Name	Category	Theorems
ι₀₂ 📖	CompOp	1 math math: isPushout
ι₁₂ 📖	CompOp	1 math math: isPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPushout 📖	mathematical	—	CategoryTheory.IsPushout SSet SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.Subcomplex.toSSet SSet.horn CategoryTheory.CosimplicialObject.δ ι₀₂ ι₁₂	—	CategoryTheory.IsPushout.of_iso' Lattice.BicartSq.le₁₂ sq Lattice.BicartSq.le₁₃ Lattice.BicartSq.le₂₄ Lattice.BicartSq.le₃₄ SSet.Subcomplex.BicartSq.isPushout
sq 📖	mathematical	—	SSet.Subcomplex.BicartSq CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet SSet.largeCategory SSet.stdSimplex SSet.stdSimplex.face Finset Finset.instSingleton Finset.instInsert SSet.horn	—	le_antisymm sup_le_iff SSet.face_le_horn SSet.horn_eq_iSup iSup_le_iff Fintype.complete le_sup_right le_sup_left SSet.stdSimplex.face_inter_face Finset.inter_insert_of_notMem Nat.instCharZero Nat.instAtLeastTwoHAddOfNat Finset.inter_singleton_of_mem

SSet.horn₃₁

Definitions

Name	Category	Theorems
desc 📖	CompOp	6 math math: ι₂_desc_assoc, ι₃_desc_assoc, ι₂_desc, ι₀_desc_assoc, ι₃_desc, ι₀_desc
ι₀ 📖	CompOp	3 math math: exists_desc, ι₀_desc_assoc, ι₀_desc
ι₂ 📖	CompOp	3 math math: exists_desc, ι₂_desc_assoc, ι₂_desc
ι₃ 📖	CompOp	3 math math: exists_desc, ι₃_desc_assoc, ι₃_desc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₀ ι₂ ι₃	—	ι₀_desc ι₂_desc ι₃_desc
ι₀_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₀ desc	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc SSet.horn.faceSingletonComplIso_inv_ι CategoryTheory.Limits.IsColimit.fac SSet.horn.multicoequalizerDiagram Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
ι₀_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₀ desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_desc
ι₂_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₂ desc	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc SSet.horn.faceSingletonComplIso_inv_ι CategoryTheory.Limits.IsColimit.fac SSet.horn.multicoequalizerDiagram
ι₂_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₂ desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₂_desc
ι₃_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₃ desc	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc SSet.horn.faceSingletonComplIso_inv_ι CategoryTheory.Limits.IsColimit.fac SSet.horn.multicoequalizerDiagram
ι₃_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₃ desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₃_desc

SSet.horn₃₁.desc

Definitions

Name	Category	Theorems
multicofork 📖	CompOp	7 math math: multicofork_π_two, multicofork_pt, multicofork_π_two_assoc, multicofork_π_zero_assoc, multicofork_π_three_assoc, multicofork_π_zero, multicofork_π_three

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multicofork_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor multicofork	—	SSet.horn.multicoequalizerDiagram
multicofork_π_three 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.Multicofork.π CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor multicofork SSet.Subcomplex.toSSet CategoryTheory.Iso.inv SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram
multicofork_π_three_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan multicofork CategoryTheory.Limits.Multicofork.π CategoryTheory.Iso.inv SSet.Subcomplex.toSSet SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' multicofork_π_three
multicofork_π_two 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.Multicofork.π CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor multicofork SSet.Subcomplex.toSSet CategoryTheory.Iso.inv SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram
multicofork_π_two_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan multicofork CategoryTheory.Limits.Multicofork.π CategoryTheory.Iso.inv SSet.Subcomplex.toSSet SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' multicofork_π_two
multicofork_π_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.Multicofork.π CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor multicofork SSet.Subcomplex.toSSet CategoryTheory.Iso.inv SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram
multicofork_π_zero_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan multicofork CategoryTheory.Limits.Multicofork.π CategoryTheory.Iso.inv SSet.Subcomplex.toSSet SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' multicofork_π_zero

SSet.horn₃₂

Definitions

Name	Category	Theorems
desc 📖	CompOp	6 math math: ι₁_desc, ι₃_desc, ι₀_desc, ι₁_desc_assoc, ι₃_desc_assoc, ι₀_desc_assoc
ι₀ 📖	CompOp	3 math math: exists_desc, ι₀_desc, ι₀_desc_assoc
ι₁ 📖	CompOp	3 math math: ι₁_desc, exists_desc, ι₁_desc_assoc
ι₃ 📖	CompOp	3 math math: exists_desc, ι₃_desc, ι₃_desc_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₀ ι₁ ι₃	—	ι₀_desc ι₁_desc ι₃_desc
ι₀_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₀ desc	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc SSet.horn.faceSingletonComplIso_inv_ι CategoryTheory.Limits.IsColimit.fac SSet.horn.multicoequalizerDiagram
ι₀_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₀ desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_desc
ι₁_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₁ desc	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc SSet.horn.faceSingletonComplIso_inv_ι CategoryTheory.Limits.IsColimit.fac SSet.horn.multicoequalizerDiagram
ι₁_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₁ desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₁_desc
ι₃_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₃ desc	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc SSet.horn.faceSingletonComplIso_inv_ι CategoryTheory.Limits.IsColimit.fac SSet.horn.multicoequalizerDiagram
ι₃_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	SSet.Subcomplex.toSSet SSet.horn ι₃ desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₃_desc

SSet.horn₃₂.desc

Definitions

Name	Category	Theorems
multicofork 📖	CompOp	7 math math: multicofork_π_one, multicofork_π_zero_assoc, multicofork_π_three, multicofork_pt, multicofork_π_zero, multicofork_π_three_assoc, multicofork_π_one_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multicofork_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor multicofork	—	SSet.horn.multicoequalizerDiagram
multicofork_π_one 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.Multicofork.π CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor multicofork SSet.Subcomplex.toSSet CategoryTheory.Iso.inv SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram
multicofork_π_one_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan multicofork CategoryTheory.Limits.Multicofork.π CategoryTheory.Iso.inv SSet.Subcomplex.toSSet SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' multicofork_π_one
multicofork_π_three 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.Multicofork.π CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor multicofork SSet.Subcomplex.toSSet CategoryTheory.Iso.inv SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram
multicofork_π_three_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan multicofork CategoryTheory.Limits.Multicofork.π CategoryTheory.Iso.inv SSet.Subcomplex.toSSet SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' multicofork_π_three
multicofork_π_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.Multicofork.π CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor multicofork SSet.Subcomplex.toSSet CategoryTheory.Iso.inv SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram
multicofork_π_zero_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanShape.ofLinearOrder Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet Subtype.instLinearOrder Fin.instLinearOrder Set.instMembership CategoryTheory.Limits.MultispanIndex.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.toLinearOrder CompleteLattice.MulticoequalizerDiagram.multispanIndex SSet.horn SSet.stdSimplex.face Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton Finset.instInsert SSet.horn.multicoequalizerDiagram SSet.Subcomplex.toSSetFunctor CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan multicofork CategoryTheory.Limits.Multicofork.π CategoryTheory.Iso.inv SSet.Subcomplex.toSSet SSet.stdSimplex.faceSingletonComplIso	—	SSet.horn.multicoequalizerDiagram CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' multicofork_π_zero

---

← Back to Index