Hopf problem: period family · holomorphic period map 2 #
Supporting definitions and proofs for this stage of the six-sphere construction.
@[instance_reducible]
noncomputable def
Mathoverflow1973.HolomorphicPeriodMap.periodPullbackCoveringChartedSpace
{V : Type u_1}
{B : Type u_2}
[NormedAddCommGroup V]
[TopologicalSpace B]
[ChartedSpace V B]
:
ChartedSpace (V × ComplexPlane₂) (B × ComplexPlane₂)
The charted-space structure on the pullback of the period cover.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Mathoverflow1973.HolomorphicPeriodMap.periodPullbackCoveringManifold
{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₂)