The free-product presentation in van Kampen's theorem

For two path-connected subspaces whose interiors cover a space and whose intersection is path connected, the fundamental group is the free product of the two subspace groups modulo the normal closure of the intersection relations. Each relation identifies the two images of one loop in the intersection. No injectivity of either intersection homomorphism is needed.

TauCeti.ker_vanKampenLift identifies the kernel of the inclusion-induced free-product map. TauCeti.vanKampenQuotientEquiv gives the resulting quotient isomorphism, with formulas on both factors. These formulas permit group presentations of the cover members to be combined by adjoining the intersection relations.

For an indexed family with a common pairwise intersection, TauCeti.ker_vanKampenWideLift and TauCeti.vanKampenWideQuotientEquiv give the corresponding presentation. Its relators identify the images of each loop in the common intersection in every pair of factors.

The proof uses the universal property of the based van Kampen theorem in TauCeti.AlgebraicTopology.FundamentalGroup.VanKampen.Basic and Mathlib's normal closure and quotient-group constructions.

References

• A. Hatcher, Algebraic Topology, Section 1.2, Theorem 1.20.
• R. Brown, Topology and Groupoids, 3rd ed., Chapters 6–7.

noncomputable def TauCeti.vanKampenRelations {X : Type u_1} [TopologicalSpace X] (A B : Set X) (x : X) (hxA : x ∈ A) (hxB : x ∈ B) : Subgroup (Monoid.Coprod (FundamentalGroup ↑A ⟨x, hxA⟩) (FundamentalGroup ↑B ⟨x, hxB⟩))

The normal subgroup of the free product generated by identifying the two images of each loop in the intersection.

Equations

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

theorem TauCeti.vanKampenRelations_def {X : Type u_1} [TopologicalSpace X] (A B : Set X) (x : X) (hxA : x ∈ A) (hxB : x ∈ B) : vanKampenRelations A B x hxA hxB = Subgroup.normalClosure (Set.range fun (g : FundamentalGroup ↑(A ∩ B) ⟨x, ⋯⟩) => Monoid.Coprod.inl ((FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩) g) * (Monoid.Coprod.inr ((FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩) g))⁻¹)

The defining normal-closure description of the intersection relations.

instance TauCeti.instNormalCoprodFundamentalGroupElemMkMemSetVanKampenRelations {X : Type u_1} [TopologicalSpace X] (A B : Set X) (x : X) (hxA : x ∈ A) (hxB : x ∈ B) : (vanKampenRelations A B x hxA hxB).Normal

The intersection relations form a normal subgroup.

theorem TauCeti.mul_inv_mem_vanKampenRelations {X : Type u_1} [TopologicalSpace X] (A B : Set X) (x : X) (hxA : x ∈ A) (hxB : x ∈ B) (g : FundamentalGroup ↑(A ∩ B) ⟨x, ⋯⟩) : Monoid.Coprod.inl ((FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩) g) * (Monoid.Coprod.inr ((FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩) g))⁻¹ ∈ vanKampenRelations A B x hxA hxB

Each loop in the intersection supplies a relator.

theorem TauCeti.vanKampenRelations_le_ker {X : Type u_1} [TopologicalSpace X] (A B : Set X) (x : X) (hxA : x ∈ A) (hxB : x ∈ B) : vanKampenRelations A B x hxA hxB ≤ (vanKampenLift A B x hxA hxB).ker

Intersection relations vanish under the inclusion-induced free-product map, with no cover or connectedness assumptions.

theorem TauCeti.ker_vanKampenLift {X : Type u_1} [TopologicalSpace X] {A B : Set X} {x : X} (hxA : x ∈ A) (hxB : x ∈ B) (hCover : interior A ∪ interior B = Set.univ) (hA : IsPathConnected A) (hB : IsPathConnected B) (hAB : IsPathConnected (A ∩ B)) : (vanKampenLift A B x hxA hxB).ker = vanKampenRelations A B x hxA hxB

The relations half of the based van Kampen theorem. The kernel of the canonical map from the free product is exactly the normal closure of the intersection relators.

noncomputable def TauCeti.vanKampenQuotientEquiv {X : Type u_1} [TopologicalSpace X] {A B : Set X} {x : X} (hxA : x ∈ A) (hxB : x ∈ B) (hCover : interior A ∪ interior B = Set.univ) (hA : IsPathConnected A) (hB : IsPathConnected B) (hAB : IsPathConnected (A ∩ B)) : Monoid.Coprod (FundamentalGroup ↑A ⟨x, hxA⟩) (FundamentalGroup ↑B ⟨x, hxB⟩) ⧸ vanKampenRelations A B x hxA hxB ≃* FundamentalGroup X x

The free-product quotient presentation of the fundamental group. For a cover by two path-connected sets with path-connected intersection containing the basepoint, the inclusion-induced map identifies the fundamental group with the free product modulo the normal closure of the intersection relations.

Equations

• TauCeti.vanKampenQuotientEquiv hxA hxB hCover hA hB hAB = QuotientGroup.liftEquiv (TauCeti.vanKampenRelations A B x hxA hxB) ⋯ ⋯

@[simp]

theorem TauCeti.vanKampenQuotientEquiv_mk {X : Type u_1} [TopologicalSpace X] {A B : Set X} {x : X} (hxA : x ∈ A) (hxB : x ∈ B) (hCover : interior A ∪ interior B = Set.univ) (hA : IsPathConnected A) (hB : IsPathConnected B) (hAB : IsPathConnected (A ∩ B)) (g : Monoid.Coprod (FundamentalGroup ↑A ⟨x, hxA⟩) (FundamentalGroup ↑B ⟨x, hxB⟩)) : (vanKampenQuotientEquiv hxA hxB hCover hA hB hAB) ↑g = (vanKampenLift A B x hxA hxB) g

The presentation isomorphism is induced by the canonical map from the free product.

@[simp]

theorem TauCeti.vanKampenQuotientEquiv_symm_map_left {X : Type u_1} [TopologicalSpace X] {A B : Set X} {x : X} (hxA : x ∈ A) (hxB : x ∈ B) (hCover : interior A ∪ interior B = Set.univ) (hA : IsPathConnected A) (hB : IsPathConnected B) (hAB : IsPathConnected (A ∩ B)) (g : FundamentalGroup ↑A ⟨x, hxA⟩) : (vanKampenQuotientEquiv hxA hxB hCover hA hB hAB).symm (Path.Homotopic.Quotient.map g (ContinuousMap.subtypeVal A)) = ↑(Monoid.Coprod.inl g)

The inverse presentation map sends a loop from the left cover member to its left free-product generator modulo the intersection relations.

@[simp]

theorem TauCeti.vanKampenQuotientEquiv_symm_map_right {X : Type u_1} [TopologicalSpace X] {A B : Set X} {x : X} (hxA : x ∈ A) (hxB : x ∈ B) (hCover : interior A ∪ interior B = Set.univ) (hA : IsPathConnected A) (hB : IsPathConnected B) (hAB : IsPathConnected (A ∩ B)) (g : FundamentalGroup ↑B ⟨x, hxB⟩) : (vanKampenQuotientEquiv hxA hxB hCover hA hB hAB).symm (Path.Homotopic.Quotient.map g (ContinuousMap.subtypeVal B)) = ↑(Monoid.Coprod.inr g)

The inverse presentation map sends a loop from the right cover member to its right free-product generator modulo the intersection relations.

noncomputable def TauCeti.vanKampenWideRelations {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} (C : Set X) (hCU : ∀ (i : ι), C ⊆ U i) (hx : x ∈ C) : Subgroup (Monoid.CoprodI fun (i : ι) => FundamentalGroup ↑(U i) ⟨x, ⋯⟩)

The normal subgroup of the indexed free product generated by identifying, in every pair of factors, the two images of each loop in the common intersection.

Equations

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

theorem TauCeti.vanKampenWideRelations_def {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} (C : Set X) (hCU : ∀ (i : ι), C ⊆ U i) (hx : x ∈ C) : vanKampenWideRelations C hCU hx = Subgroup.normalClosure {r : Monoid.CoprodI fun (i : ι) => FundamentalGroup ↑(U i) ⟨x, ⋯⟩ | ∃ (i : ι) (j : ι) (g : FundamentalGroup ↑C ⟨x, hx⟩), r = Monoid.CoprodI.of ((FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, hx⟩) g) * (Monoid.CoprodI.of ((FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, hx⟩) g))⁻¹}

The defining normal-closure description of the indexed intersection relations.

instance TauCeti.instNormalCoprodIFundamentalGroupElemMkMemSetVanKampenWideRelations {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} (C : Set X) (hCU : ∀ (i : ι), C ⊆ U i) (hx : x ∈ C) : (vanKampenWideRelations C hCU hx).Normal

The indexed intersection relations form a normal subgroup.

theorem TauCeti.mul_inv_mem_vanKampenWideRelations {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} (C : Set X) (hCU : ∀ (i : ι), C ⊆ U i) (hx : x ∈ C) (i j : ι) (g : FundamentalGroup ↑C ⟨x, hx⟩) : Monoid.CoprodI.of ((FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, hx⟩) g) * (Monoid.CoprodI.of ((FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, hx⟩) g))⁻¹ ∈ vanKampenWideRelations C hCU hx

Each loop in the common intersection and pair of factors supplies a relator.

theorem TauCeti.vanKampenWideRelations_le_ker {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} (C : Set X) (hCU : ∀ (i : ι), C ⊆ U i) (hx : x ∈ C) : vanKampenWideRelations C hCU hx ≤ (vanKampenWideLift U x ⋯).ker

The indexed intersection relations vanish under the inclusion-induced free-product map, without cover or connectedness assumptions.

theorem TauCeti.ker_vanKampenWideLift {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} {C : Set X} {hCU : ∀ (i : ι), C ⊆ U i} {hx : x ∈ C} (hU : ∀ (y : X), ∃ (i : ι), U i ∈ nhds y) (hUp : ∀ (i : ι), IsPathConnected (U i)) (hC : IsPathConnected C) (hUC : Pairwise fun (i j : ι) => U i ∩ U j ⊆ C) : (vanKampenWideLift U x ⋯).ker = vanKampenWideRelations C hCU hx

The relations half of van Kampen's theorem for a family. The kernel of the canonical map from the indexed free product is exactly the normal closure of the common-intersection relators.

noncomputable def TauCeti.vanKampenWideQuotientEquiv {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} {C : Set X} {hCU : ∀ (i : ι), C ⊆ U i} {hx : x ∈ C} (hU : ∀ (y : X), ∃ (i : ι), U i ∈ nhds y) (hUp : ∀ (i : ι), IsPathConnected (U i)) (hC : IsPathConnected C) (hUC : Pairwise fun (i j : ι) => U i ∩ U j ⊆ C) : (Monoid.CoprodI fun (i : ι) => FundamentalGroup ↑(U i) ⟨x, ⋯⟩) ⧸ vanKampenWideRelations C hCU hx ≃* FundamentalGroup X x

The free-product quotient presentation of the fundamental group for a family. For a cover by path-connected sets with a common path-connected pairwise intersection containing the basepoint, the fundamental group is the indexed free product modulo the overlap relations.

Equations

• TauCeti.vanKampenWideQuotientEquiv hU hUp hC hUC = QuotientGroup.liftEquiv (TauCeti.vanKampenWideRelations C hCU hx) ⋯ ⋯

@[simp]

theorem TauCeti.vanKampenWideQuotientEquiv_mk {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} {C : Set X} {hCU : ∀ (i : ι), C ⊆ U i} {hx : x ∈ C} (hU : ∀ (y : X), ∃ (i : ι), U i ∈ nhds y) (hUp : ∀ (i : ι), IsPathConnected (U i)) (hC : IsPathConnected C) (hUC : Pairwise fun (i j : ι) => U i ∩ U j ⊆ C) (g : Monoid.CoprodI fun (i : ι) => FundamentalGroup ↑(U i) ⟨x, ⋯⟩) : (vanKampenWideQuotientEquiv hU hUp hC hUC) ↑g = (vanKampenWideLift U x ⋯) g

The indexed presentation isomorphism is induced by the canonical free-product map.

@[simp]

theorem TauCeti.vanKampenWideQuotientEquiv_symm_map {X : Type u_1} [TopologicalSpace X] {x : X} {ι : Type u_2} {U : ι → Set X} {C : Set X} {hCU : ∀ (i : ι), C ⊆ U i} {hx : x ∈ C} (hU : ∀ (y : X), ∃ (i : ι), U i ∈ nhds y) (hUp : ∀ (i : ι), IsPathConnected (U i)) (hC : IsPathConnected C) (hUC : Pairwise fun (i j : ι) => U i ∩ U j ⊆ C) (i : ι) (g : FundamentalGroup ↑(U i) ⟨x, ⋯⟩) : (vanKampenWideQuotientEquiv hU hUp hC hUC).symm (Path.Homotopic.Quotient.map g (ContinuousMap.subtypeVal (U i))) = ↑(Monoid.CoprodI.of g)

The inverse indexed presentation map sends a loop from a cover member to its free-product generator modulo the common-intersection relations.