The opposite of a join

The covariant involution SSet.opFunctor reverses the order of the vertices of every simplex. A simplex of the join K ⋆ L splits into an initial segment in K and a final segment in L; reversing its vertices gives a simplex that splits into an initial segment in Lᵒᵖ and a final segment in Kᵒᵖ. Hence (K ⋆ L)ᵒᵖ ≅ Lᵒᵖ ⋆ Kᵒᵖ (SSet.join.opIso), naturally in K and L and exchanging the two inclusions. This duality exchanges the two variables of the join, so that constructions and statements for one factor, such as slices C_{/p} built from the joins X ⋆ K, transfer to the other, such as coslices C_{p/} built from the joins K ⋆ X.

Main definitions

• SSet.JoinData.op: the opposite of join data on X for K ⋆ L, which are join data on Xᵒᵖ for Lᵒᵖ ⋆ Kᵒᵖ.
• SSet.join.opIso: the isomorphism (K ⋆ L)ᵒᵖ ≅ Lᵒᵖ ⋆ Kᵒᵖ.

Main results

• SSet.joinFiber_op: the parts of Xᵒᵖ over the vertices of Δ[1] along the opposite of p : X ⟶ Δ[1] are the opposites of the parts of X over the reversed vertices.
• SSet.JoinData.op_op: taking opposite join data is involutive.
• SSet.join.homEquiv_opFunctor_map_comp_opIso_hom: under the universal property of the join, SSet.join.opIso corresponds to taking opposite join data.
• SSet.join.opFunctor_map_inl_comp_opIso_hom, SSet.join.opFunctor_map_inr_comp_opIso_hom: the isomorphism exchanges the inclusions of the two factors.
• SSet.join.opFunctor_map_map_comp_opIso_hom: the isomorphism is natural in both factors.

References

• J. Lurie, Higher Topos Theory, §1.2.8.

theorem SSet.joinFiber_op {X : SSet} (p : X ⟶ stdSimplex.obj { len := 1 }) {e e' : Fin 2} (h : e.rev = e') : joinFiber (CategoryTheory.CategoryStruct.comp (opFunctor.map p) (stdSimplex.opIso { len := 1 }).hom) e' = (joinFiber p e).op

The part of Xᵒᵖ over the vertex e' of Δ[1] along the opposite of p : X ⟶ Δ[1] is the opposite of the part of X over the reversed vertex e.

def SSet.JoinData.op {X K L : SSet} (d : X.JoinData K L) : X.op.JoinData L.op K.op

The opposite of join data on X for K ⋆ L: join data on Xᵒᵖ for Lᵒᵖ ⋆ Kᵒᵖ, whose map to Δ[1] is the opposite of the original one, with the two vertices exchanged.

@[simp]

theorem SSet.JoinData.op_p {X K L : SSet} (d : X.JoinData K L) : d.op.p = CategoryTheory.CategoryStruct.comp (opFunctor.map d.p) (stdSimplex.opIso { len := 1 }).hom

The map to Δ[1] of the opposite join data is the opposite of the original one.

@[simp]

theorem SSet.JoinData.op_left_app {X K L : SSet} (d : X.JoinData K L) {n : SimplexCategoryᵒᵖ} (x : X.op.obj n) (hx : x ∈ (joinFiber d.op.p 0).obj n) : (CategoryTheory.ConcreteCategory.hom (d.op.left.app n)) ⟨x, hx⟩ = opObjEquiv.symm ((CategoryTheory.ConcreteCategory.hom (d.right.app n)) ⟨opObjEquiv x, ⋯⟩)

Over the vertex 0, the opposite join data on Xᵒᵖ are the opposite of the map to L of the original join data.

@[simp]

theorem SSet.JoinData.op_right_app {X K L : SSet} (d : X.JoinData K L) {n : SimplexCategoryᵒᵖ} (x : X.op.obj n) (hx : x ∈ (joinFiber d.op.p 1).obj n) : (CategoryTheory.ConcreteCategory.hom (d.op.right.app n)) ⟨x, hx⟩ = opObjEquiv.symm ((CategoryTheory.ConcreteCategory.hom (d.left.app n)) ⟨opObjEquiv x, ⋯⟩)

Over the vertex 1, the opposite join data on Xᵒᵖ are the opposite of the map to K of the original join data.

@[simp]

theorem SSet.JoinData.op_precomp {X Y K L : SSet} (d : X.JoinData K L) (g : Y ⟶ X) : (d.precomp g).op = d.op.precomp (opFunctor.map g)

Taking opposite join data commutes with restriction along a map g : Y ⟶ X.

@[simp]

theorem SSet.JoinData.op_postcomp {X K L K' L' : SSet} (d : X.JoinData K L) (f : K ⟶ K') (g : L ⟶ L') : (d.postcomp f g).op = d.op.postcomp (opFunctor.map g) (opFunctor.map f)

Taking opposite join data commutes with composition with maps f : K ⟶ K' and g : L ⟶ L', which exchange their roles.

theorem SSet.JoinData.op_op {X K L : SSet} (d : X.JoinData K L) : d.op.op = (d.precomp (opFunctorCompOpFunctorIso.hom.app X)).postcomp (opFunctorCompOpFunctorIso.inv.app K) (opFunctorCompOpFunctorIso.inv.app L)

Taking opposite join data twice gives back the original join data, through the involution Xᵒᵖᵒᵖ ≅ X.

def SSet.join.opIso (K L : SSet) : (K.join L).op ≅ L.op.join K.op

The opposite of a join: (K ⋆ L)ᵒᵖ ≅ Lᵒᵖ ⋆ Kᵒᵖ. A simplex of (K ⋆ L)ᵒᵖ is a simplex of K ⋆ L with its vertices read in reverse order, so its initial segment in K becomes a final segment in Kᵒᵖ, and its final segment in L an initial segment in Lᵒᵖ.

@[simp]

theorem SSet.join.objEquiv_opIso_hom_app {K L : SSet} {n : SimplexCategoryᵒᵖ} (x : (K.join L).op.obj n) : objEquiv ((CategoryTheory.ConcreteCategory.hom ((opIso K L).hom.app n)) x) = (objEquiv (opObjEquiv x)).op.precomp (stdSimplex.opIso (Opposite.unop n)).inv

The join data of the simplex of Lᵒᵖ ⋆ Kᵒᵖ corresponding to a simplex x of (K ⋆ L)ᵒᵖ are the opposite of the join data of x, transported along Δ[n] ≅ Δ[n]ᵒᵖ.

theorem SSet.join.homEquiv_opFunctor_map_comp_opIso_hom {X K L : SSet} (G : X ⟶ K.join L) : homEquiv (CategoryTheory.CategoryStruct.comp (opFunctor.map G) (opIso K L).hom) = (homEquiv G).op

Under the universal property of the join, the opposite Xᵒᵖ ⟶ (K ⋆ L)ᵒᵖ ≅ Lᵒᵖ ⋆ Kᵒᵖ of a map G : X ⟶ K ⋆ L corresponds to the opposite of the join data of G.

@[simp]

theorem SSet.join.homEquiv_opIso_hom (K L : SSet) : homEquiv (opIso K L).hom = (univ K L).op

Under the universal property of the join, the isomorphism (K ⋆ L)ᵒᵖ ≅ Lᵒᵖ ⋆ Kᵒᵖ corresponds to the opposite of the tautological join data on K ⋆ L.

@[simp]

theorem SSet.join.opFunctor_map_inl_comp_opIso_hom (K L : SSet) : CategoryTheory.CategoryStruct.comp (opFunctor.map (inl K L)) (opIso K L).hom = inr L.op K.op

The opposite of the inclusion of K into K ⋆ L is the inclusion of Kᵒᵖ into Lᵒᵖ ⋆ Kᵒᵖ.

@[simp]

theorem SSet.join.opFunctor_map_inl_comp_opIso_hom_assoc (K L : SSet) {Z : SSet} (h : L.op.join K.op ⟶ Z) : CategoryTheory.CategoryStruct.comp (opFunctor.map (inl K L)) (CategoryTheory.CategoryStruct.comp (opIso K L).hom h) = CategoryTheory.CategoryStruct.comp (inr L.op K.op) h

The opposite of the inclusion of K into K ⋆ L is the inclusion of Kᵒᵖ into Lᵒᵖ ⋆ Kᵒᵖ.

@[simp]

theorem SSet.join.opFunctor_map_inr_comp_opIso_hom (K L : SSet) : CategoryTheory.CategoryStruct.comp (opFunctor.map (inr K L)) (opIso K L).hom = inl L.op K.op

The opposite of the inclusion of L into K ⋆ L is the inclusion of Lᵒᵖ into Lᵒᵖ ⋆ Kᵒᵖ.

@[simp]

theorem SSet.join.opFunctor_map_inr_comp_opIso_hom_assoc (K L : SSet) {Z : SSet} (h : L.op.join K.op ⟶ Z) : CategoryTheory.CategoryStruct.comp (opFunctor.map (inr K L)) (CategoryTheory.CategoryStruct.comp (opIso K L).hom h) = CategoryTheory.CategoryStruct.comp (inl L.op K.op) h

The opposite of the inclusion of L into K ⋆ L is the inclusion of Lᵒᵖ into Lᵒᵖ ⋆ Kᵒᵖ.

@[simp]

theorem SSet.join.opFunctor_map_map_comp_opIso_hom {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') : CategoryTheory.CategoryStruct.comp (opFunctor.map (map f g)) (opIso K' L').hom = CategoryTheory.CategoryStruct.comp (opIso K L).hom (map (opFunctor.map g) (opFunctor.map f))

The isomorphism (K ⋆ L)ᵒᵖ ≅ Lᵒᵖ ⋆ Kᵒᵖ is natural in K and L.

@[simp]

theorem SSet.join.opFunctor_map_map_comp_opIso_hom_assoc {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') {Z : SSet} (h : L'.op.join K'.op ⟶ Z) : CategoryTheory.CategoryStruct.comp (opFunctor.map (map f g)) (CategoryTheory.CategoryStruct.comp (opIso K' L').hom h) = CategoryTheory.CategoryStruct.comp (opIso K L).hom (CategoryTheory.CategoryStruct.comp (map (opFunctor.map g) (opFunctor.map f)) h)

The isomorphism (K ⋆ L)ᵒᵖ ≅ Lᵒᵖ ⋆ Kᵒᵖ is natural in K and L.