Hopf problem: period family · holomorphic period map 1 #
Supporting definitions and proofs for this stage of the six-sphere construction.
@[instance_reducible]
noncomputable def
Mathoverflow1973.HolomorphicPeriodMap.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 used on the period-map cover.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Mathoverflow1973.HolomorphicPeriodMap.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₂)