Naturality of the value under pull-back of the list

Kollár's functoriality for smooth morphisms [Kol07, 34.1] with the empty-blow-up convention [Kol07, 32], for the value built from a list (valueOf): if T'' on the last stage of π^* L is an empty extension of the pull-back of T' on the last stage of L along the last-stage lift π_r (IsEmptyExtensionOfPullback), then the value built from π^* L and T'', read along ι, is the value built from L and T', read along π ∘ ι. The input family BMO_{n,1} supplies the two facts about its values that this needs — it is indifferent to empty members and commutes with local analytic isomorphisms (IndifferentToEmptyMembers, CommutesWithLocalIsos, both fields of the structure BMOanFam) — combined by seqOn_eq_of_isEmptyExtensionOfPullback; the shrink-and-append step is handled by pullback_shrinkAppend_eraseEmpty, and the two reading opens are compared by the input family's own compatibility clause (the image of the smaller reading open lies in the larger one, image_pullbackLiftLast_liftRange_subset). Used by Padding.lean for the canonicity of the shrinking chain.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.seqOn_congr {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) {M : AnalyticManifold 𝕜 E} {T₁ T₂ : Manifold.AnalyticTriple ψ₀ M} (e : T₁ = T₂) (h₁ : Dom T₁) (h₂ : Dom T₂) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (B.fam T₁ h₁).seqOn U hU = (B.fam T₂ h₂).seqOn U hU

The value of a family functor is compatible with an equality of triples.

The input family on an empty extension of a pull-back

theorem Hironaka.Manifold.BMOanFam.seqOn_eq_of_isEmptyExtensionOfPullback {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (h : T'.IsEmptyExtensionOfPullback T g) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : (bmo.functor.fam T' hT').seqOn U' hU' = (((bmo.functor.fam T hT).seqOn (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

[Kol07, 34.1] with the empty-blow-up convention [Kol07, 32]: the value of BMO_{n,1} on a triple T' that is an empty extension of the pull-back of T along a local analytic isomorphism g is the pull-back of its value on T, read on the image open, with the empty rounds erased — IndifferentToEmptyMembers (the extra empty members do not change the value) followed by CommutesWithLocalIsos.

The value under pull-back of the list

theorem Hironaka.Manifold.valueOf_pullback {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X' X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X') (π : AnalyticMap X X') (hπ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑π) (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (ι' : AnalyticMap N X') (hι' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι') (hcomp : ContMDiffMap.comp π ι = ι') (hc : IsCompact (closure (Set.range ⇑ι))) (hc' : IsCompact (closure (Set.range ⇑ι'))) (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (L.stage (Fin.last L.length))) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (T'' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((L.pullback π hπ).stage (Fin.last (L.pullback π hπ).length))) (hT'' : Manifold.AnalyticTriple.BMOClass 1 T'') (h : T''.IsEmptyExtensionOfPullback T' (L.pullbackLiftLast π hπ)) : valueOf bmo (L.pullback π hπ) T'' hT'' ι hι hc = valueOf bmo L T' hT' ι' hι' hc'

The value is natural under pull-back of the list ([Kol07, 34.1]; [Kol07, 32]): the value built from π^* L and a triple T'' that is an empty extension of the pull-back of T' along the last-stage lift π_r, read along ι, is the value built from L and T' read along π ∘ ι.