Homotopic maps induce isomorphic functors on the fundamental groupoid

The main definition in this file is SSet.congrMapFundamentalGroupoid. Given two morphisms of simplicial sets f : X ⟶ Y and g : X ⟶ Y and a homotopy h : Homotopy f g, this is an isomorphism between the functors mapFundamentalGroupoid f and mapFundamentalGroupoid g.

Implementation notes

We first define the variant SSet.congrMapFundamentalGroupoid' which takes as an input a combinatorial simplicial homotopy (as h : SimplicialObject.Homotopy f g), and we deduce the result for terms in SSet.Homotopy f g which involve a morphism X ⊗ Δ[1] ⟶ Y.

Given ``h : SimplicialObject.Homotopy f gwherefandgare morphisms of simplicial setsX ⟶ Y, we define an edge ofSimplicialObjectHomotopy h xconnectingf.app _ xandg.app _ xfor anyx : X _⦋0⦌. If eis an edge fromxtoy, we obtain a diagram involving edges which gives a commutative diagram in the fundamental groupoid (see the lemma FundamentalGroupoid.comm_of_ofSimplicialObjectHomotopy`):

f.app _ x ---> g.app _ x
    |     \        |
    |      \       |
    |       \      |
    |        \     |
    v         v    v
f.app _ y ---> g.app _ y

The horizontal edges are obtained by Edge.ofSimplicialObjectHomotopy, the vertical edges are the images of e by f and g, and the diagonal edge is defined as Edge.diagOfSimplicialObjectHomotopy h e. The commutativity of the lower left triangle is justified by Edge.CompStruct.ofSimplicialObjectHomotopy, and the commutativity of the upper right triangle is justified by Edge.CompStruct.ofSimplicialObjectHomotopy'.

def SSet.Edge.ofSimplicialObjectHomotopy {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) (x : X.obj (Opposite.op { len := 0 })) : Edge ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 0 }))) x)

The edge connecting f.app _ x and g.app _ x when h : SimplicialObject.Homotopy f g and x is a 0-simplex.

Equations

• SSet.Edge.ofSimplicialObjectHomotopy h x = SSet.Edge.mk ((CategoryTheory.ConcreteCategory.hom (h.h 0)) x) ⋯ ⋯

@[simp]

theorem SSet.Edge.ofSimplicialObjectHomotopy_edge {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) (x : X.obj (Opposite.op { len := 0 })) : (ofSimplicialObjectHomotopy h x).edge = (CategoryTheory.ConcreteCategory.hom (h.h 0)) x

def SSet.Edge.diagOfSimplicialObjectHomotopy {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : Edge ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 0 }))) y)

Given h : SimplicialObject.Homotopy f g and an edge e : Edge x y, this is the edge that is the diagonal of the "commutative square" involving f.app _ x, g.app _ x, g.app _ y and f.app _ y.

Equations

• One or more equations did not get rendered due to their size.

theorem SSet.Edge.diagOfSimplicialObjectHomotopy_edge {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : (diagOfSimplicialObjectHomotopy h e).edge = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Y 1)) ((CategoryTheory.ConcreteCategory.hom (h.h 1)) e.edge)

theorem SSet.Edge.diagOfSimplicialObjectHomotopy_edge' {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : (diagOfSimplicialObjectHomotopy h e).edge = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Y 1)) ((CategoryTheory.ConcreteCategory.hom (h.h 0)) e.edge)

def SSet.Edge.CompStruct.ofSimplicialObjectHomotopy {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : (e.map f).CompStruct (Edge.ofSimplicialObjectHomotopy h y) (diagOfSimplicialObjectHomotopy h e)

The lower left triangle of the "commutative square" that diagOfSimplicialObjectHomotopy h e is part of, when h : SimplicialObject.Homotopy f g and e is an edge.

Equations

• SSet.Edge.CompStruct.ofSimplicialObjectHomotopy h e = SSet.Edge.CompStruct.mk ((CategoryTheory.ConcreteCategory.hom (h.h 1)) e.edge) ⋯ ⋯ ⋯

def SSet.Edge.CompStruct.ofSimplicialObjectHomotopy' {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : (Edge.ofSimplicialObjectHomotopy h x).CompStruct (e.map g) (diagOfSimplicialObjectHomotopy h e)

The upper right triangle of the "commutative square" that diagOfSimplicialObjectHomotopy h e is part of, when h : SimplicialObject.Homotopy f g and e is an edge.

Equations

• SSet.Edge.CompStruct.ofSimplicialObjectHomotopy' h e = SSet.Edge.CompStruct.mk ((CategoryTheory.ConcreteCategory.hom (h.h 0)) e.edge) ⋯ ⋯ ⋯

theorem SSet.FundamentalGroupoid.comm_of_ofSimplicialObjectHomotopy {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : CategoryTheory.CategoryStruct.comp (homMk (e.map f)) (homMk (Edge.ofSimplicialObjectHomotopy h y)) = CategoryTheory.CategoryStruct.comp (homMk (Edge.ofSimplicialObjectHomotopy h x)) (homMk (e.map g))

theorem SSet.FundamentalGroupoid.comm_of_ofSimplicialObjectHomotopy_assoc {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) {Z : Y.FundamentalGroupoid} (h✝ : mk ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 0 }))) y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (homMk (e.map f)) (CategoryTheory.CategoryStruct.comp (homMk (Edge.ofSimplicialObjectHomotopy h y)) h✝) = CategoryTheory.CategoryStruct.comp (homMk (Edge.ofSimplicialObjectHomotopy h x)) (CategoryTheory.CategoryStruct.comp (homMk (e.map g)) h✝)

noncomputable def SSet.congrMapFundamentalGroupoid' {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) : mapFundamentalGroupoid f ≅ mapFundamentalGroupoid g

Two homotopic maps of simplicial sets (where the homotopy is given by a term in SimplicialObject.Homotopy) induce isomorphic functors between the fundamental groupoids.

Equations

• One or more equations did not get rendered due to their size.

theorem SSet.congrMapFundamentalGroupoid'_hom_app_mk {X Y : SSet} {f g : X ⟶ Y} (h : CategoryTheory.SimplicialObject.Homotopy f g) (x : X.obj (Opposite.op { len := 0 })) : (congrMapFundamentalGroupoid' h).hom.app (FundamentalGroupoid.mk x) = FundamentalGroupoid.homMk (Edge.ofSimplicialObjectHomotopy h x)

noncomputable def SSet.congrMapFundamentalGroupoid {X Y : SSet} {f g : X ⟶ Y} (h : Homotopy f g) : mapFundamentalGroupoid f ≅ mapFundamentalGroupoid g

Two homotopic maps of simplicial sets (where the homotopy is given by a term in SSet.Homotopy) induce isomorphic functors between the fundamental groupoids.

Equations

• SSet.congrMapFundamentalGroupoid h = SSet.congrMapFundamentalGroupoid' h.toSimplicialObjectHomotopy

theorem SSet.congrMapFundamentalGroupoid_hom_app_mk {X Y : SSet} {f g : X ⟶ Y} (h : Homotopy f g) (x : X.obj (Opposite.op { len := 0 })) : (congrMapFundamentalGroupoid h).hom.app (FundamentalGroupoid.mk x) = FundamentalGroupoid.homMk (Edge.ofSimplicialObjectHomotopy h.toSimplicialObjectHomotopy x)