The chart logarithmic derivative ideal under a ring map carrying the transformed derivations

The logarithmic counterpart of Hironaka/Algebra/Local/TransformDerivMap.lean, for [Kol07, (87.3)] ("proved the same way using (75.4)"): the chart logarithmic derivative ideal chartDlog r h K = K + y_h ∂'_h K + ∑_{j ≠ h} ∂'_j K of Hironaka/Algebra/Local/TransformLogDeriv.lean maps, under a ring homomorphism χ carrying the transported derivations ∂'ⱼ to derivations δ j of the target, into the logarithmic derivative ideal D(−log (χ y_h))(χ K) of the target (Ideal.logDerivative, Hironaka/Scheme/IdealSheaf/Derivative/Logarithmic.lean), provided the δ j, j ≠ h, preserve the ideal (χ y_h) (map_chartDlog_le_logDerivative); the derivation χ(y_h) • δ h always preserves (χ y_h). On a manifold the δ j are the partial derivatives of a blow-up chart and χ y_h is one of its coordinates, killed by the other partials. Iterating gives the statement for chartDlogpow (map_chartDlogpow_le_logDerivativeIter).

Also here, a converse of map_chartD_le_derivative: if every k-derivation of the target is, pointwise, a combination of the δ j, then D(χ K) ⊆ χ(D' K) (derivative_map_le_map_chartD_of_span) and D^s(χ K) ⊆ χ(D'^s K) (derivativeIter_map_le_map_iterate_chartD_of_span); this is how the chart-level inclusion ⊆ of [Kol07, (88.1)] (Hironaka/Algebra/Local/TransformDerivNormalForm.lean) is read on the stalks of a blow-up of a manifold.

Used in Hironaka/Manifold/BlowUp/Transform/LogDerivBlowUp.lean.

theorem IsLocalRing.RegularCoords.map_chartDlog_le_logDerivative {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {S : Type u_3} [CommRing S] [Algebra k S] (χ : ↥(chartRing c.x r) →+* S) (δ : Fin n → Derivation k S S) (hδ : ∀ (j : Fin n) (g : ↥(chartRing c.x r)), χ ((c.chartDerivRing r j) g) = (δ j) (χ g)) (h : Fin n) (hpres : ∀ (j : Fin n), j ≠ h → (δ j).PreservesIdeal (Ideal.span {χ (chartYR c.x r h)})) (K : Ideal ↥(chartRing c.x r)) : Ideal.map χ (c.chartDlog r h K) ≤ Ideal.logDerivative k (Ideal.span {χ (chartYR c.x r h)}) (Ideal.map χ K)

The logarithmic counterpart of map_chartD_le_derivative ([Kol07, (87.3)] at the chart level): if χ carries the transported derivations ∂'_j to derivations δ j of S, and the δ j for j ≠ h preserve the ideal (χ y_h), then χ(D'(−log y_h)(K)) ⊆ D(−log (χ y_h))(χ K).

theorem IsLocalRing.RegularCoords.map_chartDlogpow_le_logDerivativeIter {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {S : Type u_3} [CommRing S] [Algebra k S] (χ : ↥(chartRing c.x r) →+* S) (δ : Fin n → Derivation k S S) (hδ : ∀ (j : Fin n) (g : ↥(chartRing c.x r)), χ ((c.chartDerivRing r j) g) = (δ j) (χ g)) (h : Fin n) (hpres : ∀ (j : Fin n), j ≠ h → (δ j).PreservesIdeal (Ideal.span {χ (chartYR c.x r h)})) (j : ℕ) (K : Ideal ↥(chartRing c.x r)) : Ideal.map χ (c.chartDlogpow r h j K) ≤ Ideal.logDerivativeIter k (Ideal.span {χ (chartYR c.x r h)}) j (Ideal.map χ K)

The iterated form: χ(D'^j(−log y_h)(K)) ⊆ D^j(−log (χ y_h))(χ K).

A converse of map_chartD_le_derivative under a spanning hypothesis

theorem IsLocalRing.RegularCoords.derivative_map_le_map_chartD_of_span {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {S : Type u_3} [CommRing S] [Algebra k S] (χ : ↥(chartRing c.x r) →+* S) (δ : Fin n → Derivation k S S) (hδ : ∀ (j : Fin n) (g : ↥(chartRing c.x r)), χ ((c.chartDerivRing r j) g) = (δ j) (χ g)) (hspan : ∀ (D : Derivation k S S) (f : S), ∃ (a : Fin n → S), D f = ∑ j : Fin n, a j * (δ j) f) (K : Ideal ↥(chartRing c.x r)) : Ideal.derivative k (Ideal.map χ K) ≤ Ideal.map χ (c.chartD r K)

A converse of map_chartD_le_derivative, used to read the inclusion ⊆ of [Kol07, (88.1)] in the chart: if χ carries the transported derivations ∂'_j to derivations δ j of S and every k-derivation of S is, pointwise, an S-combination of the δ j (as the partial derivatives of a chart of a manifold are), then D(χ K) ⊆ χ(D' K).

theorem IsLocalRing.RegularCoords.derivativeIter_map_le_map_iterate_chartD_of_span {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {S : Type u_3} [CommRing S] [Algebra k S] (χ : ↥(chartRing c.x r) →+* S) (δ : Fin n → Derivation k S S) (hδ : ∀ (j : Fin n) (g : ↥(chartRing c.x r)), χ ((c.chartDerivRing r j) g) = (δ j) (χ g)) (hspan : ∀ (D : Derivation k S S) (f : S), ∃ (a : Fin n → S), D f = ∑ j : Fin n, a j * (δ j) f) (s : ℕ) (K : Ideal ↥(chartRing c.x r)) : Ideal.derivativeIter k s (Ideal.map χ K) ≤ Ideal.map χ ((c.chartD r)^[s] K)

The iterated form of derivative_map_le_map_chartD_of_span: D^s(χ K) ⊆ χ(D'^s K).