Jacobians of compact Riemann surfaces

11 statement formalized3 ready to state3 planned

Jacobian Challenge

DefinitionGenus of a compact Riemann surface#●ready to state

For a compact Riemann surface \(X\), that is, a compact connected Hausdorff space with a complex-analytic atlas modelled on \(\mathbb{C}\), the genus of \(X\) is a natural number.

public def_wanted genus (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ω X] : ℕ

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Used by 5

Used byA compact Riemann surface has genus zero iff it is a sphere · The Abel–Jacobi map is holomorphic · The Abel–Jacobi map is injective in positive genus · The pullback map on Jacobians is holomorphic · The pushforward on Jacobians is holomorphic

TheoremA compact Riemann surface has genus zero iff it is a sphere#●statement formalized

Let \(X\) be a compact Riemann surface, that is, a compact connected Hausdorff space with a complex-analytic atlas modelled on \(\mathbb{C}\). The genus of \(X\) is \(0\) if and only if \(X\) is homeomorphic to the unit sphere in Euclidean space \(\mathbb{R}^3\).

public theorem_wanted genus_eq_zero_iff_homeo :
    ❰genus❱ X = 0 ↔ Nonempty (X ≃ₜ (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1))

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 1

Statement usesGenus of a compact Riemann surface

DefinitionJacobian of a compact Riemann surface#●ready to state

For a compact Riemann surface \(X\), that is, a compact connected Hausdorff space with a complex-analytic atlas modelled on \(\mathbb{C}\), the Jacobian \(J(X)\) of \(X\) is a type in the same universe as \(X\).

Separate wanted instances make \(J(X)\) a compact Hausdorff commutative complex Lie group modelled on \(\mathbb{C}^g\), where \(g\) is the genus of \(X\).

public def_wanted Jacobian (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ω X] : Type u

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Used by 13

Used byAbel–Jacobi map · The Abel–Jacobi map is holomorphic · The Abel–Jacobi map is injective in positive genus · The Abel–Jacobi map sends the base point to zero · Pullback on Jacobians · Pullback on Jacobians is compatible with composition · The pullback map on Jacobians is holomorphic · Pullback along the identity · Pushforward on Jacobians · Pushforward respects composition · The pushforward on Jacobians is holomorphic · Pushforward along the identity · Pushforward of a pullback is multiplication by the degree

Jacobian

DefinitionAbel–Jacobi map#●planned

Let \(X\) be a compact Riemann surface with Jacobian \(J(X)\). Each point \(P \in X\) gives a map \(X \to J(X)\), the Abel–Jacobi map based at \(P\).

public def_wanted ofCurve (P : X) : X → ❰Jacobian❱ X

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 1 · Used by 3

Statement usesJacobian of a compact Riemann surface

Used byThe Abel–Jacobi map is holomorphic · The Abel–Jacobi map is injective in positive genus · The Abel–Jacobi map sends the base point to zero

TheoremThe Abel–Jacobi map is holomorphic#●statement formalized

Let \(X\) be a compact Riemann surface of genus \(g\), and let \(J(X)\) be its Jacobian, a complex manifold modelled on \(\mathbb{C}^g\). For every point \(P \in X\), the Abel–Jacobi map \(X \to J(X)\) based at \(P\) is holomorphic.

public theorem_wanted ofCurve_contMDiff (P : X) :
    ContMDiff (modelWithCornersSelf ℂ ℂ)
      (modelWithCornersSelf ℂ (Fin (❰genus❱ X) → ℂ)) ω (❰ofCurve❱ P)

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 3

Statement usesJacobian of a compact Riemann surface · Abel–Jacobi map · Genus of a compact Riemann surface

TheoremThe Abel–Jacobi map sends the base point to zero#●statement formalized

Let \(X\) be a compact Riemann surface with Jacobian \(J(X)\), an abelian group. For every point \(P \in X\), the Abel–Jacobi map \(X \to J(X)\) based at \(P\) sends \(P\) to \(0\).

public theorem_wanted ofCurve_self (P : X) : ❰ofCurve❱ P P = 0

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 2

Statement usesJacobian of a compact Riemann surface · Abel–Jacobi map

TheoremThe Abel–Jacobi map is injective in positive genus#●statement formalized

Let \(X\) be a compact Riemann surface with Jacobian \(J(X)\), and let \(P \in X\). If the genus of \(X\) is positive, then the Abel–Jacobi map \(X \to J(X)\) based at \(P\) is injective.

public theorem_wanted ofCurve_inj (P : X) : 0 < ❰genus❱ X → Function.Injective (❰ofCurve❱ P)

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 3

Statement usesJacobian of a compact Riemann surface · Abel–Jacobi map · Genus of a compact Riemann surface

DefinitionPushforward on Jacobians#●planned

Let \(X\) and \(Y\) be compact Riemann surfaces, that is, compact, connected, Hausdorff complex-analytic manifolds of dimension one, and write \(J(X)\) for the Jacobian of \(X\), an abelian group with a topology. For a holomorphic map \(f : X \to Y\), the pushforward \(f_*\) is a continuous group homomorphism from \(J(X)\) to \(J(Y)\). It is meant to be the homomorphism induced by \(f\); its properties are stated separately.

public def_wanted pushforward (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ❰Jacobian❱ X →ₜ+ ❰Jacobian❱ Y

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 1 · Used by 4

Statement usesJacobian of a compact Riemann surface

Used byPushforward respects composition · The pushforward on Jacobians is holomorphic · Pushforward along the identity · Pushforward of a pullback is multiplication by the degree

TheoremThe pushforward on Jacobians is holomorphic#●statement formalized

Let \(X\) and \(Y\) be compact Riemann surfaces, that is, compact, connected, Hausdorff complex-analytic manifolds of dimension one, of genera \(g_X\) and \(g_Y\). The Jacobian \(J(X)\) of \(X\) is a complex-analytic manifold modeled on \(\mathbb{C}^{g_X}\), and likewise \(J(Y)\) on \(\mathbb{C}^{g_Y}\). For every holomorphic map \(f : X \to Y\), the pushforward \(f_* : J(X) \to J(Y)\) is holomorphic.

public theorem_wanted pushforward_contMDiff (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ContMDiff (modelWithCornersSelf ℂ (Fin (❰genus❱ X) → ℂ))
      (modelWithCornersSelf ℂ (Fin (❰genus❱ Y) → ℂ)) ω (❰pushforward❱ f hf)

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 3

Statement usesJacobian of a compact Riemann surface · Pushforward on Jacobians · Genus of a compact Riemann surface

TheoremPushforward along the identity#●statement formalized

Let \(X\) be a compact Riemann surface, that is, a compact, connected, Hausdorff complex-analytic manifold of dimension one, and write \(J(X)\) for its Jacobian. For every \(P \in J(X)\), the pushforward of \(P\) along the identity map of \(X\) is \(P\): \((\mathrm{id}_X)_*(P) = P\).

public theorem_wanted pushforward_id_apply :
    ∀ P : ❰Jacobian❱ X, ❰pushforward❱ id contMDiff_id P = P

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 2

Statement usesJacobian of a compact Riemann surface · Pushforward on Jacobians

TheoremPushforward respects composition#●statement formalized

Let \(X\), \(Y\) and \(Z\) be compact Riemann surfaces, that is, compact, connected, Hausdorff complex-analytic manifolds of dimension one, and write \(J(X)\) for the Jacobian of \(X\). For all holomorphic maps \(f : X \to Y\) and \(g : Y \to Z\) and every \(P \in J(X)\), the pushforwards satisfy \((g \circ f)_*(P) = g_*(f_*(P))\).

public theorem_wanted pushforward_comp_apply (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω g) :
    ∀ P : ❰Jacobian❱ X,
      ❰pushforward❱ (g ∘ f) (hg.comp hf) P = ❰pushforward❱ g hg (❰pushforward❱ f hf P)

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 2

Statement usesJacobian of a compact Riemann surface · Pushforward on Jacobians

DefinitionPullback on Jacobians#●planned

Let \(X\) and \(Y\) be compact Riemann surfaces, that is, compact, connected, Hausdorff complex-analytic manifolds of dimension one, and write \(J(X)\) for the Jacobian of \(X\), an abelian group with a topology. For a holomorphic map \(f : X \to Y\), the pullback \(f^*\) is a continuous group homomorphism from \(J(Y)\) to \(J(X)\). It is meant to be the zero map when \(f\) is constant and the usual pullback along \(f\) otherwise; its properties are stated separately.

public def_wanted pullback (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ❰Jacobian❱ Y →ₜ+ ❰Jacobian❱ X

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 1 · Used by 4

Statement usesJacobian of a compact Riemann surface

Used byPullback on Jacobians is compatible with composition · The pullback map on Jacobians is holomorphic · Pullback along the identity · Pushforward of a pullback is multiplication by the degree

TheoremThe pullback map on Jacobians is holomorphic#●statement formalized

Let \(X\) and \(Y\) be compact Riemann surfaces of genus \(g_X\) and \(g_Y\), with Jacobians \(J(X)\) and \(J(Y)\), complex manifolds modelled on \(\mathbb{C}^{g_X}\) and \(\mathbb{C}^{g_Y}\). For every holomorphic map \(f : X \to Y\), the induced pullback map \(f^* : J(Y) \to J(X)\) is holomorphic.

public theorem_wanted pullback_contMDiff (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ContMDiff (modelWithCornersSelf ℂ (Fin (❰genus❱ Y) → ℂ))
      (modelWithCornersSelf ℂ (Fin (❰genus❱ X) → ℂ)) ω (❰pullback❱ f hf)

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 3

Statement usesJacobian of a compact Riemann surface · Pullback on Jacobians · Genus of a compact Riemann surface

TheoremPullback along the identity#●statement formalized

Let \(X\) be a compact Riemann surface, that is, a compact, connected, Hausdorff complex-analytic manifold of dimension one, and write \(J(X)\) for its Jacobian. For every \(P \in J(X)\), the pullback of \(P\) along the identity map of \(X\) is \(P\): \((\mathrm{id}_X)^*(P) = P\).

public theorem_wanted pullback_id_apply :
    ∀ P : ❰Jacobian❱ X, ❰pullback❱ id contMDiff_id P = P

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 2

Statement usesJacobian of a compact Riemann surface · Pullback on Jacobians

TheoremPullback on Jacobians is compatible with composition#●statement formalized

Let \(X\), \(Y\) and \(Z\) be compact Riemann surfaces, and for a holomorphic map \(h\) between compact Riemann surfaces write \(h^*\) for the induced pullback map on Jacobians. For all holomorphic maps \(f : X \to Y\) and \(g : Y \to Z\) and every point \(P\) of the Jacobian \(J(Z)\), we have \((g \circ f)^*(P) = f^*(g^*(P))\).

public theorem_wanted pullback_comp_apply (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω g) :
    ∀ P : ❰Jacobian❱ Z,
      ❰pullback❱ (g.comp f) (hg.comp hf) P = ❰pullback❱ f hf (❰pullback❱ g hg P)

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 2

Statement usesJacobian of a compact Riemann surface · Pullback on Jacobians

DefinitionDegree of a holomorphic map#●ready to state

Let \(X\) and \(Y\) be compact Riemann surfaces, that is, compact connected Hausdorff spaces with a complex-analytic atlas modelled on \(\mathbb{C}\). Every holomorphic map \(f : X \to Y\) has a degree, which is a natural number.

The intended value is \(0\) when \(f\) is constant and the usual degree of \(f\) otherwise.

public def_wanted degree (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) : ℕ  -- 0 for constant case

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Used by 1

Used byPushforward of a pullback is multiplication by the degree

TheoremPushforward of a pullback is multiplication by the degree#●statement formalized

Let \(X\) and \(Y\) be compact Riemann surfaces, that is, compact, connected, Hausdorff complex-analytic manifolds of dimension one, and write \(J(Y)\) for the Jacobian of \(Y\), an abelian group. For every holomorphic map \(f : X \to Y\) and every \(P \in J(Y)\), the pushforward along \(f\) of the pullback of \(P\) along \(f\) is \(\deg(f) \cdot P\), where the degree \(\deg(f)\) is a natural number: \(f_*(f^*(P)) = \deg(f) \cdot P\).

public theorem_wanted pushforward_pullback (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ∀ P : ❰Jacobian❱ Y, ❰pushforward❱ f hf (❰pullback❱ f hf P) = (❰degree❱ f hf) • P

Sources

• https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge. Problem jacobian_challenge_diffgeo of the lean-eval benchmark.

Uses 4

Statement usesJacobian of a compact Riemann surface · Degree of a holomorphic map · Pullback on Jacobians · Pushforward on Jacobians

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.