Transforms along a square of analytic isomorphisms across the models

The notions attached to an analytic map f : M' → M in the vocabulary of the main theorems — Hironaka's weak transform [Hir64, p. 142], the reduced transform red(f⁻¹(E) ∪ f⁻¹(D)) [Hir64, Main Theorem II'(N) (iii), p. 156], the isomorphism-over-a-set clause IsAnalyticIsoOver and properness — transport along a square f ∘ g' = g ∘ f' of analytic isomorphisms g : N ≃ M, g' : N' ≃ M' across the models (IsModelSquare, Hironaka/Resolution/Analytic/ModelTransport/IdealSheaf.lean): f' is g⁻¹ ∘ f ∘ g', the same map read on the re-modelled manifolds. For the main theorems the squares are the identities of Hironaka/Resolution/Analytic/ModelTransport/Manifold.lean at the stages of a transported succession (Succession.lean) and at the space of a transported family (Family.lean).

• The weak transform: both sides are the unique ideal sheaf with the colon stalks (f⁻¹(J)_{a'} : f⁻¹(D)_{a'}^{ν}) (IsDivExceptional.unique); the colon data correspond under the stalk isomorphism of g' (Ideal.map_colon_pow_of_bijective), the exponent — the generic order of J along the centre through f a' — transports because the order along a centre is read on stalks (ordAlongIdeal_pullbackDiffeomorph) and the connected component of the centre is carried by the homeomorphism g (genericOrdAlong_pullbackDiffeomorph); when no ideal sheaf with the colon stalks exists on one side, none exists on the other, and both sides are the unit ideal. The same argument as weakTransform_comap_liftStep of Hironaka/Manifold/Sequence/Functor/, across the models.
• The reduced transform: the closed sets f⁻¹(E) ∪ f⁻¹(D) correspond under g'; the vanishing stalks are carried by the stalk isomorphism (vanishingStalk_preimage_pullbackDiffeomorph, the two-model form of vanishingStalk_preimage_of_isLocalDiffeomorphAt' of Hironaka/Resolution/Analytic/IdealSheaf/VanishingPreimage.lean); the local-generator condition transports both ways — forward by hasLocalGenerators_pullback, back by the forward direction along g⁻¹ (g is a bijection). The same argument as reducedTransform_comap_of_surjective.
• IsAnalyticIsoOver: the local inverses are conjugated by g, g' (PartialDiffeomorph.trans); the bijection onto the set is read through the square.
• IsProperMap: f' = g⁻¹ ∘ f ∘ g' with homeomorphisms.

The Jacobian ideal and the monoidal transformations along a square, which need charts, are in Hironaka/Resolution/Analytic/ModelTransport/SquareChart.lean.

theorem Hironaka.Manifold.Germ.vanishesOn_compTendsto_of_isLocalDiffeomorphAt_models {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] {h : N → M} (hh : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ h) {b : N} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ h b) (Z : Set M) (k : (nhds (h b)).Germ 𝕜) : Manifold.Germ.VanishesOn (h ⁻¹' Z) b (k.compTendsto h ⋯) ↔ Manifold.Germ.VanishesOn Z (h b) k

A germ at h b vanishes on Z iff its pull-back along the local analytic isomorphism h vanishes on h⁻¹(Z) at b: the two-model form of Germ.vanishesOn_compTendsto_of_isLocalDiffeomorphAt' (Hironaka/Resolution/Analytic/IdealSheaf/VanishingPreimage.lean), the same proof with the models free.

theorem Hironaka.Manifold.vanishingStalk_preimage_of_isLocalDiffeomorphAt_models {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] {h : N → M} (hh : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ h) {b : N} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ h b) (Z : Set M) : Manifold.vanishingStalk (h ⁻¹' Z) b = Ideal.map (Manifold.germMap h hh b) (Manifold.vanishingStalk Z (h b))

The vanishing stalk of h⁻¹(Z) at b is the image of the vanishing stalk of Z at h b under the germ map: the two-model form of vanishingStalk_preimage_of_isLocalDiffeomorphAt'.

theorem Hironaka.Manifold.vanishingStalk_preimage_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 ⊤) (Z : Set M.carrier) (b : N.carrier) : Manifold.vanishingStalk (⇑g ⁻¹' Z) b = Ideal.map (g.stalkRingEquiv b) (Manifold.vanishingStalk Z (g b))

The vanishing stalk along an analytic isomorphism across the models.

theorem Hironaka.Manifold.hasLocalGenerators_vanishingStalk_preimage_diffeomorph {𝕜 : 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 ⊤) (W : Set M.carrier) (hW : Manifold.IdealSheaf.HasLocalGenerators fun (y : M.carrier) => Manifold.vanishingStalk W y) : Manifold.IdealSheaf.HasLocalGenerators fun (x : N.carrier) => Manifold.vanishingStalk (⇑g ⁻¹' W) x

Local generators of the vanishing stalks of a set are carried along g (hasLocalGenerators_pullback).

theorem Hironaka.Manifold.hasLocalGenerators_vanishingStalk_preimage_diffeomorph_iff {𝕜 : 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 ⊤) (W : Set M.carrier) : (Manifold.IdealSheaf.HasLocalGenerators fun (x : N.carrier) => Manifold.vanishingStalk (⇑g ⁻¹' W) x) ↔ Manifold.IdealSheaf.HasLocalGenerators fun (y : M.carrier) => Manifold.vanishingStalk W y

Local generators of the vanishing stalks, both ways (g is a bijection: the other way is the forward direction along g⁻¹).

theorem Manifold.IdealSheaf.ordAlongIdeal_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 ⊤) (D J : M.IdealSheaf) (b : N.carrier) : ordAlongIdeal (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g D) (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g J) b = ordAlongIdeal D J (g b)

The order along a centre along g: the stalk isomorphism preserves inclusions and powers.

theorem Manifold.IdealSheaf.genericOrdAlong_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 ⊤) (D J : M.IdealSheaf) (b : N.carrier) : genericOrdAlong (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g D) (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g J) b = genericOrdAlong D J (g b)

The generic order along a centre along g: the connected component of the centre through the point is carried by the homeomorphism g (Homeomorph.image_connectedComponentIn), the order pointwise.

theorem Hironaka.Manifold.IsModelSquare.apply_eq {𝕜 : 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') (x : N'.carrier) : f' x = g.symm (f (g' x))

The pointwise form of the square f ∘ g' = g ∘ f': f' = g⁻¹ ∘ f ∘ g'.

theorem Hironaka.Manifold.IsModelSquare.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 ⊤) {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') : IsModelSquare g.symm g'.symm f' f

The reversed square, for g⁻¹, g'⁻¹.

theorem Manifold.IdealSheaf.IsDivExceptional.pullbackDiffeomorph_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') (J D : M.IdealSheaf) {J' : M'.IdealSheaf} (h : (pullback ⇑f ⋯ J).IsDivExceptional (pullback ⇑f ⋯ D) (fun (a : ↑↧M'.carrier) => (genericOrdAlong D J (f a)).toNat) J') : (pullback ⇑f' ⋯ (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g J)).IsDivExceptional (pullback ⇑f' ⋯ (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g D)) (fun (x : ↑↧N'.carrier) => (genericOrdAlong (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g D) (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g J) (f' x)).toNat) (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g' J')

The colon stalks (IsDivExceptional) along a square: the stalk isomorphism carries colon ideals and powers (Ideal.map_colon_pow_of_bijective), the exponent (the generic order along the centre) transports by genericOrdAlong_pullbackDiffeomorph.

theorem AnalyticManifold.IdealSheaf.weakTransform_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') (D J : M.IdealSheaf) : weakTransform f' (pullbackDiffeomorph g J) (pullbackDiffeomorph g D) = pullbackDiffeomorph g' (weakTransform f J D)

Hironaka's weak transform [Hir64, p. 142] along a square of analytic isomorphisms across the models: both sides are the unique ideal sheaf with the colon stalks (IsDivExceptional.unique), the colon data corresponding under g'; when no such sheaf exists on one side none exists on the other (pull back along g'⁻¹), and both are the unit ideal.

theorem AnalyticManifold.IdealSheaf.reducedTransform_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') (D E₀ : M.IdealSheaf) : reducedTransform f' (pullbackDiffeomorph g E₀) (pullbackDiffeomorph g D) = pullbackDiffeomorph g' (reducedTransform f E₀ D)

Hironaka's red(f⁻¹(E) ∪ f⁻¹(D)) [Hir64, Main Theorem II'(N) (iii), p. 156] along a square: the closed sets correspond, the vanishing stalks along the stalk isomorphisms, the local-generator condition both ways.

theorem Hironaka.Manifold.isLocalDiffeomorphOn_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') {U : Set M.carrier} (h : IsLocalDiffeomorphOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑f) (⇑f ⁻¹' U)) : IsLocalDiffeomorphOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E') ⊤ (⇑f') (⇑f' ⁻¹' ⇑g ⁻¹' U)

A local analytic isomorphism on a set transports along a square: the local inverse is conjugated by the two isomorphisms (PartialDiffeomorph.trans).

theorem Hironaka.Manifold.bijOn_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') {U : Set M.carrier} (h : Set.BijOn (⇑f) (⇑f ⁻¹' U) U) : Set.BijOn (⇑f') (⇑f' ⁻¹' ⇑g ⁻¹' U) (⇑g ⁻¹' U)

A bijection onto a set transports along a square.

theorem AnalyticMap.isAnalyticIsoOver_of_square_iff {𝕜 : 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') (U : Set M.carrier) : f'.IsIsoOver (⇑g ⁻¹' U) ↔ f.IsIsoOver U

IsAnalyticIsoOver along a square: both directions by the forward lemmas at the square and at the reversed square.

theorem Hironaka.Manifold.isProperMap_of_square_iff {𝕜 : 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') : IsProperMap ⇑f' ↔ IsProperMap ⇑f

Properness along a square: f' = g⁻¹ ∘ f ∘ g' with g, g' homeomorphisms (Homeomorph.isProperMap, IsProperMap.comp).