Local covers, coproducts of open embeddings and fibre products

The covering and fibre-product steps of the proof of [Kol07, Theorem 105] on manifolds. (i) From clause (2) of the theorem (every point has a local triple over it along an open embedding, and the local triples are closed under countable disjoint unions), every global triple has a local cover (exists_isLocalCover_of_globalizationData): choose 𝓜-morphisms gₓᵢ : Uₓᵢ → X whose images cover X (countably many by second countability), and let g : X' := ∐ᵢ Uₓᵢ → X be the induced map (sigmaManifold). (ii) The two projections τ₁, τ₂ : X'' → X' of the fibre product X'' := X' ×_X X' are again surjections in 𝓜: with a coproduct of open embeddings they are coproducts of open embeddings (pieces the preimages of the other factor's pieces) and surjective (IsFibreProduct.isCoprodOfOpenEmbeddings_fst/_snd, surjective_fst/_snd), the pull-back data along the two projections agree (isPullbackOf_pullback_fst_snd), and coproducts of open embeddings compose (IsCoprodOfOpenEmbeddings.comp). (iii) The convention of [Kol07, 32] for the descended list: a list whose pull-back along a surjective local analytic isomorphism has no empty centre has none (noEmptyCenters_of_pullback_of_surjective).

[Kol07, 32] for the descended list

theorem AnalyticManifold.BlowUpSequence.noEmptyCenters_of_pullback_of_surjective {𝕜 : 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) : Function.Surjective ⇑h → (L.pullback h hh).NoEmptyCenters → L.NoEmptyCenters

A list whose pull-back along a surjective local analytic isomorphism has no empty centre has none (the centres pull back to their preimages, empty only if empty).

Coproducts of open embeddings

theorem Manifold.IsCoprodOfOpenEmbeddings.comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N P : AnalyticManifold 𝕜 E} {h : AnalyticMap N M} {k : AnalyticMap P N} (hh : IsCoprodOfOpenEmbeddings h) (hk : IsCoprodOfOpenEmbeddings k) : IsCoprodOfOpenEmbeddings (ContMDiffMap.comp h k)

Coproducts of open embeddings compose (pieces Vⱼ ∩ k⁻¹(Uᵢ)).

theorem Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithSurjectiveLocalIsos.commutesWithSurjectionsIn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} {B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} (hB : B.CommutesWithSurjectiveLocalIsos) (𝓜 : {M N : AnalyticManifold 𝕜 E} → AnalyticMap N M → Prop) : B.CommutesWithSurjectionsIn fun {M N : AnalyticManifold 𝕜 E} => 𝓜

A functor commuting with all surjective local analytic isomorphisms commutes with the surjections of any class.

The projections of a fibre product

theorem Manifold.IsFibreProduct.comp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) : ContMDiffMap.comp g₁ p₁ = ContMDiffMap.comp g₂ p₂

theorem Manifold.IsFibreProduct.surjective_fst {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) (hs : Function.Surjective ⇑g₂) : Function.Surjective ⇑p₁

theorem Manifold.IsFibreProduct.surjective_snd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) (hs : Function.Surjective ⇑g₁) : Function.Surjective ⇑p₂

theorem Manifold.IsFibreProduct.injOn_fst {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) {V : Set N₂.carrier} (hV : Set.InjOn (⇑g₂) V) : Set.InjOn (⇑p₁) (⇑p₂ ⁻¹' V)

theorem Manifold.IsFibreProduct.injOn_snd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) {U : Set N₁.carrier} (hU : Set.InjOn (⇑g₁) U) : Set.InjOn (⇑p₂) (⇑p₁ ⁻¹' U)

theorem Manifold.IsFibreProduct.isCoprodOfOpenEmbeddings_fst {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) (h₂ : IsCoprodOfOpenEmbeddings g₂) : IsCoprodOfOpenEmbeddings p₁

The proof of [Kol07, Theorem 105] (the two projections τ₁, τ₂ : X'' → X' are surjective and in 𝓜): the first projection of a fibre product with a coproduct of open embeddings is one — its pieces the preimages under p₂ of the pieces of g₂.

theorem Manifold.IsFibreProduct.isCoprodOfOpenEmbeddings_snd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) (h₁ : IsCoprodOfOpenEmbeddings g₁) : IsCoprodOfOpenEmbeddings p₂

theorem Manifold.IsFibreProduct.isPullbackOf_pullback_fst_snd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) {T : AnalyticTriple ψ₀ M} {T₁ : AnalyticTriple ψ₀ N₁} {T₂ : AnalyticTriple ψ₀ N₂} (h₁ : T₁.IsPullbackOf T g₁) (h₂ : T₂.IsPullbackOf T g₂) : (T₁.pullback p₁ ⋯).IsPullbackOf T₂ p₂

The pull-back data of T₁ along p₁ are the pull-back data of T₂ along p₂ when T₁, T₂ carry the pull-back data of T along g₁, g₂.

The disjoint union of a family of open embeddings

def Manifold.sigmaDescMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) : AnalyticMap (sigmaManifold N) M

The proof of [Kol07, Theorem 105]: the map ∐ᵢ Uₓᵢ → X induced by a family.

Equations

• Manifold.sigmaDescMap ι = ⟨fun (p : (Manifold.sigmaManifold N).carrier) => (ι p.fst) p.snd, ⋯⟩

theorem Manifold.sigmaDescMap_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (p : (sigmaManifold N).carrier) : (sigmaDescMap ι) p = (ι p.fst) p.snd

theorem Manifold.sigmaDescMap_comp_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (i : σ) : ContMDiffMap.comp (sigmaDescMap ι) (sigmaMk N i) = ι i

theorem Manifold.isLocalDiffeomorph_sigmaDescMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(ι i)) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(sigmaDescMap ι)

theorem Manifold.isCoprodOfOpenEmbeddings_sigmaDescMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), IsAnalyticOpenEmbedding (ι i)) : IsCoprodOfOpenEmbeddings (sigmaDescMap ι)

The induced map of a family of analytic open embeddings is a coproduct of open embeddings.

theorem Manifold.surjective_sigmaDescMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hcov : ⋃ (i : σ), Set.range ⇑(ι i) = Set.univ) : Function.Surjective ⇑(sigmaDescMap ι)

theorem Manifold.isSigmaOf_pullback_sigmaDescMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (T : AnalyticTriple ψ₀ M) (hι : ∀ (i : σ), IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(ι i)) (Ts : (i : σ) → AnalyticTriple ψ₀ (N i)) (hTs : ∀ (i : σ), (Ts i).IsPullbackOf T (ι i)) : (T.pullback (sigmaDescMap ι) ⋯).IsSigmaOf Ts (sigmaMk N)

The pull-back data along the induced map are the disjoint union of the pull-back data along the members of the family.

theorem Manifold.AnalyticTriple.exists_isLocalCover_of_globalizationData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {GT LT : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (D : GlobalizationData (fun {M : AnalyticManifold 𝕜 E} => GT) fun {M : AnalyticManifold 𝕜 E} => LT) (T : AnalyticTriple ψ₀ M) (hG : GT T) : ∃ (N : AnalyticManifold 𝕜 E) (T' : AnalyticTriple ψ₀ N) (g : AnalyticMap N M), IsLocalCover (fun {M : AnalyticManifold 𝕜 E} => GT) (fun {M : AnalyticManifold 𝕜 E} => LT) T T' g

The first step of the proof of [Kol07, Theorem 105]: under clause (2), every global triple has a local cover by a local triple — the disjoint union of countably many of the local triples over its points (second countability), with the induced map.

Local cover data (generalisation, in place)

structure Manifold.AnalyticTriple.LocalCoverData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (GT LT : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop) : Prop

The single hypothesis the construction of [Kol07, Theorem 105] uses: every global triple has a local cover by a local triple. GlobalizationData supplies it through exists_isLocalCover_of_globalizationData (toLocalCoverData); the classes of the global case of the proof of [Kol07, Theorem 103] (BOClass, not closed under countable disjoint unions) supply it directly (localCoverData_localMCClass).

• exists_isLocalCover {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) : GT T → ∃ (N : AnalyticManifold 𝕜 E) (T' : AnalyticTriple ψ₀ N) (g : AnalyticMap N M), IsLocalCover (fun {M : AnalyticManifold 𝕜 E} => GT) (fun {M : AnalyticManifold 𝕜 E} => LT) T T' g

  Every global triple has a local cover.

theorem Manifold.AnalyticTriple.GlobalizationData.toLocalCoverData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {GT LT : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (D : GlobalizationData (fun {M : AnalyticManifold 𝕜 E} => GT) fun {M : AnalyticManifold 𝕜 E} => LT) : LocalCoverData (fun {M : AnalyticManifold 𝕜 E} => GT) fun {M : AnalyticManifold 𝕜 E} => LT

Clause (2) of [Kol07, Theorem 105] provides the local cover data (step (i) of its proof).