The composite of two family functors along induced triples: the functor

ComposeInduced.lean built the link of the composite of F : AnalyticFamilyFunctor ψ₀ Dom₁ with G : AnalyticFamilyFunctor ψ₀ Dom₂ at the induced triples (alongList over a pair of opens closure V ⊆ W, its order clause, its relation alongList_rel along a local analytic isomorphism). This module makes the composite a family functor on Dom₁, following the assembly of the second step of the order reduction (Step2Assembly.lean, Step2AssemblyComm.lean) with its link replaced by the generic one:

• composeAlong F G s … T hT W V hW hV hVW U hUV : CenterList ψ₀ (M.restrict U), the composite over (W, V) restricted to U ≤ V, with the empty blow-ups deleted; composeAlong_eq_join and composeAlong_rel, the independence from the chain: two pairs of opens above U give the same value (alongList_rel at the identity, against the common refinement (W ⊓ W′, V ⊓ V′));
• composeOn F G s … T hT U hU, the value on U along the canonical pair (chainOpens (exhaustion M) n₀ 1 0, chainOpens (exhaustion M) n₀ 1 1) with n₀ = exhaustionIdx _ hU (the exhaustion index of hfStep2FamOn); composeOn_compat (the second condition of [Kol07, 34.1], [Wlo09, Theorem 2.0.3 (4)]) by the independence from the chain for the canonical pair of the larger open read on the smaller;
• composeInduced F G s … : AnalyticFamilyFunctor ψ₀ Dom₁, the functor, with composeInduced_isOfOrderGe (the order clause at the mark s, from alongList_isOfOrderGe), composeInduced_commutesWithLocalIsos (alongList_rel along g against the trace of the canonical pair of g(U′) intersected with the canonical pair of U′) and composeInduced_indifferentToEmptyMembers (the indifference of F for the first list, that of G through IndifferentToEmptyMembers.seqOn_induced_indiff for the appended value: alongList_indiff).

The hypotheses are the properties of the two functors and the class hypotheses of ComposeInduced.lean: hF, hFG, hFc, hG, hG', hDom, hDomE, and hDom₁ : ClassPullbackClosed Dom₁ (the triple pulled back along the identity, the pivot of the argument for the independence from the chain, stays in the class of F).

noncomputable def Hironaka.Manifold.AnalyticFamilyFunctor.composeAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W V : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (U : TopologicalSpace.Opens M.carrier) (hUV : U ≤ V) : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U)

The composite over (W, V) read on U ≤ V, with the empty blow-ups deleted.

Equations

• F.composeAlong G s hF hFG T hT W V hW hV hVW U hUV = ((F.alongList G s ⋯ ⋯ T hT W hW V hV hVW).pullback (M.restrictLE hUV) ⋯).eraseEmpty

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeAlong_eq_join {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDom₁ : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₁) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W V : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (W₀ V₀ : TopologicalSpace.Opens M.carrier) (hW₀ : IsCompact (closure ↑W₀)) (hV₀ : IsCompact (closure ↑V₀)) (hW₀W : W₀ ≤ W) (hV₀V : V₀ ≤ V) (hV₀W₀ : closure ↑V₀ ⊆ ↑W₀) (U : TopologicalSpace.Opens M.carrier) (hUV₀ : U ≤ V₀) : F.composeAlong G s ⋯ ⋯ T hT W V hW hV hVW U ⋯ = ((F.alongList G s ⋯ ⋯ (T.pullback ContMDiffMap.id ⋯) ⋯ W₀ hW₀ V₀ hV₀ hV₀W₀).eraseEmpty.pullback (M.restrictLE hUV₀) ⋯).eraseEmpty

The composite over (W, V) read on U is the composite over any smaller pair (W₀, V₀) above U, for the triple pulled back along the identity, pulled back to U and cleaned: alongList_rel at the identity.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeAlong_rel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDom₁ : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₁) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W V : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (W' V' : TopologicalSpace.Opens M.carrier) (hW' : IsCompact (closure ↑W')) (hV' : IsCompact (closure ↑V')) (hV'W' : closure ↑V' ⊆ ↑W') (U : TopologicalSpace.Opens M.carrier) (hUV : U ≤ V) (hUV' : U ≤ V') : F.composeAlong G s ⋯ ⋯ T hT W V hW hV hVW U hUV = F.composeAlong G s ⋯ ⋯ T hT W' V' hW' hV' hV'W' U hUV'

Independence from the chain: two pairs of opens above U give the same composite on U, both being the composite over the common refinement (W ⊓ W′, V ⊓ V′) (composeAlong_eq_join).

noncomputable def Hironaka.Manifold.AnalyticFamilyFunctor.composeOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U)

The composite on U, along the canonical pair of opens above U, chainOpens (exhaustion M) n₀ 1 0 ⊇ closure (chainOpens (exhaustion M) n₀ 1 1) ⊇ … ⊇ U with n₀ = exhaustionIdx (exhaustion M) hU (the exhaustion index of hfStep2FamOn).

Equations

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

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeOn_noEmptyCenters {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (F.composeOn G s ⋯ ⋯ T hT U hU).NoEmptyCenters

The value of the composite has no empty centres [Kol07, 32].

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeOn_compat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDom₁ : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₁) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U V : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : F.composeOn G s ⋯ ⋯ T hT U hU = ((F.composeOn G s ⋯ ⋯ T hT V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The compatibility of the composite under restriction (the second condition of [Kol07, 34.1]; [Wlo09, Theorem 2.0.3 (4)]): for U ≤ V the value on U is the value on V restricted to U with its empty blow-ups deleted (the independence from the chain, for the canonical pair of V read on U).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeOn_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (hGo : ∀ {N : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ N) (hT' : Dom₂ T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((G.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I s (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (F.composeOn G s ⋯ ⋯ T hT U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf

The order clause of the value of the composite at the mark s, from those of F (hF) and G (hGo): alongList_isOfOrderGe pulled back to U (isOfOrderGe_pullback, pullback_inclusion_restrictLE) and cleaned (isOfOrderGe_eraseEmpty).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.alongList_indiff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hG' : G.IndifferentToEmptyMembers) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (hFi : F.IndifferentToEmptyMembers) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hT' : Dom₁ { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) (W V : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : F.alongList G s ⋯ ⋯ T hT W hW V hV hVW = F.alongList G s ⋯ ⋯ { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } hT' W hW V hV hVW

The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], for the composite over (W, V): deleting empty boundary members of T does not change the composite. The indifference of F identifies the first lists, that of G (IndifferentToEmptyMembers.seqOn_induced_indiff) the appended values at the induced triples of the common first list (the restricted triple of T with its boundary replaced is the restricted triple with the restricted replacement, definitionally).

The functor and its clauses

noncomputable def Hironaka.Manifold.AnalyticFamilyFunctor.composeInduced {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDom₁ : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₁) : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁

The composite family functor on Dom₁: composeOn on every relatively compact open, without empty centres, compatible under restriction (composeOn_compat).

Equations

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

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeInduced_fam_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDom₁ : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₁) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((F.composeInduced G s ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯).fam T hT).seqOn U hU = F.composeOn G s ⋯ ⋯ T hT U hU

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeInduced_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDom₁ : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₁) (hGo : ∀ {N : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ N) (hT' : Dom₂ T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((G.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I s (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (((F.composeInduced G s ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯).fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf

The order clause of the composite functor at the mark s (composeOn_isOfOrderGe).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeInduced_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDom₁ : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₁) : (F.composeInduced G s ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯).CommutesWithLocalIsos

[Kol07, 34.1] for the composite functor: it commutes with local analytic isomorphisms; the value on U′ for the pulled-back triple is the value on g(U′) pulled back along g|_{U′} and cleaned. The independence from the chain on the source manifold moves the canonical pair of U′ to the trace (g⁻¹(W) ⊓ W₁, g⁻¹(V) ⊓ V₁) of the canonical pair (W, V) of g(U′); alongList_rel along g relates the composites over the two pairs; the pull-backs are composed (pullback_comp) and compared (pullback_congr).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.composeInduced_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDom₁ : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₁) (hFi : F.IndifferentToEmptyMembers) : (F.composeInduced G s ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯).IndifferentToEmptyMembers

The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], for the composite functor: indifference to empty boundary members, from that of F (hFi) and of G (hG') through alongList_indiff (the canonical pair depends on the open only).