Hopf problem: pi 1 · fundamental group van kampen 1

Supporting definitions and proofs for this stage of the six-sphere construction.

structure Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover (X : Type u_1) [TopologicalSpace X] : Type u_1

A pointed two-open cover with a connected overlap for van Kampen's theorem.

• U : TopologicalSpace.Opens X

  The first open set of the cover.

• V : TopologicalSpace.Opens X

  The second open set of the cover.

• cover : ↑self.U ∪ ↑self.V = Set.univ
• pathConnectedU : IsPathConnected ↑self.U
• pathConnectedV : IsPathConnected ↑self.V
• pathConnectedIntersection : IsPathConnected (↑self.U ∩ ↑self.V)
• base : X

  The chosen base point in the overlap.

• baseU : self.base ∈ self.U
• baseV : self.base ∈ self.V

@[reducible, inline]

abbrev Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.overlap {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : TopologicalSpace.Opens X

The intersection of the two open sets.

Equations

• D.overlap = D.U ⊓ D.V

@[reducible, inline]

abbrev Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.baseUPoint {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : ↥D.U

The base point regarded as a point of the first open set.

Equations

• D.baseUPoint = ⟨D.base, ⋯⟩

@[reducible, inline]

abbrev Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.baseVPoint {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : ↥D.V

The base point regarded as a point of the second open set.

Equations

• D.baseVPoint = ⟨D.base, ⋯⟩

@[reducible, inline]

abbrev Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.baseOverlapPoint {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : ↥D.overlap

The base point regarded as a point of the overlap.

Equations

• D.baseOverlapPoint = ⟨D.base, ⋯⟩

@[reducible, inline]

abbrev Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.UGroup {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : Type u_1

The fundamental group of the first open set at the chosen base point.

Equations

• D.UGroup = FundamentalGroup (↥D.U) D.baseUPoint

@[reducible, inline]

abbrev Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.VGroup {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : Type u_1

The fundamental group of the second open set at the chosen base point.

Equations

• D.VGroup = FundamentalGroup (↥D.V) D.baseVPoint

@[reducible, inline]

abbrev Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.OverlapGroup {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : Type u_1

The fundamental group of the overlap at the chosen base point.

Equations

• D.OverlapGroup = FundamentalGroup (↥D.overlap) D.baseOverlapPoint

noncomputable def Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.overlapHomV {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : D.OverlapGroup →* D.VGroup

The fundamental-group homomorphism from the overlap into the second open set.

Equations

• D.overlapHomV = FundamentalGroup.map (Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.overlapToV✝ D) D.baseOverlapPoint

noncomputable def Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.inclusionHomU {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) : D.UGroup →* FundamentalGroup X D.base

The fundamental-group homomorphism induced by including the first open set.

Equations

• D.inclusionHomU = FundamentalGroup.map (Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.inclusionU✝ D) D.baseUPoint