`Form1.pullback` — the easy direction (jacobian-functoriality §3) #

Unit: jacobian-functoriality. Pullback of a holomorphic 1-form along any holomorphic f : X → Y (chain rule via mfderiv, no branch-point subtlety).

Main declarations:

RS.Form1.pullback f hf : Form1 Y →ₗ[ℂ] Form1 X.
RS.coeffAt_pullback — the preferred-chart coefficient formula.
RS.coeffIn_pullback — the any-maximal-atlas-chart coefficient formula.
RS.Form1.pullback_id, RS.Form1.pullback_comp — functoriality at the Form1 level.

`Compat` (to be filed upstream, `docs/requests/holomorphic-forms.md`) #

RS.analyticAt_of_mem_maximalAtlas — reading a ContMDiffAt f x map through arbitrary maximal-atlas charts on source and target is analytic (mathlib's own contMDiffWithinAt_iff_of_mem_maximalAtlas specialized to 𝓘(ℂ)/ω, generalizing RS.contMDiffAt_iff_analyticAt_of_mem_source from a ℂ-valued target to an arbitrary charted target).
RS.mfderiv_chartAt_self — the (forward) chart map's own mfderiv at its base point is the identity (the symmetric counterpart of RS.mfderiv_chartAt_symm_chartAt_self).
RS.tangentCoord_mfderiv_chart_comp — two-manifold generalization of RS.tangentCoord_mfderiv_comp, reading the target through its own preferred chart.

`Compat`: two-manifold chart bridges (requested upstream, proved locally) #

source

theorem RS.analyticAt_of_mem_maximalAtlas {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx : x ∈ e.source) {e' : OpenPartialHomeomorph Y ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) (hy : f x ∈ e'.source) :

AnalyticAt ℂ (↑e' ∘ f ∘ ↑e.symm) (↑e x)

Reading a ContMDiffAt map through arbitrary maximal-atlas charts on both source and target is analytic. Generalizes RS.contMDiffAt_iff_analyticAt_of_mem_source (f : X → ℂ) to an arbitrary charted target Y.

source

theorem RS.mfderiv_chartAt_self {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (y : Y) :

mfderiv% ↑(chartAt ℂ y) y = ContinuousLinearMap.id ℂ ℂ

The (forward) preferred chart's own mfderiv at its base point is the identity — the symmetric counterpart of RS.mfderiv_chartAt_symm_chartAt_self.

source

theorem RS.tangentCoord_mfderiv_chart_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {g : ℂ → X} {z : ℂ} (hF : MDiffAt F (g z)) (hg : MDiffAt g z) :

tangentCoord ((mfderiv% F (g z)) ((mfderiv% g z) 1)) = deriv (↑(chartAt ℂ (F (g z))) ∘ F ∘ g) z

Two-manifold generalization of RS.tangentCoord_mfderiv_comp: the composite mfderiv, read in the target's own preferred chart, is the planar derivative of the chart-composite.

`pullbackSection` and its coefficient formula #

source

noncomputable def RS.pullbackSection {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (f : X → Y) (η : Form1 Y) (x : X) :

TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ ] Bundle.Trivial X ℂ x

The pulled-back covector at x: precompose η's covector at f x with the differential of f at x (crossing the TangentSpace ↦ Bundle.Trivial defeq in the codomain, as in Form1CoeffData.toSection/mdifferentialSection).

Equations

RS.pullbackSection f η x = η (f x) ∘SL mfderiv% f x

Instances For

source

theorem RS.coeffInFun_pullbackSection {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 Y) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {e' : OpenPartialHomeomorph Y ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) {z : ℂ} (hz : z ∈ e.target) (hy : f (↑e.symm z) ∈ e'.source) :

coeffInFun e (pullbackSection f η) z = deriv (↑e' ∘ f ∘ ↑e.symm) z * coeffIn e' η (↑e' (f (↑e.symm z)))

Master computation (mirrors Form1CoeffData.coeffInFun_toSection): in any maximal-atlas source chart e and target chart e' (with f mapping the relevant point into e'.source), the raw coefficient of pullbackSection f η is the chain-rule pullback formula.

`Form1.pullback` #

source

noncomputable def RS.pullbackForm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 Y) :

Form1 X

Pullback of η along f, as a raw Form1 X (before packaging as a linear map).

Equations

RS.pullbackForm f hf η = RS.Form1.ofSectionAnalytic (RS.pullbackSection f η) ⋯

Instances For

source

theorem RS.coeffIn_pullbackForm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 Y) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {e' : OpenPartialHomeomorph Y ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) {z : ℂ} (hz : z ∈ e.target) (hy : f (↑e.symm z) ∈ e'.source) :

coeffIn e (pullbackForm f hf η) z = deriv (↑e' ∘ f ∘ ↑e.symm) z * coeffIn e' η (↑e' (f (↑e.symm z)))

source

theorem RS.coeffAt_pullbackForm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 Y) (x : X) :

coeffAt x (pullbackForm f hf η) = deriv (↑(chartAt ℂ (f x)) ∘ f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x) * coeffAt (f x) η

The preferred-chart coefficient formula (§3.1).

source

noncomputable def RS.Form1.pullback {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) :

Form1 Y →ₗ[ℂ ] Form1 X

Form1.pullback (§3.1): pullback of a holomorphic 1-form along any holomorphic f : X → Y, as a ℂ-linear map Form1 Y →ₗ[ℂ] Form1 X. Automatically 0 for constant f (no case split: a constant map has vanishing mfderiv, so pullbackSection vanishes identically).