The based Seifert--van Kampen theorem #
Suppose that the interiors of two sets A and B cover a space X, that A, B and A ∩ B
are path connected, and that all three contain a basepoint x. This file proves that the square
of fundamental groups induced by the inclusions
π₁(A ∩ B, x) ⟶ π₁(A, x)
↓ ↓
π₁(B, x) ⟶ π₁(X, x)
is a pushout of groups: π₁(X, x) is the amalgamated free product of π₁(A, x) and π₁(B, x)
over π₁(A ∩ B, x). When A ∩ B is moreover simply connected, the amalgamation is trivial and the
canonical map π₁(A, x) ∗ π₁(B, x) →* π₁(X, x) from the free product is an isomorphism.
The same holds for a family of sets U i, with interiors covering X, whose pairwise
intersections are all one path-connected set C ∋ x: π₁(X, x) is the wide pushout of the groups
π₁(U i, x) over π₁(C, x), and their free product when C is simply connected. This is the
form of the theorem that computes the fundamental group of a wedge sum, where U i is the i-th
summand together with a contractible neighbourhood C of the wedge point.
The homomorphism out of π₁(X, x) induced by compatible homomorphisms fA and fB out of
π₁(A, x) and π₁(B, x) is built from the fundamental-groupoid gluing theorem for two sets,
TauCeti.FundamentalGroupoid.glueTwo. Choose for every point z of A a morphism from x to
z in the fundamental groupoid of A, taken inside A ∩ B whenever z ∈ A ∩ B, and similarly
for B. Conjugating by these morphisms turns fA and fB into functors out of the fundamental
groupoids of A and B; on A ∩ B both functors are induced by the common restriction of fA
and fB to π₁(A ∩ B, x), so they glue. Uniqueness is the generation half of van Kampen,
TauCeti.FundamentalGroup.range_map_subtypeVal_sup_eq_top.
Main declarations #
TauCeti.vanKampenDesc: the homomorphismπ₁(X, x) →* Kinduced by homomorphisms out ofπ₁(A, x)andπ₁(B, x)which agree onπ₁(A ∩ B, x).TauCeti.vanKampenDesc_map_left,TauCeti.vanKampenDesc_map_right: it restricts to the given homomorphisms.TauCeti.vanKampen_hom_ext: homomorphisms out ofπ₁(X, x)are determined by their restrictions toπ₁(A, x)andπ₁(B, x).TauCeti.isPushout_fundamentalGroup: the based Seifert--van Kampen theorem, as a pushout square in the category of groups.TauCeti.vanKampenLift,TauCeti.vanKampenLift_bijective,TauCeti.vanKampenEquiv: the canonical homomorphism from the free product, and the theorem that it is bijective whenA ∩ Bis simply connected.TauCeti.vanKampenLift_surjective: the canonical homomorphism is surjective whenA ∩ Bis path connected.TauCeti.vanKampenWideDesc,TauCeti.vanKampenWideDesc_map: the universal property ofπ₁(X, x)for a family whose pairwise intersections are allC.TauCeti.vanKampenWide_hom_ext: homomorphisms out ofπ₁(X, x)are determined by their restrictions to the groupsπ₁(U i, x), for any family of sets containingxwhose interiors coverXand whose pairwise intersections are path connected.TauCeti.isColimitFundamentalGroupWideCocone: the Seifert--van Kampen theorem for such a family, as a wide pushout in the category of groups.TauCeti.vanKampenWideLift_surjective: the canonical map from the indexed free product is surjective when all pairwise intersections are path connected.TauCeti.vanKampenWideLift,TauCeti.vanKampenWideEquiv: the canonical homomorphism from the free product of the groupsπ₁(U i, x), and the resulting isomorphism whenCis simply connected.
References #
- A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Theorem 1.20 and Example 1.21.
- R. Brown, Topology and Groupoids, Section 6.7.
The homomorphism out of π₁(X, x) given by the based Seifert--van Kampen theorem.
If the interiors of A and B cover X and A, B and A ∩ B are path connected, then two
homomorphisms out of π₁(A, x) and π₁(B, x) which agree on π₁(A ∩ B, x) are the restrictions
of this homomorphism out of π₁(X, x) (TauCeti.vanKampenDesc_map_left,
TauCeti.vanKampenDesc_map_right); it is the unique such homomorphism
(TauCeti.vanKampen_hom_ext).
Equations
- One or more equations did not get rendered due to their size.
Instances For
vanKampenDesc restricts to fA on π₁(A, x).
vanKampenDesc restricts to fB on π₁(B, x).
vanKampenDesc restricts to fA on π₁(A, x).
vanKampenDesc restricts to fB on π₁(B, x).
Uniqueness in the based Seifert--van Kampen theorem. If the interiors of A and B
cover X and A, B and A ∩ B are path connected, then two homomorphisms out of π₁(X, x)
which agree on the images of π₁(A, x) and π₁(B, x) are equal.
The based Seifert--van Kampen theorem. If the interiors of A and B cover X, the sets
A, B and A ∩ B are path connected, and all three contain the basepoint x, then the square
of fundamental groups induced by the inclusions of A ∩ B into A and B and of A and B
into X is a pushout of groups. That is, π₁(X, x) is the free product of π₁(A, x) and
π₁(B, x) amalgamated over π₁(A ∩ B, x).
The canonical homomorphism from the free product of the fundamental groups of two subspaces to the fundamental group of the ambient space.
Equations
- TauCeti.vanKampenLift A B x hxA hxB = Monoid.Coprod.lift (FundamentalGroup.map (ContinuousMap.subtypeVal A) ⟨x, hxA⟩) (FundamentalGroup.map (ContinuousMap.subtypeVal B) ⟨x, hxB⟩)
Instances For
The canonical free-product map is the lift of the two inclusion-induced homomorphisms.
vanKampenLift restricts on the left factor to the map induced by inclusion.
vanKampenLift restricts on the right factor to the map induced by inclusion.
The generation half of the based van Kampen theorem. Every loop class is an image of an element of the free product of the two subspace groups.
The based Seifert--van Kampen theorem for a simply connected overlap.
If the interiors of two path-connected sets cover X, their intersection is simply connected,
and both contain the basepoint, then the canonical homomorphism from the free product of their
fundamental groups to the fundamental group of X is bijective.
The equivalence in the based Seifert--van Kampen theorem for two path-connected sets with
simply connected intersection. Its underlying homomorphism is vanKampenLift.
Equations
- TauCeti.vanKampenEquiv hCover hA hB hAB hxA hxB = MulEquiv.ofBijective (TauCeti.vanKampenLift A B x hxA hxB) ⋯
Instances For
The homomorphism underlying vanKampenEquiv is vanKampenLift.
Families of sets with a common pairwise intersection #
Let U : ι → Set X be a family whose interiors cover X, all of whose members contain a
path-connected set C ∋ x, and any two distinct members of which meet exactly in C. Then
π₁(X, x) is the wide pushout of the groups π₁(U i, x) over π₁(C, x); when C is simply
connected, it is their free product. For two sets, C is A ∩ B. The homomorphism out of
π₁(X, x) is built as in the two-set case, gluing with TauCeti.FundamentalGroupoid.glue in place
of TauCeti.FundamentalGroupoid.glueTwo.
The homomorphism out of π₁(X, x) given by the Seifert--van Kampen theorem for a family
with a common pairwise intersection.
Let the sets U i have interiors covering X, be path connected, and contain the path-connected
set C ∋ x, and let two distinct members meet inside C. Then homomorphisms out of the groups
π₁(U i, x) which agree on π₁(C, x) are the restrictions of this homomorphism out of
π₁(X, x) (TauCeti.vanKampenWideDesc_map); it is the unique such homomorphism
(TauCeti.vanKampenWide_hom_ext).
Equations
- One or more equations did not get rendered due to their size.
Instances For
vanKampenWideDesc restricts to f i on π₁(U i, x).
vanKampenWideDesc restricts to f i on π₁(U i, x).
Uniqueness in the Seifert--van Kampen theorem for a family. If the interiors of the sets
U i ∋ x cover X and their pairwise intersections are path connected, then two homomorphisms out
of π₁(X, x) which agree on the image of every π₁(U i, x) are equal.
The wide span of fundamental groups of the inclusions of C into the sets U i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cocone over fundamentalGroupWideSpan with vertex π₁(X, x), whose legs are induced by
the inclusions of C and of the sets U i into X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The vertex of fundamentalGroupWideCocone is π₁(X, x).
The leg of fundamentalGroupWideCocone at C is induced by the inclusion of C.
The leg of fundamentalGroupWideCocone at U i is induced by the inclusion of U i.
The Seifert--van Kampen theorem for a family with a common pairwise intersection. If the
interiors of the path-connected sets U i cover X, all of them contain the path-connected set
C ∋ x, and two distinct members meet inside C, then π₁(X, x) is the wide pushout in the
category of groups of the groups π₁(U i, x) over π₁(C, x), along the maps induced by the
inclusions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical homomorphism from the free product of the fundamental groups of a family of
subspaces containing x to the fundamental group of the ambient space.
Equations
- TauCeti.vanKampenWideLift U x hx = Monoid.CoprodI.lift fun (i : ι) => FundamentalGroup.map (ContinuousMap.subtypeVal (U i)) ⟨x, ⋯⟩
Instances For
vanKampenWideLift restricts on the i-th factor to the map induced by inclusion.
The generation half of van Kampen's theorem for a family. Every loop class is the image of an element of the indexed free product when all pairwise intersections of the cover members are path connected.
The Seifert--van Kampen theorem for a family with a simply connected common pairwise
intersection. If the interiors of the path-connected sets U i cover X, all of them contain
the simply connected set C ∋ x, and two distinct members meet inside C, then the canonical
homomorphism from the free product of the groups π₁(U i, x) to π₁(X, x) is an isomorphism.
Its underlying homomorphism is vanKampenWideLift.
Equations
- TauCeti.vanKampenWideEquiv hU hUp hC hCU hUC hx = (TauCeti.vanKampenWideLift U x ⋯).toMulEquiv (TauCeti.vanKampenWideDesc hU hUp ⋯ hCU hUC hx (fun (i : ι) => Monoid.CoprodI.of) ⋯) ⋯ ⋯
Instances For
The homomorphism underlying vanKampenWideEquiv is vanKampenWideLift.