The two stop clauses across the composite of two family functors #
The modified functor is the composite composeInduced of its phases (ModifiedFam.lean): on an
open U its value is composeOn, the composite alongList over the canonical pair (W, V) of
opens above U (the first functor's value on W restricted to V, followed by the second
functor's value at the induced triple on the lifted range, shrinkAppend), pulled back to U and
cleaned of its empty blow-ups. This module carries the output clause and the stopped clause of
ClauseTools.lean across that construction, statement by statement alongside the order clause of
ComposeInduced.lean and ComposeInducedFunctor.lean at the mark 1:
BlowUpSequence.outputClause_shrinkAppend,stoppedClause_shrinkAppend(the analogues ofisOfOrderGe_shrinkAppend): the appended value's clause for the induced triple restricted to the lifted range pulls back along the corestricted lift to the clause for the induced triple of the restricted list (induced_pullback), and the concatenation inherits the clause (outputClause_concat,stoppedClause_concat); for the stopped clause the list so far pulls back too.alongList_outputClause,alongList_stoppedClause(the analogues ofalongList_isOfOrderGe): the composite over(W, V)from the second functor's output clause, resp. both functors' stopped clauses, the restricted triple rewritten bypullback_inclusion_restrictLE.composeOn_outputClause,composeOn_stoppedClause(the analogues ofcomposeOn_isOfOrderGe): the pull-back toU(outputClause_pullback,stoppedClause_pullback) and the deletion of the empty blow-ups (outputClause_eraseEmpty,stoppedClause_eraseEmpty).composeInduced_outputClauseFam,composeInduced_stoppedClauseFam: the clauses of the composite functor. The output clause needs only the second functor's (the last stage is its); the stopped clause needs both.
Sources: the phases in succession per open in the proof of [Wlo09, Theorem 7.4.1]; [Kol07, 104, Step 2.1] and [Kol07, 34.1] for the concatenation of blow-up sequences and the deletion of empty blow-ups. The statements themselves are not in the sources.
theorem
AnalyticManifold.BlowUpSequence.outputClause_shrinkAppend
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N : AnalyticManifold 𝕜 E}
(L : BlowUpSequence ψ₀ M)
(h : AnalyticMap N M)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h)
(T : Manifold.AnalyticTriple ψ₀ M)
(hL : L.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf)
(L' : BlowUpSequence ψ₀ ((L.stage (Fin.last L.length)).restrict (L.liftRange h hh)))
(hL' :
L'.toSuccession.IsOfOrderGe
((T.induced 1 L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).I 1
((T.induced 1 L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).F.idealSheaf)
(hP' :
FiniteSuccession.OutputClause ψ₀ L'.toSuccession
((T.induced 1 L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).I
((T.induced 1 L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).F)
:
FiniteSuccession.OutputClause ψ₀ (L.shrinkAppend h hh L').toSuccession (T.pullback h hh).I (T.pullback h hh).F
The chain step keeps the output clause (the analogue of isOfOrderGe_shrinkAppend): the
appended value's clause for the induced triple restricted to the lifted range pulls back along the
corestricted lift (outputClause_pullback) to the clause for the induced triple of the restricted
list (induced_pullback), and the concatenation has the clause (outputClause_concat).
theorem
AnalyticManifold.BlowUpSequence.stoppedClause_shrinkAppend
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N : AnalyticManifold 𝕜 E}
(L : BlowUpSequence ψ₀ M)
(h : AnalyticMap N M)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h)
(T : Manifold.AnalyticTriple ψ₀ M)
(hL : L.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf)
(hP : FiniteSuccession.StoppedClause ψ₀ L.toSuccession T.I T.F)
(L' : BlowUpSequence ψ₀ ((L.stage (Fin.last L.length)).restrict (L.liftRange h hh)))
(hL' :
L'.toSuccession.IsOfOrderGe
((T.induced 1 L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).I 1
((T.induced 1 L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).F.idealSheaf)
(hP' :
FiniteSuccession.StoppedClause ψ₀ L'.toSuccession
((T.induced 1 L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).I
((T.induced 1 L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).F)
:
FiniteSuccession.StoppedClause ψ₀ (L.shrinkAppend h hh L').toSuccession (T.pullback h hh).I (T.pullback h hh).F
The chain step keeps the stopped clause: the list so far pulls back (stoppedClause_pullback),
the appended value pulls back along the corestricted lift to the induced triple of the restricted
list, and the concatenation has the clause (stoppedClause_concat).
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.alongList_outputClause
{𝕜 : 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₂)
(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 1
(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 1 ((F.fam T hT).seqOn U hU) ⋯))
{M : AnalyticManifold 𝕜 E}
(T : Manifold.AnalyticTriple ψ₀ M)
(hT : Dom₁ T)
(W : TopologicalSpace.Opens M.carrier)
(hW : IsCompact (closure ↑W))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(hVW : closure ↑V ⊆ ↑W)
(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 1
(T'.pullback (N.inclusion U') ⋯).F.idealSheaf)
(hG1 : OutputClauseFam ψ₀ G)
:
AnalyticManifold.FiniteSuccession.OutputClause ψ₀ (F.alongList G 1 ⋯ ⋯ T hT W hW V hV hVW).toSuccession
(T.pullback (M.inclusion V) ⋯).I (T.pullback (M.inclusion V) ⋯).F
The output clause of the composite over (W, V) from that of G (the analogue of
alongList_isOfOrderGe): outputClause_shrinkAppend with the order clause of G and its output
clause at the induced triple on the lifted range, the restricted triple rewritten by
pullback_inclusion_restrictLE.
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.alongList_stoppedClause
{𝕜 : 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₂)
(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 1
(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 1 ((F.fam T hT).seqOn U hU) ⋯))
{M : AnalyticManifold 𝕜 E}
(T : Manifold.AnalyticTriple ψ₀ M)
(hT : Dom₁ T)
(W : TopologicalSpace.Opens M.carrier)
(hW : IsCompact (closure ↑W))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(hVW : closure ↑V ⊆ ↑W)
(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 1
(T'.pullback (N.inclusion U') ⋯).F.idealSheaf)
(hF8 : StoppedClauseFam ψ₀ F)
(hG8 : StoppedClauseFam ψ₀ G)
:
AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (F.alongList G 1 ⋯ ⋯ T hT W hW V hV hVW).toSuccession
(T.pullback (M.inclusion V) ⋯).I (T.pullback (M.inclusion V) ⋯).F
The stopped clause of the composite over (W, V) from those of F and G
(stoppedClause_shrinkAppend).
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.composeOn_outputClause
{𝕜 : 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₂)
(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 1
(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 1 ((F.fam T hT).seqOn U hU) ⋯))
(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 1
(T'.pullback (N.inclusion U') ⋯).F.idealSheaf)
(hG1 : OutputClauseFam ψ₀ G)
{M : AnalyticManifold 𝕜 E}
(T : Manifold.AnalyticTriple ψ₀ M)
(hT : Dom₁ T)
(U : TopologicalSpace.Opens M.carrier)
(hU : IsCompact (closure ↑U))
:
AnalyticManifold.FiniteSuccession.OutputClause ψ₀ (F.composeOn G 1 ⋯ ⋯ T hT U hU).toSuccession
(T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F
The output clause of the composite's value on U (the analogue of composeOn_isOfOrderGe): the
composite over the canonical pair pulled back to U (outputClause_pullback,
pullback_inclusion_restrictLE) and cleaned of its empty blow-ups (outputClause_eraseEmpty).
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.composeOn_stoppedClause
{𝕜 : 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₂)
(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 1
(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 1 ((F.fam T hT).seqOn U hU) ⋯))
(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 1
(T'.pullback (N.inclusion U') ⋯).F.idealSheaf)
(hF8 : StoppedClauseFam ψ₀ F)
(hG8 : StoppedClauseFam ψ₀ G)
{M : AnalyticManifold 𝕜 E}
(T : Manifold.AnalyticTriple ψ₀ M)
(hT : Dom₁ T)
(U : TopologicalSpace.Opens M.carrier)
(hU : IsCompact (closure ↑U))
:
AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (F.composeOn G 1 ⋯ ⋯ T hT U hU).toSuccession
(T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F
The stopped clause of the composite's value on U (stoppedClause_pullback,
stoppedClause_eraseEmpty).
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.composeInduced_outputClauseFam
{𝕜 : 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₂)
(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 1
(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 1 ((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 1 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 1
(T'.pullback (N.inclusion U') ⋯).F.idealSheaf)
(hG1 : OutputClauseFam ψ₀ G)
:
OutputClauseFam ψ₀ (F.composeInduced G 1 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)
The output clause of the composite functor (the analogue of composeInduced_isOfOrderGe).
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.composeInduced_stoppedClauseFam
{𝕜 : 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₂)
(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 1
(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 1 ((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 1 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 1
(T'.pullback (N.inclusion U') ⋯).F.idealSheaf)
(hF8 : StoppedClauseFam ψ₀ F)
(hG8 : StoppedClauseFam ψ₀ G)
:
StoppedClauseFam ψ₀ (F.composeInduced G 1 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)
The stopped clause of the composite functor from the stopped clauses of both functors.