Hopf problem: pi 1 · mapping torus

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

@[reducible, inline]

abbrev Mathoverflow1973.ThreefoldOverlapMappingTorus.Cusp.monodromy : RealTorus₄ ≃ₜ RealTorus₄

The torus monodromy used for the cusp boundary mapping torus.

Equations

• Mathoverflow1973.ThreefoldOverlapMappingTorus.Cusp.monodromy = Mathoverflow1973.SpecialPeriods.CuspFamily.cuspTorusHomeomorph 1