Documentation

TauCeti.AlgebraicTopology.SimplicialSet.Pointed.Circle

The simplicial circle as `Δ[1]/∂Δ[1]` #

Mathlib defines the simplicial circle SSet.S1 as the coequalizer of the two vertex inclusions Δ[0] ⟶ Δ[1]. This file names its quotient map TauCeti.SSet.S1.quotient, its descent TauCeti.SSet.S1.desc and its basepoint TauCeti.SSet.S1.basepoint, shows that both vertices of the interval are sent to the basepoint, and proves TauCeti.SSet.S1.isPushout: the circle is the pushout of the boundary inclusion ∂Δ[1] ⟶ Δ[1] along the collapse ∂Δ[1] ⟶ Δ[0], i.e. the interval with its boundary collapsed to the basepoint.

Like Mathlib's SSet.S1, everything in this file lives in universe 0.

The final section equips the interval and circle with their distinguished vertices. It gives the quotient as a based map and packages its universal property directly in PointedSSet.

def TauCeti.SSet.S1.boundaryCollapse :

(SSet.boundary 1).toSSet ⟶ SSet.stdSimplex.obj { len := 0 }

The map which collapses the boundary of the simplicial interval to Δ[0].

Instances For

noncomputable def TauCeti.SSet.S1.quotient :

SSet.stdSimplex.obj { len := 1 } ⟶ SSet.S1

The quotient map from the simplicial interval to the simplicial circle.

Instances For

instance TauCeti.SSet.S1.instEpiSSetQuotient :

CategoryTheory.Epi quotient

noncomputable def TauCeti.SSet.S1.desc {X : SSet} (f : SSet.stdSimplex.obj { len := 1 } ⟶ X) (h : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f) :

A map from the simplicial interval which identifies its two vertices descends to the simplicial circle.

Instances For

@[simp]

theorem TauCeti.SSet.S1.quotient_desc {X : SSet} (f : SSet.stdSimplex.obj { len := 1 } ⟶ X) (h : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f) :

CategoryTheory.CategoryStruct.comp quotient (desc f h) = f

The descent of f to the circle restricts back to f along the quotient map.

@[simp]

theorem TauCeti.SSet.S1.quotient_desc_assoc {X : SSet} (f : SSet.stdSimplex.obj { len := 1 } ⟶ X) (h : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f) {Z : SSet} (h✝ : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp quotient (CategoryTheory.CategoryStruct.comp (desc f h) h✝) = CategoryTheory.CategoryStruct.comp f h✝

The descent of f to the circle restricts back to f along the quotient map.

noncomputable def TauCeti.SSet.S1.basepoint :

SSet.stdSimplex.obj { len := 0 } ⟶ SSet.S1

The distinguished vertex of the simplicial circle.

Instances For

@[simp]

theorem TauCeti.SSet.S1.δ_quotient (i : Fin 2) :

CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) quotient = basepoint

Both vertices of the simplicial interval map to the basepoint of the circle.

@[simp]

theorem TauCeti.SSet.S1.δ_quotient_assoc (i : Fin 2) {Z : SSet} (h : SSet.S1 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) (CategoryTheory.CategoryStruct.comp quotient h) = CategoryTheory.CategoryStruct.comp basepoint h

Both vertices of the simplicial interval map to the basepoint of the circle.

@[simp]

theorem TauCeti.SSet.S1.boundary_ι_quotient :

CategoryTheory.CategoryStruct.comp (SSet.boundary 1).ι quotient = CategoryTheory.CategoryStruct.comp boundaryCollapse basepoint

The quotient map agrees with the basepoint after collapsing the boundary.

@[simp]

theorem TauCeti.SSet.S1.boundary_ι_quotient_assoc {Z : SSet} (h : SSet.S1 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (SSet.boundary 1).ι (CategoryTheory.CategoryStruct.comp quotient h) = CategoryTheory.CategoryStruct.comp boundaryCollapse (CategoryTheory.CategoryStruct.comp basepoint h)

The quotient map agrees with the basepoint after collapsing the boundary.

theorem TauCeti.SSet.S1.hom_ext {X : SSet} {f g : SSet.S1 ⟶ X} (h : CategoryTheory.CategoryStruct.comp quotient f = CategoryTheory.CategoryStruct.comp quotient g) :

f = g

Maps from the simplicial circle are determined by their composites with the quotient map.

theorem TauCeti.SSet.S1.hom_ext_iff {X : SSet} {f g : SSet.S1 ⟶ X} :

f = g ↔ CategoryTheory.CategoryStruct.comp quotient f = CategoryTheory.CategoryStruct.comp quotient g

theorem TauCeti.SSet.S1.isPushout :

CategoryTheory.IsPushout (SSet.boundary 1).ι boundaryCollapse quotient basepoint

The simplicial circle is Δ[1]/∂Δ[1]: the pushout of the boundary inclusion along the collapse of the boundary to the basepoint.

@[reducible, inline]

noncomputable abbrev TauCeti.PointedSSet.interval :

The simplicial interval pointed at vertex 1, the image of δ 0. Its underlying simplicial set is definitionally Δ[1].

Instances For

@[reducible, inline]

noncomputable abbrev TauCeti.PointedSSet.circle :

The simplicial circle pointed at the image of either endpoint of the interval. Its underlying simplicial set is definitionally Mathlib's SSet.S1.

Instances For

noncomputable def TauCeti.PointedSSet.circleQuotient :

interval ⟶ circle

The quotient from the pointed interval to the pointed simplicial circle.

Instances For

@[simp]

theorem TauCeti.PointedSSet.circleQuotient_right :

CategoryTheory.Under.Hom.right circleQuotient = SSet.S1.quotient

noncomputable def TauCeti.PointedSSet.circleDesc {X : PointedSSet} (f : interval ⟶ X) (h : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) (CategoryTheory.Under.Hom.right f) = CategoryTheory.Under.hom X) :

A based map from the interval which also sends vertex 0, the image of δ 1, to the basepoint descends to a based map from the simplicial circle.

Instances For

@[simp]

theorem TauCeti.PointedSSet.circleDesc_right {X : PointedSSet} (f : interval ⟶ X) (h : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) (CategoryTheory.Under.Hom.right f) = CategoryTheory.Under.hom X) :

CategoryTheory.Under.Hom.right (circleDesc f h) = SSet.S1.desc (CategoryTheory.Under.Hom.right f) ⋯

The underlying map of the based descent is the unpointed circle descent.

@[simp]

theorem TauCeti.PointedSSet.circleQuotient_circleDesc {X : PointedSSet} (f : interval ⟶ X) (h : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) (CategoryTheory.Under.Hom.right f) = CategoryTheory.Under.hom X) :

CategoryTheory.CategoryStruct.comp circleQuotient (circleDesc f h) = f

Descending a based interval map and then pulling back along the circle quotient recovers the original map.

theorem TauCeti.PointedSSet.circleHom_ext {X : PointedSSet} {f g : circle ⟶ X} (h : CategoryTheory.CategoryStruct.comp circleQuotient f = CategoryTheory.CategoryStruct.comp circleQuotient g) :

f = g

Based maps out of the simplicial circle are determined by their pullback to the pointed interval.

theorem TauCeti.PointedSSet.circleHom_ext_iff {X : PointedSSet} {f g : circle ⟶ X} :

f = g ↔ CategoryTheory.CategoryStruct.comp circleQuotient f = CategoryTheory.CategoryStruct.comp circleQuotient g

noncomputable def TauCeti.PointedSSet.circleHomEquiv (X : PointedSSet) :

(circle ⟶ X) ≃ { f : interval ⟶ X // CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) (CategoryTheory.Under.Hom.right f) = CategoryTheory.Under.hom X }

Based maps from the simplicial circle are equivalent to based maps from the interval which send vertex 0, the image of δ 1, to the basepoint.

Instances For

@[simp]

theorem TauCeti.PointedSSet.circleHomEquiv_apply (X : PointedSSet) (f : circle ⟶ X) :

↑(X.circleHomEquiv f) = CategoryTheory.CategoryStruct.comp circleQuotient f

@[simp]

theorem TauCeti.PointedSSet.circleHomEquiv_symm_apply (X : PointedSSet) (f : { f : interval ⟶ X // CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) (CategoryTheory.Under.Hom.right f) = CategoryTheory.Under.hom X }) :

X.circleHomEquiv.symm f = circleDesc ↑f ⋯