Functoriality of the pullback data of triples

The inverse image ideal sheaf is functorial (IdealSheaf.pullback_pullback of Hironaka.Manifold.BlowUp.Transform.GermIso: pulling back twice is pulling back along the composite), so the pullback data of triples compose (AnalyticTriple.IsPullbackOf.comp, the analogue of IsPullbackOf.comp for schemes), and the pulled-back triples compose (AnalyticTriple.pullback_pullback). This is the functoriality behind the pull-back of blow-up sequences [Kol07, Definition 30, 30.1] and [Kol07, 34.1].

@[simp]

theorem AnalyticManifold.IdealSheaf.pullback_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N P : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (h : AnalyticMap N M) (k : AnalyticMap P N) : Manifold.IdealSheaf.pullback ⇑k ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ J) = Manifold.IdealSheaf.pullback ⇑(ContMDiffMap.comp h k) ⋯ J

The pullback along analytic maps is functorial (IdealSheaf.pullback_pullback, with the composite as an analytic map).

@[simp]

theorem Manifold.HypersurfaceFamily.comap_comap {M N P : Type u} (F : HypersurfaceFamily M) (h : N → M) (k : P → N) : comap k (comap h F) = comap (h ∘ k) F

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

[Kol07, 34.1] (IsPullbackOf.comp): pullback data compose along composites.

theorem Manifold.AnalyticTriple.pullback_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N P : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (k : AnalyticMap P N) (hk : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k) : (T.pullback h hh).pullback k hk = T.pullback (ContMDiffMap.comp h k) ⋯

The pulled-back triples compose.