15.3. FormTraceSheetCovector🔗

Jacobians.FormTraceSheetCovector — source

symmL_self_one

The self-frame unit tangent is the model unit. The trivialization-at-a of the tangent bundle, evaluated at a on the unit 1 : ℂ, is 1: by trivAt_symmL_one_eq_fderiv_C it is the derivative of the self chart-transition chart_a ∘ chart_a.symm = id, which is 1.

theorem symmL_self_one (a : X) :
    (trivTS a).symmL ℂ a (1 : ℂ) = (1 : ℂ)

localRep_self_eq_toFun_one

The centred local representative is the pairing against the model unit. localRep ω₀ a a = ω₀.toFun a (1 : ℂ) (since the self-frame unit tangent is 1).

theorem localRep_self_eq_toFun_one (ω₀ : HolomorphicOneForms X) (a : X) :
    Jacobians.Montel.localRep ω₀ a a = ω₀.toFun a (1 : ℂ)

toFun_apply_eq_mul_localRep

Covector pairing in the self frame. For a holomorphic 1-form ω₀ and a tangent w at a (in the model fibre ℂ), the pairing ω₀.toFun a w is w times the centred local representative localRep ω₀ a a. ℂ-linearity: w = w • 1, and ω₀.toFun a 1 = localRep ω₀ a a.

theorem toFun_apply_eq_mul_localRep (ω₀ : HolomorphicOneForms X) (a : X) (w : ℂ) :
    ω₀.toFun a w = w * Jacobians.Montel.localRep ω₀ a a

localRep_eq_transition_mul_self

Frame-transition law for localRep. For y in the chart source of a, the local representative of ω₀ based at a and read at y equals the centred representative at y times the dz-transition Jacobian deriv(chart_y ∘ chart_a.symm)(chart_a y):

localRep ω₀ a y = deriv (chart_y ∘ chart_a.symm) (chart_a y) · localRep ω₀ y y.

This is the general cotangent-coefficient change-of-frame (cf. the ∞-case ProjectiveLine.inftyCoeff_eq_transition). It is the cancellation that reconciles the bundle per-sheet covector (read at the moving fibre point P's *own* chart) with the planar fibre trace coefficient (read in a *fixed* sheet chart): the localRep ratio is the inverse of the deriv ratio, so the dz-coefficient localRep·deriv(section) is frame-independent.

theorem localRep_eq_transition_mul_self (ω₀ : HolomorphicOneForms X) (a y : X)
    (hy : y ∈ (chartAt ℂ a).source) :
    Jacobians.Montel.localRep ω₀ a y
      = deriv (fun w => (chartAt ℂ y) ((chartAt ℂ a).symm w)) ((chartAt ℂ a) y)
        * Jacobians.Montel.localRep ω₀ y y