Pairs of simplicial sets

In this file, we define the category SSetPair of pairs of simplicial sets, which consist of monomorphisms i : X ⟶ Y of simplicial sets.

@[reducible, inline]

abbrev SSetPair : Type (u + 1)

The category SSetPair is the category of pairs of simplicial sets, i.e. monomorphisms i : X ⟶ Y, see SSetPair.of.

Equations

• SSetPair = (CategoryTheory.MorphismProperty.monomorphisms SSet).Arrow ⊤ ⊤

instance SSetPair.instMonoSSetHom (P : SSetPair) : CategoryTheory.Mono P.hom

@[reducible, inline]

abbrev SSetPair.of {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] : SSetPair

Constructor for SSetPair.

Equations

• SSetPair.of i = CategoryTheory.MorphismProperty.Arrow.mk i inst✝

@[reducible, inline]

abbrev SSetPair.forget : CategoryTheory.Functor SSetPair (CategoryTheory.Arrow SSet)

The forget functor from SSetPair to the category Arrow SSet.

Equations

• SSetPair.forget = CategoryTheory.MorphismProperty.Arrow.forget (CategoryTheory.MorphismProperty.monomorphisms SSet) ⊤ ⊤

@[reducible, inline]

abbrev SSetPair.homMk {X Y : SSetPair} (left : X.left ⟶ Y.left) (right : X.right ⟶ Y.right) (w : CategoryTheory.CategoryStruct.comp left Y.hom = CategoryTheory.CategoryStruct.comp X.hom right := by cat_disch) : X ⟶ Y

Constructor for morphisms in SSetPair.

Equations

• SSetPair.homMk left right w = CategoryTheory.MorphismProperty.Arrow.Hom.mk (CategoryTheory.Arrow.homMk left right w) ⋯ ⋯

@[reducible, inline]

abbrev SSet.Subcomplex.pair {X : SSet} (A : X.Subcomplex) : SSetPair

Given a subcomplex A of a simplical set X, this is the pair in SSetPair corresponding to the inclusion A.ι : (A : SSet) ⟶ X.

Equations

• A.pair = SSetPair.of A.ι

@[implicit_reducible]

def SSet.Subcomplex.toPairFunctor (X : SSet) : CategoryTheory.Functor X.Subcomplex SSetPair

Given X : SSet, this is the functor X.Subcomplex ⥤ SSetPair which sends A : X.Subcomplex to the pair corresponding to the inclusion A.ι : (A : SSet) ⟶ X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.Subcomplex.toPairFunctor_map (X : SSet) {X✝ Y✝ : X.Subcomplex} (f : X✝ ⟶ Y✝) : (toPairFunctor X).map f = SSetPair.homMk (homOfLE ⋯) (CategoryTheory.CategoryStruct.id X✝.pair.right) ⋯

@[simp]

theorem SSet.Subcomplex.toPairFunctor_obj (X : SSet) (A : X.Subcomplex) : (toPairFunctor X).obj A = A.pair

@[reducible, inline]

abbrev SSet.pair (X : SSet) : SSetPair

If X is a simplicial set, this is the pair in SSetPair corresponding to the inclusion of the empty subcomplex in X.

Equations

• X.pair = ⊥.pair

@[implicit_reducible]

def SSet.toPairFunctor : CategoryTheory.Functor SSet SSetPair

The functor SSet ⥤ SSetPair which sends X : SSet to the pair corresponding to the inclusion of the empty subcomplex in X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.toPairFunctor_map {X✝ Y✝ : SSet} (f : X✝ ⟶ Y✝) : toPairFunctor.map f = SSetPair.homMk (Subcomplex.lift (CategoryTheory.CategoryStruct.comp ⊥.ι f) ⋯) f ⋯

@[simp]

theorem SSet.toPairFunctor_obj (X : SSet) : toPairFunctor.obj X = X.pair