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

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)

def ContinuousAlternatingMap.toContinuousMultilinearMapCLM {𝕜 : 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] (R : Type u_5) [Semiring R] [Module R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜 R F] :

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

The inclusion of alternating continuous multi-linear maps into continuous multi-linear maps as a continuous linear map.

Equations

ContinuousAlternatingMap.toContinuousMultilinearMapCLM R = { toLinearMap := ContinuousAlternatingMap.toContinuousMultilinearMapLinear, cont := ⋯ }

Instances For

@[simp]

theorem ContinuousAlternatingMap.toContinuousMultilinearMapCLM_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] (R : Type u_5) [Semiring R] [Module R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜 R F] :

⇑(toContinuousMultilinearMapCLM R) = toContinuousMultilinearMap

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 𝕜')

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.liftCLM {𝕜 : 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] {G : Type u_5} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) => E) F) (hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0) :

G →L[𝕜] E [⋀^ι]→L[𝕜] F

Given a continuous linear map taking values in the space of continuous multilinear maps such that all of its values are alternating maps, lift it to a continuous linear map taking values in the space of continuous alternating maps.

Equations

ContinuousAlternatingMap.liftCLM f hf = { toFun := fun (x : G) => { toContinuousMultilinearMap := f x, map_eq_zero_of_eq' := ⋯ }, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Instances For

@[simp]

theorem ContinuousAlternatingMap.liftCLM_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] {G : Type u_5} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) => E) F) (hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0) (x : G) (v : ι → E) :

((liftCLM f hf) x) v = (f x) v

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] [ContinuousConstSMul 𝕜 F] [ContinuousSMul 𝕜 E] (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] [ContinuousConstSMul 𝕜 F] [ContinuousSMul 𝕜 E] {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] {α : Type u_5} {p : α → E [⋀^ι]→L[𝕜] F} [T2Space F] (hp : Summable p) (m : ι → E) :

(∑' (a : α), p a) m = ∑' (a : α), (p a) m