The pulled-back triple (N, h^* 𝓘, h⁻¹(E)) along a local analytic isomorphism

The pullback data of a triple (X, I, E) along a smooth morphism h : Y → X form a triple ([Kol07, Definition 30, 30.1]; [Kol07, 34.1], "B(Y, h^* I, h⁻¹(E))"). On manifolds, for a local analytic isomorphism h : N → M: the inverse image ideal sheaf h^* 𝓘 (comap) has nonzero stalks because the stalk map of a local isomorphism is a ring isomorphism (ord_pullback_of_isLocalDiffeomorphAt: ν_b(h^* 𝓘) = ν_{h b}(𝓘), and ν = ⊤ iff the stalk is zero); the inverse image family h⁻¹(E) is a simple normal crossings divisor because its components are the preimages of closed hypersurfaces (IsClosedSubmanifold.preimage_of_isLocalDiffeomorph), local finiteness pulls back along continuous maps, and a simple normal crossings chart at h a transported along a local inverse of h (transportChart) is such a chart at a.

• IdealSheaf.isNonzeroEverywhere_comap, HypersurfaceFamily.isSnc_comap;
• AnalyticTriple.pullback T h hh : AnalyticTriple ψ₀ N, isPullbackOf_pullback, ext', IsPullbackOf.eq (the pullback data determine the triple).

The arguments are routine and not in the source.

theorem Manifold.finiteDimensional_of_chartIso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) : FiniteDimensional 𝕜 E

The model chart iso ψ₀ : E ≃L[𝕜] 𝕜ⁿ makes E finite-dimensional (the standing hypothesis of order theory, IdealSheaf.ord_eq_top_iff).

theorem Manifold.IdealSheaf.isNonzeroEverywhere_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] {I : M.IdealSheaf} (hI : IsNonzeroEverywhere I) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : (pullback ⇑h ⋯ I).IsNonzeroEverywhere

Nonzero stalks pull back along a local analytic isomorphism: the stalk map at b is an isomorphism onto the stalk at h b (ord_pullback_of_isLocalDiffeomorphAt, read through ν = ⊤ ↔ stalk = 0).

theorem Manifold.HypersurfaceFamily.isSnc_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ₀ F) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : IsSnc ψ₀ (comap (⇑h) F)

The simple normal crossings property pulls back along a local analytic isomorphism: the components are the preimages of closed hypersurfaces, local finiteness pulls back, and an snc chart at h a transported along a local inverse of h is an snc chart at a.

noncomputable def Manifold.AnalyticTriple.pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : AnalyticTriple ψ₀ N

[Kol07, Definition 30, 30.1], 34.1: the pulled-back triple (N, h^* 𝓘, h⁻¹(E)) of T = (M, 𝓘, E) along a local analytic isomorphism h : N → M.

Equations

• T.pullback h hh = { I := Manifold.IdealSheaf.pullback ⇑h ⋯ T.I, isNonzeroEverywhere := ⋯, F := Manifold.HypersurfaceFamily.comap (⇑h) T.F, isSnc := ⋯ }

theorem Manifold.AnalyticTriple.isPullbackOf_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : (T.pullback h hh).IsPullbackOf T h

The pulled-back triple carries the pullback data (isPullbackOf_pullback).

theorem Manifold.AnalyticTriple.ext' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T₁ T₂ : AnalyticTriple ψ₀ M} (hI : T₁.I = T₂.I) (hF : T₁.F = T₂.F) : T₁ = T₂

A triple is its ideal sheaf and its divisor (the other fields are proofs).

theorem Manifold.AnalyticTriple.IsPullbackOf.eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {T₁ T₂ : AnalyticTriple ψ₀ N} {T : AnalyticTriple ψ₀ M} {h : AnalyticMap N M} (h₁ : T₁.IsPullbackOf T h) (h₂ : T₂.IsPullbackOf T h) : T₁ = T₂

The pullback data determine the triple.