Documentation

Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

ZerothHomotopy and connected components of TopCat.toSSet.obj X #

In this file, given X : TopCat, we define a bijection TopCat.zerothHomotopyEquiv between ZerothHomotopy X and (TopCat.toSSet.obj X).π₀.

source
noncomputable def TopCat.toSSetObj₁Equiv {X : TopCat} :
(toSSet.obj X).obj (Opposite.op { len := 1 }) ≃ (I ⟶ X)

Given X : TopCat, this is the bijection between 1-simplices of the singular simplicial set of X and the type of morphisms I ⟶ X.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TopCat.toSSetObj₁Equiv_apply_zero {X : TopCat} (s : (toSSet.obj X).obj (Opposite.op { len := 1 })) :
    (CategoryTheory.ConcreteCategory.hom (toSSetObj₁Equiv s)) 0 = toSSetObj₀Equiv ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 1)) s)
    source
    @[simp]
    theorem TopCat.toSSetObj₁Equiv_apply_one {X : TopCat} (s : (toSSet.obj X).obj (Opposite.op { len := 1 })) :
    (CategoryTheory.ConcreteCategory.hom (toSSetObj₁Equiv s)) 1 = toSSetObj₀Equiv ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 0)) s)
    source
    @[simp]
    theorem TopCat.δ_one_toSSetObj₁Equiv.symm {X : TopCat} (f : I ⟶ X) :
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 1)) (toSSetObj₁Equiv.symm f) = toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) 0)
    source
    @[simp]
    theorem TopCat.δ_zero_toSSetObj₁Equiv.symm {X : TopCat} (f : I ⟶ X) :
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 0)) (toSSetObj₁Equiv.symm f) = toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) 1)
    source
    noncomputable def TopCat.toSSetObjEdgeEquiv {X : TopCat} {x y : ↑X} :
    SSet.Edge (toSSetObj₀Equiv.symm x) (toSSetObj₀Equiv.symm y) ≃ X.Path x y

    Given two points x and y of X : TopCat, this is the bijection between edges in the simplicial set toSSet.obj X connecting the vertices corresponding to x and y, and paths from x to y.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TopCat.toSSetObjEdgeEquiv_symm_apply {X : TopCat} {x y : ↑X} (p : X.Path x y) :
      toSSetObjEdgeEquiv.symm p = SSet.Edge.mk (toSSetObj₁Equiv.symm p.hom) ⋯ ⋯
      source
      @[simp]
      theorem TopCat.toSSetObjEdgeEquiv_apply_hom {X : TopCat} {x y : ↑X} (e : SSet.Edge (toSSetObj₀Equiv.symm x) (toSSetObj₀Equiv.symm y)) :
      (toSSetObjEdgeEquiv e).hom = toSSetObj₁Equiv e.edge
      source
      noncomputable def TopCat.zerothHomotopyEquiv {X : TopCat} :
      ZerothHomotopy ↑X ≃ (toSSet.obj X).π₀

      Given X : TopCat, this is the bijection between ZerothHomotopy X and the type of connected components of the simplicial set toSSet.obj X.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TopCat.zerothHomotopyEquiv_mk {X : TopCat} (x : ↑X) :
        zerothHomotopyEquiv (ZerothHomotopy.mk x) = SSet.π₀.mk (toSSetObj₀Equiv.symm x)
        source
        @[simp]
        theorem TopCat.zerothHomotopyEquiv_symm_mk {X : TopCat} (x : (toSSet.obj X).obj (Opposite.op { len := 0 })) :
        zerothHomotopyEquiv.symm (SSet.π₀.mk x) = ZerothHomotopy.mk (toSSetObj₀Equiv x)
        source
        instance TopCat.instIsConnectedObjSSetToSSetOfPathConnectedSpaceCarrier {X : TopCat} [PathConnectedSpace ↑X] :
        (toSSet.obj X).IsConnected