The chart-coefficient API for holomorphic 1-forms (CC1)

For a chart e and a 1-form η, RS.coeffIn e η : ℂ → ℂ is the coefficient function "η = (coeffIn e η) dz" in the chart: coeffIn e η z = η (e.symm z) (d(e.symm)_z 1), junk off e.target. RS.coeffAt x η is the coefficient in the preferred chart at the image of x.

Main results:

• RS.coeffAt_eq_apply_one, RS.Form1.apply_eq_smul_coeffAt — the canonical identification of the tangent fiber with ℂ in the preferred chart (all TangentSpace ≡ ℂ ≡ Bundle.Trivial defeq-crossings of this unit are concentrated here and in evalC).
• RS.Form1.ext_coeffAt — a form is determined by its preferred-chart coefficients.
• ℂ-linearity of coeffIn/coeffAt in the form (simp lemmas).
• RS.coeffIn_trans — the transition rule coeffIn e' η z = deriv (e ∘ e.symm') z * coeffIn e η (e (e'.symm z)) on chart overlaps, for charts in the ω-maximal atlas (CC1 orientation).
• RS.coeffIn_restr — restricting the chart does not change the coefficient (rfl).

All downstream units interact with 1-forms exclusively through this API.

noncomputable def RS.coeffInFun {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (e : OpenPartialHomeomorph X ℂ) (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) (z : ℂ) : ℂ

The coefficient function of a raw covector section in the chart e: for z ∈ e.target, coeffInFun e σ z = σ (e.symm z) (d(e.symm)_z 1). Junk (unspecified) off e.target.

Equations

• RS.coeffInFun e σ z = (σ (↑e.symm z)) ((mfderiv% ↑e.symm z) 1)

noncomputable def RS.coeffIn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (η : Form1 X) (z : ℂ) : ℂ

The coefficient function of a 1-form in the chart e: for z ∈ e.target, coeffIn e η z = η (e.symm z) (d(e.symm)_z 1), i.e. "η = (coeffIn e η) dz" in the chart. Junk (unspecified) off e.target.

Equations

• RS.coeffIn e η z = RS.coeffInFun e (⇑η) z

theorem RS.coeffIn_def {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (η : Form1 X) : coeffIn e η = coeffInFun e ⇑η

noncomputable def RS.coeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (η : Form1 X) : ℂ

Coefficient in the preferred chart, at the image of the base point.

Equations

• RS.coeffAt x η = RS.coeffIn (chartAt ℂ x) η (↑(chartAt ℂ x) x)

@[simp]

theorem RS.coeffIn_restr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (V : Set X) (η : Form1 X) : coeffIn (e.restr V) η = coeffIn e η

Restricting a chart does not change the coefficient function (the underlying chart maps are unchanged by restr).

@[simp]

theorem RS.coeffInFun_restr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (e : OpenPartialHomeomorph X ℂ) (V : Set X) (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) : coeffInFun (e.restr V) σ = coeffInFun e σ

Linearity in the form

@[simp]

theorem RS.coeffIn_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (η η' : Form1 X) (z : ℂ) : coeffIn e (η + η') z = coeffIn e η z + coeffIn e η' z

@[simp]

theorem RS.coeffIn_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (c : ℂ) (η : Form1 X) (z : ℂ) : coeffIn e (c • η) z = c * coeffIn e η z

@[simp]

theorem RS.coeffIn_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (z : ℂ) : coeffIn e 0 z = 0

@[simp]

theorem RS.coeffIn_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (η : Form1 X) (z : ℂ) : coeffIn e (-η) z = -coeffIn e η z

@[simp]

theorem RS.coeffIn_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (η η' : Form1 X) (z : ℂ) : coeffIn e (η - η') z = coeffIn e η z - coeffIn e η' z

@[simp]

theorem RS.coeffAt_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (η η' : Form1 X) : coeffAt x (η + η') = coeffAt x η + coeffAt x η'

@[simp]

theorem RS.coeffAt_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (c : ℂ) (η : Form1 X) : coeffAt x (c • η) = c * coeffAt x η

@[simp]

theorem RS.coeffAt_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) : coeffAt x 0 = 0

@[simp]

theorem RS.coeffAt_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (η : Form1 X) : coeffAt x (-η) = -coeffAt x η

@[simp]

theorem RS.coeffAt_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (η η' : Form1 X) : coeffAt x (η - η') = coeffAt x η - coeffAt x η'

The concentrated defeq layer

Every TangentSpace 𝓘(ℂ) q ≡ ℂ ≡ Bundle.Trivial X ℂ q crossing of this unit happens in the next few declarations, and nowhere else.

@[reducible, inline]

abbrev RS.tangentCoord {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {y : Y} (v : TangentSpace (modelWithCornersSelf ℂ ℂ) y) : ℂ

The canonical (definitional) identification of a tangent fiber of a ℂ-charted space with ℂ. TangentSpace is not reducible, so instance search does not see through it; this reducible wrapper lets scalar formulas (HMul etc.) elaborate.

Equations

• RS.tangentCoord v = v

noncomputable def RS.evalC {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) (q : X) (w : ℂ) : ℂ

Non-dependent evaluation of a raw covector section, through the definitional equality TangentSpace 𝓘(ℂ) q ≡ ℂ ≡ Bundle.Trivial X ℂ q. Point-congruences for the dependent evaluation are done through this function.

Equations

• RS.evalC σ q w = (σ q) w

theorem RS.coeffInFun_eq_evalC {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (e : OpenPartialHomeomorph X ℂ) (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) (z : ℂ) : coeffInFun e σ z = evalC σ (↑e.symm z) ((mfderiv% ↑e.symm z) 1)

theorem RS.evalC_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) (q : X) (c w : ℂ) : evalC σ q (c * w) = c * evalC σ q w

Scalars pull out of the non-dependent evaluation (the fiberwise CLM is ℂ-linear).

theorem RS.tangentCLM_apply_eq_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {w : ℂ} {q : X} (T : TangentSpace (modelWithCornersSelf ℂ ℂ) w →L[ℂ] TangentSpace (modelWithCornersSelf ℂ ℂ) q) (c : ℂ) : tangentCoord (T c) = c * tangentCoord (T 1)

A continuous linear map between a tangent fiber of the model ℂ and a tangent fiber of X (both definitionally ℂ) is multiplication by its value at 1.

theorem RS.mfderiv_chartAt_symm_chartAt_self {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) : mfderiv% ↑(chartAt ℂ x).symm (↑(chartAt ℂ x) x) = ContinuousLinearMap.id ℂ ℂ

The mfderiv of the inverse of the preferred chart, at the image of the base point, is the identity (canonical identification of the tangent fiber with ℂ).

theorem RS.coeffAt_eq_apply_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) (x : X) : coeffAt x η = (η x) 1

In the preferred chart, the coefficient at the base point is the evaluation at the canonical tangent vector 1.

theorem RS.Form1.apply_eq_smul_coeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) (x : X) (v : TangentSpace (modelWithCornersSelf ℂ ℂ) x) : (η x) v = tangentCoord v * coeffAt x η

Evaluation of a 1-form on a tangent vector, via the canonical identification: the fiber is one-dimensional and η x v = v * coeffAt x η.

theorem RS.evalC_eq_mul_coeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) (q : X) (w : ℂ) : evalC (⇑η) q w = w * coeffAt q η

The non-dependent-evaluation version of Form1.apply_eq_smul_coeffAt.

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

A holomorphic 1-form is determined by its preferred-chart coefficients.

theorem RS.Form1.ext_coeffAt_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η η' : Form1 X} : η = η' ↔ ∀ (x : X), coeffAt x η = coeffAt x η'

The transition rule

theorem RS.differentiableAt_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hzt : z ∈ e'.target) (hzs : ↑e'.symm z ∈ e.source) : DifferentiableAt ℂ (↑e ∘ ↑e'.symm) z

The transition map between two charts, as read in the maximal atlas, is C^ω (hence differentiable) at every point of the image of the overlap.

theorem RS.coeffIn_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (η : Form1 X) {z : ℂ} (hz : z ∈ ↑e' '' (e.source ∩ e'.source)) : coeffIn e' η z = deriv (↑e ∘ ↑e'.symm) z * coeffIn e η (↑e (↑e'.symm z))

Transition rule for chart coefficients (CC1 orientation): on the image of a chart overlap, coeffIn e' η z = deriv (e ∘ e'.symm) z * coeffIn e η (e (e'.symm z)).