Hopf problem: foundations · two affine charts

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

structure Mathoverflow1973.TwoAffineCharts (Y : Type u_1) [TopologicalSpace Y] : Type u_1

Two complex affine charts related by inversion on their common punctured domain.

• left : ℂ → Y

  The left affine chart.

• right : ℂ → Y

  The right affine chart.

• continuous_left : Continuous self.left
• continuous_right : Continuous self.right
• left_injective : Function.Injective self.left
• right_injective : Function.Injective self.right
• inversion (z : ℂ) : z ≠ 0 → self.left z = self.right z⁻¹
• endpoints_ne : self.left 0 ≠ self.right 0
• covered (y : Y) : (∃ (z : ℂ), self.left z = y) ∨ ∃ (z : ℂ), self.right z = y

theorem Mathoverflow1973.TwoAffineCharts.range_right {Y : Type u_1} [TopologicalSpace Y] (A : TwoAffineCharts Y) : Set.range A.right = {A.left 0}ᶜ