Gluing functors out of the fundamental groupoid

Let U : ι → Set X be a family of subsets such that every point of X has some U i as a neighbourhood, and let F i be functors, with values in any category, out of the fundamental groupoids of the sets U i, which agree on the fundamental groupoids of the pairwise intersections U i ∩ U j. This file constructs the functor TauCeti.FundamentalGroupoid.glue out of the fundamental groupoid of X which restricts to every F i. Together with the uniqueness statement TauCeti.FundamentalGroupoid.functor_ext, this is the universal property behind the groupoid Seifert--van Kampen theorem; no connectedness assumption is made on the sets U i or on their intersections.

The covering hypothesis holds for every open cover of X, and more generally for every family whose interiors cover X. To define a functor out of the fundamental groupoid of X, it therefore suffices to give compatible functors out of the fundamental groupoids of the members of such a cover; map_subtypeVal_comp_glue and glue_obj_mk compute the result on each member. This is how TauCeti.FundamentalGroupoid.isColimitCechCocone constructs the functor induced by a cocone over the Čech diagram of an open cover.

Main declarations

• TauCeti.FundamentalGroupoid.glue: the functor glued from the functors F i.
• TauCeti.FundamentalGroupoid.map_subtypeVal_comp_glue: the glued functor restricts to F i on the fundamental groupoid of U i.
• TauCeti.FundamentalGroupoid.eq_glue: it is the only functor with this property.

References

• R. Brown, Topology and Groupoids, 3rd ed., Section 6.7.
• A. Hatcher, Algebraic Topology, Section 1.2, proof of Theorem 1.20.

noncomputable def TauCeti.FundamentalGroupoid.glue {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {U : ι → Set X} {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (hU : ∀ (x : X), ∃ (i : ι), U i ∈ nhds x) (F : (i : ι) → CategoryTheory.Functor (FundamentalGroupoid ↑(U i)) D) (hF : ∀ (i j : ι), (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp (F i) = (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp (F j)) : CategoryTheory.Functor (FundamentalGroupoid X) D

Gluing functors out of fundamental groupoids. Let every point of X have some U i as a neighbourhood, and let F i be functors out of the fundamental groupoids of the sets U i which agree on the fundamental groupoids of the pairwise intersections. This is the functor out of the fundamental groupoid of X which restricts to every F i (TauCeti.FundamentalGroupoid.map_subtypeVal_comp_glue); it is the unique such functor (TauCeti.FundamentalGroupoid.eq_glue).

Equations

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

@[simp]

theorem TauCeti.FundamentalGroupoid.map_subtypeVal_comp_glue {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {U : ι → Set X} {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (hU : ∀ (x : X), ∃ (i : ι), U i ∈ nhds x) (F : (i : ι) → CategoryTheory.Functor (FundamentalGroupoid ↑(U i)) D) (hF : ∀ (i j : ι), (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp (F i) = (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp (F j)) (i : ι) : (FundamentalGroupoid.map (ContinuousMap.subtypeVal (U i))).comp (glue hU F hF) = F i

The glued functor restricts to F i on the fundamental groupoid of U i.

theorem TauCeti.FundamentalGroupoid.glue_obj_mk {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {U : ι → Set X} {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (hU : ∀ (x : X), ∃ (i : ι), U i ∈ nhds x) (F : (i : ι) → CategoryTheory.Functor (FundamentalGroupoid ↑(U i)) D) (hF : ∀ (i j : ι), (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp (F i) = (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp (F j)) (i : ι) {x : X} (hx : x ∈ U i) : (glue hU F hF).obj { as := x } = (F i).obj { as := ⟨x, hx⟩ }

On objects, the glued functor agrees with each F i.

theorem TauCeti.FundamentalGroupoid.eq_glue {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {U : ι → Set X} {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (hU : ∀ (x : X), ∃ (i : ι), U i ∈ nhds x) (F : (i : ι) → CategoryTheory.Functor (FundamentalGroupoid ↑(U i)) D) (hF : ∀ (i j : ι), (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp (F i) = (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp (F j)) {G : CategoryTheory.Functor (FundamentalGroupoid X) D} (hG : ∀ (i : ι), (FundamentalGroupoid.map (ContinuousMap.subtypeVal (U i))).comp G = F i) : G = glue hU F hF

A functor out of the fundamental groupoid of X which restricts to F i on the fundamental groupoid of every U i is the glued functor.