Disjoint unions of triples, and the unfolding of the commutation predicates

• The inclusion sigmaMk N i of a piece into the disjoint union sigmaManifold N is an analytic open embedding (isLocalDiffeomorph_sigmaMk: the local inverse is the projection to the piece on the open range, analytic because its composite with the inclusion is the identity, contMDiffAt_sigmaMk_comp_iff); a triple on the disjoint union whose data restrict along the inclusions to given triples on the pieces is their disjoint union (isSigmaOf_sigma, [Kol07, Warning 38]); the class of all triples is closed under disjoint unions.
• The equations of the push-forward of lists on nil and its length (pushforward_nil, length_pushforward; [Kol07, Definition 30, 30.3]).
• The unfolding lemmas of the two commutation classes of [Kol07, 34.1], the commutation with a composite (commutesWith_comp) and its converse along a surjective local isomorphism (commutesWith_of_surjective_comp, the "(34.1) is a local property" of the proof of [Kol07, Theorem 36]).

noncomputable def Manifold.sigmaProj {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (i : σ) (x : (N i).carrier) : (sigmaManifold N).carrier → (N i).carrier

The projection of the disjoint union onto the i-th piece, x on the other pieces.

Equations

• Manifold.sigmaProj N i x p = if h : p.fst = i then h ▸ p.snd else x

theorem Manifold.sigmaProj_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (i : σ) (x y : (N i).carrier) : sigmaProj N i x ((sigmaMk N i) y) = y

noncomputable def Manifold.sigmaMkPartialDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (i : σ) (x : (N i).carrier) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (N i).carrier (sigmaManifold N).carrier ⊤

The local inverse of the inclusion sigmaMk N i: the projection on the open range.

Equations

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

theorem Manifold.isLocalDiffeomorph_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (i : σ) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(sigmaMk N i)

The inclusion of a piece into the disjoint union is a local analytic isomorphism.

theorem Manifold.isAnalyticOpenEmbedding_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (i : σ) : IsAnalyticOpenEmbedding (sigmaMk N i)

The inclusion of a piece is an analytic open embedding.

theorem Manifold.AnalyticTriple.isSigmaOf_sigma {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (T : AnalyticTriple ψ₀ (sigmaManifold N)) (Ts : (i : σ) → AnalyticTriple ψ₀ (N i)) (hTs : ∀ (i : σ), (Ts i).IsPullbackOf T (sigmaMk N i)) : T.IsSigmaOf Ts (sigmaMk N)

[Kol07, Warning 38]: a triple on the disjoint union whose data restrict along the inclusions to given triples on the pieces is their disjoint union.

theorem Manifold.AnalyticTriple.closedUnderSigma_univ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} : ClosedUnderSigma fun {x : AnalyticManifold 𝕜 E} (x_1 : AnalyticTriple ψ₀ x) => True

[Kol07, Warning 38]: the class of all triples is closed under countable disjoint unions.

[Kol07, Definition 30, 30.3] on lists: the equations of pushforward

theorem AnalyticManifold.BlowUpSequence.length_pushforwardAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : Manifold.PushforwardStage ψ s Tᵢ) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Tᵢ) : (pushforwardAux P L).length = L.length

theorem AnalyticManifold.BlowUpSequence.pushforward_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S s) : pushforward hS (nil hS.toAnalyticManifold) = nil M

theorem AnalyticManifold.BlowUpSequence.length_pushforward {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S s) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hS.toAnalyticManifold) : (pushforward hS L).length = L.length

The unfolding of 34.1's classes

theorem Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithSurjectiveLocalIsos.commutesWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} {M N : AnalyticManifold 𝕜 E} {B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} (hB : B.CommutesWithSurjectiveLocalIsos) {T : AnalyticTriple ψ₀ M} {T' : AnalyticTriple ψ₀ N} {h : AnalyticMap N M} (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) (hT' : T'.IsPullbackOf T h) : B.CommutesWith T T' h hh

theorem Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithOpenEmbeddings.seq_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} {M N : AnalyticManifold 𝕜 E} {B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} (hB : B.CommutesWithOpenEmbeddings) {T : AnalyticTriple ψ₀ M} {T' : AnalyticTriple ψ₀ N} {h : AnalyticMap N M} (hh : IsAnalyticOpenEmbedding h) (hT' : T'.IsPullbackOf T h) (hT : Dom T) (hT'' : Dom T') : B.seq T' hT'' = ((B.seq T hT).pullback h ⋯).eraseEmpty

theorem Manifold.AnalyticBlowUpSequenceAssignment.commutesWith_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} {M N : AnalyticManifold 𝕜 E} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) {P : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {T' : AnalyticTriple ψ₀ N} {T'' : AnalyticTriple ψ₀ P} {h : AnalyticMap N M} {hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h} {k : AnalyticMap P N} {hk : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k} (hT' : Dom T') (h₁ : B.CommutesWith T T' h hh) (h₂ : B.CommutesWith T' T'' k hk) : B.CommutesWith T T'' (ContMDiffMap.comp h k) ⋯

[Kol07, 34.1] with 30.1's functoriality: a functor commutes with a composite of maps it commutes with, the middle triple in the class.

theorem Manifold.AnalyticBlowUpSequenceAssignment.commutesWith_of_surjective_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} {M N : AnalyticManifold 𝕜 E} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) {P : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {T' : AnalyticTriple ψ₀ N} {T'' : AnalyticTriple ψ₀ P} {h : AnalyticMap N M} (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {g : AnalyticMap P N} (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hgs : Function.Surjective ⇑g) (hT'' : Dom T'') (h₁ : B.CommutesWith T' T'' g hg) (h₂ : B.CommutesWith T T'' (ContMDiffMap.comp h g) ⋯) : B.CommutesWith T T' h hh

The proof of [Kol07, Theorem 36] ("(34.1) is a local property"): if B commutes with a surjective local analytic isomorphism g : P → N and with h ∘ g, it commutes with h : N → M.