Relative morphisms of simplicial sets

Given two simplicial sets X and Y, and subcomplexes A of X, and B of Y, we introduce a type RelativeMorphism A B φ of morphisms X ⟶ Y which induce a given morphism of simplicial sets A ⟶ B. We define homotopies between these relative morphisms and introduce the quotient type of homotopy classes.

structure SSet.RelativeMorphism {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) (φ : A.toSSet ⟶ B.toSSet) : Type u

Given a morphism of simplicial sets φ : A ⟶ B with A : X.Subcomplex and B : Y.Subcomplex, this is the type of morphisms X ⟶ Y which induce φ.

• map : X ⟶ Y

  The underlying morphism of simplicial sets.

• comm : CategoryTheory.CategoryStruct.comp A.ι self.map = CategoryTheory.CategoryStruct.comp φ B.ι

theorem SSet.RelativeMorphism.ext {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {x y : RelativeMorphism A B φ} (map : x.map = y.map) : x = y

theorem SSet.RelativeMorphism.ext_iff {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {x y : RelativeMorphism A B φ} : x = y ↔ x.map = y.map

@[simp]

theorem SSet.RelativeMorphism.comm_assoc {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (self : RelativeMorphism A B φ) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp A.ι (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp B.ι h)

def SSet.RelativeMorphism.const {X Y : SSet} {A : X.Subcomplex} {y : Y.obj (Opposite.op (SimplexCategory.mk 0))} {φ : A.toSSet ⟶ (Subcomplex.ofSimplex y).toSSet} : RelativeMorphism A (Subcomplex.ofSimplex y) φ

The constant relative morphism when the given subcomplex of the target is generated by a 0-simplex.

@[simp]

theorem SSet.RelativeMorphism.const_map {X Y : SSet} {A : X.Subcomplex} {y : Y.obj (Opposite.op (SimplexCategory.mk 0))} {φ : A.toSSet ⟶ (Subcomplex.ofSimplex y).toSSet} : const.map = SSet.const y

def SSet.RelativeMorphism.ofSimplex₀ {X Y : SSet} (f : X ⟶ Y) (x : X.obj (Opposite.op (SimplexCategory.mk 0))) (y : Y.obj (Opposite.op (SimplexCategory.mk 0))) (h : f.app (Opposite.op (SimplexCategory.mk 0)) x = y) : RelativeMorphism (Subcomplex.ofSimplex x) (Subcomplex.ofSimplex y) (SSet.const ⟨y, ⋯⟩)

Given a morphism f : X ⟶ Y of simplicial set which sends a 0-simplex x to y, this is the pointed morphism (X, x) ⟶ (Y, y).

@[simp]

theorem SSet.RelativeMorphism.ofSimplex₀_map {X Y : SSet} (f : X ⟶ Y) (x : X.obj (Opposite.op (SimplexCategory.mk 0))) (y : Y.obj (Opposite.op (SimplexCategory.mk 0))) (h : f.app (Opposite.op (SimplexCategory.mk 0)) x = y) : (ofSimplex₀ f x y h).map = f

theorem SSet.RelativeMorphism.map_eq_of_mem {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) {n : SimplexCategoryᵒᵖ} (a : X.obj n) (ha : a ∈ A.obj n) : f.map.app n a = ↑(φ.app n ⟨a, ha⟩)

@[simp]

theorem SSet.RelativeMorphism.map_coe {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) {n : SimplexCategoryᵒᵖ} (a : ↑(A.obj n)) : f.map.app n ↑a = ↑(φ.app n a)

theorem SSet.RelativeMorphism.image_le {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) : A.image f.map ≤ B

theorem SSet.RelativeMorphism.le_preimage {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) : A ≤ B.preimage f.map

structure SSet.RelativeMorphism.Homotopy {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f g : RelativeMorphism A B φ) : Type u

The type of homotopies between morphisms of simplicial sets relatively to given subcomplexes.

• h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (stdSimplex.obj (SimplexCategory.mk 1)) ⟶ Y

  The homotopy.

• h₀ : CategoryTheory.CategoryStruct.comp ι₀ self.h = f.map
• h₁ : CategoryTheory.CategoryStruct.comp ι₁ self.h = g.map
• rel : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (stdSimplex.obj (SimplexCategory.mk 1))) self.h = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (stdSimplex.obj (SimplexCategory.mk 1))) (CategoryTheory.CategoryStruct.comp φ B.ι)

theorem SSet.RelativeMorphism.Homotopy.ext_iff {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} {x y : f.Homotopy g} : x = y ↔ x.h = y.h

theorem SSet.RelativeMorphism.Homotopy.ext {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} {x y : f.Homotopy g} (h : x.h = y.h) : x = y

@[simp]

theorem SSet.RelativeMorphism.Homotopy.rel_assoc {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} (self : f.Homotopy g) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (stdSimplex.obj (SimplexCategory.mk 1))) (CategoryTheory.CategoryStruct.comp self.h h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (stdSimplex.obj (SimplexCategory.mk 1))) (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp B.ι h))

@[simp]

theorem SSet.RelativeMorphism.Homotopy.h₁_assoc {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} (self : f.Homotopy g) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp self.h h) = CategoryTheory.CategoryStruct.comp g.map h

@[simp]

theorem SSet.RelativeMorphism.Homotopy.h₀_assoc {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} (self : f.Homotopy g) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp self.h h) = CategoryTheory.CategoryStruct.comp f.map h

noncomputable def SSet.RelativeMorphism.Homotopy.ofEq {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} (h : f = g) : f.Homotopy g

Two equal relative morphisms are homotopic.

@[simp]

theorem SSet.RelativeMorphism.Homotopy.ofEq_h {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} (h : f = g) : (ofEq h).h = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X (stdSimplex.obj (SimplexCategory.mk 1))) f.map

noncomputable def SSet.RelativeMorphism.Homotopy.refl {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) : f.Homotopy f

A relative morphism is homotopic to itself.

@[simp]

theorem SSet.RelativeMorphism.Homotopy.refl_h {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) : (refl f).h = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X (stdSimplex.obj (SimplexCategory.mk 1))) f.map

def SSet.RelativeMorphism.HomotopyClass {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) (φ : A.toSSet ⟶ B.toSSet) : Type u

The type of homotopy classes of relative morphisms.

def SSet.RelativeMorphism.homotopyClass {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) : HomotopyClass A B φ

The homotopy class of a relative morphism.

theorem SSet.RelativeMorphism.Homotopy.eq {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} (h : f.Homotopy g) : f.homotopyClass = g.homotopyClass

theorem SSet.RelativeMorphism.HomotopyClass.eq_homotopyClass {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (x : HomotopyClass A B φ) : ∃ (f : RelativeMorphism A B φ), f.homotopyClass = x

def SSet.RelativeMorphism.comp {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (f' : RelativeMorphism B C ψ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : RelativeMorphism A C φψ

The composition of relative morphisms.

@[simp]

theorem SSet.RelativeMorphism.comp_map {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : RelativeMorphism A B φ) {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (f' : RelativeMorphism B C ψ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : (f.comp f' fac).map = CategoryTheory.CategoryStruct.comp f.map f'.map

noncomputable def SSet.RelativeMorphism.Homotopy.postcomp {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (h : f.Homotopy g) (f' : RelativeMorphism B C ψ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : (f.comp f' fac).Homotopy (g.comp f' fac)

The postcomposition of an homotopy with a relative morphism.

@[simp]

theorem SSet.RelativeMorphism.Homotopy.postcomp_h {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : RelativeMorphism A B φ} {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (h : f.Homotopy g) (f' : RelativeMorphism B C ψ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : (h.postcomp f' fac).h = CategoryTheory.CategoryStruct.comp h.h f'.map

noncomputable def SSet.RelativeMorphism.Homotopy.precomp {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} {f' g' : RelativeMorphism B C ψ} (h : f'.Homotopy g') (f : RelativeMorphism A B φ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : (f.comp f' fac).Homotopy (f.comp g' fac)

The precomposition of an homotopy with a relative morphism.

@[simp]

theorem SSet.RelativeMorphism.Homotopy.precomp_h {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} {f' g' : RelativeMorphism B C ψ} (h : f'.Homotopy g') (f : RelativeMorphism A B φ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : (h.precomp f fac).h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.map (stdSimplex.obj (SimplexCategory.mk 1))) h.h

def SSet.RelativeMorphism.HomotopyClass.postcomp {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (h : HomotopyClass A B φ) (f' : RelativeMorphism B C ψ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : HomotopyClass A C φψ

The postcomposition of an homotopy class by a relative morphism.

@[simp]

theorem SSet.RelativeMorphism.postcomp_homotopyClass {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (f : RelativeMorphism A B φ) (f' : RelativeMorphism B C ψ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : f.homotopyClass.postcomp f' fac = (f.comp f' fac).homotopyClass

noncomputable def SSet.RelativeMorphism.HomotopyClass.precomp {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (h : HomotopyClass B C ψ) (f' : RelativeMorphism A B φ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : HomotopyClass A C φψ

The precomposition of an homotopy class with a relative morphism.

@[simp]

theorem SSet.RelativeMorphism.precomp_homotopyClass {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (f : RelativeMorphism A B φ) (f' : RelativeMorphism B C ψ) {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) : f'.homotopyClass.precomp f fac = (f.comp f' fac).homotopyClass