3.10. Forms.LocalRep🔗

Jacobians.Forms.LocalRep — source

localRep

The local representative of a holomorphic 1-form α at y, using the trivialization of the tangent bundle at x₀. In the chart around x₀, α = localRep α x₀ y · dz where z is the chart coordinate.

noncomputable def localRep {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) (y : X) : ℂ

continuousOn_symmL_const

A constant section of a vector bundle (via inverse trivialization) is continuous on the trivialization's base set.

Proof: the section's total-space form equals e.toOpenPartialHomeomorph.symm composed with fun y => (y, v), which is continuous on e.baseSet since e.symm is continuous on its source (= baseSet × univ).

theorem continuousOn_symmL_const {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (e : Trivialization ℂ (Bundle.TotalSpace.proj (E := fun x : X =>
      TangentSpace 𝓘(ℂ, ℂ) x)))
    [MemTrivializationAtlas e] (v : ℂ) :
    ContinuousOn
      (fun y : X => TotalSpace.mk' ℂ (E := fun x : X => TangentSpace 𝓘(ℂ, ℂ) x)
        y (e.symmL ℂ y v))
      e.baseSet

localRep_continuousOn

localRep α x₀ is continuous on the trivialization's base set.

theorem localRep_continuousOn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) :
    ContinuousOn (localRep α x₀)
      (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet

localRep_add

localRep is additive: localRep (α + β) = localRep α + localRep β.

theorem localRep_add {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α β : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ y : X) :
    localRep (α + β) x₀ y = localRep α x₀ y + localRep β x₀ y

localRep_smul

localRep is homogeneous: localRep (c • α) = c • localRep α.

theorem localRep_smul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (c : ℂ)
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ y : X) :
    localRep (c • α) x₀ y = c • localRep α x₀ y

localRep_neg

localRep on a negation: localRep (-α) = -localRep α.

theorem localRep_neg {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ y : X) :
    localRep (-α) x₀ y = -localRep α x₀ y