@[reducible, inline]
abbrev
SSet.Truncated.Edge.edgeMap
{S : SSet}
{y₀ y₁ : ((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := edgeMap._proof_1 })}
(e : Edge y₀ y₁)
:
Equations
- e.edgeMap = SSet.yonedaEquiv.symm e.edge
Instances For
The inclusion ι₁₂ : Δ[1] ⟶ Λ[2, 1] restricts Λ[2, 1].ι to the face map δ 0.
The inclusion ι₀₁ : Δ[1] ⟶ Λ[2, 1] restricts Λ[2, 1].ι to the face map δ 2.
theorem
SSet.horn₂₁.path_edges_comm
{S : SSet}
{x₀ x₁ x₂ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(e₀₁ : Edge x₀ x₁)
(e₁₂ : Edge x₁ x₂)
:
noncomputable def
SSet.horn₂₁.fromEdges
{S : SSet}
{x₀ x₁ x₂ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(e₀₁ : Edge x₀ x₁)
(e₁₂ : Edge x₁ x₂)
:
Given the data of two consecutive edges e₀₁ and e₁₂, construct a map
Λ[2, 1].toSSet ⟶ S which restricts to maps Δ[1] ⟶ S corresponding
to the two edges (this is made precise in the lemmas horn_from_edges_restr₀ and
horn_from_edges_restr₁).
Equations
- SSet.horn₂₁.fromEdges e₀₁ e₁₂ = SSet.horn₂₁.isPushout.desc (SSet.Truncated.Edge.edgeMap e₀₁) (SSet.Truncated.Edge.edgeMap e₁₂) ⋯
Instances For
theorem
SSet.horn₂₁.horn_from_edges_restr₀
{S : SSet}
{x₀ x₁ x₂ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(e₀₁ : Edge x₀ x₁)
(e₁₂ : Edge x₁ x₂)
:
See horn_from_edges for details.
theorem
SSet.horn₂₁.horn_from_edges_restr₁
{S : SSet}
{x₀ x₁ x₂ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(e₀₁ : Edge x₀ x₁)
(e₁₂ : Edge x₁ x₂)
:
See horn_from_edges for details.
def
SSet.horn₂₁.fromHornExtension
{S : SSet}
{x₀ x₁ x₂ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(e₀₁ : Edge x₀ x₁)
(e₁₂ : Edge x₁ x₂)
(g : stdSimplex.obj { len := 2 } ⟶ S)
(comm : fromEdges e₀₁ e₁₂ = CategoryTheory.CategoryStruct.comp (horn 2 1).ι g)
:
(e₀₂ : Edge x₀ x₂) × e₀₁.CompStruct e₁₂ e₀₂
Given a map Δ[2] ⟶ S extending the horn given by horn_from_edges, construct
and edge e₀₂ such that e₀₁, e₁₂, e₀₂ bound a 2-simplex of S (this is witnessed
by CompStruct e₀₁ e₁₂ e₀₂).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SSet.δ_comp_yonedaEquiv_symm_eq
{S : SSet}
{i j : Fin 3}
{σ τ : S.obj (Opposite.op { len := 2 })}
(h :
(CategoryTheory.ConcreteCategory.hom (S.map (SimplexCategory.δ i).op)) σ = (CategoryTheory.ConcreteCategory.hom (S.map (SimplexCategory.δ j).op)) τ)
:
If two 2-simplices of S have equal i-th and j-th faces, then the corresponding face
restrictions Δ[1] ⟶ S of their classifying maps Δ[2] ⟶ S agree.
The face inclusions ι₀/ι₂/ι₃ : Δ[2] ⟶ Λ[3, 1] restrict Λ[3, 1].ι to δ 0/2/3.
noncomputable def
SSet.horn₃₁.fromFaces
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃)
:
Glue the three faces f₃, f₀, f₂ into a map Λ[3, 1].toSSet ⟶ S via the multicoequalizer
presentation of the horn (horn₃₁.desc). The three hypotheses are the compatibilities of the
faces along their shared edges e₁₂, e₁₃, e₀₁.
Equations
- SSet.horn₃₁.fromFaces f₃ f₀ f₂ = SSet.horn₃₁.desc (SSet.yonedaEquiv.symm f₀.simplex) (SSet.yonedaEquiv.symm f₂.simplex) (SSet.yonedaEquiv.symm f₃.simplex) ⋯ ⋯ ⋯
Instances For
theorem
SSet.horn₃₁.horn_extension_face₀
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃)
{g : stdSimplex.obj { len := 3 } ⟶ S}
(comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g)
:
theorem
SSet.horn₃₁.horn_extension_face₂
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃)
{g : stdSimplex.obj { len := 3 } ⟶ S}
(comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g)
:
theorem
SSet.horn₃₁.horn_extension_face₃
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃)
{g : stdSimplex.obj { len := 3 } ⟶ S}
(comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g)
:
def
SSet.horn₃₁.fromHornExtension
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃)
(g : stdSimplex.obj { len := 3 } ⟶ S)
(comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g)
:
Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃
Given a map Δ[3] ⟶ S extending the horn given by fromFaces, obtain a
2-simplex bounded by edges e₀₂, e₂₃ and e₀₃. See also Quasicategory₂.fill31.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The face inclusions ι₀/ι₁/ι₃ : Δ[2] ⟶ Λ[3, 2] restrict Λ[3, 2].ι to δ 0/1/3.
noncomputable def
SSet.horn₃₂.fromFaces
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃)
:
Glue the three faces f₃, f₀, f₁ into a map Λ[3, 2].toSSet ⟶ S via the multicoequalizer
presentation of the horn (horn₃₂.desc). The three hypotheses are the compatibilities of the
faces along their shared edges e₀₂, e₁₂, e₂₃.
Equations
- SSet.horn₃₂.fromFaces f₃ f₀ f₁ = SSet.horn₃₂.desc (SSet.yonedaEquiv.symm f₀.simplex) (SSet.yonedaEquiv.symm f₁.simplex) (SSet.yonedaEquiv.symm f₃.simplex) ⋯ ⋯ ⋯
Instances For
theorem
SSet.horn₃₂.horn_extension_face₀
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃)
{g : stdSimplex.obj { len := 3 } ⟶ S}
(comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g)
:
theorem
SSet.horn₃₂.horn_extension_face₁
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃)
{g : stdSimplex.obj { len := 3 } ⟶ S}
(comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g)
:
theorem
SSet.horn₃₂.horn_extension_face₃
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃)
{g : stdSimplex.obj { len := 3 } ⟶ S}
(comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g)
:
def
SSet.horn₃₂.fromHornExtension
{S : SSet}
{x₀ x₁ x₂ x₃ :
((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{e₀₁ : Edge x₀ x₁}
{e₁₂ : Edge x₁ x₂}
{e₂₃ : Edge x₂ x₃}
{e₀₂ : Edge x₀ x₂}
{e₁₃ : Edge x₁ x₃}
{e₀₃ : Edge x₀ x₃}
(f₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂)
(f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃)
(f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃)
(g : stdSimplex.obj { len := 3 } ⟶ S)
(comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g)
:
Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃
Given a map Δ[3] ⟶ S extending the horn given by fromFaces, obtain a
2-simplex bounded by edges e₀₁, e₁₃ and e₀₃. See also Quasicategory₂.fill32.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
SSet.Truncated.two_truncatation_of_qc_is_2_trunc_qc
{X : SSet}
[X.Quasicategory]
:
((truncation 2).obj X).Quasicategory₂
The 2-truncation of a quasi-category is a 2-truncated quasi-category.
theorem
SSet.Quasicategory₂.HomotopicL.refl
{A : Truncated 2}
{x y : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f : Truncated.Edge x y}
:
Left homotopy relation is reflexive
theorem
SSet.Quasicategory₂.HomotopicL.symm
{A : Truncated 2}
[A.Quasicategory₂]
{x y : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f g : Truncated.Edge x y}
(hfg : Truncated.HomotopicL f g)
:
Left homotopy relation is symmetric
theorem
SSet.Quasicategory₂.HomotopicL.trans
{A : Truncated 2}
[A.Quasicategory₂]
{x y : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f g h : Truncated.Edge x y}
(hfg : Truncated.HomotopicL f g)
(hgh : Truncated.HomotopicL g h)
:
Left homotopy relation is transitive
theorem
SSet.Quasicategory₂.HomotopicR.refl
{A : Truncated 2}
{x y : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f : Truncated.Edge x y}
:
Right homotopy relation is reflexive
theorem
SSet.Quasicategory₂.HomotopicR.symm
{A : Truncated 2}
[A.Quasicategory₂]
{x y : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f g : Truncated.Edge x y}
(hfg : Truncated.HomotopicR f g)
:
Right homotopy relation is symmetric
theorem
SSet.Quasicategory₂.HomotopicR.trans
{A : Truncated 2}
[A.Quasicategory₂]
{x y : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f g h : Truncated.Edge x y}
(hfg : Truncated.HomotopicR f g)
(hgh : Truncated.HomotopicR g h)
:
Right homotopy relation is transitive
theorem
SSet.Quasicategory₂.HomotopicL_iff_HomotopicR
{A : Truncated 2}
[A.Quasicategory₂]
{x y : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f g : Truncated.Edge x y}
:
The right and left homotopy relations coincide
theorem
SSet.Quasicategory₂.comp_unique
{A : Truncated 2}
[A.Quasicategory₂]
{x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f : Truncated.Edge x y}
{g : Truncated.Edge y z}
{h h' : Truncated.Edge x z}
(s : f.CompStruct g h)
(s' : f.CompStruct g h')
:
Truncated.HomotopicL h h'
theorem
SSet.Quasicategory₂.comp_unique'
{A : Truncated 2}
[A.Quasicategory₂]
{x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f : Truncated.Edge x y}
{g : Truncated.Edge y z}
{h h' : Truncated.Edge x z}
(s : Nonempty (f.CompStruct g h))
(s' : Nonempty (f.CompStruct g h'))
:
Truncated.HomotopicL h h'
theorem
SSet.Quasicategory₂.transport_edge₀
{A : Truncated 2}
[A.Quasicategory₂]
{x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f : Truncated.Edge x y}
{g g' : Truncated.Edge y z}
{h : Truncated.Edge x z}
(s : f.CompStruct g h)
(htpy : Truncated.HomotopicL g g')
:
Nonempty (f.CompStruct g' h)
theorem
SSet.Quasicategory₂.transport_edge₁
{A : Truncated 2}
[A.Quasicategory₂]
{x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f : Truncated.Edge x y}
{g : Truncated.Edge y z}
{h h' : Truncated.Edge x z}
(s : f.CompStruct g h)
(htpy : Truncated.HomotopicL h h')
:
Nonempty (f.CompStruct g h')
theorem
SSet.Quasicategory₂.transport_edge₂
{A : Truncated 2}
[A.Quasicategory₂]
{x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f f' : Truncated.Edge x y}
{g : Truncated.Edge y z}
{h : Truncated.Edge x z}
(s : f.CompStruct g h)
(htpy : Truncated.HomotopicL f f')
:
Nonempty (f'.CompStruct g h)
theorem
SSet.Quasicategory₂.transport_all_edges
{A : Truncated 2}
[A.Quasicategory₂]
{x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f f' : Truncated.Edge x y}
{g g' : Truncated.Edge y z}
{h h' : Truncated.Edge x z}
(hf : Truncated.HomotopicL f f')
(hg : Truncated.HomotopicL g g')
(hh : Truncated.HomotopicL h h')
(s : f.CompStruct g h)
:
Nonempty (f'.CompStruct g' h')
noncomputable def
SSet.Quasicategory₂.quotientReflPrefunctor₂
{A : Truncated 2}
[A.Quasicategory₂]
:
The reflexive prefunctor sending edges (in the 1-truncation) of A to their homotopy class.
Equations
- SSet.Quasicategory₂.quotientReflPrefunctor₂ = { obj := fun (X : SSet.OneTruncation₂ A) => { pt := X }, map := fun {X Y : SSet.OneTruncation₂ A} (f : X ⟶ Y) => Quotient.mk' f, map_id := ⋯ }
Instances For
By the adjunction ReflQuiv.adj, we obtain a functor from the free category on the reflexive
quiver underlying A to the homotopy category corresponding to quotientReflPrefunctor₂.
Equations
Instances For
The adjoint relation between quotientReflPrefunctor₂ and quotientFunctor₂ expressed
on the level of functors.
theorem
SSet.Quasicategory₂.qFunctor_map_toPath
{A : Truncated 2}
[A.Quasicategory₂]
(x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A))
(f : Truncated.Edge x.as y.as)
:
theorem
SSet.Quasicategory₂.composeEdges_unique
{A : Truncated 2}
[A.Quasicategory₂]
{x₀ x₁ x₂ : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
{f : Truncated.Edge x₀ x₁}
{g : Truncated.Edge x₁ x₂}
{h : Truncated.Edge x₀ x₂}
(s : f.CompStruct g h)
:
Truncated.HomotopicL h (f.comp g)
The edge composeEdges f g is the unique edge up to homotopy such that there is
a 2-simplex with spine given by f and g.
theorem
SSet.Quasicategory₂.qFunctor_respects_horel₂
{A : Truncated 2}
[A.Quasicategory₂]
(x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A))
(f g : x ⟶ y)
(r : OneTruncation₂.HoRel₂ A f g)
:
quotientFunctor₂ respects the hom relation HoRel₂.
def
SSet.Quasicategory₂.edgeToHom
{A : Truncated 2}
{x₀ x₁ : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(f : Truncated.Edge x₀ x₁)
:
An edge from x₀ to x₁ in a 2-truncated simplicial set defines an arrow in the refl quiver
OneTruncation₂.{u} A) from x₀ to x₁.
Equations
Instances For
def
SSet.Quasicategory₂.edgeToFreeHom
{A : Truncated 2}
{x₀ x₁ : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(f : Truncated.Edge x₀ x₁)
:
An edge from x₀ to x₁ in a 2-truncated simplicial set defines an arrow in the free category
generated from the refl quiver OneTruncation₂.{u} A) from x₀ to x₁.
Equations
Instances For
theorem
SSet.Quasicategory₂.compose_id_path
{A : Truncated 2}
{x₀ x₁ : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(f : Truncated.Edge x₀ x₁)
:
theorem
SSet.Quasicategory₂.homotopic_edges_are_equiv
{A : Truncated 2}
{x₀ x₁ : A.obj (Opposite.op { obj := { len := 0 }, property := Truncated.Edge.edgeMap._proof_1 })}
(f g : Truncated.Edge x₀ x₁)
(htpy : Truncated.HomotopicL f g)
:
OneTruncation₂.HoRel₂ A (edgeToFreeHom f) (edgeToFreeHom g)
Two (left) homotopic edges f, g are equivalent under the hom-relation HoRel₂
generated by 2-simplices.
noncomputable def
SSet.Quasicategory₂.liftRq₂
{A : Truncated 2}
[A.Quasicategory₂]
{C : Type u_1}
[CategoryTheory.ReflQuiver C]
(F : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A) ⥤rq C)
(h :
∀ (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y),
OneTruncation₂.HoRel₂ A f g → F.map f = F.map g)
:
If a reflexive prefunctor F : FreeRefl (OneTruncation₂ A) ⥤rq C respects
the hom-relation HoRel₂, then it can be lifted to HomotopyCategory₂ A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SSet.Quasicategory₂.lift_unique_rq₂
{A : Truncated 2}
[A.Quasicategory₂]
{C : Type u}
[CategoryTheory.ReflQuiver C]
(F₁ F₂ : A.HomotopyCategory₂ ⥤rq C)
(h : quotientReflPrefunctor₂ ⋙rq F₁ = quotientReflPrefunctor₂ ⋙rq F₂)
:
noncomputable def
SSet.Quasicategory₂.lift₂
{A : Truncated 2}
[A.Quasicategory₂]
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
(F : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) C)
(h :
∀ (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y),
OneTruncation₂.HoRel₂ A f g → F.map f = F.map g)
:
If a functor F : FreeRefl (OneTruncation₂ A) ⥤ C respects the hom-relation HoRel₂,
then it can be lifted to HomotopyCategory₂ A (see the weaker statement liftRq₂).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SSet.Quasicategory₂.is_lift₂
{A : Truncated 2}
[A.Quasicategory₂]
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
(F : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) C)
(h :
∀ (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y),
OneTruncation₂.HoRel₂ A f g → F.map f = F.map g)
:
theorem
SSet.Quasicategory₂.HomotopyCategory₂.lift_unique'
{A : Truncated 2}
[A.Quasicategory₂]
{C : Type u}
[CategoryTheory.Category.{u, u} C]
(F₁ F₂ : CategoryTheory.Functor A.HomotopyCategory₂ C)
(h : quotientFunctor₂.comp F₁ = quotientFunctor₂.comp F₂)
:
Lifts to the homotopy category are unique.
Since both HomotopyCategory A and HomotopyCategory₂ A satisfy the same universal property,
they are isomorphic.
Equations
- One or more equations did not get rendered due to their size.