3.9. Forms.HolomorphicForms🔗

Jacobians.Forms.HolomorphicForms — source

finrank_HolomorphicOneForms_eq_genus

Dimension of holomorphic 1-forms = genus. With genus X defined as Module.finrank ℂ (HolomorphicOneForms X) (see Jacobians.Genus), this is rfl.

theorem finrank_HolomorphicOneForms_eq_genus :
    Module.finrank ℂ (HolomorphicOneForms X) = genus X

pullbackForm

Pullback of a holomorphic 1-form along a holomorphic map of complex manifolds.

Pointwise: (pullbackForm g α)(x) = α(g x) ∘ mfderiv g x.

The smoothness (contMDiff_toFun) is the chain rule on bundle sections: α(g x) ∘ mfderiv g x : TX_x →L[ℂ] ℂ varies smoothly with x because both factors vary smoothly (α is smooth on Y, mfderiv g is smooth on X) when read in tangent coordinates.

noncomputable def pullbackForm (g : X → Y) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g) :
    HolomorphicOneForms Y →ₗ[ℂ] HolomorphicOneForms X where

pullbackForm_id

pullbackForm id = id. Follows from mfderiv id = id and ContinuousLinearMap.comp_id.

theorem pullbackForm_id : pullbackForm (id : X → X) contMDiff_id =
    LinearMap.id (R := ℂ) (M := HolomorphicOneForms X)

pullbackForm_comp

Contravariance of pullback: (g ∘ f)^* = f^* ∘ g^*. Follows from the chain rule mfderiv_comp + associativity of composition.

theorem pullbackForm_comp (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g)
    (hgf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (g ∘ f)) :
    pullbackForm (g ∘ f) hgf =
      (pullbackForm f hf).comp (pullbackForm g hg)

ambientIso

A linear isomorphism (Fin (genus X) → ℂ) ≃ₗ[ℂ] HolomorphicOneForms X from a choice of basis, via Module.finBasisOfFinrankEq + the dimension equality finrank_HolomorphicOneForms_eq_genus.

noncomputable def ambientIso (X : Type*) [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] :
    (Fin (genus X) → ℂ) ≃ₗ[ℂ] HolomorphicOneForms X

ambientPsi

The ambient ℂ-linear map Ψ induced by the pullback of forms along f : X → Y. Defined via ambientIso + pullbackForm: Ψ = (ambientIso X).symm ∘ pullbackForm f hf ∘ ambientIso Y (when the genus sizes match; otherwise zero — this branch is never used in the challenge). This is a concrete definition (no gaps at this level), but it depends on ambientIso which internally depends on finrank_HolomorphicOneForms_eq_genus.

noncomputable def ambientPsi {gX gY : ℕ}
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    (Fin gY → ℂ) →L[ℂ] (Fin gX → ℂ)

ambientPhi

The ambient ℂ-linear map Φ induced by the pushforward of forms along f : X → Y. Defined as the matrix-transpose of ambientPsi f hf (= Mᵀ, via the standard Pi basis). The transpose reverses composition order, so covariant ambientPhi_comp is automatic from contravariant ambientPsi_comp.

noncomputable def ambientPhi {gX gY : ℕ}
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    (Fin gX → ℂ) →L[ℂ] (Fin gY → ℂ)

ambientPsi_id

ambientPsi id = id. Proven via pullbackForm_id.

theorem ambientPsi_id (y : Fin (genus X) → ℂ) :
    ambientPsi (X := X) (Y := X) (gX := genus X) (gY := genus X) id contMDiff_id y = y

ambientPsi_comp

Contravariant composition: ambientPsi (g ∘ f) = ambientPsi f ∘ ambientPsi g. Proven via pullbackForm_comp.

theorem ambientPsi_comp {Z : Type*} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
    [ConnectedSpace Z] [ChartedSpace ℂ Z] [IsManifold 𝓘(ℂ) ω Z]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g)
    (hgf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (g ∘ f))
    (z : Fin (genus Z) → ℂ) :
    ambientPsi (gX := genus X) (gY := genus Z) (g ∘ f) hgf z =
      ambientPsi (gX := genus X) (gY := genus Y) f hf
        (ambientPsi (gX := genus Y) (gY := genus Z) g hg z)

ambientPhi_id

ambientPhi id = id — follows from ambientPsi_id via the transpose construction: transpose of identity matrix is identity.

theorem ambientPhi_id (x : Fin (genus X) → ℂ) :
    ambientPhi (X := X) (Y := X) (gX := genus X) (gY := genus X) id contMDiff_id x = x

ambientPhi_comp

Covariant composition: ambientPhi (g ∘ f) = ambientPhi g ∘ ambientPhi f. Follows from ambientPsi_comp via matrix transpose reversing composition order.

theorem ambientPhi_comp {Z : Type*} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
    [ConnectedSpace Z] [ChartedSpace ℂ Z] [IsManifold 𝓘(ℂ) ω Z]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g)
    (hgf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (g ∘ f))
    (x : Fin (genus X) → ℂ) :
    ambientPhi (gX := genus X) (gY := genus Z) (g ∘ f) hgf x =
      ambientPhi (gX := genus Y) (gY := genus Z) g hg
        (ambientPhi (gX := genus X) (gY := genus Y) f hf x)