SubcomplexColimits

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

Statistics

Metric	Count
Definitions BicartSq, isColimit, isColimit'	3
Theorems isPushout	1
Total	4

SSet.Subcomplex

Definitions

Name	Category	Theorems
BicartSq 📖	MathDef	3 math math: SSet.horn₂₂.sq, SSet.horn₂₀.sq, SSet.horn₂₁.sq

SSet.Subcomplex.BicartSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPushout 📖	mathematical	SSet.Subcomplex.BicartSq	CategoryTheory.IsPushout SSet SSet.largeCategory SSet.Subcomplex.toSSet SSet.Subcomplex.homOfLE Lattice.BicartSq.le₁₂ SSet.Subcomplex ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Lattice.BicartSq.le₁₃ Lattice.BicartSq.le₂₄ Lattice.BicartSq.le₃₄	—	Lattice.BicartSq.le₁₂ Lattice.BicartSq.le₁₃ Lattice.BicartSq.le₂₄ Lattice.BicartSq.le₃₄ Lattice.BicartSq.sup_eq Lattice.BicartSq.inf_eq CategoryTheory.Limits.Types.isPushout_of_bicartSq

SSet.Subcomplex.MulticoequalizerDiagram

Definitions

Name	Category	Theorems
isColimit 📖	CompOp	—
isColimit' 📖	CompOp	—

---

← Back to Index