The pull-back of a hypersurface of maximal contact

[Kol07, Theorem 103 (2)] for the local functor of Steps 1 and 2 uses that the hypersurface of maximal contact chosen from the class for the pulled-back triple may be replaced by the pull-back of the one chosen for the original triple (Step 2.3 of the proof; a hypersurface of maximal contact pulls back along a local analytic isomorphism, as Kollár uses in [Kol07, 104, Step 2.3]).

• AnalyticTriple.idealSheaf_preimage_le_iteratedDeriv_pullback — the pull-back of a hypersurface of maximal contact has maximal contact for the pulled-back ideal sheaf.

It enters the commutation of the local functor in the compatible-family form (LocalFunctorFam.lean).

theorem Manifold.AnalyticTriple.idealSheaf_preimage_le_iteratedDeriv_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {H : Set M.carrier} (hH : IsClosedSubmanifold ψ₀ H 1) {r : ℕ} (hle : hH.idealSheaf ≤ IdealSheaf.iteratedDeriv T.I r) : ⋯.idealSheaf ≤ IdealSheaf.iteratedDeriv (T.pullback h hh).I r

A hypersurface of maximal contact pulls back along a local analytic isomorphism: if the ideal sheaf of H lies in the r-th derivative ideal sheaf of 𝓘, then the ideal sheaf of h⁻¹(H) lies in the r-th derivative ideal sheaf of the pull-back of 𝓘 (the inequality behind hasMaximalContact_of_isPullbackOf, for the explicit preimage). Not in the sources as a separate statement.