The Jacobian ideal and the monoidal transformations along a square across the models

The chart-level notions of the vocabulary — adapted charts and closed submanifolds, the ideal sheaf of a submanifold, blow-up charts, blowings-up and monoidal transformations ([BM88, Definition 4.1]), the Jacobian ideal ([BM97, Theorem 1.10, the sentence after it]) — transport along a square f ∘ g' = g ∘ f' of analytic isomorphisms g : N ≃ M, g' : N' ≃ M' across the models (IsModelSquare). The device is one chart: chartOfSquare g ψ φ := ψ ∘ φ ∘ g, a chart of N read from a chart φ of M through g and a linear isomorphism ψ : E ≃L[𝕜] E' of the models. It is in the maximal atlas of N (mem_maximalAtlas_of_contMDiffOn), its source is g⁻¹(φ.source), and reading a chart of N through g⁻¹, ψ⁻¹ and back gives the chart (chartOfSquare_chartOfSquare_symm).

• The predicates carry a chart isomorphism ψ₀ : E ≃L[𝕜] (Fin n → 𝕜); on N it becomes ψ.symm.trans ψ₀. An adapted chart of M reads as an adapted chart of N and back (IsAdaptedChart.of_square, of_square_symm), a closed submanifold Y pulls back to g⁻¹(Y), the ideal sheaf of Y pulls back to the ideal sheaf of g⁻¹(Y) — the coordinate germs correspond under the stalk isomorphism of g (stalkRingEquiv_coord), whatever the witnesses of the two submanifolds (IsClosedSubmanifold.idealSheaf_pullbackDiffeomorph) — and a blow-up chart of f over ψ⁻¹ ∘ φ' ∘ g⁻¹ reads as a blow-up chart of f' over φ' (IsBlowUpChart.of_square), so a blowing-up transports (IsBlowUp.of_square) and with it a monoidal transformation (AnalyticMap.IsMonoidalTransformation.of_square).
• The Jacobian: in the charts read from those of f, the chart representative of f' is the conjugate ψ ∘ (φ ∘ f ∘ φ'⁻¹) ∘ ψ⁻¹ of the representative of f, so the Jacobian determinants are equal (LinearMap.det_conj, det_clm_conj) — no unit germs enter — and the Jacobian stalk transports along the stalk isomorphism of g' (jacobianStalk_of_square), whence the Jacobian ideal (AnalyticMap.jacobianIdeal_of_square). This needs no model isomorphism: at a point b of N' the inverse differential of g' (Diffeomorph.mfderivToContinuousLinearEquiv) serves as ψ.
• The monoidal transformation takes the model isomorphism ψ: the chart isomorphism of N is ψ.symm.trans ψ₀, and without some E ≃L[𝕜] E' the statement fails when N and N' are empty and E' is not linearly isomorphic to Fin n → 𝕜.

These are the steps by which the successions of the resolution are carried between the models (Hironaka/Resolution/Analytic/ModelTransport/Succession.lean).

The chart of N read from a chart of M

def Hironaka.Manifold.chartOfSquare {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (φ : OpenPartialHomeomorph M.carrier E) : OpenPartialHomeomorph N.carrier E'

The chart of N read from a chart φ of M through the analytic isomorphism g : N ≃ M and the linear isomorphism ψ of the models, ψ ∘ φ ∘ g.

Equations

• Hironaka.Manifold.chartOfSquare g ψ φ = (g.toHomeomorph.toOpenPartialHomeomorph.trans φ).trans ψ.toHomeomorph.toOpenPartialHomeomorph

theorem Hironaka.Manifold.chartOfSquare_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (φ : OpenPartialHomeomorph M.carrier E) (x : N.carrier) : ↑(chartOfSquare g ψ φ) x = ψ (↑φ (g x))

chartOfSquare g ψ φ x = ψ (φ (g x)).

theorem Hironaka.Manifold.chartOfSquare_symm_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (φ : OpenPartialHomeomorph M.carrier E) (v : E') : ↑(chartOfSquare g ψ φ).symm v = g.symm (↑φ.symm (ψ.symm v))

The inverse of the read chart is g⁻¹ ∘ φ⁻¹ ∘ ψ⁻¹.

theorem Hironaka.Manifold.coe_chartOfSquare {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (φ : OpenPartialHomeomorph M.carrier E) : ↑(chartOfSquare g ψ φ) = fun (x : N.carrier) => ψ (↑φ (g x))

The read chart as a function.

theorem Hironaka.Manifold.coe_chartOfSquare_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (φ : OpenPartialHomeomorph M.carrier E) : ↑(chartOfSquare g ψ φ).symm = fun (v : E') => g.symm (↑φ.symm (ψ.symm v))

The inverse of the read chart as a function.

theorem Hironaka.Manifold.chartOfSquare_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (φ : OpenPartialHomeomorph M.carrier E) : (chartOfSquare g ψ φ).source = ⇑g ⁻¹' φ.source

The source of the read chart is g⁻¹(φ.source).

theorem Hironaka.Manifold.chartOfSquare_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (φ : OpenPartialHomeomorph M.carrier E) : (chartOfSquare g ψ φ).target = ⇑ψ.symm ⁻¹' φ.target

The target of the read chart is ψ(φ.target), as a preimage under ψ⁻¹.

theorem Hironaka.Manifold.chartOfSquare_mem_maximalAtlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {φ : OpenPartialHomeomorph M.carrier E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) : chartOfSquare g ψ φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E') ⊤ N.carrier

A chart of the maximal atlas of M reads as a chart of the maximal atlas of N (mem_maximalAtlas_of_contMDiffOn: ψ ∘ φ ∘ g and its inverse are analytic on the source and the target).

Adapted charts, closed submanifolds, the ideal sheaf of a submanifold

theorem Manifold.IsAdaptedChart.congr_cle {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {φ : OpenPartialHomeomorph M.carrier E} {n : ℕ} {ψ₁ ψ₂ : E ≃L[𝕜] Fin n → 𝕜} (h : ∀ (v : E), ψ₁ v = ψ₂ v) {Y : Set M.carrier} {c : ℕ} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ₁ Y φ σ) : IsAdaptedChart ψ₂ Y φ σ

The adapted-chart predicate depends on the chart isomorphism only pointwise.

theorem Manifold.IsAdaptedChart.of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {φ : OpenPartialHomeomorph M.carrier E} {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {Y : Set M.carrier} {c : ℕ} {σ : Fin c ↪ Fin n} (h : IsAdaptedChart ψ₀ Y φ σ) : IsAdaptedChart (ψ.symm.trans ψ₀) (⇑g ⁻¹' Y) (Hironaka.Manifold.chartOfSquare g ψ φ) σ

An adapted chart of M for Y reads as an adapted chart of N for g⁻¹(Y), with the chart isomorphism ψ.symm.trans ψ₀.

theorem Manifold.IsClosedSubmanifold.preimage_of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) : IsClosedSubmanifold (ψ.symm.trans ψ₀) (⇑g ⁻¹' Y) c

A closed submanifold of M pulls back along g to a closed submanifold of N of the same codimension.

theorem Manifold.IsAdaptedChart.of_square_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {Y : Set M.carrier} {c : ℕ} {σ : Fin c ↪ Fin n} {φ' : OpenPartialHomeomorph N.carrier E'} (h : IsAdaptedChart (ψ.symm.trans ψ₀) (⇑g ⁻¹' Y) φ' σ) : IsAdaptedChart ψ₀ Y (Hironaka.Manifold.chartOfSquare g.symm ψ.symm φ') σ

The adapted chart of M read from an adapted chart of N (the converse direction, through g⁻¹ and ψ⁻¹).

theorem Hironaka.Manifold.stalkRingEquiv_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {φ : OpenPartialHomeomorph M.carrier E} {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {a : N.carrier} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) (ha : g a ∈ φ.source) (i : Fin n) : (g.stalkRingEquiv a) (Manifold.coord E ψ₀ φ hφ ha i) = Manifold.coord E' (ψ.symm.trans ψ₀) (chartOfSquare g ψ φ) ⋯ ⋯ i

The coordinate germs along g: the stalk isomorphism of g carries the i-th coordinate germ of φ to the i-th coordinate germ of ψ ∘ φ ∘ g.

theorem Hironaka.Manifold.coord_congr_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {φ₁ φ₂ : OpenPartialHomeomorph M.carrier E} (h : φ₁ = φ₂) (hφ₁ : φ₁ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) {a : M.carrier} (ha₁ : a ∈ φ₁.source) (i : Fin n) : Manifold.coord E ψ₀ φ₁ hφ₁ ha₁ i = Manifold.coord E ψ₀ φ₂ ⋯ ⋯ i

The coordinate germs of equal charts agree.

theorem Hironaka.Manifold.chartOfSquare_chartOfSquare_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (φ' : OpenPartialHomeomorph N.carrier E') : chartOfSquare g ψ (chartOfSquare g.symm ψ.symm φ') = φ'

Reading a chart of N through g⁻¹, ψ⁻¹ and back through g, ψ gives the chart.

theorem Manifold.IsIdealSheafOf.pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {Y : Set M.carrier} {c : ℕ} {D : M.IdealSheaf} (hD : IsIdealSheafOf ψ₀ Y c D) : IsIdealSheafOf (ψ.symm.trans ψ₀) (⇑g ⁻¹' Y) c (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g D)

The ideal sheaf of a closed submanifold Y pulls back along g to the ideal sheaf of g⁻¹(Y): the cosupport by cosupport_pullback, the stalks at the points of g⁻¹(Y) because the coordinate germs of the adapted charts correspond (stalkRingEquiv_coord), each adapted chart of N being the reading of an adapted chart of M.

theorem Manifold.IsClosedSubmanifold.idealSheaf_pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {n' c c' : ℕ} {ψ₁ : E' ≃L[𝕜] Fin n' → 𝕜} {Y : Set M.carrier} {Y' : Set N.carrier} (hY : IsClosedSubmanifold ψ₀ Y c) (hY' : IsClosedSubmanifold ψ₁ Y' c') (e : Y' = ⇑g ⁻¹' Y) : AnalyticManifold.IdealSheaf.pullbackDiffeomorph g hY.idealSheaf = hY'.idealSheaf

The ideal sheaf of a closed submanifold Y of M pulls back along g to the ideal sheaf of g⁻¹(Y), whatever witnesses of IsClosedSubmanifold the two carry: the pull-back is an ideal sheaf of g⁻¹(Y) (IsIdealSheafOf.pullbackDiffeomorph), which is unique (IsIdealSheafOf.eq_idealSheaf) and depends only on the set (IsClosedSubmanifold.idealSheaf_congr).

Blow-up charts, blowings-up, monoidal transformations along a square

theorem Manifold.IsBlowUpChart.of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M' : AnalyticManifold 𝕜 E} {N' : AnalyticManifold 𝕜 E'} (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (f : AnalyticMap M' M) (f' : AnalyticMap N' N) (hsq : Hironaka.Manifold.IsModelSquare g g' f f') {c : ℕ} {σ : Fin c ↪ Fin n} {i : Fin c} {φ' : OpenPartialHomeomorph N.carrier E'} {Φ : OpenPartialHomeomorph M'.carrier E} (hΦ : IsBlowUpChart ψ₀ (⇑f) (Hironaka.Manifold.chartOfSquare g.symm ψ.symm φ') σ i Φ) : IsBlowUpChart (ψ.symm.trans ψ₀) (⇑f') φ' σ i (Hironaka.Manifold.chartOfSquare g' ψ Φ)

A blow-up chart of f over the chart of M read from φ' is, read on N' through g' and ψ, a blow-up chart of f' over φ': the four fields through the square.

theorem Manifold.IsBlowUp.of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M' : AnalyticManifold 𝕜 E} {N' : AnalyticManifold 𝕜 E'} (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (f : AnalyticMap M' M) (f' : AnalyticMap N' N) (hsq : Hironaka.Manifold.IsModelSquare g g' f f') {Y : Set M.carrier} {c : ℕ} (hB : IsBlowUp ψ₀ Y c ⇑f) : IsBlowUp (ψ.symm.trans ψ₀) (⇑g ⁻¹' Y) c ⇑f'

A blowing-up [BM88, Definition 4.1] along a square: analyticity, properness (isProperMap_of_square_iff), the local-isomorphism and bijection clauses off the centre, and the blow-up charts by IsBlowUpChart.of_square, each chart of N being the reading of a chart of M.

theorem AnalyticMap.IsMonoidalTransformation.of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {M' : AnalyticManifold 𝕜 E} {N' : AnalyticManifold 𝕜 E'} (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (f : AnalyticMap M' M) (f' : AnalyticMap N' N) (hsq : Hironaka.Manifold.IsModelSquare g g' f f') {D : M.IdealSheaf} (h : f.IsMonoidalTransformation D) : f'.IsMonoidalTransformation (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g D)

A monoidal transformation along a square of analytic isomorphisms across the models, with the model isomorphism ψ, which names the chart isomorphism of N as ψ.symm.trans ψ₀ (without some E ≃L[𝕜] E' the statement fails when N and N' are empty and E' is not linearly isomorphic to Fin n → 𝕜). The centre Y pulls back to g⁻¹(Y), its ideal sheaf to the pull-back of the ideal sheaf, the blowing-up transports by IsBlowUp.of_square.

The Jacobian ideal along a square

theorem Hironaka.Manifold.det_clm_conj {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (ψ : E ≃L[𝕜] E') (A : E →L[𝕜] E) : (↑ψ ∘SL A ∘SL ↑ψ.symm).det = A.det

The determinant of the conjugate ψ ∘ A ∘ ψ⁻¹ of an endomorphism A of E by the linear isomorphism ψ : E ≃L[𝕜] E' is the determinant of A (Mathlib's LinearMap.det_conj through the coercion to linear maps).

theorem Hironaka.Manifold.jacobianFun_of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {M' : AnalyticManifold 𝕜 E} {N' : AnalyticManifold 𝕜 E'} (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (f : AnalyticMap M' M) (f' : AnalyticMap N' N) (hsq : IsModelSquare g g' f f') (χ : OpenPartialHomeomorph M.carrier E) (φ : OpenPartialHomeomorph M'.carrier E) (y : N'.carrier) : Manifold.jacobianFun 𝕜 (⇑f') (chartOfSquare g ψ χ) (chartOfSquare g' ψ φ) y = Manifold.jacobianFun 𝕜 (⇑f) χ φ (g' y)

The Jacobian determinant of f' in the charts read from those of f is the Jacobian determinant of f at the corresponding point: the chart representatives are conjugate by ψ (det_clm_conj), so the two are equal — no unit germ enters.

theorem Hironaka.Manifold.jacobianStalk_of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {M' : AnalyticManifold 𝕜 E} {N' : AnalyticManifold 𝕜 E'} (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (f : AnalyticMap M' M) (f' : AnalyticMap N' N) (hsq : IsModelSquare g g' f f') (b : N'.carrier) : Manifold.jacobianStalk (⇑f') b = Ideal.map (g'.stalkRingEquiv b) (Manifold.jacobianStalk (⇑f) (g' b))

The Jacobian stalk along a square: the stalk isomorphism of g' carries the Jacobian stalk of f at g' b to the Jacobian stalk of f' at b, the generators (the Jacobian determinants in charts) corresponding by jacobianFun_of_square in the charts read through g, g'. No model isomorphism is assumed: the inverse differential of g' at b (Diffeomorph.mfderivToContinuousLinearEquiv) serves as the ψ of the read charts.

theorem AnalyticMap.jacobianIdeal_of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {M' : AnalyticManifold 𝕜 E} {N' : AnalyticManifold 𝕜 E'} (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (f : AnalyticMap M' M) (f' : AnalyticMap N' N) (hsq : Hironaka.Manifold.IsModelSquare g g' f f') : f'.jacobianIdeal = AnalyticManifold.IdealSheaf.pullbackDiffeomorph g' f.jacobianIdeal

The Jacobian ideal [BM97, Theorem 1.10, the sentence after it] along a square of analytic isomorphisms across the models: stalk by stalk, jacobianStalk_of_square; no model isomorphism in the statement.