Fundamental Group

Results named in Tau Ceti's TauCeti.AlgebraicTopology.FundamentalGroup modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe 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).

TauCeti.isPushout_fundamentalGroup.{u_1} {X : Type u_1} [TopologicalSpace X] {A B : Set X} {x : X}
  (hCover : interior A ∪ interior B = Set.univ) (hA : IsPathConnected A) (hB : IsPathConnected B)
  (hAB : IsPathConnected (A ∩ B)) (hxA : x ∈ A) (hxB : x ∈ B) :
  CategoryTheory.IsPushout (GrpCat.ofHom (FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩))
    (GrpCat.ofHom (FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩))
    (GrpCat.ofHom (FundamentalGroup.map (ContinuousMap.subtypeVal A) ⟨x, hxA⟩))
    (GrpCat.ofHom (FundamentalGroup.map (ContinuousMap.subtypeVal B) ⟨x, hxB⟩))

Lean

Formalized in Tau Ceti as TauCeti.isPushout_fundamentalGroup.

Other forms

The based Seifert--van Kampen theorem for a simply connected overlap. Formalized in Tau Ceti as TauCeti.vanKampenLift_bijective.

TauCeti.vanKampenLift_bijective.{u_1} {X : Type u_1} [TopologicalSpace X] {A B : Set X} {x : X}
  (hCover : interior A ∪ interior B = Set.univ) (hA : IsPathConnected A) (hB : IsPathConnected B)
  (hAB : IsSimplyConnected (A ∩ B)) (hxA : x ∈ A) (hxB : x ∈ B) :
  Function.Bijective ⇑(TauCeti.vanKampenLift A B x hxA hxB)

Sources

• Tau Ceti documentation: TauCeti.isPushout_fundamentalGroup
• Source of TauCeti.isPushout_fundamentalGroup in TauCeti/AlgebraicTopology/FundamentalGroup/VanKampen/Basic.lean

LeanTauCeti.isPushout_fundamentalGroup · TauCeti.vanKampenLift_bijective

Used by 1

Used byConnected covers of ℂ ∖ {0, 1} of degree n up to isomorphism are classified by the isomorphism classes of connected triples of degree n

TheoremThe based van Kampen theorem for a neighborhood cover, in universal-property form#

Pairwise compatible homomorphisms out of the fundamental groups of the cover members extend uniquely to the ambient fundamental group. Repeated indices in the triple-intersection hypothesis imply path connectedness of the double intersections and individual members. No common pairwise intersection is required, and the target can be any monoid.

TauCeti.existsUnique_vanKampenDesc.{u, v, w} {K : Type w} [Monoid K] {X : Type v}
  [TopologicalSpace X] {ι : Type u} (U : ι → Set X) (x : X) (hCover : ∀ (y : X), ∃ i, U i ∈ nhds y)
  (hx : ∀ (i : ι), x ∈ U i) (hTriple : ∀ (i j k : ι), IsPathConnected (U i ∩ U j ∩ U k))
  (f : (i : ι) → FundamentalGroup ↑(U i) ⟨x, ⋯⟩ →* K)
  (hcompat :
    ∀ (i j : ι),
      (f i).comp (FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩) =
        (f j).comp (FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩)) :
  ∃! d, ∀ (i : ι), d.comp (FundamentalGroup.map (ContinuousMap.subtypeVal (U i)) ⟨x, ⋯⟩) = f i

Lean

Formalized in Tau Ceti as TauCeti.existsUnique_vanKampenDesc.

Sources

• Tau Ceti documentation: TauCeti.existsUnique_vanKampenDesc
• Source of TauCeti.existsUnique_vanKampenDesc in TauCeti/AlgebraicTopology/FundamentalGroup/VanKampen/Cover.lean

LeanTauCeti.existsUnique_vanKampenDesc

Uses 1

Proof usesUniqueness in the Seifert--van Kampen theorem for a family

TheoremThe 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.

TauCeti.vanKampenWideLift_surjective.{u_1, u_2} {X : Type u_1} [TopologicalSpace X] {ι : Type u_2}
  {U : ι → Set X} {x : X} (hU : ∀ (y : X), ∃ i, U i ∈ nhds y) (hxU : ∀ (i : ι), x ∈ U i)
  (hpc : ∀ (i j : ι), IsPathConnected (U i ∩ U j)) :
  Function.Surjective ⇑(TauCeti.vanKampenWideLift U x hxU)

Lean

Formalized in Tau Ceti as TauCeti.vanKampenWideLift_surjective.

Sources

• Tau Ceti documentation: TauCeti.vanKampenWideLift_surjective
• Source of TauCeti.vanKampenWideLift_surjective in TauCeti/AlgebraicTopology/FundamentalGroup/VanKampen/Basic.lean

LeanTauCeti.vanKampenWideLift_surjective

TheoremThe 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.

TauCeti.ker_vanKampenWideLift.{u_1, u_2} {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) :
  (TauCeti.vanKampenWideLift U x ⋯).ker = TauCeti.vanKampenWideRelations C hCU hx

Lean

Formalized in Tau Ceti as TauCeti.ker_vanKampenWideLift.

Sources

• Tau Ceti documentation: TauCeti.ker_vanKampenWideLift
• Source of TauCeti.ker_vanKampenWideLift in TauCeti/AlgebraicTopology/FundamentalGroup/VanKampen/Presentation/Basic.lean

LeanTauCeti.ker_vanKampenWideLift

DefinitionThe 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.

TauCeti.isColimitFundamentalGroupWideCocone.{u_1, u_2} {X : Type u_1} [TopologicalSpace X]
  {ι : Type u_2} {U : ι → Set X} {C : Set X} {x : X} (hU : ∀ (y : X), ∃ i, U i ∈ nhds y)
  (hUp : ∀ (i : ι), IsPathConnected (U i)) (hC : IsPathConnected C) (hCU : ∀ (i : ι), C ⊆ U i)
  (hUC : Pairwise fun i j => U i ∩ U j ⊆ C) (hx : x ∈ C) :
  CategoryTheory.Limits.IsColimit (TauCeti.fundamentalGroupWideCocone hCU hx)

Lean

Formalized in Tau Ceti as TauCeti.isColimitFundamentalGroupWideCocone.

Other forms

The Seifert--van Kampen theorem for a family with a simply connected common pairwise intersection. Formalized in Tau Ceti as TauCeti.vanKampenWideEquiv.

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

Sources

• Tau Ceti documentation: TauCeti.isColimitFundamentalGroupWideCocone
• Source of TauCeti.isColimitFundamentalGroupWideCocone in TauCeti/AlgebraicTopology/FundamentalGroup/VanKampen/Basic.lean

LeanTauCeti.isColimitFundamentalGroupWideCocone · TauCeti.vanKampenWideEquiv

Uses 1 · Used by 3

Proof usesUniqueness in the Seifert--van Kampen theorem for a family

Used byThe cellular and the simplicial classifying spaces agree · The cellular classifying space is a CW complex · Uniqueness of aspherical spaces of CW type

TheoremTwo-set van Kampen criterion for simple connectedness#

A space covered by the interiors of two simply connected sets with path-connected intersection is simply connected.

TauCeti.simplyConnectedSpace_of_interior_union.{u_1} {X : Type u_1} [TopologicalSpace X]
  {A B : Set X} (hCover : interior A ∪ interior B = Set.univ) (hAB : IsPathConnected (A ∩ B))
  [SimplyConnectedSpace ↑A] [SimplyConnectedSpace ↑B] : SimplyConnectedSpace X

Lean

Formalized in Tau Ceti as TauCeti.simplyConnectedSpace_of_interior_union.

Sources

• Tau Ceti documentation: TauCeti.simplyConnectedSpace_of_interior_union
• Source of TauCeti.simplyConnectedSpace_of_interior_union in TauCeti/AlgebraicTopology/FundamentalGroup/VanKampen/Basic.lean

LeanTauCeti.simplyConnectedSpace_of_interior_union

TheoremUniqueness 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.

TauCeti.vanKampenWide_hom_ext.{u_1, u_2, u_3} {X : Type u_1} [TopologicalSpace X] {ι : Type u_2}
  {U : ι → Set X} {x : X} {K : Type u_3} [Monoid K] (hU : ∀ (y : X), ∃ i, U i ∈ nhds y)
  (hx : ∀ (i : ι), x ∈ U i) (hpc : ∀ (i j : ι), IsPathConnected (U i ∩ U j))
  {f g : FundamentalGroup X x →* K}
  (hfg :
    ∀ (i : ι),
      f.comp (FundamentalGroup.map (ContinuousMap.subtypeVal (U i)) ⟨x, ⋯⟩) =
        g.comp (FundamentalGroup.map (ContinuousMap.subtypeVal (U i)) ⟨x, ⋯⟩)) :
  f = g

Lean

Formalized in Tau Ceti as TauCeti.vanKampenWide_hom_ext.

Sources

• Tau Ceti documentation: TauCeti.vanKampenWide_hom_ext
• Source of TauCeti.vanKampenWide_hom_ext in TauCeti/AlgebraicTopology/FundamentalGroup/VanKampen/Basic.lean

LeanTauCeti.vanKampenWide_hom_ext

Used by 2

Used byThe based van Kampen theorem for a neighborhood cover, in universal-property form · The Seifert--van Kampen theorem for a family with a common pairwise intersection

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.