Transverse fibre products of manifolds

For transverse smooth maps f : X → N and g : Y → N, the subtype {p : X × Y // f p.1 = g p.2} is an embedded manifold with its inherited topology and model dimension dim X + dim Y - dim N. Its tangent vectors are exactly the pairs with equal images under the differentials of f and g.

TauCeti.transverseFiberProductChartedSpace glues the coordinate-patch fibre products of PartialDiffeomorph.exists_isManifold_localFiberProduct_isSmoothEmbedding. It is a named, non-instance atlas, characterized by TauCeti.isManifold_transverseFiberProduct, TauCeti.isSmoothEmbedding_coe_transverseFiberProduct, and TauCeti.mem_range_mfderiv_coe_transverseFiberProduct_iff. The existence-only form is TauCeti.exists_isManifold_transverseFiberProduct_isSmoothEmbedding. The embedding gives the smooth universal property via Manifold.IsSmoothEmbedding.contMDiff_iff_comp: a map into the fibre product is smooth exactly when both component maps are smooth. In particular both projections are smooth. No Hausdorff or countability assumptions are used, and the fibre product may be empty.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer (2013), Theorem 6.30 (transverse preimages), applied to the diagonal in N × N.

theorem TauCeti.exists_isManifold_transverseFiberProduct_isSmoothEmbedding {EX : Type u_1} {HX : Type u_2} {X : Type u_3} {EY : Type u_4} {HY : Type u_5} {Y : Type u_6} {EN : Type u_7} {HN : Type u_8} {N : Type u_9} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [TopologicalSpace HX] [NormedAddCommGroup EY] [NormedSpace ℝ EY] [TopologicalSpace HY] [NormedAddCommGroup EN] [NormedSpace ℝ EN] [TopologicalSpace HN] {IX : ModelWithCorners ℝ EX HX} {IY : ModelWithCorners ℝ EY HY} {IN : ModelWithCorners ℝ EN HN} [TopologicalSpace X] [ChartedSpace HX X] [TopologicalSpace Y] [ChartedSpace HY Y] [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} [IsManifold IN n N] {f : X → N} {g : Y → N} [IsManifold IX n X] [IsManifold IY n Y] [IX.Boundaryless] [IY.Boundaryless] [IN.Boundaryless] [FiniteDimensional ℝ EX] [FiniteDimensional ℝ EY] [FiniteDimensional ℝ EN] (hn : 1 ≤ n) (hf : ContMDiff IX IN n f) (hg : ContMDiff IY IN n g) (htrans : ∀ (p : X × Y), f p.1 = g p.2 → (↑(mfderiv% f p.1)).range ⊔ (↑(↑(tangentSpaceCast IN (g p.2) (f p.1)) ∘SL mfderiv% g p.2)).range = ⊤) : ∃ (cs : ChartedSpace (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ) { p : X × Y // f p.1 = g p.2 }), IsManifold (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ)) n { p : X × Y // f p.1 = g p.2 } ∧ Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ)) (IX.prod IY) n Subtype.val ∧ ∀ (p : { p : X × Y // f p.1 = g p.2 }) (v : TangentSpace (IX.prod IY) ↑p), v ∈ (↑(mfderiv% Subtype.val p)).range ↔ (mfderiv% f (↑p).1) v.1 = (tangentSpaceCast IN (g (↑p).2) (f (↑p).1)) ((mfderiv% g (↑p).2) v.2)

The transverse fibre-product theorem. The actual equal-value subtype of two transverse C^n maps, n ≥ 1, is a C^n manifold of dimension dim X + dim Y - dim N with its subspace topology. Its inclusion is a smooth embedding, and its tangent image consists of pairs whose images under the two differentials agree. Empty fibre products are allowed; no separation or countability hypotheses are needed.

@[instance_reducible]

noncomputable def TauCeti.transverseFiberProductChartedSpace {EX : Type u_1} {HX : Type u_2} {X : Type u_3} {EY : Type u_4} {HY : Type u_5} {Y : Type u_6} {EN : Type u_7} {HN : Type u_8} {N : Type u_9} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [TopologicalSpace HX] [NormedAddCommGroup EY] [NormedSpace ℝ EY] [TopologicalSpace HY] [NormedAddCommGroup EN] [NormedSpace ℝ EN] [TopologicalSpace HN] {IX : ModelWithCorners ℝ EX HX} {IY : ModelWithCorners ℝ EY HY} {IN : ModelWithCorners ℝ EN HN} [TopologicalSpace X] [ChartedSpace HX X] [TopologicalSpace Y] [ChartedSpace HY Y] [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} [IsManifold IN n N] {f : X → N} {g : Y → N} [IsManifold IX n X] [IsManifold IY n Y] [IX.Boundaryless] [IY.Boundaryless] [IN.Boundaryless] [FiniteDimensional ℝ EX] [FiniteDimensional ℝ EY] [FiniteDimensional ℝ EN] (hn : 1 ≤ n) (hf : ContMDiff IX IN n f) (hg : ContMDiff IY IN n g) (htrans : ∀ (p : X × Y), f p.1 = g p.2 → (↑(mfderiv% f p.1)).range ⊔ (↑(↑(tangentSpaceCast IN (g p.2) (f p.1)) ∘SL mfderiv% g p.2)).range = ⊤) : ChartedSpace (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ) { p : X × Y // f p.1 = g p.2 }

A fixed atlas on the transverse fibre product, chosen from the construction by gluing embedded target-coordinate patches. It uses the subspace topology and is not a global instance. Its manifold, embedding, and tangent-image properties are given by the lemmas below.

theorem TauCeti.isManifold_transverseFiberProduct {EX : Type u_1} {HX : Type u_2} {X : Type u_3} {EY : Type u_4} {HY : Type u_5} {Y : Type u_6} {EN : Type u_7} {HN : Type u_8} {N : Type u_9} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [TopologicalSpace HX] [NormedAddCommGroup EY] [NormedSpace ℝ EY] [TopologicalSpace HY] [NormedAddCommGroup EN] [NormedSpace ℝ EN] [TopologicalSpace HN] {IX : ModelWithCorners ℝ EX HX} {IY : ModelWithCorners ℝ EY HY} {IN : ModelWithCorners ℝ EN HN} [TopologicalSpace X] [ChartedSpace HX X] [TopologicalSpace Y] [ChartedSpace HY Y] [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} [IsManifold IN n N] {f : X → N} {g : Y → N} [IsManifold IX n X] [IsManifold IY n Y] [IX.Boundaryless] [IY.Boundaryless] [IN.Boundaryless] [FiniteDimensional ℝ EX] [FiniteDimensional ℝ EY] [FiniteDimensional ℝ EN] (hn : 1 ≤ n) (hf : ContMDiff IX IN n f) (hg : ContMDiff IY IN n g) (htrans : ∀ (p : X × Y), f p.1 = g p.2 → (↑(mfderiv% f p.1)).range ⊔ (↑(↑(tangentSpaceCast IN (g p.2) (f p.1)) ∘SL mfderiv% g p.2)).range = ⊤) : IsManifold (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ)) n { p : X × Y // f p.1 = g p.2 }

The transverse fibre product with its chosen atlas is a C^n manifold.

theorem TauCeti.isSmoothEmbedding_coe_transverseFiberProduct {EX : Type u_1} {HX : Type u_2} {X : Type u_3} {EY : Type u_4} {HY : Type u_5} {Y : Type u_6} {EN : Type u_7} {HN : Type u_8} {N : Type u_9} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [TopologicalSpace HX] [NormedAddCommGroup EY] [NormedSpace ℝ EY] [TopologicalSpace HY] [NormedAddCommGroup EN] [NormedSpace ℝ EN] [TopologicalSpace HN] {IX : ModelWithCorners ℝ EX HX} {IY : ModelWithCorners ℝ EY HY} {IN : ModelWithCorners ℝ EN HN} [TopologicalSpace X] [ChartedSpace HX X] [TopologicalSpace Y] [ChartedSpace HY Y] [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} [IsManifold IN n N] {f : X → N} {g : Y → N} [IsManifold IX n X] [IsManifold IY n Y] [IX.Boundaryless] [IY.Boundaryless] [IN.Boundaryless] [FiniteDimensional ℝ EX] [FiniteDimensional ℝ EY] [FiniteDimensional ℝ EN] (hn : 1 ≤ n) (hf : ContMDiff IX IN n f) (hg : ContMDiff IY IN n g) (htrans : ∀ (p : X × Y), f p.1 = g p.2 → (↑(mfderiv% f p.1)).range ⊔ (↑(↑(tangentSpaceCast IN (g p.2) (f p.1)) ∘SL mfderiv% g p.2)).range = ⊤) : Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ)) (IX.prod IY) n Subtype.val

The inclusion of the transverse fibre product with its chosen atlas is a smooth embedding.

theorem TauCeti.mem_range_mfderiv_coe_transverseFiberProduct_iff {EX : Type u_1} {HX : Type u_2} {X : Type u_3} {EY : Type u_4} {HY : Type u_5} {Y : Type u_6} {EN : Type u_7} {HN : Type u_8} {N : Type u_9} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [TopologicalSpace HX] [NormedAddCommGroup EY] [NormedSpace ℝ EY] [TopologicalSpace HY] [NormedAddCommGroup EN] [NormedSpace ℝ EN] [TopologicalSpace HN] {IX : ModelWithCorners ℝ EX HX} {IY : ModelWithCorners ℝ EY HY} {IN : ModelWithCorners ℝ EN HN} [TopologicalSpace X] [ChartedSpace HX X] [TopologicalSpace Y] [ChartedSpace HY Y] [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} [IsManifold IN n N] {f : X → N} {g : Y → N} [IsManifold IX n X] [IsManifold IY n Y] [IX.Boundaryless] [IY.Boundaryless] [IN.Boundaryless] [FiniteDimensional ℝ EX] [FiniteDimensional ℝ EY] [FiniteDimensional ℝ EN] (hn : 1 ≤ n) (hf : ContMDiff IX IN n f) (hg : ContMDiff IY IN n g) (htrans : ∀ (p : X × Y), f p.1 = g p.2 → (↑(mfderiv% f p.1)).range ⊔ (↑(↑(tangentSpaceCast IN (g p.2) (f p.1)) ∘SL mfderiv% g p.2)).range = ⊤) (p : { p : X × Y // f p.1 = g p.2 }) (v : TangentSpace (IX.prod IY) ↑p) : v ∈ (↑(mfderiv% Subtype.val p)).range ↔ (mfderiv% f (↑p).1) v.1 = (tangentSpaceCast IN (g (↑p).2) (f (↑p).1)) ((mfderiv% g (↑p).2) v.2)

A tangent vector lies in the image of the fibre-product inclusion exactly when its two components have equal images under the differentials of the defining maps.