Functoriality laws and the projection formula for Form1.trace (jacobian-functoriality §6.5, §9)

Unit: jacobian-functoriality. The Form1-level laws feeding the Jacobian-level pullback functoriality and pushforward_pullback:

• RS.Form1.trace_id — Tr_id = id.
• RS.Form1.trace_comp — Tr_{g∘f} = Tr_g ∘ Tr_f (via the doubly-regular density argument).
• RS.Form1.trace_pullback — the projection formula Tr_f (f^* η) = (deg f) • η.

All three are proved at regular values via RS.coeffAt_traceForm_of_isRegularValue and extended everywhere by RS.Form1.eq_of_eqOn_dense (density of regular values).

Nonvanishing of the chart-read derivative at unramified points

theorem RS.deriv_chartRead_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} {k : ℕ} (A : AdaptedChartsAt f x k) (hk : k = 1) {e₀ : OpenPartialHomeomorph Y ℂ} (he₀ : e₀ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) (hfx : f x ∈ e₀.source) : deriv (↑e₀ ∘ f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x) ≠ 0

At a point where f reads as z ↦ z^1 in adapted charts, the chart-read derivative of f does not vanish.

theorem RS.not_exists_const_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] : ¬∃ (c : X), ∀ (x : X), id x = c

X (a positive-dimensional charted space) carries no constant identity: id is nonconstant.

trace_id

theorem RS.Form1.trace_id {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : trace id ⋯ = LinearMap.id

trace_comp

theorem RS.qCoeff_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {Z : Type u_3} [TopologicalSpace Z] [ChartedSpace ℂ Z] {f : X → Y} {g : Y → Z} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) {e₂ : OpenPartialHomeomorph Z ℂ} (he₂ : e₂ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Z) {x : X} (hgfx : g (f x) ∈ e₂.source) (η : Form1 X) : qCoeff (g ∘ f) η e₂ x = (deriv (↑e₂ ∘ g ∘ ↑(chartAt ℂ (f x)).symm) (↑(chartAt ℂ (f x)) (f x)))⁻¹ * qCoeff f η (chartAt ℂ (f x)) x

Chain rule for qCoeff: the canonical coefficient of a composite splits through the preferred chart at the intermediate point. Unconditional (junk-inverse compatible).

theorem RS.Form1.trace_comp {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] [CompactSpace Y] [ConnectedSpace Y] {Z : Type u_3} [TopologicalSpace Z] [T2Space Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) : trace (g ∘ f) ⋯ = trace g hg ∘ₗ trace f hf

trace_comp: the trace is functorial, Tr_{g∘f} = Tr_g ∘ Tr_f.

The projection formula

theorem RS.qCoeff_pullback {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) {yhat : Y} (hyhat : IsRegularValue f yhat) {x : X} (hx : f x = yhat) (η : Form1 Y) : qCoeff f ((Form1.pullback f hf) η) (chartAt ℂ yhat) x = coeffAt yhat η

Per-point cancellation: the canonical trace coefficient of a pulled-back form at an unramified fibre point is the coefficient of the original form.

theorem RS.traceForm_pullback {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] [ConnectedSpace Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 Y) : traceForm hf hne ((Form1.pullback f hf) η) = ↑(degree f) • η

The projection formula (raw form): Tr_f (f^* η) = (deg f) • η.

theorem RS.Form1.trace_pullback {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] [ConnectedSpace Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 Y) : (trace f hf) ((pullback f hf) η) = ↑(ContMDiff.degree f hf) • η

The projection formula (challenge form): Form1.trace f hf ∘ Form1.pullback f hf is multiplication by the challenge degree ContMDiff.degree f hf — including the constant case (both sides vanish).