The per-open closed-embeddings predicate for family functors

The commutation with closed embeddings of [Kol07, 34.3], in the form of [Kol07, Theorem 103, (3)], per relatively compact open: the family functor B at the model (E, ψ₀) commutes with closed embeddings whenever E = ∅, through the family functor B' at the model 𝕜^{n−s}; this is the per-open version of AnalyticBlowUpSequenceAssignment.CommutesWithClosedEmbeddingsOfEmptyDivisor (Hironaka.Manifold.FiniteSuccession.Functor.Basic), the (n−s)-dimensional family read at U ∩ S and pushed forward by BlowUpSequence.pushforwardRestrict.

def Hironaka.Manifold.AnalyticFamilyFunctor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) {s : ℕ} {Dom' : {M' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} → Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) M' → Prop} (B' : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} => Dom') : Prop

B commutes with closed embeddings whenever E = ∅, through B' — for every closed submanifold τ : S ↪ M of codimension s, ideal sheaves 𝓘 on M and J on the bundled S with 𝓘 ⊇ I_S and J = τ^* 𝓘, and every relatively compact open U ⊆ M, the value of B on U is the push-forward of the value of B' on U_S.

Equations

• One or more equations did not get rendered due to their size.