Splitting and regrouping finite coordinates

Continuous linear equivalences split vectors indexed by Fin (n + m) into two blocks, split Fin n at an index d ≤ n, and regroup the initial blocks of a pair of vectors before the remaining blocks. The vanishing characterizations identify products of coordinate subspaces with a single coordinate subspace, as needed for product charts.

The constructions combine Mathlib's ContinuousLinearEquiv.piCongrLeft, sumPiEquivProdPi, and prodProdProdComm with finite-index equivalences.

def TauCeti.splitCoords {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] (n m : ℕ) : (Fin (n + m) → M) ≃L[𝕜] (Fin n → M) × (Fin m → M)

Split a concatenated vector into its two coordinate blocks.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.splitCoords_apply {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n m : ℕ} (x : Fin (n + m) → M) : (splitCoords n m) x = (fun (i : Fin n) => x (Fin.castAdd m i), fun (i : Fin m) => x (Fin.natAdd n i))

The two blocks of a split vector are its initial and final coordinates.

def TauCeti.splitAt {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n d : ℕ} (h : d ≤ n) : (Fin n → M) ≃L[𝕜] (Fin d → M) × (Fin (n - d) → M)

Split a vector into its first d coordinates and its remaining coordinates.

Equations

• TauCeti.splitAt h = (ContinuousLinearEquiv.piCongrLeft 𝕜 (fun (x : Fin n) => M) (finCongr ⋯)).symm.trans (TauCeti.splitCoords d (n - d))

@[simp]

theorem TauCeti.splitAt_fst_apply {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n d : ℕ} (h : d ≤ n) (x : Fin n → M) (i : Fin d) : ((splitAt h) x).1 i = x (Fin.castLE h i)

The initial block of a vector split at d consists of its first d coordinates.

@[simp]

theorem TauCeti.splitAt_snd_apply {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n d : ℕ} (h : d ≤ n) (x : Fin n → M) (i : Fin (n - d)) : ((splitAt h) x).2 i = x ⟨d + ↑i, ⋯⟩

The final block of a vector split at d consists of its coordinates starting at d.

@[simp]

theorem TauCeti.splitAt_snd_eq_zero_iff {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n d : ℕ} (h : d ≤ n) (x : Fin n → M) : ((splitAt h) x).2 = 0 ↔ ∀ (i : Fin n), d ≤ ↑i → x i = 0

The final block vanishes exactly when all coordinates at or beyond d vanish.

def TauCeti.productCoords {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n m d e : ℕ} (hd : d ≤ n) (he : e ≤ m) : ((Fin n → M) × (Fin m → M)) ≃L[𝕜] Fin (n + m) → M

Regroup two vectors so their initial blocks of sizes d and e come first, followed by both remaining blocks. This identifies products of coordinate subspaces with the coordinate subspace of dimension d + e.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.productCoords_apply_fst_initial {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n m d e : ℕ} (hd : d ≤ n) (he : e ≤ m) (x : (Fin n → M) × (Fin m → M)) (i : Fin d) : (productCoords hd he) x ⟨↑i, ⋯⟩ = x.1 (Fin.castLE hd i)

The first block of regrouped coordinates is the first vector's initial block.

@[simp]

theorem TauCeti.productCoords_apply_snd_initial {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n m d e : ℕ} (hd : d ≤ n) (he : e ≤ m) (x : (Fin n → M) × (Fin m → M)) (i : Fin e) : (productCoords hd he) x ⟨d + ↑i, ⋯⟩ = x.2 (Fin.castLE he i)

The second block of regrouped coordinates is the second vector's initial block.

@[simp]

theorem TauCeti.productCoords_apply_fst_final {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n m d e : ℕ} (hd : d ≤ n) (he : e ≤ m) (x : (Fin n → M) × (Fin m → M)) (i : Fin (n - d)) : (productCoords hd he) x ⟨d + e + ↑i, ⋯⟩ = x.1 ⟨d + ↑i, ⋯⟩

The third block of regrouped coordinates is the first vector's final block.

@[simp]

theorem TauCeti.productCoords_apply_snd_final {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n m d e : ℕ} (hd : d ≤ n) (he : e ≤ m) (x : (Fin n → M) × (Fin m → M)) (i : Fin (m - e)) : (productCoords hd he) x ⟨d + e + (n - d) + ↑i, ⋯⟩ = x.2 ⟨e + ↑i, ⋯⟩

The fourth block of regrouped coordinates is the second vector's final block.

theorem TauCeti.productCoords_vanishing_iff {𝕜 : Type u_1} {M : Type u_2} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M] {n m d e : ℕ} (hd : d ≤ n) (he : e ≤ m) (x : (Fin n → M) × (Fin m → M)) : (∀ (i : Fin (n + m)), d + e ≤ ↑i → (productCoords hd he) x i = 0) ↔ (∀ (i : Fin n), d ≤ ↑i → x.1 i = 0) ∧ ∀ (i : Fin m), e ≤ ↑i → x.2 i = 0

Regrouped coordinates vanish at or beyond d + e exactly when each original vector vanishes beyond its initial block.