Topology on continuous alternating maps

In this file we define UniformSpace and TopologicalSpace structures on the space of continuous alternating maps between topological vector spaces.

The structures are induced by those on ContinuousMultilinearMaps, and most of the lemmas follow from the corresponding lemmas about ContinuousMultilinearMaps.

instance ContinuousAlternatingMap.instUniformSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : UniformSpace (E [⋀^ι]→L[𝕜] F)

Equations

• ContinuousAlternatingMap.instUniformSpace = UniformSpace.comap ContinuousAlternatingMap.toContinuousMultilinearMap inferInstance

theorem ContinuousAlternatingMap.uniformEmbedding_toContinuousMultilinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : UniformEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap

theorem ContinuousAlternatingMap.uniformContinuous_toContinuousMultilinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : UniformContinuous ContinuousAlternatingMap.toContinuousMultilinearMap

theorem ContinuousAlternatingMap.uniformContinuous_coe_fun {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜 E] : UniformContinuous DFunLike.coe

theorem ContinuousAlternatingMap.uniformContinuous_eval_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜 E] (x : ι → E) : UniformContinuous fun (f : E [⋀^ι]→L[𝕜] F) => f x

instance ContinuousAlternatingMap.instUniformAddGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : UniformAddGroup (E [⋀^ι]→L[𝕜] F)

Equations

• ⋯ = ⋯

instance ContinuousAlternatingMap.instUniformContinuousConstSMul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] : UniformContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)

Equations

• ⋯ = ⋯

theorem ContinuousAlternatingMap.completeSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [T2Space F] (h : RestrictGenTopology {s : Set (ι → E) | Bornology.IsVonNBounded 𝕜 s}) : CompleteSpace (E [⋀^ι]→L[𝕜] F)

instance ContinuousAlternatingMap.instCompleteSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [T2Space F] [TopologicalAddGroup E] [SequentialSpace (ι → E)] : CompleteSpace (E [⋀^ι]→L[𝕜] F)

Equations

• ⋯ = ⋯

theorem ContinuousAlternatingMap.uniformEmbedding_restrictScalars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousSMul 𝕜 E] : UniformEmbedding (ContinuousAlternatingMap.restrictScalars 𝕜')

theorem ContinuousAlternatingMap.uniformContinuous_restrictScalars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousSMul 𝕜 E] : UniformContinuous (ContinuousAlternatingMap.restrictScalars 𝕜')

instance ContinuousAlternatingMap.instTopologicalSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] : TopologicalSpace (E [⋀^ι]→L[𝕜] F)

Equations

• ContinuousAlternatingMap.instTopologicalSpace = TopologicalSpace.induced ContinuousAlternatingMap.toContinuousMultilinearMap inferInstance

theorem ContinuousAlternatingMap.embedding_toContinuousMultilinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] : Embedding ContinuousAlternatingMap.toContinuousMultilinearMap

theorem ContinuousAlternatingMap.continuous_toContinuousMultilinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] : Continuous ContinuousAlternatingMap.toContinuousMultilinearMap

instance ContinuousAlternatingMap.instContinuousConstSMul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] : ContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)

Equations

• ⋯ = ⋯

instance ContinuousAlternatingMap.instContinuousSMul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] : ContinuousSMul 𝕜 (E [⋀^ι]→L[𝕜] F)

Equations

• ⋯ = ⋯

theorem ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] {ι' : Type u_5} {p : ι' → Prop} {b : ι' → Set F} (h : (nhds 0).HasBasis p b) : (nhds 0).HasBasis (fun (Si : Set (ι → E) × ι') => Bornology.IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set (ι → E) × ι') => {f : E [⋀^ι]→L[𝕜] F | Set.MapsTo (⇑f) Si.1 (b Si.2)}

theorem ContinuousAlternatingMap.hasBasis_nhds_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] : (nhds 0).HasBasis (fun (SV : Set (ι → E) × Set F) => Bornology.IsVonNBounded 𝕜 SV.1 ∧ SV.2 ∈ nhds 0) fun (SV : Set (ι → E) × Set F) => {f : E [⋀^ι]→L[𝕜] F | Set.MapsTo (⇑f) SV.1 SV.2}

theorem ContinuousAlternatingMap.continuous_eval_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] (x : ι → E) : Continuous fun (p : E [⋀^ι]→L[𝕜] F) => p x

theorem ContinuousAlternatingMap.continuous_coe_fun {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] : Continuous DFunLike.coe

instance ContinuousAlternatingMap.instT2Space {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F] : T2Space (E [⋀^ι]→L[𝕜] F)

Equations

• ⋯ = ⋯

instance ContinuousAlternatingMap.instT3Space {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F] : T2Space (E [⋀^ι]→L[𝕜] F)

Equations

• ⋯ = ⋯

theorem ContinuousAlternatingMap.embedding_restrictScalars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : Embedding (ContinuousAlternatingMap.restrictScalars 𝕜')

theorem ContinuousAlternatingMap.continuous_restrictScalars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : Continuous (ContinuousAlternatingMap.restrictScalars 𝕜')

@[simp]

theorem ContinuousAlternatingMap.restrictScalarsCLM_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousConstSMul 𝕜' F] : ⇑(ContinuousAlternatingMap.restrictScalarsCLM 𝕜') = ContinuousAlternatingMap.restrictScalars 𝕜'

def ContinuousAlternatingMap.restrictScalarsCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousConstSMul 𝕜' F] : E [⋀^ι]→L[𝕜] F →L[𝕜'] E [⋀^ι]→L[𝕜'] F

ContinuousMultilinearMap.restrictScalars as a ContinuousLinearMap.

Equations

• ContinuousAlternatingMap.restrictScalarsCLM 𝕜' = { toFun := ContinuousAlternatingMap.restrictScalars 𝕜', map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

def ContinuousAlternatingMap.apply (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] (m : ι → E) : E [⋀^ι]→L[𝕜] F →L[𝕜] F

The application of a multilinear map as a ContinuousLinearMap.

Equations

• ContinuousAlternatingMap.apply 𝕜 E F m = { toFun := fun (c : E [⋀^ι]→L[𝕜] F) => c m, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] {m : ι → E} {c : E [⋀^ι]→L[𝕜] F} : (ContinuousAlternatingMap.apply 𝕜 E F m) c = c m

theorem ContinuousAlternatingMap.hasSum_eval {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] {α : Type u_5} {p : α → E [⋀^ι]→L[𝕜] F} {q : E [⋀^ι]→L[𝕜] F} (h : HasSum p q) (m : ι → E) : HasSum (fun (a : α) => (p a) m) (q m)

theorem ContinuousAlternatingMap.tsum_eval {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F] {α : Type u_5} {p : α → E [⋀^ι]→L[𝕜] F} (hp : Summable p) (m : ι → E) : (∑' (a : α), p a) m = ∑' (a : α), (p a) m