Transverse fibre products in a target-coordinate patch

For smooth maps f : X → N and g : Y → N transverse along their fibre product, a target coordinate patch φ gives an embedded manifold on the actual subtype {p : X × Y // f p.1 = g p.2 ∧ f p.1 ∈ φ.source}. Its topology is the subspace topology and its dimension is dim X + dim Y - dim N. Its tangent image consists exactly of pairs of vectors with equal images under df and dg.

PartialDiffeomorph.exists_isManifold_localFiberProduct_isSmoothEmbedding constructs this structure by applying the regular-level theorem to the coordinate-difference equation on the open subset where both maps take values in φ.source. This local construction allows fibre-product charts to be glued over different target-coordinate patches. No Hausdorff or countability hypotheses are used, and the local fibre product may be empty.

The smooth universal property is supplied by the returned embedding and Manifold.IsSmoothEmbedding.contMDiff_iff_comp: a map to this subtype is smooth exactly when its composite with the inclusion into X × Y is smooth.

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 PartialDiffeomorph.exists_isManifold_localFiberProduct_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 ℕ∞} (φ : PartialDiffeomorph IN (modelWithCornersSelf ℝ EN) N EN n) {f : X → N} {g : Y → N} (hn : 1 ≤ n) (hf : ContMDiff IX IN n f) (hg : ContMDiff IY IN n g) [IsManifold IX n X] [IsManifold IY n Y] [IX.Boundaryless] [IY.Boundaryless] [FiniteDimensional ℝ EX] [FiniteDimensional ℝ EY] [FiniteDimensional ℝ EN] (htrans : ∀ (p : X × Y), f p.1 = g p.2 → f p.1 ∈ φ.source → (↑(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 ∧ f p.1 ∈ φ.source }), IsManifold (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ)) n { p : X × Y // f p.1 = g p.2 ∧ f p.1 ∈ φ.source } ∧ 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 ∧ f p.1 ∈ φ.source }) (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 transverse fibre product in a target-coordinate patch is an embedded submanifold. The topology is the inherited subspace topology, the model dimension is dim X + dim Y - dim N, and the tangent image is the space of pairs with equal derivative images. Transversality is required only at equal-value pairs in the chosen patch.

The returned smooth embedding also gives the smooth universal property through Manifold.IsSmoothEmbedding.contMDiff_iff_comp, without a separate continuity hypothesis.