The circle chart #
Two interior charts whose overlap is disconnected wrap around and close M into a
circle: after normalizing, the overlap has exactly two components, one at each end of
each chart. We shrink the charts' coordinates (Möbius) into a controlled numeric regime,
choose a split point in each component, and glue the two charts — each embedded as an
arc of AddCircle 1 — with OpenPartialHomeomorph.piecewise along a closed sub-arc
whose frontier is the two split points. The result is a chart of M onto the whole of
AddCircle 1 with source a.source ∪ b.source.
Small helpers #
theorem
OneMfld.exists_circle_chart
{M : Type u_1}
[TopologicalSpace M]
[T2Space M]
(a b : OChart M)
(h : Overlap a.source b.source)
(hdisc : ¬IsConnected (a.source ∩ b.source))
:
The circle chart. Two O-charts with Overlap and a disconnected overlap glue to
a chart of M onto the whole of AddCircle 1.