Documentation

Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

2-truncated quasicategories and homotopy relations #

We define 2-truncated quasicategories Quasicategory₂ by three horn-filling properties, and the left and right homotopy relations HomotopicL and HomotopicR on the edges in a 2-truncated simplicial set.

We prove that for 2-truncated quasicategories, both homotopy relations are equivalence relations, and that the left and right homotopy relations coincide.

Implementation notes #

Throughout this file, we make use of Edge and CompStruct to conveniently deal with edges and triangles in a 2-truncated simplicial set.

source
class SSet.Truncated.Quasicategory₂ (X : Truncated 2) :
Prop

A 2-truncated quasicategory is a 2-truncated simplicial set with the properties:

  • (2, 1)-filling: given two consecutive Edges e₀₁ and e₁₂, there exists a CompStruct with (0, 1)-edge e₀₁ and (0, 2)-edge e₁₂.
  • (3, 1)-filling: given three CompStructs f₃, f₀ and f₂ which form a (3, 1)-horn, there exists a fourth CompStruct such that the four faces form the boundary ∂Δ[3] of a 3-simplex.
  • (3, 2)-filling: given three CompStructs f₃, f₀ and f₁ which form a (3, 2)-horn, there exists a fourth CompStruct such that the four faces form the boundary ∂Δ[3] of a 3-simplex.
Instances
    source
    @[reducible, inline]
    abbrev SSet.Truncated.HomotopicL {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f g : Edge x y) :
    Prop

    Two edges f and g are left homotopic if there is a CompStruct with (0, 1)-edge f, (1, 2)-edge id and (0, 2)-edge g. We use Nonempty to have a Prop valued HomotopicL.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev SSet.Truncated.HomotopicR {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f g : Edge x y) :
      Prop

      Two edges f and g are right homotopic if there is a CompStruct with (0, 1)-edge id, (1, 2)-edge f, and (0, 2)-edge g. We use Nonempty to have a Prop valued HomotopicR.

      Equations
      Instances For
        source
        theorem SSet.Truncated.HomotopicL.refl {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Edge x y} :
        HomotopicL f f

        Left homotopy relation is reflexive

        source
        theorem SSet.Truncated.HomotopicL.symm {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g : Edge x y} (hfg : HomotopicL f g) :
        HomotopicL g f

        Left homotopy relation is symmetric

        source
        theorem SSet.Truncated.HomotopicL.trans {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g h : Edge x y} (hfg : HomotopicL f g) (hgh : HomotopicL g h) :
        HomotopicL f h

        Left homotopy relation is transitive

        source
        theorem SSet.Truncated.HomotopicR.refl {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Edge x y} :
        HomotopicR f f

        Right homotopy relation is reflexive

        source
        theorem SSet.Truncated.HomotopicR.symm {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g : Edge x y} (hfg : HomotopicR f g) :
        HomotopicR g f

        Right homotopy relation is symmetric

        source
        theorem SSet.Truncated.HomotopicR.trans {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g h : Edge x y} (hfg : HomotopicR f g) (hgh : HomotopicR g h) :
        HomotopicR f h

        Right homotopy relation is transitive

        source
        theorem SSet.Truncated.HomotopicL.homotopicR {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g : Edge x y} (h : HomotopicL f g) :
        HomotopicR f g

        In a 2-truncated quasicategory, left homotopy implies right homotopy

        source
        theorem SSet.Truncated.HomotopicR.homotopicL {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g : Edge x y} (h : HomotopicR f g) :
        HomotopicL f g

        In a 2-truncated quasicategory, right homotopy implies left homotopy

        source
        theorem SSet.Truncated.homotopicL_iff_homotopicR {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g : Edge x y} :
        HomotopicL f g ↔ HomotopicR f g

        In a 2-truncated quasicategory, the right and left homotopy relations coincide