Tangent-bundle trivializations, coordinate changes on T(TM), and open submanifolds

The canonical tangent-bundle trivialization at a point x is built from the chart at x, so on the fibre over x itself it is the identity. This file records that fact in both directions, and notes that reading a tangent vector through the preferred trivializations of two charts is the tangent coordinate change between them, which is C^n in the base point. Consequently the differential of the preferred chart at x undoes the extension FiberBundle.extend of a tangent vector at x, so differentiating a function along that extension near x is differentiating its coordinate expression.

It then computes the coordinate changes of the tangent bundle of the tangent bundle: a tangent vector (u, w) to TM at a point with x-coordinates u, read in the tangent-bundle chart centred at the zero vector over x₀, has base component the tangent coordinate change of u, and fibre component the product-rule sum of the derivative of that coordinate change in the base point and the coordinate change applied to w. This is the transformation law obeyed by a second-order vector field on TM, such as a geodesic spray, when it is carried between tangent-bundle charts.

It then identifies the tangent spaces of an open submanifold with those of its ambient manifold and shows that, near each point, the inverse tangent-bundle trivializations agree under that identification.

It then identifies the tangent space of a product manifold with the product of the tangent spaces of the factors, and shows that under this identification tangent coordinate changes and inverse tangent-bundle trivializations act componentwise. Finally, the charts of a disjoint union are those of its summands, so its tangent coordinate changes are those of the summands.

Main results

• TangentBundle.extChartAt_symm_mem_trivializationAt_baseSet: the inverse of the extended chart at x maps its target into the base set of the canonical trivialization at x.
• TangentBundle.chartFrame: the canonical tangent trivialization of the intrinsic chart source at its centre, which covers the whole source.
• TangentBundle.mdifferentiableAt_trivializationAt_symm_apply and TangentBundle.trivializationAt_symm_apply_self: a vector field with constant coordinates in the canonical trivialization at x is differentiable at x and takes the value u there.
• TauCeti.Manifold.mfderiv_atlas_eq_continuousLinearMapAt: the derivative of an atlas chart is the actual continuous linear map of its tangent-core trivialization.
• TauCeti.Manifold.continuousLinearMapAt_trivializationAt_self and TauCeti.Manifold.symmL_trivializationAt_self: the canonical trivialization at x and its inverse act as the identity on the fibre over x.
• TauCeti.Manifold.extend_eq_trivializationAt_symm: the extension of a tangent vector w at x is the vector field with constant coordinates w in the canonical trivialization at x.
• TauCeti.Manifold.inTangentCoordinates_eq_self_of_eq: a field of linear maps read in the tangent coordinates of a point with the same base points is unchanged, and TauCeti.Manifold.inCoordinates_tangentSpace_self is the same statement for a single map.
• TauCeti.Manifold.localFrame_trivializationAt_self: consequently its local frame at x is the chosen basis of the model space.
• TauCeti.Manifold.inverse_mfderiv_extChartAt: the inverse of the differential of an extended chart is the inverse of the canonical tangent-bundle trivialization at its centre.
• TauCeti.Manifold.mfderiv_extChartAt_extend: the differential of the preferred chart at x sends the extension FiberBundle.extend E w of a tangent vector at x back to w.
• TauCeti.Manifold.mvfderiv_extend_eventuallyEq: consequently, near x, differentiating a function along that extension is differentiating its coordinate expression along w.
• TauCeti.Manifold.contDiffOn_tangentCoordChange: the tangent coordinate change between the charts at two points is C^n on the overlap of their sources, read in the chart at the first point.
• TauCeti.Manifold.contMDiffAt_tangentCoordChange: that coordinate change is C^n at the base point of its first chart, as a map of manifolds into the linear endomorphisms of the model space.
• TauCeti.Manifold.tangentCoordChange_tangent_apply: the coordinate-change formula on the tangent bundle of the tangent bundle.
• TauCeti.Manifold.continuousLinearMapAt_symmL_coordChange: reading a tangent vector through the preferred trivializations of two charts is the tangent coordinate change between them.
• TauCeti.Manifold.tangentCoordChange_toMatrix: in a finite basis, this coordinate change is the change-of-basis matrix between the corresponding chart-local frames.
• TauCeti.Manifold.tangentSpaceOpenEquiv: the canonical continuous linear equivalence between the tangent space of an open submanifold and the ambient tangent space.
• TauCeti.Manifold.mfderiv_subtype_val: the differential of the inclusion is the canonical tangent-space equivalence.
• TauCeti.Manifold.tangentMap_subtype_val: the tangent map of the inclusion under this equivalence.
• TauCeti.Manifold.mvfderiv_subtype_val_apply and TauCeti.Manifold.injective_mvfderiv_subtype_val: for an open subset of a normed space, the derivative of the inclusion, read in the normed space, fixes each tangent vector.
• TauCeti.Manifold.tangentSpaceOpenEquiv_mfderiv_apply: under this equivalence, the differential of a map between open submanifolds is that of any ambient map it restricts.
• TauCeti.Manifold.instT2SpaceTangentBundleModelSpace: a model space has a Hausdorff tangent bundle. It is an instance in the TauCeti scope, for model spaces H whose Hausdorffness is not already an instance; over a Hausdorff manifold the tangent bundle is Hausdorff by the general instance TauCeti.FiberBundle.t2Space_totalSpace.
• TauCeti.Manifold.eventually_tangentSpaceOpenEquiv_symmL_trivializationAt_eq: near a point, the inverse tangent-bundle trivializations agree through this equivalence.
• TauCeti.Manifold.restrictOpenTangentSpaceBilinear: restriction of a field of bilinear maps on the tangent spaces to an open submanifold, and TauCeti.Manifold.contMDiffAt_restrictOpenTangentSpaceBilinear: restriction preserves C^n regularity.
• TauCeti.Manifold.tangentSpaceProdEquiv: the canonical continuous linear equivalence between the tangent space of a product and the product of the tangent spaces.
• TauCeti.Manifold.mfderiv_prodMap_apply: differentials of product maps act componentwise under this equivalence.
• TauCeti.Manifold.isInvertible_mfderiv_prodMap: the differential of a product map is invertible where the differentials of both factors are.
• TauCeti.Manifold.contMDiff_prod_right_comm and TauCeti.Manifold.isInvertible_mfderiv_prod_right_comm: the map ((x, y), z) ↦ ((x, z), y) exchanging the last two factors of a triple product is smooth with invertible differential.
• TauCeti.Manifold.tangentSpaceProdEquiv_mfderiv_prodMap_id and TauCeti.Manifold.isInvertible_mfderiv_prodMap_id: the differential of (x, t) ↦ (x, φ t) on M × 𝕜 multiplies the 𝕜-component by φ' t, so it is invertible where φ' t ≠ 0.
• TauCeti.Manifold.isInvertible_mfderiv_prodMap_id_subtypeVal_Icc: the differential of the inclusion M × [a, b] → M × ℝ is invertible, also at the boundary.
• TauCeti.Manifold.tangentCoordChange_prod: the tangent coordinate change of a product is the product of the tangent coordinate changes of the factors.
• TauCeti.Manifold.tangentSpaceProdEquiv_symmL_trivializationAt: the inverse tangent-bundle trivialization of a product is the product of those of the factors.
• TauCeti.Manifold.tangentCoordChange_sumInl and TauCeti.Manifold.tangentCoordChange_sumInr: the tangent coordinate changes of a disjoint union between charts at points of one summand are those of that summand.
• TauCeti.Manifold.symmL_trivializationAt_sumInl and TauCeti.Manifold.symmL_trivializationAt_sumInr: so are its inverse tangent-bundle trivializations.

theorem TangentBundle.trivializationAt_apply_tangentCoordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x y : M} (v : TangentSpace I y) : (↑(trivializationAt E (TangentSpace I) x) ⟨y, v⟩).2 = (tangentCoordChange I y x y) v

The fibre coordinate of the canonical tangent-bundle trivialization is the tangent coordinate change. Keeping this representation bridge named avoids making consumers unfold the chart extension when they move between the two APIs.

theorem TangentBundle.extChartAt_symm_mem_trivializationAt_baseSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x : M} {z : E} (hz : z ∈ (extChartAt I x).target) : ↑(extChartAt I x).symm z ∈ (trivializationAt E (TangentSpace I) x).baseSet

The inverse of the extended chart at x sends its target into the base set of the canonical tangent-bundle trivialization at x.

theorem TangentBundle.trivializationAt_chartSource_baseSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) : (trivializationAt E (TangentSpace I) ⟨x, ⋯⟩).baseSet = Set.univ

The canonical tangent trivialization of an intrinsic chart source covers that whole source.

@[reducible, inline]

noncomputable abbrev TangentBundle.chartFrame {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) : Bundle.Trivialization E Bundle.TotalSpace.proj

The tangent frame of the intrinsic chart source at its centre; it covers the whole source (TangentBundle.trivializationAt_chartSource_baseSet).

@[simp]

theorem TangentBundle.coe_chartAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {p q : TangentBundle I M} : (↑(chartAt (ModelProd H E) q) p).2 = (tangentCoordChange I p.proj q.proj p.proj) p.snd

The second component of the chart of a tangent bundle at q, read at a point with base point in the chart source. Together with TangentBundle.coe_chartAt_fst this describes the tangent-bundle charts completely.

theorem TauCeti.Manifold.mfderiv_atlas_eq_continuousLinearMapAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (e : ↑(atlas H M)) {x : M} (hx : x ∈ (↑e).source) : mfderiv% ↑↑e x = Bundle.Trivialization.continuousLinearMapAt 𝕜 ((tangentBundleCore I M).localTriv e) x

The derivative of an atlas chart reads tangent vectors in that chart's core trivialization.

@[simp]

theorem TauCeti.Manifold.continuousLinearMapAt_trivializationAt_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) (v : TangentSpace I x) : (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x) x) v = v

Read in the canonical trivialization at x, a tangent vector at x itself is its own coordinate vector: the trivialization is built from the chart at x, whose transition function with itself has derivative the identity.

@[simp]

theorem TauCeti.Manifold.symmL_trivializationAt_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) (v : E) : (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) x) v = v

The inverse form of TauCeti.Manifold.continuousLinearMapAt_trivializationAt_self: over its own base point, the inverse of the canonical trivialization is the identity.

@[simp]

theorem TangentBundle.trivializationAt_symm_apply_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) (u : E) : (trivializationAt E (TangentSpace I) x).symm x u = u

The vector field with constant coordinates u in the trivialization of the tangent bundle at x takes the value u at x.

theorem TauCeti.Manifold.extend_eq_trivializationAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x : M} (w : TangentSpace I x) : FiberBundle.extend E w = fun (y : M) => (trivializationAt E (TangentSpace I) x).symm y w

The extension FiberBundle.extend E w of a tangent vector w at x is the vector field with constant coordinates w in the canonical trivialization of the tangent bundle at x.

theorem TangentBundle.mdifferentiableAt_trivializationAt_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) (u : E) : (MDiffAt fun (y : M) => ⟨y, (trivializationAt E (TangentSpace I) x).symm y u⟩) x

The vector field with constant coordinates u in the trivialization of the tangent bundle at x is differentiable at x.

theorem TauCeti.Manifold.inTangentCoordinates_eq_self_of_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} {N : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] (f : N → M) (g : N → M') (ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)) {x₀ x : N} (hf : f x = f x₀) (hg : g x = g x₀) : inTangentCoordinates I I' f g ϕ x₀ x = ϕ x

At a point x whose base points f x and g x agree with those of x₀, reading ϕ x in the tangent coordinates of x₀ changes nothing: both coordinate changes are from a chart to itself.

@[simp]

theorem TauCeti.Manifold.inCoordinates_tangentSpace_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] (x : M) (y : M') (ϕ : TangentSpace I x →L[𝕜] TangentSpace I' y) : ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') x x y y ϕ = ϕ

A linear map between tangent spaces, read in the canonical trivializations at its own base points, is unchanged.

theorem TauCeti.Manifold.inverse_mfderiv_extChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x₀ : M) {x : M} (hx : x ∈ (extChartAt I x₀).source) : (mfderiv% ↑(extChartAt I x₀) x).inverse = Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x₀) x

The differential of the extended chart at x₀, at a point x of its source, is inverted by the inverse of the canonical tangent-bundle trivialization at x₀. This is the inverse form of TangentBundle.symmL_trivializationAt.

theorem TauCeti.Manifold.mfderiv_extChartAt_extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x y : M} (w : TangentSpace I x) (hy : y ∈ (chartAt H x).source) : (mfderiv% ↑(extChartAt I x) y) (FiberBundle.extend E w y) = w

On the source of the preferred chart at x, the derivative of extChartAt I x sends the extension FiberBundle.extend E w of a tangent vector w at x back to w.

theorem TauCeti.Manifold.mvfderiv_extend_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x : M} [I.Boundaryless] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : M → F} (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 F) 1 f x) (w : TangentSpace I x) : (fun (y : M) => (d% f y) (FiberBundle.extend E w y)) =ᶠ[nhds x] (fun (z : E) => (fderiv 𝕜 (f ∘ ↑(extChartAt I x).symm) z) w) ∘ ↑(extChartAt I x)

Near x, the derivative of a C¹ function f along the extension of a tangent vector w at x is the derivative of the coordinate expression of f along w, read through the preferred chart.

theorem TauCeti.Manifold.contDiffOn_trivializationAt_extChartAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (v : (x : M) → TangentSpace I x) (a : M) {V : Set M} : ContMDiffOn I I.tangent n (fun (x : M) => ⟨x, v x⟩) V → ContDiffOn 𝕜 n (fun (z : E) => (↑(trivializationAt E (TangentSpace I) a) ⟨↑(extChartAt I a).symm z, v (↑(extChartAt I a).symm z)⟩).2) (interior (extChartAt I a).target ∩ ↑(extChartAt I a).symm ⁻¹' V)

If a tangent vector field is C^n on V, then its coordinate expression in the preferred trivialization of the tangent bundle at a, read through the inverse extended chart, is C^n on the interior points of the chart target which lie over V.

theorem TauCeti.Manifold.contDiffOn_tangentCoordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (x y : M) : ContDiffOn 𝕜 n (fun (a : E) => tangentCoordChange I x y (↑(extChartAt I x).symm a)) ((extChartAt I x).symm.trans (extChartAt I y)).source

The tangent coordinate change between the charts at x and y is C^n on the overlap of the two chart sources, read in the chart at x. This is Mathlib's contDiffOn_fderiv_coord_change for the preferred charts at two points.

theorem TauCeti.Manifold.contMDiffAt_tangentCoordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {x y : M} (hy : x ∈ (extChartAt I y).source) : ContMDiffAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] E)) n (tangentCoordChange I x y) x

The tangent coordinate change between the charts at x and y is C^n at x, as a map of manifolds into the continuous linear endomorphisms of the model space.

Coordinate changes on the tangent of the tangent bundle

theorem TauCeti.Manifold.tangentCoordChange_tangent_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {x x₀ : M} (hx₀ : x ∈ (extChartAt I x₀).source) (u : TangentSpace I x) (w : E) : have v := (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x) x) u; (tangentCoordChange I.tangent ⟨x, u⟩ ⟨x₀, 0⟩ ⟨x, u⟩) (v, w) = ((tangentCoordChange I x x₀ x) v, ((d% fun (y : M) => (tangentCoordChange I x x₀ y) v) x) u + (tangentCoordChange I x x₀ x) w)

The tangent coordinate change on TM sends the tangent vector (v, w) at u ∈ TₓM to the derivative of the base coordinate change together with the product-rule expression for the fibre coordinate, where v is the coordinate of u in the preferred trivialization at x. The target chart is centred at the zero vector over x₀.

theorem TauCeti.Manifold.continuousLinearMapAt_symmL_coordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x x₀ y : M} (hyx : y ∈ (chartAt H x).source) (hyx₀ : y ∈ (chartAt H x₀).source) (u : E) : (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x₀) y) ((Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) y) u) = (tangentCoordChange I x x₀ y) u

The reading map of the preferred trivialization centred at x₀ sends the tangent vector at y whose x-coordinates are u to its x₀-coordinates.

theorem TauCeti.Manifold.tangentCoordChange_toMatrix {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (α β : M) (b : Module.Basis ι 𝕜 E) {x : M} (hα : x ∈ (trivializationAt E (TangentSpace I) α).baseSet) (hβ : x ∈ (trivializationAt E (TangentSpace I) β).baseSet) : (LinearMap.toMatrix b b) ↑(tangentCoordChange I α β x) = ((trivializationAt E (TangentSpace I) β).basisAt b hβ).toMatrix ⇑((trivializationAt E (TangentSpace I) α).basisAt b hα)

The matrix of a tangent coordinate change in a finite basis of the model space is the change-of-basis matrix between the corresponding chart-local frames.

@[simp]

theorem TauCeti.Manifold.localFrame_trivializationAt_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {ι : Type u_5} (b : Module.Basis ι 𝕜 E) (x : M) (i : ι) : (trivializationAt E (TangentSpace I) x).localFrame b i x = b i

Over its own base point, the local frame attached to the canonical trivialization at x is the given basis of the model space.

noncomputable def TauCeti.Manifold.tangentSpaceOpenEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) : TangentSpace I x ≃L[𝕜] TangentSpace I ↑x

The canonical identification between the tangent space of an open submanifold and the ambient tangent space. Both are Mathlib's type synonym for the common model vector space.

This is deliberately a named equivalence rather than ContinuousLinearEquiv.refl 𝕜 E: because TangentSpace is not reducible, a statement phrased with refl is type-correct only after unfolding it, so rw and simp fail on such statements. Mathlib introduces NormedSpace.fromTangentSpace for the analogous identification for the same reason.

@[simp]

theorem TauCeti.Manifold.tangentSpaceOpenEquiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) (v : TangentSpace I x) : (tangentSpaceOpenEquiv x) v = v

@[simp]

theorem TauCeti.Manifold.tangentSpaceOpenEquiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) (v : TangentSpace I ↑x) : (tangentSpaceOpenEquiv x).symm v = v

@[simp]

theorem TauCeti.Manifold.mfderiv_subtype_val {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) : mfderiv% Subtype.val x = ↑(tangentSpaceOpenEquiv x)

The differential of the inclusion of an open submanifold is the canonical tangent-space identification.

theorem TauCeti.Manifold.mfderiv_subtype_val_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (x : ↥U) : Function.Injective ⇑(mfderiv% Subtype.val x)

The differential of an open-submanifold inclusion is injective.

@[simp]

theorem TauCeti.Manifold.tangentMap_subtype_val {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} (p : TangentBundle I ↥U) : tangentMap I I Subtype.val p = ⟨↑p.proj, (tangentSpaceOpenEquiv p.proj) p.snd⟩

The tangent map of an open submanifold's inclusion identifies its tangent vectors with ambient tangent vectors through tangentSpaceOpenEquiv.

theorem TauCeti.Manifold.tangentSpaceOpenEquiv_mfderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {U : TopologicalSpace.Opens M} {V : TopologicalSpace.Opens M'} {f : ↥U → ↥V} {A : M → M'} {x : ↥U} (hf : MDiffAt f x) (hcomp : Subtype.val ∘ f = A ∘ Subtype.val) (v : TangentSpace I x) : (tangentSpaceOpenEquiv (f x)) ((mfderiv% f x) v) = (mfderiv% A ↑x) ((tangentSpaceOpenEquiv x) v)

If a differentiable map f between open submanifolds is the restriction of a map A of the ambient manifolds, then under the canonical tangent-space identifications the differential of f at x is the differential of A at x.

@[simp]

theorem TauCeti.Manifold.mfderiv_inclusion_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U V : TopologicalSpace.Opens M} (h : U ≤ V) (x : ↥U) (v : TangentSpace I x) : (mfderiv% (TopologicalSpace.Opens.inclusion h) x) v = v

The differential of the inclusion of nested open submanifolds is the identity of the common model vector space.

theorem TauCeti.Manifold.mvfderiv_subtype_val_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : TopologicalSpace.Opens E} (x : ↥U) (v : TangentSpace (modelWithCornersSelf 𝕜 E) x) : (d% Subtype.val x) v = v

The derivative of the inclusion of an open subset of a normed space, read in the normed space, maps each tangent vector to itself.

theorem TauCeti.Manifold.injective_mvfderiv_subtype_val {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : TopologicalSpace.Opens E} (x : ↥U) : Function.Injective ⇑(d% Subtype.val x)

The derivative of the inclusion of an open subset of a normed space, read in the normed space, is injective.

theorem TauCeti.Manifold.instT2SpaceTangentBundleModelSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} : T2Space (TangentBundle I H)

The tangent bundle of a model space is Hausdorff.

theorem TauCeti.Manifold.eventually_tangentSpaceOpenEquiv_symmL_trivializationAt_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {U : TopologicalSpace.Opens M} (x : ↥U) : ∀ᶠ (y : ↥U) in nhds x, ∀ (z : E), (tangentSpaceOpenEquiv y) ((Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) y) z) = (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) ↑x) ↑y) z

Near a point of an open submanifold, its inverse tangent-bundle trivialization agrees with the ambient inverse trivialization under the canonical tangent-space identification.

noncomputable def TauCeti.Manifold.restrictOpenTangentSpaceBilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (b : (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] F) (U : TopologicalSpace.Opens M) (x : ↥U) : TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] F

Restrict a field of continuous bilinear maps on the tangent spaces of M to an open submanifold U, through the canonical tangent-space identification.

@[simp]

theorem TauCeti.Manifold.restrictOpenTangentSpaceBilinear_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (b : (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] F) (U : TopologicalSpace.Opens M) (x : ↥U) (v w : TangentSpace I x) : ((restrictOpenTangentSpaceBilinear b U x) v) w = ((b ↑x) ((tangentSpaceOpenEquiv x) v)) ((tangentSpaceOpenEquiv x) w)

The restriction of a bilinear field to an open submanifold evaluates the ambient field through the canonical tangent-space identification.

theorem TauCeti.Manifold.contMDiffAt_restrictOpenTangentSpaceBilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IsManifold I 1 M] {n : WithTop ℕ∞} {b : (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] F} {U : TopologicalSpace.Opens M} {x : ↥U} (hb : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E →L[𝕜] F))) n (fun (y : M) => ⟨y, b y⟩) ↑x) : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E →L[𝕜] F))) n (fun (y : ↥U) => ⟨y, restrictOpenTangentSpaceBilinear b U y⟩) x

Restricting a bilinear field on the tangent bundle to an open submanifold preserves C^n regularity at a point.

noncomputable def TauCeti.Manifold.tangentSpaceProdEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (p : M × N) : TangentSpace (I.prod J) p ≃L[𝕜] TangentSpace I p.1 × TangentSpace J p.2

The canonical identification of the tangent space of a product manifold with the product of the tangent spaces of the factors. Both are Mathlib's type synonym for the product of the model vector spaces; as for tangentSpaceOpenEquiv, the identification is named so that statements using it are type-correct without unfolding TangentSpace.

@[simp]

theorem TauCeti.Manifold.tangentSpaceProdEquiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (p : M × N) (v : TangentSpace (I.prod J) p) : (tangentSpaceProdEquiv p) v = v

@[simp]

theorem TauCeti.Manifold.tangentSpaceProdEquiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (p : M × N) (v : TangentSpace I p.1 × TangentSpace J p.2) : (tangentSpaceProdEquiv p).symm v = v

theorem TauCeti.Manifold.mfderiv_prodMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_12} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] {f : M → M'} {g : N → N'} {p : M × N} (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) (v : TangentSpace I p.1 × TangentSpace J p.2) : (mfderiv% (Prod.map f g) p) ((tangentSpaceProdEquiv p).symm v) = (tangentSpaceProdEquiv (f p.1, g p.2)).symm ((mfderiv% f p.1) v.1, (mfderiv% g p.2) v.2)

The differential of a product map acts componentwise under the canonical identifications of the product tangent spaces.

theorem TauCeti.Manifold.isInvertible_mfderiv_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_12} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] {f : M → M'} {g : N → N'} {p : M × N} (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) (hf' : (mfderiv% f p.1).IsInvertible) (hg' : (mfderiv% g p.2).IsInvertible) : (mfderiv% (Prod.map f g) p).IsInvertible

The differential of a product map is invertible at a point where the differentials of both factors are invertible.

theorem TauCeti.Manifold.isInvertible_mfderiv_prodMap_id_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {p : M × N} (hf : MDiffAt f p.1) (hf' : (mfderiv% f p.1).IsInvertible) : (mfderiv% (Prod.map f id) p).IsInvertible

The differential of (x, y) ↦ (f x, y) is invertible at a point where the differential of f is invertible.

theorem TauCeti.Manifold.contMDiff_prod_right_comm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} : ContMDiff ((I.prod J).prod I') ((I.prod I').prod J) n fun (q : (M × N) × M') => ((q.1.1, q.2), q.1.2)

The map ((x, y), z) ↦ ((x, z), y), which exchanges the last two factors of a triple product, is smooth.

theorem TauCeti.Manifold.hasMFDerivAt_prod_right_comm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] (q : (M × N) × M') : HasMFDerivAt% (fun (q : (M × N) × M') => ((q.1.1, q.2), q.1.2)) q ↑((ContinuousLinearEquiv.prodAssoc 𝕜 E F E').trans (((ContinuousLinearEquiv.refl 𝕜 E).prodCongr (ContinuousLinearEquiv.prodComm 𝕜 F E')).trans (ContinuousLinearEquiv.prodAssoc 𝕜 E E' F).symm))

The differential of ((x, y), z) ↦ ((x, z), y) is the same exchange of the last two factors of the model space, assembled from Mathlib's product equivalences.

theorem TauCeti.Manifold.isInvertible_mfderiv_prod_right_comm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] (q : (M × N) × M') : ((mfderiv% fun (q : (M × N) × M') => ((q.1.1, q.2), q.1.2)) q).IsInvertible

The differential of ((x, y), z) ↦ ((x, z), y) is invertible.

theorem TauCeti.Manifold.mfderiv_prod_right_comm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] (q : (M × N) × M') (v : TangentSpace ((I.prod J).prod I') q) : ((mfderiv% fun (q : (M × N) × M') => ((q.1.1, q.2), q.1.2)) q) v = ((v.1.1, v.2), v.1.2)

The differential of ((x, y), z) ↦ ((x, z), y) moves the components of a tangent vector as the map moves the coordinates.

theorem TauCeti.Manifold.tangentSpaceProdEquiv_mfderiv_prodMap_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {φ : 𝕜 → 𝕜} {p : M × 𝕜} (hφ : DifferentiableAt 𝕜 φ p.2) (v : TangentSpace (I.prod (modelWithCornersSelf 𝕜 𝕜)) p) : (tangentSpaceProdEquiv (p.1, φ p.2)) ((mfderiv% (Prod.map id φ) p) v) = (((tangentSpaceProdEquiv p) v).1, (NormedSpace.fromTangentSpace (φ p.2)).symm (deriv φ p.2 * (NormedSpace.fromTangentSpace p.2) ((tangentSpaceProdEquiv p) v).2))

The differential of (x, t) ↦ (x, φ t) on M × 𝕜 fixes the M-component and multiplies the 𝕜-component by φ' t.

theorem TauCeti.Manifold.isInvertible_mfderiv_prodMap_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {φ : 𝕜 → 𝕜} {p : M × 𝕜} (hφ' : deriv φ p.2 ≠ 0) : (mfderiv% (Prod.map id φ) p).IsInvertible

If φ' t ≠ 0, the differential of (x, t) ↦ (x, φ t) on M × 𝕜 at (x, t) is invertible.

theorem TauCeti.Manifold.tangentCoordChange_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I 1 M] [IsManifold J 1 N] {p q z : M × N} (hz : z ∈ (extChartAt (I.prod J) p).source ∩ (extChartAt (I.prod J) q).source) : tangentCoordChange (I.prod J) p q z = (tangentCoordChange I p.1 q.1 z.1).prodMap (tangentCoordChange J p.2 q.2 z.2)

On the common domain of two product charts, the tangent coordinate change of a product manifold is the product of the tangent coordinate changes of the factors.

theorem TauCeti.Manifold.tangentSpaceProdEquiv_symmL_trivializationAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I 1 M] [IsManifold J 1 N] {p q : M × N} (hq : q ∈ (chartAt (ModelProd H G) p).source) (v : E × F) : (tangentSpaceProdEquiv q) ((Bundle.Trivialization.symmL 𝕜 (trivializationAt (E × F) (TangentSpace (I.prod J)) p) q) v) = ((Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) p.1) q.1) v.1, (Bundle.Trivialization.symmL 𝕜 (trivializationAt F (TangentSpace J) p.2) q.2) v.2)

Over the domain of the chart at p, the inverse of the canonical tangent-bundle trivialization of a product manifold at p is the product of the inverse trivializations of the factors.

theorem TauCeti.Manifold.symmL_trivializationAt_prod_model_space {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IsManifold I 1 M] {p q : M × F} (s s' : F) (v : E × F) : (Bundle.Trivialization.symmL 𝕜 (trivializationAt (E × F) (TangentSpace (I.prod (modelWithCornersSelf 𝕜 F))) p) q) v = (Bundle.Trivialization.symmL 𝕜 (trivializationAt (E × F) (TangentSpace (I.prod (modelWithCornersSelf 𝕜 F))) (p.1, s)) (q.1, s')) v

On a product M × F with a normed space F, the inverse of the canonical tangent-bundle trivialization at p, over a point q, depends neither on the F-coordinate of p nor on that of q. Both sides vanish when q lies outside the domain of the chart at p.

theorem TauCeti.Manifold.tangentCoordChange_sumInl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M] [IsManifold I 1 M'] (x y z : M) : tangentCoordChange I (Sum.inl x) (Sum.inl y) (Sum.inl z) = tangentCoordChange I x y z

The tangent coordinate changes of a disjoint union M ⊕ M' between charts at points of M are those of M.

theorem TauCeti.Manifold.tangentCoordChange_sumInr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M] [IsManifold I 1 M'] (x y z : M') : tangentCoordChange I (Sum.inr x) (Sum.inr y) (Sum.inr z) = tangentCoordChange I x y z

The tangent coordinate changes of a disjoint union M ⊕ M' between charts at points of M' are those of M'.

@[simp]

theorem TauCeti.Manifold.symmL_trivializationAt_sumInl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M] [IsManifold I 1 M'] {x z : M} : Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) (Sum.inl x)) (Sum.inl z) = Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) z

The inverse of the canonical tangent-bundle trivialization of M ⊕ M' at a point x of M is the inverse trivialization of M at x. Both sides vanish outside the domain of the chart at x.

@[simp]

theorem TauCeti.Manifold.symmL_trivializationAt_sumInr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M] [IsManifold I 1 M'] {y z : M'} : Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) (Sum.inr y)) (Sum.inr z) = Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) y) z

The inverse of the canonical tangent-bundle trivialization of M ⊕ M' at a point y of M' is the inverse trivialization of M' at y. Both sides vanish outside the domain of the chart at y.

theorem TauCeti.Manifold.isInvertible_mfderiv_prodMap_id_subtypeVal_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {a b : ℝ} [Fact (a < b)] (p : M × ↑(Set.Icc a b)) : (mfderiv% (Prod.map id Subtype.val) p).IsInvertible

The differential of the inclusion M × [a, b] → M × ℝ is invertible, also at the boundary.