Quotient coordinates from a complementary parametrization

If A.coprod B is invertible, every ambient vector has a unique decomposition A u + B w. The second coordinate identifies the quotient by range A with the fixed parameter space of B. In particular, when A varies and B stays fixed, the quotient coordinates are read off from the inverse of a family of operators between fixed spaces. Ambient maps carrying one range into another induce coordinate changes satisfying the cocycle law; ambient equivalences preserving the ranges give invertible changes. This is useful for local coordinates on normal bundles.

The construction uses Mathlib's total continuous-linear inverse and continuous quotient lift. No norm, completeness, or choice of an inner product is required. The coordinates and their coordinate changes only need a semiring; the identification with the quotient needs a ring.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, the normal-bundle construction preceding Theorem 6.24.

noncomputable def ContinuousLinearMap.quotientRangeCoordinate {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] (A : E →L[R] F) (B : G →L[R] F) : F →L[R] G

The complementary coordinate of an ambient vector in the decomposition A u + B w. It is zero when the coproduct is not invertible.

theorem ContinuousLinearMap.quotientRangeCoordinate_def {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] (A : E →L[R] F) (B : G →L[R] F) : A.quotientRangeCoordinate B = snd R E G ∘SL (A.coprod B).inverse

The coordinate operator is the second component of the inverse coproduct.

@[simp]

theorem ContinuousLinearMap.quotientRangeCoordinate_of_not_isInvertible {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] {A : E →L[R] F} {B : G →L[R] F} (h : ¬(A.coprod B).IsInvertible) : A.quotientRangeCoordinate B = 0

Without an invertible coproduct, the complementary coordinate is zero.

@[simp]

theorem ContinuousLinearMap.quotientRangeCoordinate_apply_left {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] {A : E →L[R] F} {B : G →L[R] F} (u : E) : (A.quotientRangeCoordinate B) (A u) = 0

Tangent representatives have zero complementary coordinate. Without an invertible coproduct this holds because the coordinate is zero.

@[simp]

theorem ContinuousLinearMap.quotientRangeCoordinate_apply_right {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] {A : E →L[R] F} {B : G →L[R] F} (h : (A.coprod B).IsInvertible) (w : G) : (A.quotientRangeCoordinate B) (B w) = w

A vector parametrized by the complement has its original complementary coordinate.

theorem ContinuousLinearMap.exists_apply_add_apply_quotientRangeCoordinate_eq {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] {A : E →L[R] F} {B : G →L[R] F} (h : (A.coprod B).IsInvertible) (y : F) : ∃ (u : E), A u + B ((A.quotientRangeCoordinate B) y) = y

Every ambient vector is a range vector plus the complementary representative of its coordinate.

@[simp]

theorem ContinuousLinearMap.ker_quotientRangeCoordinate {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] {A : E →L[R] F} {B : G →L[R] F} (h : (A.coprod B).IsInvertible) : (↑(A.quotientRangeCoordinate B)).ker = (↑A).range

The kernel of the complementary coordinate is exactly the range being quotiented out.

theorem ContinuousLinearMap.sub_apply_quotientRangeCoordinate_mem_range {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommGroup G] [Module R G] {A : E →L[R] F} {B : G →L[R] F} (h : (A.coprod B).IsInvertible) (y : F) : y - B ((A.quotientRangeCoordinate B) y) ∈ (↑A).range

The complementary representative differs from the original vector by an element of the range being quotiented out.

noncomputable def ContinuousLinearMap.quotientRangeEquiv {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommGroup G] [Module R G] (A : E →L[R] F) (B : G →L[R] F) (h : (A.coprod B).IsInvertible) : (F ⧸ (↑A).range) ≃L[R] G

The quotient of the ambient space by range A, parametrized by a fixed complementary map B. The forward map takes complementary coordinates and the inverse takes the class of B w.

@[simp]

theorem ContinuousLinearMap.quotientRangeEquiv_apply_mk {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommGroup G] [Module R G] {A : E →L[R] F} {B : G →L[R] F} (h : (A.coprod B).IsInvertible) (y : F) : (A.quotientRangeEquiv B h) (Submodule.Quotient.mk y) = (A.quotientRangeCoordinate B) y

On an ambient representative, the quotient equivalence reads the second inverse coordinate.

@[simp]

theorem ContinuousLinearMap.quotientRangeEquiv_symm_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommGroup G] [Module R G] {A : E →L[R] F} {B : G →L[R] F} (h : (A.coprod B).IsInvertible) (w : G) : (A.quotientRangeEquiv B h).symm w = Submodule.Quotient.mk (B w)

The inverse quotient equivalence takes the class of the fixed complementary map.

@[simp]

theorem ContinuousLinearMap.quotientRangeCoordinate_comp_of_map_range_le {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {G' : Type u_5} {E' : Type u_6} {F' : Type u_7} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] [TopologicalSpace G'] [AddCommMonoid G'] [Module R G'] [TopologicalSpace E'] [AddCommMonoid E'] [Module R E'] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] [ContinuousAdd F'] {A : E →L[R] F} {B : G →L[R] F} {A' : E' →L[R] F'} {B' : G' →L[R] F'} (hB : (A.coprod B).IsInvertible) (T : F →L[R] F') (hT : Submodule.map (↑T) (↑A).range ≤ (↑A').range) : (A'.quotientRangeCoordinate B' ∘SL T ∘SL B) ∘SL A.quotientRangeCoordinate B = A'.quotientRangeCoordinate B' ∘SL T

Replacing an ambient representative by its complementary representative does not change its coordinates after an ambient map carrying the first tangent range into the second.

@[simp]

theorem ContinuousLinearMap.quotientRangeCoordinate_comp_quotientRangeCoordinate {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {G' : Type u_5} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] [TopologicalSpace G'] [AddCommMonoid G'] [Module R G'] {A : E →L[R] F} {B : G →L[R] F} {C : G' →L[R] F} (hB : (A.coprod B).IsInvertible) : (A.quotientRangeCoordinate C ∘SL B) ∘SL A.quotientRangeCoordinate B = A.quotientRangeCoordinate C

Changing complementary representatives preserves all quotient coordinates. This identifies the transition from the B coordinates to the C coordinates.

@[simp]

theorem ContinuousLinearMap.quotientRangeCoordinate_comp_cocycle {R : Type u_1} {F : Type u_3} {G : Type u_4} {G' : Type u_5} {E' : Type u_6} {F' : Type u_7} {E'' : Type u_8} {F'' : Type u_9} {G'' : Type u_10} [Semiring R] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] [TopologicalSpace G'] [AddCommMonoid G'] [Module R G'] [TopologicalSpace E'] [AddCommMonoid E'] [Module R E'] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] [ContinuousAdd F'] [TopologicalSpace E''] [AddCommMonoid E''] [Module R E''] [TopologicalSpace F''] [AddCommMonoid F''] [Module R F''] [ContinuousAdd F''] [TopologicalSpace G''] [AddCommMonoid G''] [Module R G''] {B : G →L[R] F} {A' : E' →L[R] F'} {B' : G' →L[R] F'} {A'' : E'' →L[R] F''} {B'' : G'' →L[R] F''} (hB' : (A'.coprod B').IsInvertible) (T : F →L[R] F') (U : F' →L[R] F'') (hU : Submodule.map (↑U) (↑A').range ≤ (↑A'').range) : (A''.quotientRangeCoordinate B'' ∘SL U ∘SL B') ∘SL A'.quotientRangeCoordinate B' ∘SL T ∘SL B = A''.quotientRangeCoordinate B'' ∘SL (U ∘SL T) ∘SL B

Complementary coordinate changes satisfy the cocycle law, including changes of ambient coordinates. Range containment suffices; the ambient maps need not be invertible.

theorem ContinuousLinearMap.isInvertible_quotientRangeCoordinate_comp_of_map_range_eq {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {G' : Type u_5} {E' : Type u_6} {F' : Type u_7} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] [TopologicalSpace G'] [AddCommMonoid G'] [Module R G'] [TopologicalSpace E'] [AddCommMonoid E'] [Module R E'] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] [ContinuousAdd F'] {A : E →L[R] F} {B : G →L[R] F} {A' : E' →L[R] F'} {B' : G' →L[R] F'} (hB : (A.coprod B).IsInvertible) (hB' : (A'.coprod B').IsInvertible) (T : F ≃L[R] F') (hT : Submodule.map (↑↑T) (↑A).range = (↑A').range) : (A'.quotientRangeCoordinate B' ∘SL ↑T ∘SL B).IsInvertible

An ambient equivalence carrying one tangent range onto another induces an invertible change between any valid complementary coordinates.

theorem ContinuousLinearMap.isInvertible_quotientRangeCoordinate_comp {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {G' : Type u_5} [Semiring R] [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] [TopologicalSpace G'] [AddCommMonoid G'] [Module R G'] {A : E →L[R] F} {B : G →L[R] F} {C : G' →L[R] F} (hB : (A.coprod B).IsInvertible) (hC : (A.coprod C).IsInvertible) : (A.quotientRangeCoordinate C ∘SL B).IsInvertible

Transitions between two valid complementary parametrizations are invertible.