Continuous linear equivalences on (dependent) product types

Main Definitions

• sumPiEquivProdPi: Equiv.sumPiEquivProdPi as a continuous linear equivalence.
• piUnique: Equiv.piUnique as a continuous linear equivalence.
• piCongrLeft: Equiv.piCongrLeft as a continuous linear equivalence.
• piCongrRight: Equiv.piCongrRight as a continuous linear equivalence.
• Fin.consEquivL: Fin.consEquiv as a continuous linear equivalence.
• ContinuousLinearMap.finCons: Fin.cons in the codomain of continuous linear maps.

def ContinuousLinearMap.iInfKerProjEquiv (R : Type u_1) [Semiring R] {ι : Type u_4} (φ : ι → Type u_5) [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I J : Set ι} [DecidablePred fun (i : ι) => i ∈ I] (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) : ↥(⨅ i ∈ J, (↑(proj i)).ker) ≃L[R] (i : ↑I) → φ ↑i

If I and J are complementary index sets, the product of the kernels of the Jth projections of φ is linearly equivalent to the product over I.

def ContinuousLinearEquiv.piCongrLeft (R : Type u_1) [Semiring R] {ι : Type u_2} {ι' : Type u_3} (φ : ι → Type u_4) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → TopologicalSpace (φ i)] (e : ι' ≃ ι) : ((i' : ι') → φ (e i')) ≃L[R] (i : ι) → φ i

Combine a family of linear equivalences into a linear equivalence of pi-types. This is Equiv.piCongrLeft as a ContinuousLinearEquiv.

def ContinuousLinearEquiv.sumPiEquivProdPi (R : Type u_1) [Semiring R] (S : Type u_2) (T : Type u_3) (A : S ⊕ T → Type u_4) [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] [(st : S ⊕ T) → TopologicalSpace (A st)] : ((st : S ⊕ T) → A st) ≃L[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))

The product over S ⊕ T of a family of topological modules is isomorphic (topologically and algebraically) to the product of (the product over S) and (the product over T).

This is Equiv.sumPiEquivProdPi as a ContinuousLinearEquiv.

def ContinuousLinearEquiv.piUnique (R : Type u_1) [Semiring R] {α : Type u_2} [Unique α] (f : α → Type u_3) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] [(x : α) → TopologicalSpace (f x)] : ((t : α) → f t) ≃L[R] f default

The product Π t : α, f t of a family of topological modules is isomorphic (both topologically and algebraically) to the space f ⬝ when α only contains ⬝.

This is Equiv.piUnique as a ContinuousLinearEquiv.

@[simp]

theorem ContinuousLinearEquiv.piUnique_apply (R : Type u_1) [Semiring R] {α : Type u_2} [Unique α] (f : α → Type u_3) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] [(x : α) → TopologicalSpace (f x)] : ⇑(piUnique R f) = fun (f : (i : α) → f i) => f default

@[simp]

theorem ContinuousLinearEquiv.piUnique_symm_apply (R : Type u_1) [Semiring R] {α : Type u_2} [Unique α] (f : α → Type u_3) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] [(x : α) → TopologicalSpace (f x)] : ⇑(piUnique R f).symm = uniqueElim

def ContinuousLinearEquiv.piCongrRight {R : Type u_1} [Semiring R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_4} [(i : ι) → TopologicalSpace (N i)] [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i ≃L[R] N i) : ((i : ι) → M i) ≃L[R] (i : ι) → N i

Combine a family of continuous linear equivalences into a continuous linear equivalence of pi-types.

@[simp]

theorem ContinuousLinearEquiv.piCongrRight_apply {R : Type u_1} [Semiring R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_4} [(i : ι) → TopologicalSpace (N i)] [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i ≃L[R] N i) (m : (i : ι) → M i) (i : ι) : (piCongrRight f) m i = (f i) (m i)

@[simp]

theorem ContinuousLinearEquiv.piCongrRight_symm_apply {R : Type u_1} [Semiring R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_4} [(i : ι) → TopologicalSpace (N i)] [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i ≃L[R] N i) (n : (i : ι) → N i) (i : ι) : (piCongrRight f).symm n i = (f i).symm (n i)

def ContinuousLinearEquiv.funUnique (ι : Type u_2) (R : Type u_3) (M : Type u_4) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] : (ι → M) ≃L[R] M

If ι has a unique element, then ι → M is continuously linear equivalent to M.

@[simp]

theorem ContinuousLinearEquiv.coe_funUnique {ι : Type u_2} {R : Type u_3} {M : Type u_4} [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] : ⇑(funUnique ι R M) = Function.eval default

@[simp]

theorem ContinuousLinearEquiv.coe_funUnique_symm {ι : Type u_2} {R : Type u_3} {M : Type u_4} [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] : ⇑(funUnique ι R M).symm = Function.const ι

def ContinuousLinearEquiv.piFinTwo (R : Type u_3) [Semiring R] (M : Fin 2 → Type u_5) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] [(i : Fin 2) → TopologicalSpace (M i)] : ((i : Fin 2) → M i) ≃L[R] M 0 × M 1

Continuous linear equivalence between dependent functions (i : Fin 2) → M i and M 0 × M 1.

@[simp]

theorem ContinuousLinearEquiv.piFinTwo_symm_apply (R : Type u_3) [Semiring R] (M : Fin 2 → Type u_5) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] [(i : Fin 2) → TopologicalSpace (M i)] : ⇑(piFinTwo R M).symm = fun (p : M 0 × M 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)

@[simp]

theorem ContinuousLinearEquiv.piFinTwo_apply (R : Type u_3) [Semiring R] (M : Fin 2 → Type u_5) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] [(i : Fin 2) → TopologicalSpace (M i)] : ⇑(piFinTwo R M) = fun (f : (i : Fin 2) → M i) => (f 0, f 1)

def ContinuousLinearEquiv.finTwoArrow (R : Type u_3) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] : (Fin 2 → M) ≃L[R] M × M

Continuous linear equivalence between vectors in M² = Fin 2 → M and M × M.

@[simp]

theorem ContinuousLinearEquiv.finTwoArrow_symm_apply (R : Type u_3) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] : ⇑(finTwoArrow R M).symm = fun (x : M × M) => ![x.1, x.2]

@[simp]

theorem ContinuousLinearEquiv.finTwoArrow_apply (R : Type u_3) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] : ⇑(finTwoArrow R M) = fun (f : Fin 2 → M) => (f 0, f 1)

def Fin.consEquivL (R : Type u_3) [Semiring R] {n : ℕ} (M : Fin n.succ → Type u_5) [(i : Fin n.succ) → AddCommMonoid (M i)] [(i : Fin n.succ) → Module R (M i)] [(i : Fin n.succ) → TopologicalSpace (M i)] : (M 0 × ((i : Fin n) → M i.succ)) ≃L[R] (i : Fin n.succ) → M i

Fin.consEquiv as a continuous linear equivalence.

@[simp]

theorem Fin.consEquivL_apply (R : Type u_3) [Semiring R] {n : ℕ} (M : Fin n.succ → Type u_5) [(i : Fin n.succ) → AddCommMonoid (M i)] [(i : Fin n.succ) → Module R (M i)] [(i : Fin n.succ) → TopologicalSpace (M i)] (a✝ : M 0 × ((i : Fin n) → M i.succ)) (i : Fin (n + 1)) : (consEquivL R M) a✝ i = cons a✝.1 a✝.2 i

@[simp]

theorem Fin.consEquivL_symm_apply (R : Type u_3) [Semiring R] {n : ℕ} (M : Fin n.succ → Type u_5) [(i : Fin n.succ) → AddCommMonoid (M i)] [(i : Fin n.succ) → Module R (M i)] [(i : Fin n.succ) → TopologicalSpace (M i)] (a✝ : (i : Fin (n + 1)) → M i) : (consEquivL R M).symm a✝ = (a✝ 0, tail a✝)

@[reducible, inline]

abbrev ContinuousLinearMap.finCons {R : Type u_3} [Semiring R] {n : ℕ} {M : Fin n.succ → Type u_5} {N : Type u_6} [(i : Fin n.succ) → AddCommMonoid (M i)] [(i : Fin n.succ) → Module R (M i)] [(i : Fin n.succ) → TopologicalSpace (M i)] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : N →L[R] M 0) (fs : N →L[R] (i : Fin n) → M i.succ) : N →L[R] (i : Fin n.succ) → M i

Fin.cons in the codomain of continuous linear maps.