The fundamental groupoid of a simplicial set

In this file, we define the fundamental groupoid SSet.Truncated.FundamentalGroupoid X of a 2-truncated simplicial set X. We also define the fundamental groupoid SSet.FundamentalGroupoid X of a simplicial set X.

Implementation notes

In order to get good definitional properties at implicit transparency, we do not define FundamentalGroupoid X as FreeGroupoid X.HomotopyCategory, but only as an induced category via a bijection FundamentalGroupoid X ≃ FreeGroupoid X.HomotopyCategory. If f : X ⟶ Y is a morphism of simplicial sets and x : X _⦋0⦌, this allows to obtain the equality (mapFundamentalGroupoid f).obj (mk x) = mk (f.app _ x) by with_implicit rfl.

structure SSet.Truncated.FundamentalGroupoid (X : Truncated 2) : Type u

The fundamental groupoid of a 2-truncated simplicial set.

• pt : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })

  The underlying vertex.

theorem SSet.Truncated.FundamentalGroupoid.mk_surjective {X : Truncated 2} : Function.Surjective mk

def SSet.Truncated.FundamentalGroupoid.equivFreeGroupoid {X : Truncated 2} : X.FundamentalGroupoid ≃ CategoryTheory.FreeGroupoid X.HomotopyCategory

The bijection FundamentalGroupoid X ≃ FreeGroupoid X.HomotopyCategory that is used to define the category structure on FundamentalGroupoid X when X is a 2-truncated simplicial set.

Equations

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

@[instance_reducible]

instance SSet.Truncated.FundamentalGroupoid.instCategory {X : Truncated 2} : CategoryTheory.Category.{u, u} X.FundamentalGroupoid

Equations

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

def SSet.Truncated.FundamentalGroupoid.isoCatFreeGroupoid (X : Truncated 2) : CategoryTheory.IsoCat X.FundamentalGroupoid (CategoryTheory.FreeGroupoid X.HomotopyCategory)

The isomorphism of categories between FundamentalGroupoid X and FreeGroupoid X.HomotopyCategory when X is a2-truncated simplicial set.

Equations

• SSet.Truncated.FundamentalGroupoid.isoCatFreeGroupoid X = CategoryTheory.InducedCategory.isoCat SSet.Truncated.FundamentalGroupoid.equivFreeGroupoid

@[reducible, inline]

abbrev SSet.Truncated.FundamentalGroupoid.equivalenceFreeGroupoid (X : Truncated 2) : X.FundamentalGroupoid ≌ CategoryTheory.FreeGroupoid X.HomotopyCategory

The equivalence of categories between FundamentalGroupoid X and FreeGroupoid X.HomotopyCategory when X is a2-truncated simplicial set.

Equations

• SSet.Truncated.FundamentalGroupoid.equivalenceFreeGroupoid X = (SSet.Truncated.FundamentalGroupoid.isoCatFreeGroupoid X).toEquivalence

@[instance_reducible]

instance SSet.Truncated.FundamentalGroupoid.instGroupoid {X : Truncated 2} : CategoryTheory.Groupoid X.FundamentalGroupoid

Equations

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

def SSet.Truncated.FundamentalGroupoid.homMk {X : Truncated 2} {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} (e : Edge x y) : { pt := x } ⟶ { pt := y }

Constructor for morphisms in the fundamental groupoid of a 2-truncated simplicial set.

Equations

• SSet.Truncated.FundamentalGroupoid.homMk e = { hom := CategoryTheory.FreeGroupoid.homMk (SSet.Truncated.HomotopyCategory.homMk e) }

@[simp]

theorem SSet.Truncated.FundamentalGroupoid.homMk_id {X : Truncated 2} (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })) : homMk (Edge.id x) = CategoryTheory.CategoryStruct.id { pt := x }

theorem SSet.Truncated.FundamentalGroupoid.hom_rec {X : Truncated 2} {motive : ⦃x y : X.FundamentalGroupoid⦄ → (x ⟶ y) → Prop} (homMk : ∀ ⦃x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })⦄ (e : Edge x y), motive (homMk e)) (inv : ∀ ⦃x y : X.FundamentalGroupoid⦄ (f : x ⟶ y), motive f → motive (CategoryTheory.inv f)) (comp : ∀ ⦃x y z : X.FundamentalGroupoid⦄ (f : x ⟶ y) (g : y ⟶ z), motive f → motive g → motive (CategoryTheory.CategoryStruct.comp f g)) {x y : X.FundamentalGroupoid} (f : x ⟶ y) : motive f

Induction principle for morphisms in the fundamental groupoid of a 2-truncated simplicial set: in order to prove a property of all morphisms, it suffices to do it for morphisms induced by edges and show that the property is stable by inverses and by composition.

def SSet.Truncated.FundamentalGroupoid.descMap {X : Truncated 2} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 }) → D) (map : {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} → Edge x y → (obj x ⟶ obj y)) (map_comp : ∀ {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) {x y : X.FundamentalGroupoid} (f : x ⟶ y) : obj x.pt ⟶ obj y.pt

Auxiliary definition for desc.

Equations

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

@[simp]

theorem SSet.Truncated.FundamentalGroupoid.descMap_homMk {X : Truncated 2} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 }) → D) (map : {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} → Edge x y → (obj x ⟶ obj y)) (map_comp : ∀ {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} (e : Edge x y) : descMap obj (fun {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} => map) ⋯ (homMk e) = map e

@[implicit_reducible]

def SSet.Truncated.FundamentalGroupoid.desc {X : Truncated 2} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 }) → D) (map : {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} → Edge x y → (obj x ⟶ obj y)) (map_comp : ∀ {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) : CategoryTheory.Functor X.FundamentalGroupoid D

Constructor for functors from the fundamental groupoid of a 2-truncated simplicial set.

Equations

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

@[simp]

theorem SSet.Truncated.FundamentalGroupoid.desc_obj_mk {X : Truncated 2} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 }) → D) (map : {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} → Edge x y → (obj x ⟶ obj y)) (map_comp : ∀ {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })) : (desc obj (fun {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} => map) ⋯).obj { pt := x } = obj x

@[simp]

theorem SSet.Truncated.FundamentalGroupoid.desc_map_homMk {X : Truncated 2} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 }) → D) (map : {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} → Edge x y → (obj x ⟶ obj y)) (map_comp : ∀ {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} (e : Edge x y) : (desc obj (fun {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} => map) ⋯).map (homMk e) = map e

theorem SSet.Truncated.FundamentalGroupoid.functor_ext {X : Truncated 2} {D : Type u_1} [CategoryTheory.Groupoid D] {F G : CategoryTheory.Functor X.FundamentalGroupoid D} (h₁ : ∀ (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })), F.obj { pt := x } = G.obj { pt := x }) (h₂ : ∀ {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} (e : Edge x y), F.map (homMk e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map (homMk e)) (CategoryTheory.eqToHom ⋯))) : F = G

theorem SSet.Truncated.Edge.CompStruct.homMk_comp {X : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := FundamentalGroupoid._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : CategoryTheory.CategoryStruct.comp (FundamentalGroupoid.homMk e₀₁) (FundamentalGroupoid.homMk e₁₂) = FundamentalGroupoid.homMk e₀₂

theorem SSet.Truncated.Edge.CompStruct.homMk_comp_assoc {X : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := FundamentalGroupoid._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) {Z : X.FundamentalGroupoid} (h✝ : { pt := x₂ } ⟶ Z) : CategoryTheory.CategoryStruct.comp (FundamentalGroupoid.homMk e₀₁) (CategoryTheory.CategoryStruct.comp (FundamentalGroupoid.homMk e₁₂) h✝) = CategoryTheory.CategoryStruct.comp (FundamentalGroupoid.homMk e₀₂) h✝

@[implicit_reducible]

def SSet.Truncated.mapFundamentalGroupoid {X Y : Truncated 2} (f : X ⟶ Y) : CategoryTheory.Functor X.FundamentalGroupoid Y.FundamentalGroupoid

The functor FundamentalGroupoid X ⥤ FundamentalGroupoid Y that is induced by a morphism of 2-truncated simplicial sets.

Equations

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

@[simp]

theorem SSet.Truncated.mapFundamentalGroupoid_obj_mk {X Y : Truncated 2} (f : X ⟶ Y) (x : X.obj (Opposite.op { obj := { len := 0 }, property := FundamentalGroupoid._proof_1 })) : (mapFundamentalGroupoid f).obj { pt := x } = { pt := (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { obj := { len := 0 }, property := FundamentalGroupoid._proof_1 }))) x }

@[simp]

theorem SSet.Truncated.mapFundamentalGroupoid_map_homMk {X Y : Truncated 2} (f : X ⟶ Y) {x y : X.obj (Opposite.op { obj := { len := 0 }, property := FundamentalGroupoid._proof_1 })} (e : Edge x y) : (mapFundamentalGroupoid f).map (FundamentalGroupoid.homMk e) = FundamentalGroupoid.homMk (e.map f)

theorem SSet.Truncated.mapFundamentalGroupoid_id (X : Truncated 2) : mapFundamentalGroupoid (CategoryTheory.CategoryStruct.id X) = CategoryTheory.Functor.id X.FundamentalGroupoid

theorem SSet.Truncated.mapFundamentalGroupoid_comp {X Y Z : Truncated 2} (f : X ⟶ Y) (g : Y ⟶ Z) : mapFundamentalGroupoid (CategoryTheory.CategoryStruct.comp f g) = (mapFundamentalGroupoid f).comp (mapFundamentalGroupoid g)

def SSet.Truncated.mapIsoFundamentalGroupoid {X Y : Truncated 2} (e : X ≅ Y) : CategoryTheory.IsoCat X.FundamentalGroupoid Y.FundamentalGroupoid

The isomorphism of fundamental groupoids that is induced by an isomorphism of 2-truncated simplicial sets.

Equations

• SSet.Truncated.mapIsoFundamentalGroupoid e = { functor := SSet.Truncated.mapFundamentalGroupoid e.hom, inverse := SSet.Truncated.mapFundamentalGroupoid e.inv, unit_eq := ⋯, counit_eq := ⋯ }

instance SSet.Truncated.instIsEquivalenceFundamentalGroupoidMapFundamentalGroupoidOfIsIsoOfNatNat {X Y : Truncated 2} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (mapFundamentalGroupoid f).IsEquivalence

@[implicit_reducible]

def SSet.FundamentalGroupoid (X : SSet) : Type u

The fundamental groupoid of a simplicial set X.

Equations

• X.FundamentalGroupoid = ((SSet.truncation 2).obj X).FundamentalGroupoid

@[instance_reducible]

instance SSet.instGroupoidFundamentalGroupoid (X : SSet) : CategoryTheory.Groupoid X.FundamentalGroupoid

Equations

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

@[implicit_reducible]

def SSet.FundamentalGroupoid.mk {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : X.FundamentalGroupoid

Constructor for objects of the fundamental groupoid of a simplicial set X.

Equations

• SSet.FundamentalGroupoid.mk x = { pt := x }

theorem SSet.FundamentalGroupoid.mk_surjective {X : SSet} : Function.Surjective mk

@[implicit_reducible]

def SSet.FundamentalGroupoid.rec {X : SSet} {motive : X.FundamentalGroupoid → Sort u_1} (mk : (x : X.obj (Opposite.op { len := 0 })) → motive (mk x)) (x : X.FundamentalGroupoid) : motive x

Induction principle for the objects of the fundamental groupoid of a simplicial set.

Equations

• SSet.FundamentalGroupoid.rec mk x = mk x.pt

@[simp]

theorem SSet.FundamentalGroupoid.rec_mk {X : SSet} {motive : X.FundamentalGroupoid → Sort u_1} (mk : (x : X.obj (Opposite.op { len := 0 })) → motive (mk x)) (x : X.obj (Opposite.op { len := 0 })) : rec mk (FundamentalGroupoid.mk x) = mk x

def SSet.FundamentalGroupoid.homMk {X : SSet} {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : mk x ⟶ mk y

Constructor for morphisms in the fundamental groupoid of a simplicial set X.

Equations

• SSet.FundamentalGroupoid.homMk e = SSet.Truncated.FundamentalGroupoid.homMk e

@[simp]

theorem SSet.FundamentalGroupoid.homMk_id {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : homMk (Edge.id x) = CategoryTheory.CategoryStruct.id (mk x)

theorem SSet.FundamentalGroupoid.hom_rec {X : SSet} {motive : ⦃x y : X.FundamentalGroupoid⦄ → (x ⟶ y) → Prop} (homMk : ∀ ⦃x y : X.obj (Opposite.op { len := 0 })⦄ (e : Edge x y), motive (homMk e)) (inv : ∀ ⦃x y : X.FundamentalGroupoid⦄ (f : x ⟶ y), motive f → motive (CategoryTheory.inv f)) (comp : ∀ ⦃x y z : X.FundamentalGroupoid⦄ (f : x ⟶ y) (g : y ⟶ z), motive f → motive g → motive (CategoryTheory.CategoryStruct.comp f g)) {x y : X.FundamentalGroupoid} (f : x ⟶ y) : motive f

Induction principle for morphisms in the fundamental groupoid of a simplicial set: in order to prove a property of all morphisms, it suffices to do it for morphisms induced by edges and show that the property is stable by inverses and by composition;

@[implicit_reducible]

def SSet.FundamentalGroupoid.desc {X : SSet} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : X.obj (Opposite.op { len := 0 }) → D) (map : {x y : X.obj (Opposite.op { len := 0 })} → Edge x y → (obj x ⟶ obj y)) (map_comp : ∀ {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) : CategoryTheory.Functor X.FundamentalGroupoid D

Constructor for functors from the fundamental groupoid of a simplicial set.

Equations

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

@[simp]

theorem SSet.FundamentalGroupoid.desc_obj_mk {X : SSet} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : X.obj (Opposite.op { len := 0 }) → D) (map : {x y : X.obj (Opposite.op { len := 0 })} → Edge x y → (obj x ⟶ obj y)) (map_comp : ∀ {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) (x : X.obj (Opposite.op { len := 0 })) : (desc obj (fun {x y : X.obj (Opposite.op { len := 0 })} => map) ⋯).obj (mk x) = obj x

@[simp]

theorem SSet.FundamentalGroupoid.desc_map_homMk {X : SSet} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : X.obj (Opposite.op { len := 0 }) → D) (map : {x y : X.obj (Opposite.op { len := 0 })} → Edge x y → (obj x ⟶ obj y)) (map_comp : ∀ {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : (desc obj (fun {x y : X.obj (Opposite.op { len := 0 })} => map) ⋯).map (homMk e) = map e

def SSet.FundamentalGroupoid.natTransMk {X : SSet} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor X.FundamentalGroupoid D} (app : (x : X.obj (Opposite.op { len := 0 })) → F.obj (mk x) ⟶ G.obj (mk x)) (naturality : ∀ {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (app y) = CategoryTheory.CategoryStruct.comp (app x) (G.map (homMk e)) := by cat_disch) : F ⟶ G

Constructor for natural transformations between functors from the fundamental groupoid of a simplicial set.

Equations

• SSet.FundamentalGroupoid.natTransMk app naturality = { app := fun (x : X.FundamentalGroupoid) => app x.pt, naturality := ⋯ }

@[simp]

theorem SSet.FundamentalGroupoid.natTransMk_app {X : SSet} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor X.FundamentalGroupoid D} (app : (x : X.obj (Opposite.op { len := 0 })) → F.obj (mk x) ⟶ G.obj (mk x)) (naturality : ∀ {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (app y) = CategoryTheory.CategoryStruct.comp (app x) (G.map (homMk e)) := by cat_disch) (x : X.FundamentalGroupoid) : (natTransMk app naturality).app x = app x.pt

def SSet.FundamentalGroupoid.natIsoMk {X : SSet} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor X.FundamentalGroupoid D} (app : (x : X.obj (Opposite.op { len := 0 })) → F.obj (mk x) ≅ G.obj (mk x)) (naturality : ∀ {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (app y).hom = CategoryTheory.CategoryStruct.comp (app x).hom (G.map (homMk e)) := by cat_disch) : F ≅ G

Constructor for natural isomorphisms between functors from the fundamental groupoid of a simplicial set.

Equations

• SSet.FundamentalGroupoid.natIsoMk app naturality = CategoryTheory.NatIso.ofComponents (fun (x : X.FundamentalGroupoid) => app x.pt) ⋯

@[simp]

theorem SSet.FundamentalGroupoid.natIsoMk_hom_app {X : SSet} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor X.FundamentalGroupoid D} (app : (x : X.obj (Opposite.op { len := 0 })) → F.obj (mk x) ≅ G.obj (mk x)) (naturality : ∀ {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (app y).hom = CategoryTheory.CategoryStruct.comp (app x).hom (G.map (homMk e)) := by cat_disch) (X✝ : X.FundamentalGroupoid) : (natIsoMk app naturality).hom.app X✝ = (app X✝.pt).hom

@[simp]

theorem SSet.FundamentalGroupoid.natIsoMk_inv_app {X : SSet} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor X.FundamentalGroupoid D} (app : (x : X.obj (Opposite.op { len := 0 })) → F.obj (mk x) ≅ G.obj (mk x)) (naturality : ∀ {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (app y).hom = CategoryTheory.CategoryStruct.comp (app x).hom (G.map (homMk e)) := by cat_disch) (X✝ : X.FundamentalGroupoid) : (natIsoMk app naturality).inv.app X✝ = (app X✝.pt).inv

theorem SSet.FundamentalGroupoid.functor_ext {X : SSet} {D : Type u_1} [CategoryTheory.Groupoid D] {F G : CategoryTheory.Functor X.FundamentalGroupoid D} (h₁ : ∀ (x : X.obj (Opposite.op { len := 0 })), F.obj (mk x) = G.obj (mk x)) (h₂ : ∀ {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y), F.map (homMk e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map (homMk e)) (CategoryTheory.eqToHom ⋯))) : F = G

theorem SSet.Edge.CompStruct.homMk_comp {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₀₂) : CategoryTheory.CategoryStruct.comp (FundamentalGroupoid.homMk e₀₁) (FundamentalGroupoid.homMk e₁₂) = FundamentalGroupoid.homMk e₀₂

theorem SSet.Edge.CompStruct.homMk_comp_assoc {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₀₂) {Z : X.FundamentalGroupoid} (h✝ : FundamentalGroupoid.mk x₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (FundamentalGroupoid.homMk e₀₁) (CategoryTheory.CategoryStruct.comp (FundamentalGroupoid.homMk e₁₂) h✝) = CategoryTheory.CategoryStruct.comp (FundamentalGroupoid.homMk e₀₂) h✝

@[implicit_reducible]

def SSet.mapFundamentalGroupoid {X Y : SSet} (f : X ⟶ Y) : CategoryTheory.Functor X.FundamentalGroupoid Y.FundamentalGroupoid

The functor FundamentalGroupoid X ⥤ FundamentalGroupoid Y that is induced by a morphism of simplicial sets.

Equations

• SSet.mapFundamentalGroupoid f = SSet.Truncated.mapFundamentalGroupoid ((SSet.truncation 2).map f)

@[simp]

theorem SSet.mapFundamentalGroupoid_obj_mk {X Y : SSet} (f : X ⟶ Y) (x : X.obj (Opposite.op { len := 0 })) : (mapFundamentalGroupoid f).obj (FundamentalGroupoid.mk x) = FundamentalGroupoid.mk ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x)

@[simp]

theorem SSet.mapFundamentalGroupoid_map_homMk {X Y : SSet} (f : X ⟶ Y) {x y : X.obj (Opposite.op { len := 0 })} (e : Edge x y) : (mapFundamentalGroupoid f).map (FundamentalGroupoid.homMk e) = FundamentalGroupoid.homMk (e.map f)

theorem SSet.isIso_mapFundamentalGroupoid_of_isIso {X Y : SSet} (f : X ⟶ Y) (hf : CategoryTheory.IsIso ((truncation 2).map f) := by infer_instance) : (mapFundamentalGroupoid f).IsIso

The isomorphism of fundamental groupoids that is induced by a morphism of simplicial sets which induces an isomorphism on the 2-truncations.

theorem SSet.isEquivalence_mapFundamentalGroupoid {X Y : SSet} (f : X ⟶ Y) (hf : CategoryTheory.IsIso ((truncation 2).map f) := by infer_instance) : (mapFundamentalGroupoid f).IsEquivalence