Documentation

Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Dimension of a simplicial set #

For a simplicial set X and d : ℕ, we introduce a typeclass X.HasDimensionLT d saying that the dimension of X is < d, i.e. all nondegenerate simplices of X are of dimension < d.

source
class SSet.HasDimensionLT (X : SSet) (d : ℕ) :
Prop

A simplicial set X has dimension < d iff for any n : ℕ such that d ≤ n, all n-simplices are degenerate.

Instances
    source
    theorem SSet.hasDimensionLT_iff (X : SSet) (d : ℕ) :
    X.HasDimensionLT d ↔ ∀ (n : ℕ), d ≤ n → X.degenerate n = ⊤
    source
    @[reducible, inline]
    abbrev SSet.HasDimensionLE (X : SSet) (d : ℕ) :
    Prop

    A simplicial set has dimension ≤ d if it has dimension < d + 1.

    Equations
    Instances For
      source
      theorem SSet.degenerate_eq_univ_of_hasDimensionLT (X : SSet) (d : ℕ) [X.HasDimensionLT d] (n : ℕ) (hn : d ≤ n := by lia) :
      X.degenerate n = Set.univ
      source
      theorem SSet.nonDegenerate_eq_empty_of_hasDimensionLT (X : SSet) (d : ℕ) [X.HasDimensionLT d] (n : ℕ) (hn : d ≤ n := by lia) :
      X.nonDegenerate n = ∅
      source
      theorem SSet.dim_lt_of_nonDegenerate (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) (d : ℕ) [X.HasDimensionLT d] :
      n < d
      source
      theorem SSet.dim_le_of_nonDegenerate (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) (d : ℕ) [X.HasDimensionLE d] :
      n ≤ d
      source
      theorem SSet.hasDimensionLT_of_le (X : SSet) (d : ℕ) [X.HasDimensionLT d] (n : ℕ) (hn : d ≤ n := by lia) :
      X.HasDimensionLT n
      source
      instance SSet.instHasDimensionLTHAddNat (X : SSet) (n : ℕ) [X.HasDimensionLT n] (k : ℕ) :
      X.HasDimensionLT (n + k)
      source
      instance SSet.Subcomplex.instHasDimensionLTToSSet {X : SSet} (d : ℕ) [X.HasDimensionLT d] (A : X.Subcomplex) :
      A.toSSet.HasDimensionLT d
      source
      theorem SSet.Subcomplex.le_iff_of_hasDimensionLT {X : SSet} (A B : X.Subcomplex) (d : ℕ) [X.HasDimensionLT d] :
      A ≤ B ↔ ∀ i < d, A.obj (Opposite.op { len := i }) ∩ X.nonDegenerate i ⊆ B.obj (Opposite.op { len := i })
      source
      theorem SSet.Subcomplex.eq_top_iff_of_hasDimensionLT {X : SSet} (A : X.Subcomplex) (d : ℕ) [X.HasDimensionLT d] :
      A = ⊤ ↔ ∀ i < d, X.nonDegenerate i ⊆ A.obj (Opposite.op { len := i })
      source
      theorem SSet.hasDimensionLT_of_mono {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] (d : ℕ) [Y.HasDimensionLT d] :
      X.HasDimensionLT d
      source
      theorem SSet.Subcomplex.hasDimensionLT_of_le {X : SSet} {A B : X.Subcomplex} (h : A ≤ B) (d : ℕ) [B.toSSet.HasDimensionLT d] :
      A.toSSet.HasDimensionLT d
      source
      theorem SSet.hasDimensionLT_of_epi {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Epi f] (d : ℕ) [X.HasDimensionLT d] :
      Y.HasDimensionLT d
      source
      theorem SSet.hasDimensionLT_iff_of_iso {X Y : SSet} (e : X ≅ Y) (d : ℕ) :
      X.HasDimensionLT d ↔ Y.HasDimensionLT d
      source
      instance SSet.instHasDimensionLTToSSetRange {X Y : SSet} (f : X ⟶ Y) (d : ℕ) [X.HasDimensionLT d] :
      (Subcomplex.range f).toSSet.HasDimensionLT d
      source
      theorem SSet.hasDimensionLT_iSup_iff {X : SSet} {ι : Type u_1} (A : ι → X.Subcomplex) (d : ℕ) :
      (⨆ (i : ι), A i).toSSet.HasDimensionLT d ↔ ∀ (i : ι), (A i).toSSet.HasDimensionLT d
      source
      theorem SSet.hasDimensionLT_subcomplex_top_iff (X : SSet) (d : ℕ) :
      ⊤.toSSet.HasDimensionLT d ↔ X.HasDimensionLT d
      source
      instance SSet.instHasDimensionLTToSSetBotSubcomplex {X : SSet} (n : ℕ) :
      ⊥.toSSet.HasDimensionLT n