Documentation

Mathlib.AlgebraicTopology.SimplicialSet.Finite

Finite simplicial sets #

A simplicial set is finite (SSet.Finite) if it has finitely many nondegenerate simplices.

source
class SSet.Finite (X : SSet) :
Prop

A simplicial set is finite if it has finitely many nondegenerate simplices.

Instances
    source
    instance SSet.instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite (X : SSet) [X.Finite] (n : ℕ) :
    Finite ↑(X.nonDegenerate n)
    source
    theorem SSet.finite_of_hasDimensionLT (X : SSet) (d : ℕ) [X.HasDimensionLT d] (h : ∀ i < d, Finite ↑(X.nonDegenerate i)) :
    X.Finite
    source
    theorem SSet.hasDimensionLT_of_finite (X : SSet) [X.Finite] :
    ∃ (d : ℕ), X.HasDimensionLT d
    source
    instance SSet.instFiniteObjOppositeSimplexCategoryOfFinite (X : SSet) [X.Finite] (n : SimplexCategoryᵒᵖ) :
    Finite (X.obj n)
    source
    instance SSet.instFiniteToSSet (X : SSet) [X.Finite] (A : X.Subcomplex) :
    A.toSSet.Finite
    source
    theorem SSet.finite_of_mono {X Y : SSet} [Y.Finite] (f : X ⟶ Y) [hf : CategoryTheory.Mono f] :
    X.Finite
    source
    theorem SSet.finite_of_epi {X Y : SSet} [X.Finite] (f : X ⟶ Y) [hf : CategoryTheory.Epi f] :
    Y.Finite
    source
    theorem SSet.finite_of_iso {X Y : SSet} (e : X ≅ Y) [X.Finite] :
    Y.Finite
    source
    theorem SSet.finite_iff_of_iso {X Y : SSet} (e : X ≅ Y) :
    X.Finite ↔ Y.Finite
    source
    theorem SSet.finite_subcomplex_top_iff (X : SSet) :
    ⊤.toSSet.Finite ↔ X.Finite
    source
    instance SSet.finite_range {X Y : SSet} (f : Y ⟶ X) [Y.Finite] :
    (Subcomplex.range f).toSSet.Finite
    source
    theorem SSet.finite_iSup_iff {X : SSet} {ι : Type u_1} [Finite ι] (A : ι → X.Subcomplex) :
    (⨆ (i : ι), A i).toSSet.Finite ↔ ∀ (i : ι), (A i).toSSet.Finite