The pull-back and push-forward of successions with the morphism spelled out

The relations FiniteSuccession.IsPullbackUpToEmptyAlong and FiniteSuccession.IsPushforwardUpToEmptyAlong assert a morphism of successions (FiniteSuccession.Hom) with conditions on its maps and on the centres. This module restates them with the index map and the maps between the stages as separate witnesses (isPullbackUpToEmptyAlong_iff, isPushforwardUpToEmptyAlong_iff), the form in which they are constructed and taken apart.

theorem AnalyticManifold.FiniteSuccession.isPullbackUpToEmptyAlong_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} {U' : TopologicalSpace.Opens N.carrier} {R : (N.restrict U').FiniteSuccession} {S : (M.restrict U).FiniteSuccession} {g : AnalyticMap N M} : R.IsPullbackUpToEmptyAlong S g ↔ ∃ (blk : Fin (S.length + 1) → Fin (R.length + 1)) (f : (k : Fin (S.length + 1)) → AnalyticMap (R.stage (blk k)) (S.stage k)), blk 0 = 0 ∧ blk (Fin.last S.length) = Fin.last R.length ∧ (∀ (k : Fin S.length), ↑(blk k.succ) = ↑(blk k.castSucc) ∨ ↑(blk k.succ) = ↑(blk k.castSucc) + 1) ∧ (∀ (k : Fin (S.length + 1)), IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(f k)) ∧ (∀ (k : Fin (S.length + 1)) (p : (R.stage (blk k)).carrier), (M.inclusion U) ((S.stageMap k) ((f k) p)) = g ((N.inclusion U') ((R.stageMap (blk k)) p))) ∧ (∀ (k : Fin S.length) (hle : blk k.castSucc ≤ blk k.succ) (p : (R.stage (blk k.succ)).carrier), (S.map k) ((f k.succ) p) = (f k.castSucc) ((R.stageMapLE hle) p)) ∧ (∀ (k : Fin S.length) (ha : ↑(blk k.castSucc) < R.length), ↑(blk k.succ) = ↑(blk k.castSucc) + 1 → R.centerAt (blk k.castSucc) ha = Manifold.IdealSheaf.pullback ⇑(f k.castSucc) ⋯ (S.center k)) ∧ ∀ (k : Fin S.length), ↑(blk k.succ) = ↑(blk k.castSucc) → (Manifold.IdealSheaf.pullback ⇑(f k.castSucc) ⋯ (S.center k)).support = ∅

IsPullbackUpToEmptyAlong with the morphism of successions spelled out: an index map and local analytic isomorphisms between the stages with the conditions of FiniteSuccession.Hom.

theorem AnalyticManifold.FiniteSuccession.isPushforwardUpToEmptyAlong_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {U : TopologicalSpace.Opens M.carrier} {U' : TopologicalSpace.Opens N.carrier} {S : (M.restrict U).FiniteSuccession} {R : (N.restrict U').FiniteSuccession} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} : S.IsPushforwardUpToEmptyAlong R τ ↔ ∃ (blk : Fin (S.length + 1) → Fin (R.length + 1)) (f : (k : Fin (S.length + 1)) → ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) (R.stage (blk k)).carrier (S.stage k).carrier ⊤), blk 0 = 0 ∧ blk (Fin.last S.length) = Fin.last R.length ∧ (∀ (k : Fin S.length), ↑(blk k.succ) = ↑(blk k.castSucc) ∨ ↑(blk k.succ) = ↑(blk k.castSucc) + 1) ∧ (∀ (k : Fin (S.length + 1)), Topology.IsEmbedding ⇑(f k)) ∧ (∀ (k : Fin (S.length + 1)), ∀ q ∈ closure (Set.range ⇑(f k)), (M.inclusion U) ((S.stageMap k) q) ∈ ⇑τ '' ↑U' → q ∈ Set.range ⇑(f k)) ∧ (∀ (k : Fin (S.length + 1)) (p : (R.stage (blk k)).carrier), (M.inclusion U) ((S.stageMap k) ((f k) p)) = τ ((N.inclusion U') ((R.stageMap (blk k)) p))) ∧ (∀ (k : Fin S.length) (hle : blk k.castSucc ≤ blk k.succ) (p : (R.stage (blk k.succ)).carrier), (S.map k) ((f k.succ) p) = (f k.castSucc) ((R.stageMapLE hle) p)) ∧ (∀ (k : Fin S.length) (ha : ↑(blk k.castSucc) < R.length), ↑(blk k.succ) = ↑(blk k.castSucc) + 1 → ⇑(f k.castSucc) ⁻¹' Manifold.IdealSheaf.support (S.center k) = Manifold.IdealSheaf.support (R.centerAt (blk k.castSucc) ha)) ∧ (∀ (k : Fin S.length), ↑(blk k.succ) = ↑(blk k.castSucc) → ⇑(f k.castSucc) ⁻¹' Manifold.IdealSheaf.support (S.center k) = ∅) ∧ ∀ (k : Fin S.length), ∀ q ∈ Manifold.IdealSheaf.support (S.center k), (M.inclusion U) ((S.stageMap k.castSucc) q) ∈ ⇑τ '' ↑U' → q ∈ Set.range ⇑(f k.castSucc)

IsPushforwardUpToEmptyAlong with the morphism of successions spelled out: an index map and embeddings between the stages with the conditions of FiniteSuccession.Hom.