Local equations for transverse fibre products

For maps f : X → N and g : Y → N, coordinates φ on their common target give the local equation φ(f x) - φ(g y) = 0. On the preimage of the coordinate domain this equation cuts out exactly the fibre product. At a pair with f x = g y, its derivative is the invertible coordinate derivative applied to df u - dg v.

Consequently the equation is regular exactly when the two derivative ranges span the target tangent space. Its kernel is the space of pairs with equal images under the two derivatives, with dimension dim X + dim Y - dim N in finite dimension at a transverse pair. These are the local equations and tangent spaces used in the regular-level construction of a transverse fibre product. The equal target tangent spaces are identified explicitly by tangentSpaceCast; no identification of tangent spaces at distinct points is used. No separation or countability hypotheses on the manifolds are needed.

References

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

def PartialDiffeomorph.fiberProductEquation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_4} {Y : Type u_7} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [NormedAddCommGroup EN] [NormedSpace 𝕜 EN] [TopologicalSpace HN] {IN : ModelWithCorners 𝕜 EN HN} [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} (φ : PartialDiffeomorph IN (modelWithCornersSelf 𝕜 EN) N EN n) (f : X → N) (g : Y → N) (p : X × Y) : EN

The difference of target coordinates, whose zero set locally defines a fibre product. Only on the preimage of φ.source in both factors does its vanishing characterize equality.

@[simp]

theorem PartialDiffeomorph.fiberProductEquation_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_4} {Y : Type u_7} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [NormedAddCommGroup EN] [NormedSpace 𝕜 EN] [TopologicalSpace HN] {IN : ModelWithCorners 𝕜 EN HN} [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} (φ : PartialDiffeomorph IN (modelWithCornersSelf 𝕜 EN) N EN n) (f : X → N) (g : Y → N) (p : X × Y) : φ.fiberProductEquation f g p = ↑φ.toPartialEquiv (f p.1) - ↑φ.toPartialEquiv (g p.2)

theorem PartialDiffeomorph.fiberProductEquation_eq_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_4} {Y : Type u_7} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [NormedAddCommGroup EN] [NormedSpace 𝕜 EN] [TopologicalSpace HN] {IN : ModelWithCorners 𝕜 EN HN} [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} (φ : PartialDiffeomorph IN (modelWithCornersSelf 𝕜 EN) N EN n) {f : X → N} {g : Y → N} {p : X × Y} (hx : f p.1 ∈ φ.source) (hy : g p.2 ∈ φ.source) : φ.fiberProductEquation f g p = 0 ↔ f p.1 = g p.2

The equation cuts out exactly the fibre product on the coordinate domain.

theorem PartialDiffeomorph.contMDiffOn_fiberProductEquation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EX : Type u_2} {HX : Type u_3} {X : Type u_4} {EY : Type u_5} {HY : Type u_6} {Y : Type u_7} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [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} (hf : ContMDiff IX IN n f) (hg : ContMDiff IY IN n g) : ContMDiffOn (IX.prod IY) (modelWithCornersSelf 𝕜 EN) n (φ.fiberProductEquation f g) ((f ⁻¹' φ.source) ×ˢ (g ⁻¹' φ.source))

Smooth maps give a smooth defining equation throughout the coordinate domain.

theorem PartialDiffeomorph.mvfderiv_fiberProductEquation_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EX : Type u_2} {HX : Type u_3} {X : Type u_4} {EY : Type u_5} {HY : Type u_6} {Y : Type u_7} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [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) (hn : n ≠ 0) {f : X → N} {g : Y → N} {p : X × Y} (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) (hfg : f p.1 = g p.2) (hx : f p.1 ∈ φ.source) (v : TangentSpace (IX.prod IY) p) : (d% (φ.fiberProductEquation f g) p) v = (d% ↑φ.toPartialEquiv (f p.1)) ((mfderiv% f p.1) v.1 - (tangentSpaceCast IN (g p.2) (f p.1)) ((mfderiv% g p.2) v.2))

At a pair in the fibre product, the vector-valued derivative of its local equation is the coordinate derivative applied to the difference of the map derivatives.

theorem PartialDiffeomorph.mem_ker_mvfderiv_fiberProductEquation_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EX : Type u_2} {HX : Type u_3} {X : Type u_4} {EY : Type u_5} {HY : Type u_6} {Y : Type u_7} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [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) (hn : n ≠ 0) {f : X → N} {g : Y → N} {p : X × Y} (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) (hfg : f p.1 = g p.2) (hx : f p.1 ∈ φ.source) (v : TangentSpace (IX.prod IY) p) : v ∈ (↑(d% (φ.fiberProductEquation f g) p)).ker ↔ (mfderiv% f p.1) v.1 = (tangentSpaceCast IN (g p.2) (f p.1)) ((mfderiv% g p.2) v.2)

The tangent kernel of the defining equation consists of pairs of vectors with equal images under the two map derivatives. This description is independent of target coordinates.

theorem PartialDiffeomorph.isRegularPoint_fiberProductEquation_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EX : Type u_2} {HX : Type u_3} {X : Type u_4} {EY : Type u_5} {HY : Type u_6} {Y : Type u_7} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [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) (hn : n ≠ 0) {f : X → N} {g : Y → N} {p : X × Y} (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) (hfg : f p.1 = g p.2) (hx : f p.1 ∈ φ.source) : TauCeti.IsRegularPoint (IX.prod IY) (modelWithCornersSelf 𝕜 EN) (φ.fiberProductEquation f g) p ↔ (↑(mfderiv% f p.1)).range ⊔ (↑(↑(tangentSpaceCast IN (g p.2) (f p.1)) ∘SL mfderiv% g p.2)).range = ⊤

Transversality is exactly regularity of the local fibre-product equation. The range of dg is transported to the equal tangent space at f p.1 before taking the supremum.

theorem PartialDiffeomorph.finrank_ker_mvfderiv_fiberProductEquation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EX : Type u_2} {HX : Type u_3} {X : Type u_4} {EY : Type u_5} {HY : Type u_6} {Y : Type u_7} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [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 ℕ∞} [FiniteDimensional 𝕜 EX] [FiniteDimensional 𝕜 EY] (φ : PartialDiffeomorph IN (modelWithCornersSelf 𝕜 EN) N EN n) (hn : n ≠ 0) {f : X → N} {g : Y → N} {p : X × Y} (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) (hfg : f p.1 = g p.2) (hx : f p.1 ∈ φ.source) (htrans : (↑(mfderiv% f p.1)).range ⊔ (↑(↑(tangentSpaceCast IN (g p.2) (f p.1)) ∘SL mfderiv% g p.2)).range = ⊤) : Module.finrank 𝕜 ↥(↑(d% (φ.fiberProductEquation f g) p)).ker = Module.finrank 𝕜 EX + Module.finrank 𝕜 EY - Module.finrank 𝕜 EN

At a transverse pair, the kernel of the defining equation has the expected dimension. Surjectivity forces the target dimension not to exceed the sum of the source dimensions.