The model transport of an analytic manifold

The manifold-level analytic main theorems (at the ends of Hironaka/Resolution/Analytic/Wlo09/HironakaAssembly.lean and Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean) take a manifold M : AnalyticManifold ℝ E for any finite-dimensional real E, while the resolution (resolveFam) is built at the standard model Fin n → 𝕜 with the chart isomorphism ContinuousLinearEquiv.refl. The proofs therefore carry M to the standard model along a linear isomorphism ψ : E ≃L[ℝ] (Fin (finrank ℝ E) → ℝ) (ContinuousLinearEquiv.ofFinrankEq), run the resolution there, and carry the resulting family and its clauses back (Hironaka/Resolution/Analytic/ModelTransport/, of which this module is the first layer: the manifold itself).

M.transport ψ is M re-modelled on E': the same carrier and topology (so the same compacts and opens), the charts composed with ψ (transportChartedSpace); it is an analytic manifold because the transition maps of the new atlas are ψ ∘ τ ∘ ψ⁻¹ for the transitions τ of M (isManifold_transportChartedSpace, Mathlib's isManifold_of_contDiffOn with ψ.contDiff.comp_contDiffOn); Mathlib's own ModelWithCorners.transContinuousLinearEquiv changes the model with corners keeping the charts, whereas AnalyticManifold 𝕜 E' has charts into E' and the model 𝓘(𝕜, E'). The identity M → M.transport ψ is an analytic isomorphism across the two models (transportDiffeomorph, a Diffeomorph 𝓘(𝕜, E) 𝓘(𝕜, E')): in the charts it is ψ. Consequences: analyticity into or out of the re-modelled manifold is analyticity of the composite with the identity (contMDiff_transport_source_iff, contMDiff_transport_target_iff); the maximal atlas of the re-modelled manifold is the maximal atlas of M composed with ψ (mem_maximalAtlas_transport_iff, exists_trans_of_mem_maximalAtlas_transport, through the conjugation of the analytic groupoid trans_mem_contDiffGroupoid_iff); the identity of an open subset U is an analytic isomorphism between M.restrict U and (M.transport ψ).restrict U (restrictTransportDiffeomorph, the stage-0 identification of the transported successions of Hironaka/Resolution/Analytic/ModelTransport/Succession.lean).

A type ascription (x : M.transport ψ) on a point x : M is dropped by Lean when the two carriers are definitionally equal, after which instance search for ChartedSpace E' on the carrier of M fails; every statement therefore goes through the identities with their declared types (toTransport, ofTransport, transportOpens, restrictToTransport, restrictOfTransport).

@[instance_reducible]

def AnalyticManifold.transportChartedSpace {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : ChartedSpace E' M.carrier

The charts of M composed with the linear isomorphism ψ: the charted-space structure on the points of M modelled on E', chartAt x := (chartAt E x) ≫ₕ ψ.

Equations

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

theorem Hironaka.Manifold.isManifold_transportChartedSpace {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : IsManifold (modelWithCornersSelf 𝕜 E') ⊤ M.carrier

The charts composed with ψ are analytically compatible: their transition maps are ψ ∘ (transition of M) ∘ ψ⁻¹ (Mathlib's isManifold_of_contDiffOn with ψ.contDiff.comp_contDiffOn).

def AnalyticManifold.transport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : AnalyticManifold 𝕜 E'

M re-modelled on E' along ψ: the same points, the same topology (hence the same compacts and opens), the charts composed with ψ. The analytic main theorems carry their M : AnalyticManifold ℝ E to Fin (finrank ℝ E) → ℝ along ContinuousLinearEquiv.ofFinrankEq, run the resolution there, and carry the family back (Hironaka/Resolution/Analytic/ModelTransport/Family.lean).

Equations

• M.transport ψ = { carrier := M.carrier, top := M.top, charted := M.transportChartedSpace ψ, manifold := ⋯, t2 := ⋯, secondCountable := ⋯ }

def AnalyticManifold.toTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : M.carrier → (M.transport ψ).carrier

The identity M → M.transport ψ with its declared type (a type ascription on x : M is dropped when the two carriers are definitionally equal, and instance search then fails).

Equations

• M.toTransport ψ x = x

def AnalyticManifold.ofTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : (M.transport ψ).carrier → M.carrier

The identity M.transport ψ → M with its declared type.

Equations

• M.ofTransport ψ x = x

theorem AnalyticManifold.chartAt_transport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (x : M.carrier) : chartAt E' (M.toTransport ψ x) = (chartAt E x).trans ψ.toHomeomorph.toOpenPartialHomeomorph

The chart of the re-modelled manifold at a point.

theorem AnalyticManifold.contMDiff_toTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') ⊤ (M.toTransport ψ)

The identity M → M.transport ψ is analytic: in the charts it is ψ (contMDiffWithinAt_iff', the chart representative agrees with ψ on the chart's target).

theorem AnalyticManifold.contMDiff_ofTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ (M.ofTransport ψ)

The identity M.transport ψ → M is analytic: in the charts it is ψ⁻¹.

def AnalyticManifold.transportDiffeomorph {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') M.carrier (M.transport ψ).carrier ⊤

The identity M → M.transport ψ as an analytic isomorphism across the two models (Mathlib's Diffeomorph takes two models with corners). Every transport of this directory is a transport along such an isomorphism.

Equations

• M.transportDiffeomorph ψ = { toFun := M.toTransport ψ, invFun := M.ofTransport ψ, left_inv := ⋯, right_inv := ⋯, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

theorem AnalyticManifold.coe_transportDiffeomorph {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : ⇑(M.transportDiffeomorph ψ) = M.toTransport ψ

The isomorphism is the identity on points.

theorem AnalyticManifold.coe_transportDiffeomorph_symm {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') : ⇑(M.transportDiffeomorph ψ).symm = M.ofTransport ψ

Its inverse is the identity on points.

theorem Hironaka.Manifold.contMDiff_transport_source_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {ψ : E ≃L[𝕜] E'} {H : Type u_3} {F : Type u_4} [TopologicalSpace H] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {I : ModelWithCorners 𝕜 F H} {P : Type u_5} [TopologicalSpace P] [ChartedSpace H P] {f : (M.transport ψ).carrier → P} : ContMDiff (modelWithCornersSelf 𝕜 E') I ⊤ f ↔ ContMDiff (modelWithCornersSelf 𝕜 E) I ⊤ (f ∘ ⇑(M.transportDiffeomorph ψ))

Analyticity out of the re-modelled manifold.

theorem Hironaka.Manifold.contMDiff_transport_target_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {ψ : E ≃L[𝕜] E'} {H : Type u_3} {F : Type u_4} [TopologicalSpace H] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {I : ModelWithCorners 𝕜 F H} {P : Type u_5} [TopologicalSpace P] [ChartedSpace H P] {f : P → M.carrier} : ContMDiff I (modelWithCornersSelf 𝕜 E') ⊤ (⇑(M.transportDiffeomorph ψ) ∘ f) ↔ ContMDiff I (modelWithCornersSelf 𝕜 E) ⊤ f

Analyticity into the re-modelled manifold.

theorem Hironaka.Manifold.trans_mem_contDiffGroupoid_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (ψ : E ≃L[𝕜] E') (g : OpenPartialHomeomorph E E) : ψ.toHomeomorph.toOpenPartialHomeomorph.symm.trans (g.trans ψ.toHomeomorph.toOpenPartialHomeomorph) ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 E') ↔ g ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 E)

Conjugating an analytic transition of E by ψ gives an analytic transition of E': membership in the analytic groupoid is preserved.

theorem Hironaka.Manifold.mem_maximalAtlas_transport_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (φ : OpenPartialHomeomorph M.carrier E) : φ.trans ψ.toHomeomorph.toOpenPartialHomeomorph ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E') ⊤ (M.transport ψ).carrier ↔ φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier

A chart of M composed with ψ is in the maximal atlas of the re-modelled manifold iff the chart is in the maximal atlas of M.

theorem Hironaka.Manifold.exists_trans_of_mem_maximalAtlas_transport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (φ' : OpenPartialHomeomorph (M.transport ψ).carrier E') (h : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E') ⊤ (M.transport ψ).carrier) : ∃ φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier, φ' = φ.trans ψ.toHomeomorph.toOpenPartialHomeomorph

Every chart of the maximal atlas of the re-modelled manifold is a chart of M composed with ψ.

@[reducible, inline]

abbrev AnalyticManifold.transportOpens {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (U : TopologicalSpace.Opens M.carrier) : TopologicalSpace.Opens (M.transport ψ).carrier

An open set of M as an open set of the re-modelled M (the same set, the same topology), with its declared type, so that the instances of the re-modelled manifold are found.

Equations

• M.transportOpens ψ U = { carrier := ↑U, is_open' := ⋯ }

def AnalyticManifold.restrictToTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (U : TopologicalSpace.Opens M.carrier) : (M.restrict U).carrier → ((M.transport ψ).restrict (M.transportOpens ψ U)).carrier

The identity of U, from the restriction of M to the restriction of the re-modelled M.

Equations

• M.restrictToTransport ψ U q = ⟨M.toTransport ψ ↑q, ⋯⟩

def AnalyticManifold.restrictOfTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (U : TopologicalSpace.Opens M.carrier) : ((M.transport ψ).restrict (M.transportOpens ψ U)).carrier → (M.restrict U).carrier

The identity of U, back.

Equations

• M.restrictOfTransport ψ U q = ⟨M.ofTransport ψ ↑q, ⋯⟩

theorem AnalyticManifold.contMDiff_restrictToTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (U : TopologicalSpace.Opens M.carrier) : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') ⊤ (M.restrictToTransport ψ U)

The identity of U is analytic into the re-modelled restriction (Mathlib's liftPropWithinAt_subtypeVal_comp_iff).

theorem AnalyticManifold.contMDiff_restrictOfTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (U : TopologicalSpace.Opens M.carrier) : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ (M.restrictOfTransport ψ U)

The identity of U, back, is analytic.

def AnalyticManifold.restrictTransportDiffeomorph {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (U : TopologicalSpace.Opens M.carrier) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (M.restrict U).carrier ((M.transport ψ).restrict (M.transportOpens ψ U)).carrier ⊤

The identity of the open subset U, between the restriction of M and the restriction of the re-modelled M, as an analytic isomorphism across the models: the stage-0 identification of the transported successions (Hironaka/Resolution/Analytic/ModelTransport/Succession.lean).

Equations

• M.restrictTransportDiffeomorph ψ U = { toFun := M.restrictToTransport ψ U, invFun := M.restrictOfTransport ψ U, left_inv := ⋯, right_inv := ⋯, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

theorem AnalyticManifold.coe_restrictTransportDiffeomorph {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (U : TopologicalSpace.Opens M.carrier) : ⇑(M.restrictTransportDiffeomorph ψ U) = M.restrictToTransport ψ U

The isomorphism is the identity on points.

theorem AnalyticManifold.restrictTransportDiffeomorph_apply_val {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (M : AnalyticManifold 𝕜 E) (ψ : E ≃L[𝕜] E') (U : TopologicalSpace.Opens M.carrier) (q : (M.restrict U).carrier) : ↑((M.restrictTransportDiffeomorph ψ U) q) = M.toTransport ψ ↑q

The point of M.transport ψ under the isomorphism.