2.3. Theorems & lemmas
2.3.1. genus_eq_zero_iff_homeo
example :
genus X = 0 ↔ Nonempty (X ≃ₜ (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)) :=
genus_eq_zero_iff_homeo
2.3.2. ofCurve_contMDiff
example (P : X) : ContMDiff 𝓘(ℂ) 𝓘(ℂ, Fin (genus X) → ℂ) ω (ofCurve P) := ofCurve_contMDiff P
2.3.3. ofCurve_self
example (P : X) : ofCurve P P = 0 := ofCurve_self P
2.3.4. ofCurve_inj
example (P : X) (h : 0 < genus X) : Function.Injective (ofCurve P) := ofCurve_inj P h
2.3.5. pushforward_contMDiff
example :
ContMDiff 𝓘(ℂ, Fin (genus X) → ℂ) 𝓘(ℂ, Fin (genus Y) → ℂ) ω (pushforward f hf) :=
pushforward_contMDiff f hf
2.3.6. pushforward_id_apply
example (P : Jacobian X) : pushforward id contMDiff_id P = P := pushforward_id_apply P
2.3.7. pushforward_comp_apply
example (P : Jacobian X) :
pushforward (g ∘ f) (hg.comp hf) P = pushforward g hg (pushforward f hf P) := by
apply pushforward_comp_apply
2.3.8. pullback_contMDiff
example :
ContMDiff 𝓘(ℂ, Fin (genus Y) → ℂ) 𝓘(ℂ, Fin (genus X) → ℂ) ω (pullback f hf) :=
pullback_contMDiff f hf
2.3.9. pullback_id_apply
example (P : Jacobian X) : pullback id contMDiff_id P = P := pullback_id_apply P
2.3.10. pullback_comp_apply
example (P : Jacobian Z) :
pullback (g.comp f) (hg.comp hf) P = pullback f hf (pullback g hg P) := by
apply pullback_comp_apply
2.3.11. pushforward_pullback
example (P : Jacobian Y) :
pushforward f hf (pullback f hf P) = (ContMDiff.degree f hf) • P := by
apply pushforward_pullback