Documentation

LeanPool.JacobianDiffgeo.Forms.Basic

Holomorphic 1-forms: the definition (CC1) #

This file defines RS.Form1 X, the space of global holomorphic 1-forms on a Riemann surface X, as bundled C^ω sections of the bundle of ℂ-linear maps from the (holomorphic) tangent bundle to the trivial line bundle. This is the frozen core choice CC1 of docs/design/core-choices.md; the spelling is verified by the compiled spike scratch_forms.lean.

The AddCommGroup/Module ℂ structure and the ω-smooth vector bundle instance for the Hom bundle are all found by typeclass inference (checked by the examples below). Evaluation η x v : ℂ works through the reducible Bundle.Trivial X ℂ x ≡ ℂ.

source
@[reducible, inline]
abbrev RS.Form1 (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] :
Type u_1

The space of global holomorphic 1-forms on X: bundled C^ω sections of the bundle of ℂ-linear maps from the (holomorphic) tangent bundle to the trivial line bundle.

Downstream units interact with Form1 exclusively through the chart-coefficient API RS.coeffIn (see Jacobian/Forms/Coeffs.lean), never through bundle internals.

Equations
Instances For
    source
    theorem RS.Form1.ext' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η η' : Form1 X} (h : ∀ (x : X), η x = η' x) :
    η = η'

    Extensionality for holomorphic 1-forms from pointwise (covector-level) agreement.

    source
    theorem RS.Form1.ext_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η η' : Form1 X} (h : ∀ (x : X) (v : TangentSpace (modelWithCornersSelf ℂ ℂ) x), (η x) v = (η' x) v) :
    η = η'

    Extensionality for holomorphic 1-forms from pointwise agreement on tangent vectors.

    source
    theorem RS.Form1.add_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η η' : Form1 X) (x : X) (v : TangentSpace (modelWithCornersSelf ℂ ℂ) x) :
    ((η + η') x) v = (η x) v + (η' x) v
    source
    theorem RS.Form1.smul_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (η : Form1 X) (x : X) (v : TangentSpace (modelWithCornersSelf ℂ ℂ) x) :
    ((c • η) x) v = c * (η x) v
    source
    theorem RS.Form1.zero_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (v : TangentSpace (modelWithCornersSelf ℂ ℂ) x) :
    (0 x) v = 0
    source
    theorem RS.Form1.sub_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η η' : Form1 X) (x : X) (v : TangentSpace (modelWithCornersSelf ℂ ℂ) x) :
    ((η - η') x) v = (η x) v - (η' x) v
    source
    theorem RS.Form1.neg_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) (x : X) (v : TangentSpace (modelWithCornersSelf ℂ ℂ) x) :
    ((-η) x) v = -(η x) v