Documentation

Mathlib.Topology.Algebra.Module.Alternating.Topology

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.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] [IsTopologicalAddGroup F] :

TopologicalSpace (E [⋀^ι]→L[𝕜] F)

Equations

ContinuousAlternatingMap.instTopologicalSpace = TopologicalSpace.induced ContinuousAlternatingMap.toContinuousMultilinearMap inferInstance

theorem ContinuousAlternatingMap.isClosed_range_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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F] :

IsClosed (Set.range toContinuousMultilinearMap)

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] [IsUniformAddGroup F] :

UniformSpace (E [⋀^ι]→L[𝕜] F)

Equations

ContinuousAlternatingMap.instUniformSpace = UniformSpace.comap ContinuousAlternatingMap.toContinuousMultilinearMap inferInstance

theorem ContinuousAlternatingMap.isUniformEmbedding_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] [IsUniformAddGroup F] :

IsUniformEmbedding 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] [IsUniformAddGroup F] :

UniformContinuous 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] [IsUniformAddGroup 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] [IsUniformAddGroup F] [ContinuousSMul 𝕜 E] (x : ι → E) :

UniformContinuous fun (f : E [⋀^ι]→L[𝕜] F) => f x

instance ContinuousAlternatingMap.instIsUniformAddGroup {𝕜 : 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] [IsUniformAddGroup F] :

IsUniformAddGroup (E [⋀^ι]→L[𝕜] F)

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] [IsUniformAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :

UniformContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)

theorem ContinuousAlternatingMap.isUniformInducing_postcomp {𝕜 : 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] [IsUniformAddGroup F] {G : Type u_5} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [Module 𝕜 G] (g : F →L[𝕜] G) (hg : IsUniformInducing ⇑g) :

IsUniformInducing g.compContinuousAlternatingMap

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] [IsUniformAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (h : Topology.IsCoherentWith {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] [IsUniformAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [IsTopologicalAddGroup E] [SequentialSpace (ι → E)] :

CompleteSpace (E [⋀^ι]→L[𝕜] F)

theorem ContinuousAlternatingMap.isUniformEmbedding_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] [IsUniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousSMul 𝕜 E] :

IsUniformEmbedding (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] [IsUniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousSMul 𝕜 E] :

UniformContinuous (restrictScalars 𝕜')

theorem ContinuousAlternatingMap.isEmbedding_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] [IsTopologicalAddGroup F] :

Topology.IsEmbedding toContinuousMultilinearMap

@[deprecated ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap (since := "2024-10-26")]

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] [IsTopologicalAddGroup F] :

Topology.IsEmbedding toContinuousMultilinearMap

Alias of ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap.

instance ContinuousAlternatingMap.instIsTopologicalAddGroup {𝕜 : 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] [IsTopologicalAddGroup F] :

IsTopologicalAddGroup (E [⋀^ι]→L[𝕜] F)

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] [IsTopologicalAddGroup F] :

Continuous 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] [IsTopologicalAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :

ContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)

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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] :

ContinuousSMul 𝕜 (E [⋀^ι]→L[𝕜] F)

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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup 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.isClosedEmbedding_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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F] :

Topology.IsClosedEmbedding toContinuousMultilinearMap

instance ContinuousAlternatingMap.instContinuousEvalConst {𝕜 : 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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] :

ContinuousEvalConst (E [⋀^ι]→L[𝕜] F) (ι → E) F

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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F] :

T2Space (E [⋀^ι]→L[𝕜] F)

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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F] :

T3Space (E [⋀^ι]→L[𝕜] F)

theorem ContinuousAlternatingMap.isEmbedding_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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] :

Topology.IsEmbedding (restrictScalars 𝕜')

@[deprecated ContinuousAlternatingMap.isEmbedding_restrictScalars (since := "2024-10-26")]

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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] :

Topology.IsEmbedding (restrictScalars 𝕜')

Alias of ContinuousAlternatingMap.isEmbedding_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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] :

Continuous (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] [IsTopologicalAddGroup 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 := ⋯ }

Instances For

@[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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousConstSMul 𝕜' F] :

⇑(restrictScalarsCLM 𝕜') = restrictScalars 𝕜'

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] [IsTopologicalAddGroup 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 := ⋯ }

Instances For

@[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] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] {m : ι → E} {c : E [⋀^ι]→L[𝕜] F} :

(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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup 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