Currying and regrouping a tuple, topologically

A family of spaces indexed by a sigma type has the same sections as the curried family: the equivalence Equiv.piCurry is a homeomorphism for the product topologies. Composing it with a bijection between the sigma index and another index presents a tuple as a family of tuples.

Mathlib has Homeomorph.piCurry for a product index X × Y; the sigma-indexed version below is what a varying family of index types needs.

Main declarations

• TauCeti.piCurryHomeomorph: Equiv.piCurry as a homeomorphism.
• TauCeti.piSigmaHomeomorph: reindex a curried dependent family along an equivalence from its sigma index.
• TauCeti.piSigmaConstHomeomorph: along an explicit equivalence from a sigma index, a homeomorphism between a family of tuples and a tuple in a fixed space.

def TauCeti.piCurryHomeomorph {ι : Type u_1} {κ : ι → Type u_2} (Y : (i : ι) → κ i → Type u_3) [(i : ι) → (j : κ i) → TopologicalSpace (Y i j)] : ((p : (i : ι) × κ i) → Y p.fst p.snd) ≃ₜ ((i : ι) → (j : κ i) → Y i j)

Currying a sigma-indexed family of spaces, as a homeomorphism.

Equations

• TauCeti.piCurryHomeomorph Y = { toEquiv := Equiv.piCurry Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.piCurryHomeomorph_apply {ι : Type u_1} {κ : ι → Type u_2} (Y : (i : ι) → κ i → Type u_3) [(i : ι) → (j : κ i) → TopologicalSpace (Y i j)] (f : (p : (i : ι) × κ i) → Y p.fst p.snd) (i : ι) (j : κ i) : (piCurryHomeomorph Y) f i j = f ⟨i, j⟩

@[simp]

theorem TauCeti.piCurryHomeomorph_symm_apply {ι : Type u_1} {κ : ι → Type u_2} (Y : (i : ι) → κ i → Type u_3) [(i : ι) → (j : κ i) → TopologicalSpace (Y i j)] (f : (i : ι) → (j : κ i) → Y i j) (p : (i : ι) × κ i) : (piCurryHomeomorph Y).symm f p = f p.fst p.snd

def TauCeti.piSigmaHomeomorph {ι : Type u_1} {κ : ι → Type u_2} (Z : ι → Type u_3) [(i : ι) → TopologicalSpace (Z i)] {ι' : Type u_4} (e : (i : ι) × κ i ≃ ι') : ((i : ι) → κ i → Z i) ≃ₜ ((j : ι') → Z (e.symm j).fst)

Regrouping a dependent family. Curry a family indexed by a sigma type, then reindex its uncurried form along an explicit equivalence.

Equations

• TauCeti.piSigmaHomeomorph Z e = (TauCeti.piCurryHomeomorph fun (i : ι) (x : κ i) => Z i).symm.trans (Homeomorph.piCongrLeft e.symm).symm

@[simp]

theorem TauCeti.piSigmaHomeomorph_apply {ι : Type u_1} {κ : ι → Type u_2} (Z : ι → Type u_3) [(i : ι) → TopologicalSpace (Z i)] {ι' : Type u_4} (e : (i : ι) × κ i ≃ ι') (f : (i : ι) → κ i → Z i) (j : ι') : (piSigmaHomeomorph Z e) f j = f (e.symm j).fst (e.symm j).snd

def TauCeti.piSigmaConstHomeomorph (Y : Type u_1) [TopologicalSpace Y] {ι : Type u_2} {κ : ι → Type u_3} {ι' : Type u_4} (e : (i : ι) × κ i ≃ ι') : ((i : ι) → κ i → Y) ≃ₜ (ι' → Y)

Regrouping a tuple in a fixed space. An explicit bijection from a sigma type to another index type identifies a family of tuples of points of Y with one tuple of points of Y.

Equations

• TauCeti.piSigmaConstHomeomorph Y e = TauCeti.piSigmaHomeomorph (fun (x : ι) => Y) e

@[simp]

theorem TauCeti.piSigmaConstHomeomorph_apply (Y : Type u_1) [TopologicalSpace Y] {ι : Type u_2} {κ : ι → Type u_3} {ι' : Type u_4} (e : (i : ι) × κ i ≃ ι') (f : (i : ι) → κ i → Y) (j : ι') : (piSigmaConstHomeomorph Y e) f j = f (e.symm j).fst (e.symm j).snd

@[simp]

theorem TauCeti.piSigmaConstHomeomorph_symm_apply (Y : Type u_1) [TopologicalSpace Y] {ι : Type u_2} {κ : ι → Type u_3} {ι' : Type u_4} (e : (i : ι) × κ i ≃ ι') (f : ι' → Y) (i : ι) (j : κ i) : (piSigmaConstHomeomorph Y e).symm f i j = f (e ⟨i, j⟩)