Total spaces of quotients by varying operator ranges

For a family of linear operators A x : E →L[R] F, take the class of each ambient vector in F ⧸ (A x).range. With the quotient topology on the total space, this map is open whenever x ↦ A x u is continuous for every fixed u. No injectivity, complement, or constant-rank assumption is needed for openness.

The scalars form a ring because Mathlib's Submodule.hasQuotient requires one to define the fibre quotients, even when the ambient modules are additive groups.

On a domain with a fixed complementary parametrization B, the fibre equivalences ContinuousLinearMap.quotientRangeEquiv assemble into a homeomorphism with the product of the base and the complement. These are the topological local coordinates for quotient bundles such as intrinsic normal bundles. The topology is supplied as an explicit quotient-map hypothesis, so this construction preserves an existing total-space topology rather than introducing a competing instance.

The openness argument uses saturation by translations, as in Mathlib's isOpenMap_quotient_mk'_add. The coordinate construction uses ContinuousLinearMap.quotientRangeEquiv and its representative formulas. Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, the normal-bundle construction preceding Theorem 6.24.

def TauCeti.rangeQuotientMap {R : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] (A : X → E →L[R] F) : X × F → Bundle.TotalSpace G fun (x : X) => F ⧸ (↑(A x)).range

Taking ambient representatives to their classes in the quotients by a family of ranges.

@[simp]

theorem TauCeti.rangeQuotientMap_apply {R : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] (A : X → E →L[R] F) (x : X) (v : F) : rangeQuotientMap A (x, v) = { proj := x, snd := Submodule.Quotient.mk v }

theorem TauCeti.rangeQuotientMap_surjective {R : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] (A : X → E →L[R] F) : Function.Surjective (rangeQuotientMap A)

Every range-quotient class has an ambient representative with the same base point.

theorem TauCeti.preimage_image_rangeQuotientMap {R : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] (A : X → E →L[R] F) (U : Set (X × F)) : rangeQuotientMap A ⁻¹' rangeQuotientMap A '' U = ⋃ (u : E), (fun (p : X × F) => (p.1, p.2 - (A p.1) u)) ⁻¹' U

Saturation by range classes is the union of translations by range representatives.

theorem Topology.IsQuotientMap.isOpenQuotientMap_rangeQuotientMap {R : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [TopologicalSpace X] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousSub F] {A : X → E →L[R] F} [TopologicalSpace (Bundle.TotalSpace G fun (x : X) => F ⧸ (↑(A x)).range)] (hq : IsQuotientMap (TauCeti.rangeQuotientMap A)) (hA : ∀ (u : E), Continuous fun (x : X) => (A x) u) : IsOpenQuotientMap (TauCeti.rangeQuotientMap A)

The quotient by continuously varying ranges is an open quotient, including when the operators are not injective and their ranges have varying dimension.

noncomputable def TauCeti.rangeQuotientHomeomorph {R : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [TopologicalSpace X] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommGroup G] [Module R G] (A : X → E →L[R] F) (B : G →L[R] F) [TopologicalSpace (Bundle.TotalSpace G fun (x : X) => F ⧸ (↑(A x)).range)] (h : ∀ (x : X), ((A x).coprod B).IsInvertible) (hq : Topology.IsQuotientMap (rangeQuotientMap A)) (hc : Continuous fun (p : X × F) => ((A p.1).quotientRangeCoordinate B) p.2) : (Bundle.TotalSpace G fun (x : X) => F ⧸ (↑(A x)).range) ≃ₜ X × G

A common complement identifies the total range-quotient space with a product. Continuity of the complementary coordinate is tested on ambient representatives.

@[simp]

theorem TauCeti.rangeQuotientHomeomorph_apply {R : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [TopologicalSpace X] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommGroup G] [Module R G] (A : X → E →L[R] F) (B : G →L[R] F) [TopologicalSpace (Bundle.TotalSpace G fun (x : X) => F ⧸ (↑(A x)).range)] (h : ∀ (x : X), ((A x).coprod B).IsInvertible) (hq : Topology.IsQuotientMap (rangeQuotientMap A)) (hc : Continuous fun (p : X × F) => ((A p.1).quotientRangeCoordinate B) p.2) (p : Bundle.TotalSpace G fun (x : X) => F ⧸ (↑(A x)).range) : (rangeQuotientHomeomorph A B h hq hc) p = (p.proj, ((A p.proj).quotientRangeEquiv B ⋯) p.snd)

Complementary coordinates of a quotient class, with the base point retained.

@[simp]

theorem TauCeti.rangeQuotientHomeomorph_symm_apply {R : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [TopologicalSpace X] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] [TopologicalSpace G] [AddCommGroup G] [Module R G] (A : X → E →L[R] F) (B : G →L[R] F) [TopologicalSpace (Bundle.TotalSpace G fun (x : X) => F ⧸ (↑(A x)).range)] (h : ∀ (x : X), ((A x).coprod B).IsInvertible) (hq : Topology.IsQuotientMap (rangeQuotientMap A)) (hc : Continuous fun (p : X × F) => ((A p.1).quotientRangeCoordinate B) p.2) (p : X × G) : (rangeQuotientHomeomorph A B h hq hc).symm p = { proj := p.1, snd := Submodule.Quotient.mk (B p.2) }

Inverse total-space coordinates take the class of the complementary representative.