Hopf problem: period family · core 2 #
Supporting definitions and proofs for this stage of the six-sphere construction.
@[instance_reducible]
noncomputable def
Mathoverflow1973.PeriodFamily.Data.coveringChartedSpace
{V : Type u_1}
{B : Type u_2}
[NormedAddCommGroup V]
[TopologicalSpace B]
[ChartedSpace V B]
:
ChartedSpace (V × ComplexPlane₂) (B × ComplexPlane₂)
The product charted-space structure on the covering space of a period family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Mathoverflow1973.PeriodFamily.Data.coveringManifold
{V : Type u_1}
{B : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℂ V]
[TopologicalSpace B]
[ChartedSpace V B]
[IsManifold (modelWithCornersSelf ℂ V) ⊤ B]
:
IsManifold (modelWithCornersSelf ℂ (V × ComplexPlane₂)) ⊤ (B × ComplexPlane₂)