Logarithmic derivatives commute with restriction to the hypersurface

Kollár's (87.1) [Kol07, 87]: the derivative in the direction normal to S does not restrict to S, but the logarithmic derivatives do, "(D^r(−log S)(I))|_S = D^r(I|_S)".

The content is the descent of the tangential coordinate derivations along the restriction of germs ρ : 𝒪_{M,x} → 𝒪_{S,x} (the stalk map of the inclusion S ↪ M): in a chart φ adapted to S with S = (x_h = 0), the hypersurface carries the induced chart φ_S = projCompl ∘ ψ ∘ φ (IsAdaptedChart.chartOn, the coordinates other than x_h), whose inverse is φ⁻¹ ∘ ψ⁻¹ ∘ embedCompl — the adapted chart's inverse after a continuous linear embedding. The chain rule therefore identifies the j-th partial derivative of f|_S in φ_S with the restriction of the partial derivative of f in the direction of the j-th complementary coordinate (comapSection_coordDeriv_inclusionMap, then at the germ level germMap_inclusionMap_coordDerivStalk). Hence, since ρ(x_h) = 0 kills the x_h ∂_h generators and the ∂_j (j ≠ h) descend to the coordinate derivations of S, the image of D(−log S)(I)_x = ⟨I, x_h ∂_h I, ∂_j I⟩ under ρ is D(ρ I) (map_germMap_logDerivative_eq_derivative), and (87.1) follows by induction on r (logDerivIter_pullback_inclusionMap). This is the step by which order reduction on the hypersurface of maximal contact controls the logarithmic derivatives on the ambient manifold (Hironaka/Manifold/BlowUp/Transform/LogDerivTransform.lean).

The complementary embedding as a continuous linear map

noncomputable def Manifold.embedComplₗ {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : (Fin (n - c) → 𝕜) →ₗ[𝕜] Fin n → 𝕜

embedCompl σ is 𝕜-linear.

Equations

• Manifold.embedComplₗ σ = { toFun := Manifold.embedCompl σ, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Manifold.embedComplL {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : (Fin (n - c) → 𝕜) →L[𝕜] Fin n → 𝕜

embedCompl σ as a continuous linear map.

Equations

• Manifold.embedComplL σ = LinearMap.toContinuousLinearMap (Manifold.embedComplₗ σ)

@[simp]

theorem Manifold.embedComplL_apply {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (w : Fin (n - c) → 𝕜) : (embedComplL σ) w = embedCompl σ w

theorem Manifold.embedCompl_single {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (j : Fin (n - c)) : embedCompl σ (Pi.single j 1) = Pi.single (↑((complEquiv σ).symm j)) 1

embedCompl σ sends the j-th basis vector of 𝕜^{n−c} to the basis vector of 𝕜^n at the j-th complementary index.

The descent of the tangential coordinate derivations

Conventions: the point of S is p : hS.toAnalyticManifold; its image in M is written hS.inclusionMap p throughout (the chart lemmas of closed submanifolds are instantiated at that point through their implicit argument, so that rewriting matches syntactically), and the ambient adapted chart at p is taken at hS.subOf p, the same point read in the subtype ↥S — the carrier of the bundled manifold unfolds to ↥S only definitionally, and rw's motive check needs the syntactic type.

def Manifold.IsClosedSubmanifold.subOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) : ↑S

The point p of the bundled hypersurface read in the subtype ↥S (an identity cast).

Equations

• hS.subOf p = p

theorem Manifold.IsClosedSubmanifold.inclusionMap_eq_val_subOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) : hS.inclusionMap p = ↑(hS.subOf p)

theorem Manifold.chartAt_toAnalyticManifold_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) : chartAt (Fin (n - 1) → 𝕜) p = ⋯.chartOn ⋯

The chart of the bundled hypersurface at p is the chart induced by the adapted chart at p (IsClosedSubmanifold.chartedSpace, definitionally).

@[reducible, inline]

noncomputable abbrev Manifold.complIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) (j : Fin (n - 1)) : Fin n

The complementary index of the j-th coordinate of the induced chart at p.

Equations

• Manifold.complIdx hS p j = ↑((Manifold.complEquiv (hS.adaptedIdx (hS.subOf p))).symm j)

theorem Manifold.complIdx_notMem_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) (j : Fin (n - 1)) : complIdx hS p j ∉ Set.range ⇑(hS.adaptedIdx (hS.subOf p))

theorem Manifold.inclusionMap_mem_source_adaptedChartAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) : hS.inclusionMap p ∈ (hS.adaptedChartAt (hS.subOf p)).source

The image of p in M lies in the source of the adapted chart at p.

theorem Manifold.inclusionMap_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (q : hS.toAnalyticManifold.carrier) : hS.inclusionMap q ∈ S

theorem Manifold.comapSection_coordDeriv_inclusionMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ (hS.adaptedChartAt (hS.subOf p)).source) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) (j : Fin (n - 1)) : comapSection ⇑hS.inclusionMap ⋯ ((coordDeriv E ψ (hS.adaptedChartAt (hS.subOf p)) ⋯ V hV (complIdx hS p j)) f) = (coordDeriv (Fin (n - 1) → 𝕜) (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (chartAt (Fin (n - 1) → 𝕜) p) ⋯ (preimageOpens ⇑hS.inclusionMap ⋯ V) ⋯ j) (comapSection ⇑hS.inclusionMap ⋯ f)

Kollár's "∂f/∂x_i |_S = ∂(f|_S)/∂x_i for i > 1" [Kol07, 87], at the level of sections: for f on an open V inside the adapted chart at p, the j-th partial derivative of f|_S in the induced chart is the restriction of the partial derivative of f in the direction of the j-th complementary coordinate.

theorem Manifold.germMap_inclusionMap_coordDerivStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) (j : Fin (n - 1)) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk (hS.inclusionMap p))) : (germMap ⇑hS.inclusionMap ⋯ p) ((coordDerivStalk E ψ (hS.adaptedChartAt (hS.subOf p)) ⋯ ⋯ (complIdx hS p j)) s) = (coordDerivStalk (Fin (n - 1) → 𝕜) (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (chartAt (Fin (n - 1) → 𝕜) p) ⋯ ⋯ j) ((germMap ⇑hS.inclusionMap ⋯ p) s)

Kollár's "∂f/∂x_i |_S = ∂(f|_S)/∂x_i" [Kol07, 87] at the germ level: the restriction of germs carries the tangential coordinate derivation ∂_{complIdx j} of the adapted chart at p to the j-th coordinate derivation of the induced chart of S.

ρ(D(−log S)(I)) = D(ρ I) and (87.1)

theorem Manifold.stalkIdeal_idealSheaf_inclusionMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) : hS.idealSheaf.stalkIdeal (hS.inclusionMap p) = Ideal.span {coord E ψ (hS.adaptedChartAt (hS.subOf p)) ⋯ ⋯ ((hS.adaptedIdx (hS.subOf p)) 0)}

The stalk of the ideal sheaf of S at p, in the adapted chart at p: (x_h).

theorem Manifold.germMap_inclusionMap_coord_adaptedIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) : (germMap ⇑hS.inclusionMap ⋯ p) (coord E ψ (hS.adaptedChartAt (hS.subOf p)) ⋯ ⋯ ((hS.adaptedIdx (hS.subOf p)) 0)) = 0

The equation x_h of S in the adapted chart at p restricts to 0.

theorem Manifold.map_germMap_logDerivative_eq_derivative {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (p : hS.toAnalyticManifold.carrier) (I : Ideal ↑((structureSheaf 𝕜 E M).presheaf.stalk (hS.inclusionMap p))) : Ideal.map (germMap ⇑hS.inclusionMap ⋯ p) (Ideal.logDerivative 𝕜 (hS.idealSheaf.stalkIdeal (hS.inclusionMap p)) I) = Ideal.derivative 𝕜 (Ideal.map (germMap ⇑hS.inclusionMap ⋯ p) I)

Kollár's (87.1) at a stalk [Kol07, 87]: for x ∈ S and an ideal I of 𝒪_{M,x}, the image under the restriction of germs of D(−log S)(I) is the derivative of the image of I: x_h ∂_h dies (ρ x_h = 0) and the ∂_j, j ≠ h, descend to the coordinate derivations of S.

theorem Manifold.logDerivIter_pullback_inclusionMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (r : ℕ) (J : IdealSheaf (structureSheaf 𝕜 E M)) : IdealSheaf.pullback ⇑hS.inclusionMap ⋯ (IdealSheaf.logDerivIter E ψ hS r J) = (IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J).iteratedDeriv r

Kollár's (87.1) [Kol07, 87]: on the bundled hypersurface, the restriction of D^r(−log S)(J) along S ↪ M is the r-th derivative of the restriction of J. Induction on r through the stalk identity ρ(D(−log S)(I)) = D(ρ I).