Hopf problem: homology of x · threefold gluing 1

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

structure Mathoverflow1973.ThreefoldGluing.Data (B : Type u) [TopologicalSpace B] : Type (u + 1)

Compatible local pieces and transition maps for gluing a threefold over a base.

• J : Type u

  The index type of the local pieces.

• patch : self.J → TopologicalSpace.Opens B

  The open base patch indexed by each local piece.

• cover : TopologicalSpace.IsOpenCover self.patch
• piece : self.J → TopCat

  The topological space lying over each base patch.

• toBase (i : self.J) : C(↑(self.piece i), B)

  The projection from each local piece to the base.

• toBase_mem (i : self.J) (x : ↑(self.piece i)) : (self.toBase i) x ∈ self.patch i
• transition (i j : self.J) : OpenPartialHomeomorph ↑(self.piece i) ↑(self.piece j)

  The partial homeomorphism identifying a pair of local pieces.

• source_eq (i j : self.J) : (self.transition i j).source = ⇑(self.toBase i) ⁻¹' ↑(self.patch j)
• self_eq (i : self.J) : self.transition i i = OpenPartialHomeomorph.refl ↑(self.piece i)
• symm_eq (i j : self.J) : (self.transition i j).symm = self.transition j i
• preserves_base (i j : self.J) (x : ↑(self.piece i)) : x ∈ (self.transition i j).source → (self.toBase j) (↑(self.transition i j) x) = (self.toBase i) x
• cocycle (i j k : self.J) (x : ↑(self.piece i)) : x ∈ (self.transition i j).source → ↑(self.transition i j) x ∈ (self.transition j k).source → ↑(self.transition j k) (↑(self.transition i j) x) = ↑(self.transition i k) x

theorem Mathoverflow1973.ThreefoldGluing.Data.transition_map_source {B : Type u} [TopologicalSpace B] (D : Data B) (i j : D.J) {x : ↑(D.piece i)} (hx : x ∈ (D.transition i j).source) : ↑(D.transition i j) x ∈ (D.transition j i).source

theorem Mathoverflow1973.ThreefoldGluing.Data.transition_inter {B : Type u} [TopologicalSpace B] (D : Data B) (i j k : D.J) {x : ↑(D.piece i)} (hx : x ∈ (D.transition i j).source) (hk : x ∈ (D.transition i k).source) : ↑(D.transition i j) x ∈ (D.transition j k).source

@[reducible, inline]

abbrev Mathoverflow1973.ThreefoldGluing.Data.gluingCore {B : Type u} [TopologicalSpace B] (D : Data B) : TopCat.GlueData.MkCore

The core TopCat gluing datum associated to threefold gluing data.

Equations

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

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.ThreefoldGluing.Data.gluing {B : Type u} [TopologicalSpace B] (D : Data B) : TopCat.GlueData

The TopCat gluing datum associated to threefold gluing data.

Equations

• D.gluing = TopCat.GlueData.mk' D.gluingCore

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.ThreefoldGluing.Data.Space {B : Type u} [TopologicalSpace B] (D : Data B) : TopCat

The topological space obtained by gluing the local pieces.

Equations

• D.Space = D.gluing.glued