Documentation

TauCeti.AlgebraicTopology.FundamentalGroupoid.Pushout

The two-set Seifert--van Kampen theorem for fundamental groupoids #

Suppose that the interiors of two sets A and B cover a space X. This file proves that the square of fundamental groupoids induced by the inclusions

Π(A ∩ B) ⟶ Π(A)
    ↓         ↓
  Π(B)   ⟶  Π(X)

is a pushout in the category of groupoids, with no connectedness assumption on A, B or A ∩ B. More usefully for calculations, the same holds for the fundamental groupoids on a set S of basepoints, provided that S meets every path component of A, of B and of A ∩ B: the full subgroupoids on S of the four fundamental groupoids again form a pushout square. For the circle covered by two arcs, whose intersection has two path components, this requires two basepoints; with a single basepoint, it recovers the hypotheses of the based theorem TauCeti.isPushout_fundamentalGroup.

The first statement is the gluing theorem TauCeti.FundamentalGroupoid.glue for the cover of X by A and B, packaged as TauCeti.FundamentalGroupoid.glueTwo. For the second, choose for every point x a point r x of S together with a homotopy class of paths from x to r x, inside A ∩ B if x ∈ A ∩ B, inside A or B otherwise, and trivial if x ∈ S. Conjugating by these classes retracts each of the four fundamental groupoids onto its full subgroupoid on S, compatibly with the inclusions (TauCeti.InducedCategory.retraction). A cocone over the square on S then becomes a cocone over the full square, to which the first statement applies.

Main declarations #

References #

source
noncomputable def TauCeti.FundamentalGroupoid.glueTwo {X : Type u} [TopologicalSpace X] {A B : Set X} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (hCover : interior A ∪ interior B = Set.univ) (FA : CategoryTheory.Functor (FundamentalGroupoid ↑A) D) (FB : CategoryTheory.Functor (FundamentalGroupoid ↑B) D) (h : (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp FA = (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp FB) :
CategoryTheory.Functor (FundamentalGroupoid X) D

Gluing two functors out of fundamental groupoids. If the interiors of A and B cover X, and FA and FB are functors out of the fundamental groupoids of A and B which agree on the fundamental groupoid of A ∩ B, this is the functor out of the fundamental groupoid of X which restricts to FA and to FB (map_subtypeVal_comp_glueTwo_left, map_subtypeVal_comp_glueTwo_right); it is the unique such functor (eq_glueTwo).

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.FundamentalGroupoid.map_subtypeVal_comp_glueTwo_left {X : Type u} [TopologicalSpace X] {A B : Set X} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (hCover : interior A ∪ interior B = Set.univ) (FA : CategoryTheory.Functor (FundamentalGroupoid ↑A) D) (FB : CategoryTheory.Functor (FundamentalGroupoid ↑B) D) (h : (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp FA = (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp FB) :
    (FundamentalGroupoid.map (ContinuousMap.subtypeVal A)).comp (glueTwo hCover FA FB h) = FA

    The glued functor restricts to FA on the fundamental groupoid of A.

    source
    @[simp]
    theorem TauCeti.FundamentalGroupoid.map_subtypeVal_comp_glueTwo_right {X : Type u} [TopologicalSpace X] {A B : Set X} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (hCover : interior A ∪ interior B = Set.univ) (FA : CategoryTheory.Functor (FundamentalGroupoid ↑A) D) (FB : CategoryTheory.Functor (FundamentalGroupoid ↑B) D) (h : (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp FA = (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp FB) :
    (FundamentalGroupoid.map (ContinuousMap.subtypeVal B)).comp (glueTwo hCover FA FB h) = FB

    The glued functor restricts to FB on the fundamental groupoid of B.

    source
    theorem TauCeti.FundamentalGroupoid.eq_glueTwo {X : Type u} [TopologicalSpace X] {A B : Set X} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (hCover : interior A ∪ interior B = Set.univ) (FA : CategoryTheory.Functor (FundamentalGroupoid ↑A) D) (FB : CategoryTheory.Functor (FundamentalGroupoid ↑B) D) (h : (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp FA = (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)).comp FB) {G : CategoryTheory.Functor (FundamentalGroupoid X) D} (hA : (FundamentalGroupoid.map (ContinuousMap.subtypeVal A)).comp G = FA) (hB : (FundamentalGroupoid.map (ContinuousMap.subtypeVal B)).comp G = FB) :
    G = glueTwo hCover FA FB h

    A functor out of the fundamental groupoid of X which restricts to FA and to FB is the glued functor.

    source
    theorem TauCeti.isPushout_fundamentalGroupoid {X : Type u} [TopologicalSpace X] {A B : Set X} (hCover : interior A ∪ interior B = Set.univ) :
    CategoryTheory.IsPushout (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)) (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯)) (FundamentalGroupoid.map (ContinuousMap.subtypeVal A)) (FundamentalGroupoid.map (ContinuousMap.subtypeVal B))

    The two-set van Kampen theorem for fundamental groupoids. If the interiors of A and B cover X, the square of fundamental groupoids induced by the inclusions of A ∩ B into A and B and of A and B into X is a pushout in the category of groupoids.

    The theorem on a set of basepoints #

    source
    theorem TauCeti.isPushout_fundamentalGroupoidOn {X : Type u} [TopologicalSpace X] {A B S : Set X} (hSA : ∀ x ∈ A, ∃ y ∈ S, JoinedIn A x y) (hSB : ∀ x ∈ B, ∃ y ∈ S, JoinedIn B x y) (hSAB : ∀ x ∈ A ∩ B, ∃ y ∈ S, JoinedIn (A ∩ B) x y) (hCover : interior A ∪ interior B = Set.univ) :
    CategoryTheory.IsPushout (FundamentalGroupoidOn.map (ContinuousMap.inclusion ⋯) ⋯) (FundamentalGroupoidOn.map (ContinuousMap.inclusion ⋯) ⋯) (FundamentalGroupoidOn.map (ContinuousMap.subtypeVal A) ⋯) (FundamentalGroupoidOn.map (ContinuousMap.subtypeVal B) ⋯)

    The two-set van Kampen theorem for fundamental groupoids on a set of basepoints. If the interiors of A and B cover X and the set S meets every path component of A, of B and of A ∩ B, then the square of fundamental groupoids on S induced by the inclusions of A ∩ B into A and B and of A and B into X is a pushout in the category of groupoids.