Complements on the opposite of a simplicial set

Mathlib's covariant involution SSet.opFunctor : SSet ⥤ SSet reverses the order of the vertices of every simplex, and SSet.stdSimplex.opIso n : Δ[n]ᵒᵖ ≅ Δ[n] identifies the opposite of a standard simplex with itself. This file records that SSet.opFunctor is an equivalence of categories, and the compatibilities of SSet.stdSimplex.opIso with maps of standard simplices, with the involution, and with the Yoneda bijection. They are what one needs to transport constructions on simplicial sets, such as joins and slices, along the opposite.

Main results

• SSet.stdSimplex.map_comp_opIso_inv: the isomorphism Δ[n]ᵒᵖ ≅ Δ[n] is natural in n.
• SSet.stdSimplex.opFunctor_map_opIso_hom_comp_opIso_hom, SSet.stdSimplex.opIso_inv_comp_opFunctor_map_opIso_inv: it is involutive.
• SSet.stdSimplex.opFunctor_map_const_comp_opIso_hom: the opposite of a constant map to Δ[n] is the constant map at the reversed vertex.
• SSet.stdSimplex.opIso_inv_comp_opFunctor_map_yonedaEquiv_symm: the map Δ[n] ⟶ Xᵒᵖ given by an n-simplex of Xᵒᵖ is the opposite of the map Δ[n] ⟶ X given by the same simplex of X.
• SSet.Edge.opEquiv: the edges of Xᵒᵖ are the edges of X with source and target exchanged.
• SSet.Edge.CompStruct.opEquiv: a 2-simplex of X exhibiting e₀₂ as a composite of e₀₁ and e₁₂ is a 2-simplex of Xᵒᵖ exhibiting the opposite of e₀₂ as a composite of the opposites of e₁₂ and e₀₁.

instance SSet.instIsEquivalenceOpFunctor_tauCeti : opFunctor.IsEquivalence

The involution SSet.opFunctor is an equivalence of categories, so that it is full and faithful.

theorem SSet.stdSimplex.map_comp_opIso_inv {m n : SimplexCategory} (f : m ⟶ n) : CategoryTheory.CategoryStruct.comp (stdSimplex.map f) (opIso n).inv = CategoryTheory.CategoryStruct.comp (opIso m).inv (opFunctor.map (stdSimplex.map (SimplexCategory.rev.map f)))

The isomorphism Δ[n]ᵒᵖ ≅ Δ[n] reversing the order of the vertices is natural in n, where a map f of the simplex category acts on the opposite through its reverse SimplexCategory.rev.map f.

theorem SSet.stdSimplex.map_comp_opIso_inv_assoc {m n : SimplexCategory} (f : m ⟶ n) {Z : SSet} (h : (stdSimplex.obj n).op ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.map f) (CategoryTheory.CategoryStruct.comp (opIso n).inv h) = CategoryTheory.CategoryStruct.comp (opIso m).inv (CategoryTheory.CategoryStruct.comp (opFunctor.map (stdSimplex.map (SimplexCategory.rev.map f))) h)

The isomorphism Δ[n]ᵒᵖ ≅ Δ[n] reversing the order of the vertices is natural in n, where a map f of the simplex category acts on the opposite through its reverse SimplexCategory.rev.map f.

@[simp]

theorem SSet.stdSimplex.opFunctor_map_opIso_hom_comp_opIso_hom (n : SimplexCategory) : CategoryTheory.CategoryStruct.comp (opFunctor.map (opIso n).hom) (opIso n).hom = opFunctorCompOpFunctorIso.hom.app (stdSimplex.obj n)

Reversing the order of the vertices twice is the identity: the isomorphism Δ[n]ᵒᵖ ≅ Δ[n] is compatible with the involution opFunctorCompOpFunctorIso : Xᵒᵖᵒᵖ ≅ X.

@[simp]

theorem SSet.stdSimplex.opFunctor_map_opIso_hom_comp_opIso_hom_assoc (n : SimplexCategory) {Z : SSet} (h : stdSimplex.obj n ⟶ Z) : CategoryTheory.CategoryStruct.comp (opFunctor.map (opIso n).hom) (CategoryTheory.CategoryStruct.comp (opIso n).hom h) = CategoryTheory.CategoryStruct.comp (opFunctorCompOpFunctorIso.hom.app (stdSimplex.obj n)) h

Reversing the order of the vertices twice is the identity: the isomorphism Δ[n]ᵒᵖ ≅ Δ[n] is compatible with the involution opFunctorCompOpFunctorIso : Xᵒᵖᵒᵖ ≅ X.

@[simp]

theorem SSet.stdSimplex.opIso_inv_comp_opFunctor_map_opIso_inv (n : SimplexCategory) : CategoryTheory.CategoryStruct.comp (opIso n).inv (opFunctor.map (opIso n).inv) = opFunctorCompOpFunctorIso.inv.app (stdSimplex.obj n)

Reversing the order of the vertices of Δ[n] twice is the identity, in the form of the inverse of SSet.stdSimplex.opFunctor_map_opIso_hom_comp_opIso_hom.

@[simp]

theorem SSet.stdSimplex.opIso_inv_comp_opFunctor_map_opIso_inv_assoc (n : SimplexCategory) {Z : SSet} (h : opFunctor.obj (stdSimplex.obj n).op ⟶ Z) : CategoryTheory.CategoryStruct.comp (opIso n).inv (CategoryTheory.CategoryStruct.comp (opFunctor.map (opIso n).inv) h) = CategoryTheory.CategoryStruct.comp (opFunctorCompOpFunctorIso.inv.app (stdSimplex.obj n)) h

Reversing the order of the vertices of Δ[n] twice is the identity, in the form of the inverse of SSet.stdSimplex.opFunctor_map_opIso_hom_comp_opIso_hom.

@[simp]

theorem SSet.stdSimplex.opFunctor_map_const_comp_opIso_hom {X : SSet} {n : ℕ} (e : Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (opFunctor.map (SSet.const (const n e (Opposite.op { len := 0 })))) (opIso { len := n }).hom = SSet.const (const n e.rev (Opposite.op { len := 0 }))

The opposite of the constant map at the vertex e of Δ[n] is, through the isomorphism Δ[n]ᵒᵖ ≅ Δ[n] reversing the vertices, the constant map at the reversed vertex e.rev.

theorem SSet.stdSimplex.opIso_inv_comp_opFunctor_map_yonedaEquiv_symm {X : SSet} {n : SimplexCategory} (x : X.obj (Opposite.op n)) : CategoryTheory.CategoryStruct.comp (opIso n).inv (opFunctor.map (yonedaEquiv.symm x)) = yonedaEquiv.symm (opObjEquiv.symm x)

The map Δ[n] ⟶ Xᵒᵖ given by an n-simplex x of Xᵒᵖ is, through the isomorphism Δ[n] ≅ Δ[n]ᵒᵖ reversing the vertices, the opposite of the map Δ[n] ⟶ X given by x.

def SSet.Edge.opEquiv {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} : Edge x₀ x₁ ≃ Edge (opObjEquiv.symm x₁) (opObjEquiv.symm x₀)

The edges of Xᵒᵖ are the edges of X with source and target exchanged: the same 1-simplex, read with its vertices in the reverse order.

@[simp]

theorem SSet.Edge.opEquiv_edge {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : Edge x₀ x₁) : (opEquiv e).edge = opObjEquiv.symm e.edge

@[simp]

theorem SSet.Edge.opEquiv_symm_edge {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : Edge (opObjEquiv.symm x₁) (opObjEquiv.symm x₀)) : (opEquiv.symm e).edge = opObjEquiv e.edge

@[simp]

theorem SSet.Edge.opEquiv_id {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : opEquiv (id x) = id (opObjEquiv.symm x)

The opposite of an identity edge is an identity edge.

def SSet.Edge.CompStruct.opEquiv {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} : e₀₁.CompStruct e₁₂ e₀₂ ≃ (Edge.opEquiv e₁₂).CompStruct (Edge.opEquiv e₀₁) (Edge.opEquiv e₀₂)

A 2-simplex of X exhibiting e₀₂ as a composite of e₀₁ and e₁₂ is a 2-simplex of Xᵒᵖ exhibiting the opposite of e₀₂ as a composite of the opposites of e₁₂ and e₀₁.

@[simp]

theorem SSet.Edge.CompStruct.opEquiv_simplex {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : (opEquiv h).simplex = opObjEquiv.symm h.simplex

@[simp]

theorem SSet.Edge.CompStruct.opEquiv_symm_simplex {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : (Edge.opEquiv e₁₂).CompStruct (Edge.opEquiv e₀₁) (Edge.opEquiv e₀₂)) : (opEquiv.symm h).simplex = opObjEquiv h.simplex