Subcomplexes of a simplicial set

Given a simplicial set X, this file defines the type X.Subcomplex of subcomplexes of X as an abbreviation for Subfunctor X. It also introduces a coercion from X.Subcomplex to SSet.

Implementation note

SSet.{u} is defined as Cᵒᵖ ⥤ Type u, but it is not an abbreviation. This is the reason why Subfunctor.ι is redefined here as Subcomplex.ι so that this morphism appears as a morphism in SSet instead of a morphism in the category of presheaves.

instance SSet.instBalanced : CategoryTheory.Balanced SSet

@[reducible, inline]

abbrev SSet.Subcomplex (X : SSet) : Type u

The complete lattice of subcomplexes of a simplicial set.

@[reducible, inline]

abbrev SSet.Subcomplex.toSSet {X : SSet} (A : X.Subcomplex) : SSet

The underlying simplicial set of a subcomplex.

instance SSet.Subcomplex.instCoeOut {X : SSet} : CoeOut X.Subcomplex SSet

instance SSet.Subcomplex.instDecidableEqObjOppositeSimplexCategoryToSSet {X : SSet} (n : SimplexCategoryᵒᵖ) (A : X.Subcomplex) [DecidableEq (X.obj n)] : DecidableEq (A.toSSet.obj n)

@[reducible, inline]

abbrev SSet.Subcomplex.ι {X : SSet} (A : X.Subcomplex) : A.toSSet ⟶ X

If A : Subcomplex X, this is the inclusion A ⟶ X in the category SSet.

instance SSet.Subcomplex.instMonoι {X : SSet} (A : X.Subcomplex) : CategoryTheory.Mono A.ι

@[reducible, inline]

abbrev SSet.Subcomplex.homOfLE {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) : S₁.toSSet ⟶ S₂.toSSet

Given an inequality S₁ ≤ S₂ between subcomplexes of a simplicial set, this is the induced morphism in the category SSet.

theorem SSet.Subcomplex.homOfLE_comp {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) {S₃ : X.Subcomplex} (h' : S₂ ≤ S₃) : CategoryTheory.CategoryStruct.comp (homOfLE h) (homOfLE h') = homOfLE ⋯

theorem SSet.Subcomplex.homOfLE_comp_assoc {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) {S₃ : X.Subcomplex} (h' : S₂ ≤ S₃) {Z : SSet} (h✝ : S₃.toSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp (homOfLE h) (CategoryTheory.CategoryStruct.comp (homOfLE h') h✝) = CategoryTheory.CategoryStruct.comp (homOfLE ⋯) h✝

@[simp]

theorem SSet.Subcomplex.homOfLE_refl {X : SSet} (S₁ : X.Subcomplex) : homOfLE ⋯ = CategoryTheory.CategoryStruct.id S₁.toSSet

@[simp]

theorem SSet.Subcomplex.homOfLE_app_val {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) (Δ : SimplexCategoryᵒᵖ) (x : ↑(S₁.obj Δ)) : ↑((homOfLE h).app Δ x) = ↑x

@[simp]

theorem SSet.Subcomplex.homOfLE_ι {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) : CategoryTheory.CategoryStruct.comp (homOfLE h) S₂.ι = S₁.ι

@[simp]

theorem SSet.Subcomplex.homOfLE_ι_assoc {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) {Z : SSet} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (homOfLE h) (CategoryTheory.CategoryStruct.comp S₂.ι h✝) = CategoryTheory.CategoryStruct.comp S₁.ι h✝

instance SSet.Subcomplex.mono_homOfLE {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) : CategoryTheory.Mono (homOfLE h)

def SSet.Subcomplex.eqToIso {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ = S₂) : S₁.toSSet ≅ S₂.toSSet

This is the isomorphism of simplicial sets corresponding to an equality of subcomplexes.

@[simp]

theorem SSet.Subcomplex.eqToIso_hom {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ = S₂) : (Subcomplex.eqToIso h).hom = homOfLE ⋯

@[simp]

theorem SSet.Subcomplex.eqToIso_inv {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ = S₂) : (Subcomplex.eqToIso h).inv = homOfLE ⋯

def SSet.Subcomplex.toSSetFunctor {X : SSet} : CategoryTheory.Functor X.Subcomplex SSet

The functor which sends A : X.Subcomplex to A.toSSet.

@[simp]

theorem SSet.Subcomplex.toSSetFunctor_obj {X : SSet} (A : X.Subcomplex) : toSSetFunctor.obj A = A.toSSet

@[simp]

theorem SSet.Subcomplex.toSSetFunctor_map {X : SSet} {X✝ Y✝ : X.Subcomplex} (h : X✝ ⟶ Y✝) : toSSetFunctor.map h = homOfLE ⋯

def SSet.Subcomplex.topIso (X : SSet) : ⊤.toSSet ≅ X

If X : SSet, this is the isomorphism of simplicial sets from ⊤ : X.Subcomplex to X.

@[simp]

theorem SSet.Subcomplex.topIso_inv_app_coe (X : SSet) (X✝ : SimplexCategoryᵒᵖ) (a✝ : X.obj X✝) : ↑((topIso X).inv.app X✝ a✝) = a✝

@[simp]

theorem SSet.Subcomplex.topIso_hom (X : SSet) : (topIso X).hom = ⊤.ι

@[simp]

theorem SSet.Subcomplex.topIso_inv_ι (X : SSet) : CategoryTheory.CategoryStruct.comp (topIso X).inv (CategoryTheory.Subfunctor.ι ⊤) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem SSet.Subcomplex.topIso_inv_ι_assoc (X : SSet) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (topIso X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.ι ⊤) h) = h

instance SSet.Subcomplex.instSubsingletonHomToSSetBot {X Y : SSet} : Subsingleton (⊥.toSSet ⟶ Y)

instance SSet.Subcomplex.instUniqueHomToSSetBot {X Y : SSet} : Unique (⊥.toSSet ⟶ Y)

def SSet.Subcomplex.isInitialBot {X : SSet} : CategoryTheory.Limits.IsInitial ⊥.toSSet

If X is a simplicial set, then the empty subcomplex of X is an initial object in SSet.

@[reducible, inline]

abbrev SSet.Subcomplex.ofSimplex {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) : X.Subcomplex

The subcomplex of a simplicial set that is generated by a simplex.

@[simp]

theorem SSet.Subcomplex.ofSimplex_ι {X : SSet} (x : X.obj (Opposite.op (SimplexCategory.mk 0))) : (ofSimplex x).ι = const x

theorem SSet.Subcomplex.mem_ofSimplex_obj {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) : x ∈ (ofSimplex x).obj (Opposite.op (SimplexCategory.mk n))

theorem SSet.Subcomplex.ofSimplex_le_iff {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (A : X.Subcomplex) : ofSimplex x ≤ A ↔ x ∈ A.obj (Opposite.op (SimplexCategory.mk n))

theorem SSet.Subcomplex.mem_ofSimplex_obj_iff {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) {m : SimplexCategoryᵒᵖ} (y : X.obj m) : y ∈ (ofSimplex x).obj m ↔ ∃ (f : Opposite.unop m ⟶ SimplexCategory.mk n), X.map f.op x = y

@[reducible, inline]

abbrev SSet.Subcomplex.range {X Y : SSet} (f : X ⟶ Y) : Y.Subcomplex

The range of a morphism of simplicial sets, as a subcomplex.

@[reducible, inline]

abbrev SSet.Subcomplex.toRange {X Y : SSet} (f : X ⟶ Y) : X ⟶ (range f).toSSet

The morphism X ⟶ Subcomplex.range f induced by f : X ⟶ Y.

@[simp]

theorem SSet.Subcomplex.toRange_ι {X Y : SSet} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (toRange f) (range f).ι = f

@[simp]

theorem SSet.Subcomplex.toRange_ι_assoc {X Y : SSet} (f : X ⟶ Y) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (toRange f) (CategoryTheory.CategoryStruct.comp (range f).ι h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem SSet.Subcomplex.toRange_app_val {X Y : SSet} (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (x : X.obj Δ) : ↑((toRange f).app Δ x) = f.app Δ x

instance SSet.Subcomplex.instEpiToRange {X Y : SSet} (f : X ⟶ Y) : CategoryTheory.Epi (toRange f)

instance SSet.Subcomplex.instMonoToRange {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Mono (toRange f)

instance SSet.Subcomplex.instIsIsoToRangeOfMono {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.IsIso (toRange f)

theorem SSet.Subcomplex.range_eq_top_iff {X Y : SSet} (f : X ⟶ Y) : range f = ⊤ ↔ CategoryTheory.Epi f

theorem SSet.Subcomplex.range_eq_top {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Epi f] : range f = ⊤

def SSet.Subcomplex.lift {X Y : SSet} (f : X ⟶ Y) {B : Y.Subcomplex} (hf : range f ≤ B) : X ⟶ B.toSSet

Given a morphism of simplicial sets f : X ⟶ Y whose range is ≤ B for some B : Y.Subcomplex, this is the induced morphism X ⟶ B.

@[simp]

theorem SSet.Subcomplex.lift_ι {X Y : SSet} (f : X ⟶ Y) {B : Y.Subcomplex} (hf : range f ≤ B) : CategoryTheory.CategoryStruct.comp (lift f hf) B.ι = f

@[simp]

theorem SSet.Subcomplex.lift_ι_assoc {X Y : SSet} (f : X ⟶ Y) {B : Y.Subcomplex} (hf : range f ≤ B) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (lift f hf) (CategoryTheory.CategoryStruct.comp B.ι h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem SSet.Subcomplex.lift_app_coe {X Y : SSet} (f : X ⟶ Y) {B : Y.Subcomplex} (hf : range f ≤ B) {n : SimplexCategoryᵒᵖ} (x : X.obj n) : ↑((lift f hf).app n x) = f.app n x

def SSet.Subcomplex.preimage {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) : Y.Subcomplex

The preimage of a subcomplex by a morphism of simplicial sets.

@[simp]

theorem SSet.Subcomplex.preimage_obj {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) (n : SimplexCategoryᵒᵖ) : (A.preimage p).obj n = p.app n ⁻¹' A.obj n

@[simp]

theorem SSet.Subcomplex.preimage_max {X Y : SSet} (A B : X.Subcomplex) (p : Y ⟶ X) : (A ⊔ B).preimage p = A.preimage p ⊔ B.preimage p

@[simp]

theorem SSet.Subcomplex.preimage_min {X Y : SSet} (A B : X.Subcomplex) (p : Y ⟶ X) : (A ⊓ B).preimage p = A.preimage p ⊓ B.preimage p

@[simp]

theorem SSet.Subcomplex.preimage_iSup {X Y : SSet} {ι : Type u_1} (A : ι → X.Subcomplex) (p : Y ⟶ X) : (⨆ (i : ι), A i).preimage p = ⨆ (i : ι), (A i).preimage p

@[simp]

theorem SSet.Subcomplex.preimage_iInf {X Y : SSet} {ι : Type u_1} (A : ι → X.Subcomplex) (p : Y ⟶ X) : (⨅ (i : ι), A i).preimage p = ⨅ (i : ι), (A i).preimage p

def SSet.Subcomplex.image {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) : Y.Subcomplex

The image of a subcomplex by a morphism of simplicial sets.

@[simp]

theorem SSet.Subcomplex.image_obj {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) (i : SimplexCategoryᵒᵖ) : (A.image f).obj i = f.app i '' A.obj i

theorem SSet.Subcomplex.image_le_iff {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) (Z : Y.Subcomplex) : A.image f ≤ Z ↔ A ≤ Z.preimage f

theorem SSet.Subcomplex.image_top {X Y : SSet} (f : X ⟶ Y) : ⊤.image f = range f

@[simp]

theorem SSet.Subcomplex.image_id {X : SSet} (A : X.Subcomplex) : A.image (CategoryTheory.CategoryStruct.id X) = A

theorem SSet.Subcomplex.image_comp {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) {Z : SSet} (g : Y ⟶ Z) : A.image (CategoryTheory.CategoryStruct.comp f g) = (A.image f).image g

theorem SSet.Subcomplex.range_comp {X Y : SSet} (f : X ⟶ Y) {Z : SSet} (g : Y ⟶ Z) : range (CategoryTheory.CategoryStruct.comp f g) = (range f).image g

theorem SSet.Subcomplex.image_eq_range {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) : A.image f = range (CategoryTheory.CategoryStruct.comp A.ι f)

theorem SSet.Subcomplex.image_iSup {X Y : SSet} {ι : Type u_1} (S : ι → X.Subcomplex) (f : X ⟶ Y) : (⨆ (i : ι), S i).image f = ⨆ (i : ι), (S i).image f

@[simp]

theorem SSet.Subcomplex.preimage_range {X Y : SSet} (f : X ⟶ Y) : (range f).preimage f = ⊤

@[simp]

theorem SSet.Subcomplex.image_le_range {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) : A.image f ≤ range f

@[simp]

theorem SSet.Subcomplex.image_ofSimplex {X Y : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (f : X ⟶ Y) : (ofSimplex x).image f = ofSimplex (f.app (Opposite.op (SimplexCategory.mk n)) x)

def SSet.Subcomplex.toImage {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) : A.toSSet ⟶ (A.image f).toSSet

Given a morphism of simplicial sets f : X ⟶ Y and a subcomplex A of X, this is the induced morphism from A to A.image f.

@[simp]

theorem SSet.Subcomplex.toImage_app_coe {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) (U : SimplexCategoryᵒᵖ) (x : A.toSSet.obj U) : ↑((A.toImage f).app U x) = f.app U ↑x

@[simp]

theorem SSet.Subcomplex.toImage_ι {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (A.toImage f) (A.image f).ι = CategoryTheory.CategoryStruct.comp A.ι f

@[simp]

theorem SSet.Subcomplex.toImage_ι_assoc {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.toImage f) (CategoryTheory.CategoryStruct.comp (A.image f).ι h) = CategoryTheory.CategoryStruct.comp A.ι (CategoryTheory.CategoryStruct.comp f h)

instance SSet.Subcomplex.instEpiToImage {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) : CategoryTheory.Epi (A.toImage f)

theorem SSet.Subcomplex.image_monotone {X Y : SSet} (f : X ⟶ Y) : Monotone fun (S : X.Subcomplex) => S.image f

theorem SSet.Subcomplex.preimage_eq_top_iff {X Y : SSet} (B : X.Subcomplex) (f : Y ⟶ X) : B.preimage f = ⊤ ↔ range f ≤ B

@[simp]

theorem SSet.Subcomplex.image_preimage_le {X Y : SSet} (B : X.Subcomplex) (f : Y ⟶ X) : (B.preimage f).image f ≤ B

def SSet.Subcomplex.fromPreimage {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) : (A.preimage p).toSSet ⟶ A.toSSet

Given a morphism of simplicial sets p : Y ⟶ X and A : X.Subcomplex, this is the induced morphism (A.preimage p : SSet) ⟶ (A : SSet).

@[simp]

theorem SSet.Subcomplex.fromPreimage_app_coe {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) (U : SimplexCategoryᵒᵖ) (x : (A.preimage p).toSSet.obj U) : ↑((A.fromPreimage p).app U x) = p.app U ↑x

@[simp]

theorem SSet.Subcomplex.fromPreimage_ι {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (A.fromPreimage p) A.ι = CategoryTheory.CategoryStruct.comp (A.preimage p).ι p

@[simp]

theorem SSet.Subcomplex.fromPreimage_ι_assoc {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.fromPreimage p) (CategoryTheory.CategoryStruct.comp A.ι h) = CategoryTheory.CategoryStruct.comp (A.preimage p).ι (CategoryTheory.CategoryStruct.comp p h)