2.2. Instances on the Jacobian
2.2.1. AddCommGroup
The Jacobian is naturally an additive commutative group.
example : AddCommGroup (Jacobian X) := inferInstance
2.2.2. TopologicalSpace
The Jacobian is naturally a topological space.
example : TopologicalSpace (Jacobian X) := inferInstance
2.2.3. T2Space
The Jacobian is Hausdorff.
example : T2Space (Jacobian X) := inferInstance
2.2.4. CompactSpace
The Jacobian is compact.
example : CompactSpace (Jacobian X) := inferInstance
2.2.5. ChartedSpace
The Jacobian is a complex manifold of dimension equal to the genus.
example : ChartedSpace (Fin (genus X) → ℂ) (Jacobian X) := inferInstance
2.2.6. IsManifold
The Jacobian is a complex manifold.
example : IsManifold 𝓘(ℂ, Fin (genus X) → ℂ) ω (Jacobian X) := inferInstance
2.2.7. LieAddGroup
The Jacobian is a complex Lie group.
example : LieAddGroup 𝓘(ℂ, Fin (genus X) → ℂ) ω (Jacobian X) := inferInstance