Continuous linear regrouping of coordinate families

ContinuousLinearEquiv.piOptionEquivProd splits a dependent family indexed by Option ι into its none coordinate and its some coordinates. It supplies product coordinates for linear charts, with no finiteness or norm assumptions.

The construction combines LinearEquiv.piOptionEquivProd with TauCeti.piOptionEquivProdHomeomorph.

For Mathlib's ContinuousLinearEquiv.sumPiEquivProdPi, which splits a family indexed by S ⊕ T into its restrictions to S and to T, ContinuousLinearEquiv.sumPiEquivProdPi_apply and ContinuousLinearEquiv.sumPiEquivProdPi_symm_apply evaluate the equivalence and its inverse.

TauCeti.piSigmaConstContinuousLinearEquiv regroups a family of tuples along a bijection of its sigma index. Its underlying homeomorphism is TauCeti.piSigmaConstHomeomorph, which is linear coordinatewise, so coordinate calculations can use both the homeomorphism and the linear API.

def ContinuousLinearEquiv.piOptionEquivProd (R : Type u_1) [Semiring R] {ι : Type u_2} {M : Option ι → Type u_3} [(i : Option ι) → AddCommMonoid (M i)] [(i : Option ι) → Module R (M i)] [(i : Option ι) → TopologicalSpace (M i)] : ((i : Option ι) → M i) ≃L[R] M none × ((i : ι) → M (some i))

Split a family indexed by Option ι into its distinguished coordinate and the rest.

@[simp]

theorem ContinuousLinearEquiv.piOptionEquivProd_apply (R : Type u_1) [Semiring R] {ι : Type u_2} {M : Option ι → Type u_3} [(i : Option ι) → AddCommMonoid (M i)] [(i : Option ι) → Module R (M i)] [(i : Option ι) → TopologicalSpace (M i)] (x : (i : Option ι) → M i) : (piOptionEquivProd R) x = (x none, fun (i : ι) => x (some i))

The split coordinates are the none value followed by the some values.

@[simp]

theorem ContinuousLinearEquiv.piOptionEquivProd_symm_apply (R : Type u_1) [Semiring R] {ι : Type u_2} {M : Option ι → Type u_3} [(i : Option ι) → AddCommMonoid (M i)] [(i : Option ι) → Module R (M i)] [(i : Option ι) → TopologicalSpace (M i)] (q : M none × ((i : ι) → M (some i))) : (piOptionEquivProd R).symm q = fun (i : Option ι) => match i with | none => q.1 | some j => q.2 j

Reassemble an optional coordinate family from its distinguished value and the rest.

@[simp]

theorem ContinuousLinearEquiv.sumPiEquivProdPi_apply (R : Type u_1) [Semiring R] {S : Type u_4} {T : Type u_5} {A : S ⊕ T → Type u_6} [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] [(st : S ⊕ T) → TopologicalSpace (A st)] (x : (st : S ⊕ T) → A st) : (sumPiEquivProdPi R S T A) x = (fun (s : S) => x (Sum.inl s), fun (t : T) => x (Sum.inr t))

Mathlib's ContinuousLinearEquiv.sumPiEquivProdPi restricts a family on S ⊕ T to S and to T.

@[simp]

theorem ContinuousLinearEquiv.sumPiEquivProdPi_symm_apply (R : Type u_1) [Semiring R] {S : Type u_4} {T : Type u_5} {A : S ⊕ T → Type u_6} [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] [(st : S ⊕ T) → TopologicalSpace (A st)] (p : ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))) : (sumPiEquivProdPi R S T A).symm p = fun (t : S ⊕ T) => Sum.rec p.1 p.2 t

The inverse of ContinuousLinearEquiv.sumPiEquivProdPi glues a family on S and a family on T into a family on S ⊕ T.

def TauCeti.piSigmaConstContinuousLinearEquiv (R : Type u_1) [Semiring R] (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Module R E] {ι : Type u_3} {κ : ι → Type u_4} {ι' : Type u_5} (e : (i : ι) × κ i ≃ ι') : ((i : ι) → κ i → E) ≃L[R] ι' → E

Regrouping a family of tuples along a bijection of the sigma index, as a continuous linear equivalence. The underlying homeomorphism is TauCeti.piSigmaConstHomeomorph.

@[simp]

theorem TauCeti.coe_piSigmaConstContinuousLinearEquiv (R : Type u_1) [Semiring R] (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Module R E] {ι : Type u_3} {κ : ι → Type u_4} {ι' : Type u_5} (e : (i : ι) × κ i ≃ ι') : ⇑(piSigmaConstContinuousLinearEquiv R E e) = ⇑(piSigmaConstHomeomorph E e)

The continuous linear regrouping has the existing regrouping homeomorphism as its function.

@[simp]

theorem TauCeti.coe_piSigmaConstContinuousLinearEquiv_symm (R : Type u_1) [Semiring R] (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Module R E] {ι : Type u_3} {κ : ι → Type u_4} {ι' : Type u_5} (e : (i : ι) × κ i ≃ ι') : ⇑(piSigmaConstContinuousLinearEquiv R E e).symm = ⇑(piSigmaConstHomeomorph E e).symm

The inverse continuous linear regrouping has the inverse regrouping homeomorphism as its function.