1-jet bundles

This file contains the definition of the 1-jet bundle J¹(M, M'), also known as OneJetBundle I M I' M'.

We also define

• OneJetExt I I' f : M → J¹(M, M'): the 1-jet extension j¹f of a map f : M → M'

We prove

• If f is smooth, j¹f is smooth.
• If x ↦ (f₁ x, f₂ x, ϕ₁ x) : N → J¹(M₁, M₂) and x ↦ (f₂ x, f₃ x, ϕ₂ x) : N → J¹(M₂, M₃) are smooth, then so is x ↦ (f₁ x, f₃ x, ϕ₂ x ∘ ϕ₁ x) : N → J¹(M₁, M₃).

instance deleteme1 {𝕜 : 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'] (x : M × M') : Module 𝕜 ((⇑ContMDiffMap.fst *ᵖ (TangentSpace I)) x)

Equations

• deleteme1 I I' = inferInstance

instance deleteme2 {𝕜 : 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'] (x : M × M') : Module 𝕜 ((⇑ContMDiffMap.snd *ᵖ (TangentSpace I')) x)

Equations

• deleteme2 I I' = inferInstance

instance deleteme3 {𝕜 : 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 (↑⊤) 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'] : VectorBundle 𝕜 E (⇑ContMDiffMap.fst *ᵖ (TangentSpace I))

instance deleteme4 {𝕜 : 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'] [IsManifold I' (↑⊤) M'] : VectorBundle 𝕜 E' (⇑ContMDiffMap.snd *ᵖ (TangentSpace I'))

instance deleteme5 {𝕜 : 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 (↑⊤) 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'] : ContMDiffVectorBundle (↑⊤) E (⇑ContMDiffMap.fst *ᵖ (TangentSpace I)) (I.prod I')

instance deleteme6 {𝕜 : 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'] [IsManifold I' (↑⊤) M'] : ContMDiffVectorBundle (↑⊤) E' (⇑ContMDiffMap.snd *ᵖ (TangentSpace I')) (I.prod I')

def OneJetSpace {𝕜 : 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'] (p : M × M') : Type (max u_5 u_2)

The fibers of the one jet-bundle.

Equations

• OneJetSpace I I' p = ((⇑ContMDiffMap.fst *ᵖ (TangentSpace I)) p →L[𝕜] (⇑ContMDiffMap.snd *ᵖ (TangentSpace I')) p)

instance instTopologicalSpaceOneJetSpace {𝕜 : 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'] (p : M × M') : TopologicalSpace (OneJetSpace I I' p)

Equations

• instTopologicalSpaceOneJetSpace I I' p = id inferInstance

instance instAddCommGroupOneJetSpace {𝕜 : 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'] (p : M × M') : AddCommGroup (OneJetSpace I I' p)

Equations

• instAddCommGroupOneJetSpace I I' p = id inferInstance

instance instFunLikeOneJetSpaceTangentSpaceFstSnd {𝕜 : 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'] (p : M × M') : FunLike (OneJetSpace I I' p) (TangentSpace I p.1) (TangentSpace I' p.2)

Equations

• instFunLikeOneJetSpaceTangentSpaceFstSnd I I' p = { coe := fun (φ : OneJetSpace I I' p) => (↑φ).toFun, coe_injective' := ⋯ }

@[reducible]

def OneJetBundle {𝕜 : 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'] : Type (max (max u_4 u_7) u_2 u_5)

The space of one jets of maps between two smooth manifolds. Defined in terms of Bundle.TotalSpace to be able to put a suitable topology on it.

Equations

• OneJetBundle I M I' M' = Bundle.TotalSpace (E →L[𝕜] E') (OneJetSpace I I')

theorem OneJetBundle.ext {𝕜 : 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'] {x y : OneJetBundle I M I' M'} (h : x.proj.1 = y.proj.1) (h' : x.proj.2 = y.proj.2) (h'' : x.snd = y.snd) : x = y

theorem OneJetBundle.ext_iff {𝕜 : 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'] {x y : OneJetBundle I M I' M'} : x = y ↔ x.proj.1 = y.proj.1 ∧ x.proj.2 = y.proj.2 ∧ x.snd = y.snd

instance instModuleOneJetSpace {𝕜 : 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'] (x : M × M') : Module 𝕜 (OneJetSpace I I' x)

Equations

• instModuleOneJetSpace I I' M' x = id inferInstance

instance instTopologicalSpaceOneJetBundle {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] : TopologicalSpace (OneJetBundle I M I' M')

Equations

• instTopologicalSpaceOneJetBundle I M I' M' = id inferInstance

instance instFiberBundleProdContinuousLinearMapIdOneJetSpace {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] : FiberBundle (E →L[𝕜] E') (OneJetSpace I I')

Equations

• instFiberBundleProdContinuousLinearMapIdOneJetSpace I M I' M' = id inferInstance

instance instVectorBundleProdContinuousLinearMapIdOneJetSpace {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] : VectorBundle 𝕜 (E →L[𝕜] E') (OneJetSpace I I')

instance instContMDiffVectorBundleSomeENatTopProdContinuousLinearMapIdOneJetSpaceModelProdProd {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] : ContMDiffVectorBundle (↑⊤) (E →L[𝕜] E') (OneJetSpace I I') (I.prod I')

instance instChartedSpaceModelProdContinuousLinearMapIdOneJetBundle {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] : ChartedSpace (ModelProd (ModelProd H H') (E →L[𝕜] E')) (OneJetBundle I M I' M')

Equations

• instChartedSpaceModelProdContinuousLinearMapIdOneJetBundle I M I' M' = id inferInstance

instance instIsManifoldProdContinuousLinearMapIdModelProdProdModelWithCornersSelfSomeENatTopOneJetBundle {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] : IsManifold ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) (OneJetBundle I M I' M')

theorem oneJetBundle_proj_continuous {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] : Continuous Bundle.TotalSpace.proj

The tangent bundle projection on the basis is a continuous map.

theorem oneJetBundle_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] [IsManifold I (↑⊤) 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'] [IsManifold I' (↑⊤) M'] (x₀ x : OneJetBundle I M I' M') : (↑(trivializationAt (E →L[𝕜] E') (OneJetSpace I I') x₀.proj) x).2 = ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀.proj.1 x.proj.1 x₀.proj.2 x.proj.2 x.snd

theorem trivializationAt_oneJetBundle_source {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] (x₀ : M × M') : (trivializationAt (E →L[𝕜] E') (OneJetSpace I I') x₀).source = Bundle.TotalSpace.proj ⁻¹' (Prod.fst ⁻¹' (chartAt H x₀.1).source ∩ Prod.snd ⁻¹' (chartAt H' x₀.2).source)

theorem trivializationAt_oneJetBundle_target {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] (x₀ : M × M') : (trivializationAt (E →L[𝕜] E') (OneJetSpace I I') x₀).target = (Prod.fst ⁻¹' (trivializationAt E (TangentSpace I) x₀.1).baseSet ∩ Prod.snd ⁻¹' (trivializationAt E' (TangentSpace I') x₀.2).baseSet) ×ˢ Set.univ

theorem oneJetBundle_chartAt_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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] (v v' : OneJetBundle I M I' M') : ↑(chartAt (ModelProd (ModelProd H H') (E →L[𝕜] E')) v) v' = ((↑(chartAt H v.proj.1) v'.proj.1, ↑(chartAt H' v.proj.2) v'.proj.2), ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') v.proj.1 v'.proj.1 v.proj.2 v'.proj.2 v'.snd)

Computing the value of a chart around v at point v' in J¹(M, M'). The last component equals the continuous linear map v'.2, composed on both sides by an appropriate coordinate change function.

theorem oneJetBundle_chart_source {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] (x₀ : OneJetBundle I M I' M') : (chartAt (ModelProd (ModelProd H H') (E →L[𝕜] E')) x₀).source = Bundle.TotalSpace.proj ⁻¹' (chartAt (ModelProd H H') x₀.proj).source

In J¹(M, M'), the source of a chart has a nice formula

theorem trivializationAt_pullBack_baseSet {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (f : K) (x : B') : (trivializationAt F (⇑f *ᵖ E) x).baseSet = ⇑f ⁻¹' (trivializationAt F E (f x)).baseSet

@[simp]

theorem ContMDiffMap.coe_fst {𝕜 : Type u_23} [NontriviallyNormedField 𝕜] {E : Type u_24} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_25} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_26} [TopologicalSpace H] {H' : Type u_27} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_28} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_29} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} : ⇑fst = Prod.fst

@[simp]

theorem ContMDiffMap.coe_snd {𝕜 : Type u_23} [NontriviallyNormedField 𝕜] {E : Type u_24} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_25} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_26} [TopologicalSpace H] {H' : Type u_27} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_28} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_29} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} : ⇑snd = Prod.snd

@[simp]

theorem ContMDiffMap.fst_apply {𝕜 : Type u_23} [NontriviallyNormedField 𝕜] {E : Type u_24} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_25} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_26} [TopologicalSpace H] {H' : Type u_27} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_28} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_29} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (x : M) (x' : M') : fst (x, x') = x

@[simp]

theorem ContMDiffMap.snd_apply {𝕜 : Type u_23} [NontriviallyNormedField 𝕜] {E : Type u_24} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_25} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_26} [TopologicalSpace H] {H' : Type u_27} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_28} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_29} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (x : M) (x' : M') : snd (x, x') = x'

theorem oneJetBundle_chart_target {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] (x₀ : OneJetBundle I M I' M') : (chartAt (ModelProd (ModelProd H H') (E →L[𝕜] E')) x₀).target = Prod.fst ⁻¹' (chartAt (ModelProd H H') x₀.proj).target

In J¹(M, M'), the target of a chart has a nice formula

theorem contMDiff_oneJetBundle_proj {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] : ContMDiff ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (I.prod I') (↑⊤) Bundle.TotalSpace.proj

theorem ContMDiff.oneJetBundle_proj {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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 : N → OneJetBundle I M I' M'} (hf : ContMDiff J ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) f) : ContMDiff J (I.prod I') ↑⊤ fun (x : N) => (f x).proj

theorem ContMDiffAt.oneJetBundle_proj {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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 : N → OneJetBundle I M I' M'} {x₀ : N} (hf : ContMDiffAt J ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) f x₀) : ContMDiffAt J (I.prod I') (↑⊤) (fun (x : N) => (f x).proj) x₀

def OneJetBundle.mk {𝕜 : 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'] (x : M) (y : M') (f : OneJetSpace I I' (x, y)) : OneJetBundle I M I' M'

The constructor of OneJetBundle, in case Sigma.mk will not give the right type.

Equations

• OneJetBundle.mk x y f = { proj := (x, y), snd := f }

@[simp]

theorem oneJetBundle_mk_fst {𝕜 : 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'] {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} : (OneJetBundle.mk x y f).proj = (x, y)

@[simp]

theorem oneJetBundle_mk_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] {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'] {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} : (OneJetBundle.mk x y f).snd = f

theorem contMDiffAt_oneJetBundle {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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 : N → OneJetBundle I M I' M'} {x₀ : N} : ContMDiffAt J ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) f x₀ ↔ ContMDiffAt J I (↑⊤) (fun (x : N) => (f x).proj.1) x₀ ∧ ContMDiffAt J I' (↑⊤) (fun (x : N) => (f x).proj.2) x₀ ∧ ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) (↑⊤) (inTangentCoordinates I I' (fun (x : N) => (f x).proj.1) (fun (x : N) => (f x).proj.2) (fun (x : N) => (f x).snd) x₀) x₀

theorem contMDiffAt_oneJetBundle_mk {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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 : N → M} {g : N → M'} {ϕ : N → E →L[𝕜] E'} {x₀ : N} : ContMDiffAt J ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) (fun (x : N) => OneJetBundle.mk (f x) (g x) (ϕ x)) x₀ ↔ ContMDiffAt J I (↑⊤) f x₀ ∧ ContMDiffAt J I' (↑⊤) g x₀ ∧ ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) (↑⊤) (inTangentCoordinates I I' f g ϕ x₀) x₀

theorem ContMDiffAt.oneJetBundle_mk {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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 : N → M} {g : N → M'} {ϕ : N → E →L[𝕜] E'} {x₀ : N} (hf : ContMDiffAt J I (↑⊤) f x₀) (hg : ContMDiffAt J I' (↑⊤) g x₀) (hϕ : ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) (↑⊤) (inTangentCoordinates I I' f g ϕ x₀) x₀) : ContMDiffAt J ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) (fun (x : N) => OneJetBundle.mk (f x) (g x) (ϕ x)) x₀

def oneJetExt {𝕜 : 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'] (f : M → M') : M → OneJetBundle I M I' M'

The one-jet extension of a function

Equations

• oneJetExt I I' f x = OneJetBundle.mk x (f x) (mfderiv I I' f x)

theorem ContMDiffAt.oneJetExt {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] {f : M → M'} {x : M} (hf : ContMDiffAt I I' (↑⊤) f x) : ContMDiffAt I ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) (_root_.oneJetExt I I' f) x

theorem ContMDiff.oneJetExt {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] {f : M → M'} (hf : ContMDiff I I' (↑⊤) f) : ContMDiff I ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) (_root_.oneJetExt I I' f)

theorem ContinuousAt.inTangentCoordinates_comp {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] {N : Type u_13} [TopologicalSpace N] {F' : Type u_14} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_15} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J' (↑⊤) N'] {f : N → M} {g : N → M'} {h : N → N'} {ϕ' : N → E' →L[𝕜] F'} {ϕ : N → E →L[𝕜] E'} {x₀ : N} (hg : ContinuousAt g x₀) : inTangentCoordinates I J' f h (fun (x : N) => (ϕ' x).comp (ϕ x)) x₀ =ᶠ[nhds x₀] fun (x : N) => (inTangentCoordinates I' J' g h ϕ' x₀ x).comp (inTangentCoordinates I I' f g ϕ x₀ x)

theorem ContMDiffAt.clm_comp_inTangentCoordinates {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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' : Type u_14} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_15} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J' (↑⊤) N'] {f : N → M} {g : N → M'} {h : N → N'} {ϕ' : N → E' →L[𝕜] F'} {ϕ : N → E →L[𝕜] E'} {n : N} (hg : ContinuousAt g n) (hϕ' : ContMDiffAt J (modelWithCornersSelf 𝕜 (E' →L[𝕜] F')) (↑⊤) (inTangentCoordinates I' J' g h ϕ' n) n) (hϕ : ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) (↑⊤) (inTangentCoordinates I I' f g ϕ n) n) : ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] F')) (↑⊤) (inTangentCoordinates I J' f h (fun (n : N) => (ϕ' n).comp (ϕ n)) n) n

theorem ContMDiffAt.oneJet_comp {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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' : Type u_14} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_15} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J (↑⊤) N] {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {x₀ : N'} {h : (x : N') → OneJetSpace I' J (f2 x, f3 x)} {g : (x : N') → OneJetSpace I I' (f1 x, f2 x)} (hh : ContMDiffAt J' ((I'.prod J).prod (modelWithCornersSelf 𝕜 (E' →L[𝕜] F))) (↑⊤) (fun (x : N') => OneJetBundle.mk (f2 x) (f3 x) (h x)) x₀) (hg : ContMDiffAt J' ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) (fun (x : N') => OneJetBundle.mk (f1 x) (f2 x) (g x)) x₀) : ContMDiffAt J' ((I.prod J).prod (modelWithCornersSelf 𝕜 (E →L[𝕜] F))) (↑⊤) (fun (x : N') => OneJetBundle.mk (f1 x) (f3 x) (ContinuousLinearMap.comp (h x) (g x))) x₀

theorem ContMDiff.oneJet_comp {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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' : Type u_14} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_15} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J (↑⊤) N] {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {h : (x : N') → OneJetSpace I' J (f2 x, f3 x)} {g : (x : N') → OneJetSpace I I' (f1 x, f2 x)} (hh : ContMDiff J' ((I'.prod J).prod (modelWithCornersSelf 𝕜 (E' →L[𝕜] F))) ↑⊤ fun (x : N') => OneJetBundle.mk (f2 x) (f3 x) (h x)) (hg : ContMDiff J' ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) ↑⊤ fun (x : N') => OneJetBundle.mk (f1 x) (f2 x) (g x)) : ContMDiff J' ((I.prod J).prod (modelWithCornersSelf 𝕜 (E →L[𝕜] F))) ↑⊤ fun (x : N') => OneJetBundle.mk (f1 x) (f3 x) (ContinuousLinearMap.comp (h x) (g x))

theorem ContMDiff.oneJet_add {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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 : N → M} {g : N → M'} {ϕ ϕ' : (x : N) → OneJetSpace I I' (f x, g x)} (hϕ : ContMDiff J ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) ↑⊤ fun (x : N) => OneJetBundle.mk (f x) (g x) (ϕ x)) (hϕ' : ContMDiff J ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) ↑⊤ fun (x : N) => OneJetBundle.mk (f x) (g x) (ϕ' x)) : ContMDiff J ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) ↑⊤ fun (x : N) => OneJetBundle.mk (f x) (g x) (ϕ x + ϕ' x)

def OneJetBundle.map {𝕜 : 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'] {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' : Type u_14} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_15} [TopologicalSpace G'] (J' : ModelWithCorners 𝕜 F' G') {N' : Type u_16} [TopologicalSpace N'] [ChartedSpace G' N'] (f : M → N) (g : M' → N') (Dfinv : (x : M) → TangentSpace J (f x) →L[𝕜] TangentSpace I x) : OneJetBundle I M I' M' → OneJetBundle J N J' N'

A useful definition to define maps between two OneJetBundles.

Equations

• OneJetBundle.map I' J' f g Dfinv p = OneJetBundle.mk (f p.proj.1) (g p.proj.2) (((mfderiv I' J' g p.proj.2).comp p.snd).comp (Dfinv p.proj.1))

theorem OneJetBundle.map_map {𝕜 : 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'] {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' : Type u_14} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_15} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [TopologicalSpace N'] [ChartedSpace G' N'] {E₂ : Type u_17} [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] {H₂ : Type u_18} [TopologicalSpace H₂] {I₂ : ModelWithCorners 𝕜 E₂ H₂} {M₂ : Type u_19} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] {E₃ : Type u_20} [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] {H₃ : Type u_21} [TopologicalSpace H₃] {I₃ : ModelWithCorners 𝕜 E₃ H₃} {M₃ : Type u_22} [TopologicalSpace M₃] [ChartedSpace H₃ M₃] {f₂ : N → M₂} {f : M → N} {g₂ : N' → M₃} {g : M' → N'} {Dfinv : (x : M) → TangentSpace J (f x) →L[𝕜] TangentSpace I x} {Df₂inv : (x : N) → TangentSpace I₂ (f₂ x) →L[𝕜] TangentSpace J x} {x : OneJetBundle I M I' M'} (hg₂ : MDifferentiableAt J' I₃ g₂ (g x.proj.2)) (hg : MDifferentiableAt I' J' g x.proj.2) : OneJetBundle.map J' I₃ f₂ g₂ Df₂inv (OneJetBundle.map I' J' f g Dfinv x) = OneJetBundle.map I' I₃ (f₂ ∘ f) (g₂ ∘ g) (fun (x : M) => (Dfinv x).comp (Df₂inv (f x))) x

theorem OneJetBundle.map_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] {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'] (x : OneJetBundle I M I' M') : OneJetBundle.map I' I' id id (fun (x : M) => ContinuousLinearMap.id 𝕜 (TangentSpace I x)) x = x

theorem ContMDiffAt.oneJetBundle_map {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) M'] {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''] [IsManifold I'' (↑⊤) 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' : Type u_14} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_15} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J' (↑⊤) N'] [IsManifold J (↑⊤) N] {f : M'' → M → N} {g : M'' → M' → N'} {x₀ : M''} {Dfinv : (z : M'') → (x : M) → TangentSpace J (f z x) →L[𝕜] TangentSpace I x} {k : M'' → OneJetBundle I M I' M'} (hf : ContMDiffAt (I''.prod I) J (↑⊤) (Function.uncurry f) (x₀, (k x₀).proj.1)) (hg : ContMDiffAt (I''.prod I') J' (↑⊤) (Function.uncurry g) (x₀, (k x₀).proj.2)) (hDfinv : ContMDiffAt I'' (modelWithCornersSelf 𝕜 (F →L[𝕜] E)) (↑⊤) (inTangentCoordinates J I (fun (x : M'') => f x (k x).proj.1) (fun (x : M'') => (k x).proj.1) (fun (x : M'') => Dfinv x (k x).proj.1) x₀) x₀) (hk : ContMDiffAt I'' ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) k x₀) : ContMDiffAt I'' ((J.prod J').prod (modelWithCornersSelf 𝕜 (F →L[𝕜] F'))) (↑⊤) (fun (z : M'') => OneJetBundle.map I' J' (f z) (g z) (Dfinv z) (k z)) x₀

def mapLeft {𝕜 : 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'] {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 → N) (Dfinv : (x : M) → TangentSpace J (f x) →L[𝕜] TangentSpace I x) : OneJetBundle I M I' M' → OneJetBundle J N I' M'

A useful definition to define maps between two OneJetBundles.

Equations

• mapLeft f Dfinv p = OneJetBundle.mk (f p.proj.1) p.proj.2 (ContinuousLinearMap.comp p.snd (Dfinv p.proj.1))

theorem mapLeft_eq_map {𝕜 : 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'] {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 → N) (Dfinv : (x : M) → TangentSpace J (f x) →L[𝕜] TangentSpace I x) : mapLeft f Dfinv = OneJetBundle.map I' I' f id Dfinv

theorem ContMDiffAt.mapLeft {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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' : Type u_14} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_15} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J' (↑⊤) N'] [IsManifold J (↑⊤) N] {f : N' → M → N} {x₀ : N'} {Dfinv : (z : N') → (x : M) → TangentSpace J (f z x) →L[𝕜] TangentSpace I x} {g : N' → OneJetBundle I M I' M'} (hf : ContMDiffAt (J'.prod I) J (↑⊤) (Function.uncurry f) (x₀, (g x₀).proj.1)) (hDfinv : ContMDiffAt J' (modelWithCornersSelf 𝕜 (F →L[𝕜] E)) (↑⊤) (inTangentCoordinates J I (fun (x : N') => f x (g x).proj.1) (fun (x : N') => (g x).proj.1) (fun (x : N') => Dfinv x (g x).proj.1) x₀) x₀) (hg : ContMDiffAt J' ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) g x₀) : ContMDiffAt J' ((J.prod I').prod (modelWithCornersSelf 𝕜 (F →L[𝕜] E'))) (↑⊤) (fun (z : N') => _root_.mapLeft (f z) (Dfinv z) (g z)) x₀

def bundleFst {𝕜 : 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'] {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] : OneJetBundle (J.prod I) (N × M) I' M' → OneJetBundle J N I' M'

The projection J¹(E × P, F) → J¹(E, F). Not actually used.

Equations

• bundleFst = mapLeft Prod.fst fun (x : N × M) => ContinuousLinearMap.inl 𝕜 F E

def bundleSnd {𝕜 : 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'] {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] : OneJetBundle (J.prod I) (N × M) I' M' → OneJetBundle I M I' M'

The projection J¹(P × E, F) → J¹(E, F).

Equations

• bundleSnd = mapLeft Prod.snd fun (x : N × M) => mfderiv I (J.prod I) (fun (y : M) => (x.1, y)) x.2

theorem bundleSnd_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] {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'] {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] (x : OneJetBundle (J.prod I) (N × M) I' M') : bundleSnd x = mapLeft Prod.snd (fun (x : N × M) => ContinuousLinearMap.inr 𝕜 F E) x

theorem contMDiff_bundleSnd {𝕜 : 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 (↑⊤) 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'] [IsManifold I' (↑⊤) 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] [IsManifold J (↑⊤) N] : ContMDiff (((J.prod I).prod I').prod (modelWithCornersSelf 𝕜 (F × E →L[𝕜] E'))) ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) bundleSnd

theorem partialEquiv_eq_equiv {α : Type u_23} {β : Type u_24} {f : PartialEquiv α β} {e : α ≃ β} (h1 : ∀ (x : α), ↑f x = e x) (h2 : f.source = Set.univ) (h3 : f.target = Set.univ) : f = e.toPartialEquiv

@[simp]

theorem oneJetBundle_model_space_chartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} (p : OneJetBundle I H I' H') : (chartAt (ModelProd (ModelProd H H') (E →L[𝕜] E')) p).toPartialEquiv = (Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E')).toPartialEquiv

In the OneJetBundle to the model space, the charts are just the canonical identification between a product type and a bundle total space type, a.k.a. Bundle.TotalSpace.toProd.

@[simp]

theorem oneJetBundle_model_space_coe_chartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} (p : OneJetBundle I H I' H') : ↑(chartAt (ModelProd (ModelProd H H') (E →L[𝕜] E')) p) = ⇑(Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E'))

@[simp]

theorem oneJetBundle_model_space_coe_chartAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} (p : OneJetBundle I H I' H') : ↑(chartAt (ModelProd (ModelProd H H') (E →L[𝕜] E')) p).symm = ⇑(Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E')).symm

def oneJetBundleModelSpaceHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') : OneJetBundle I H I' H' ≃ₜ ModelProd (ModelProd H H') (E →L[𝕜] E')

The canonical identification between the one-jet bundle to the model space and the product, as a homeomorphism

Equations

• oneJetBundleModelSpaceHomeomorph I I' = { toEquiv := Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E'), continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem oneJetBundleModelSpaceHomeomorph_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') : ⇑(oneJetBundleModelSpaceHomeomorph I I') = ⇑(Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E'))

@[simp]

theorem oneJetBundleModelSpaceHomeomorph_coe_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') : ⇑(oneJetBundleModelSpaceHomeomorph I I').symm = ⇑(Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E')).symm