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.

@[implicit_reducible]

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)

@[implicit_reducible]

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}

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 multilinear maps into continuous multilinear maps as a continuous linear map.

Equations

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

@[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.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 𝕜')

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

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

@[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.compContinuousLinearMapCLM {𝕜 : 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] {E' : Type u_6} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [ContinuousConstSMul 𝕜 F] (f : E →L[𝕜] E') : E' [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] F

Composition of a continuous alternating map and a continuous linear map as a bundled continuous linear map.

Note that for general topological vector spaces, this function does not need to be continuous in f.

Equations

• ContinuousAlternatingMap.compContinuousLinearMapCLM f = { toLinearMap := ContinuousAlternatingMap.compContinuousLinearMapₗ f, cont := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.compContinuousLinearMapCLM_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] {E' : Type u_6} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [ContinuousConstSMul 𝕜 F] (f : E →L[𝕜] E') (g : E' [⋀^ι]→L[𝕜] F) : (compContinuousLinearMapCLM f) g = g.compContinuousLinearMap f

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

@[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

def ContinuousLinearMap.compContinuousAlternatingMapCLM (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) (G : Type u_4) (ι : Type u_5) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] : (F →L[𝕜] G) →L[𝕜] E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G

ContinuousLinearMap.compContinuousAlternatingMap as a bundled continuous bilinear map.

Given a continuous linear map g : F →L[𝕜] G and a continuous alternating map f : E [⋀^ι]→L[𝕜] F, it returns the continuous alternating map g ∘ f. This function is continuous in f (for each g) and in g (as a function taking values in continuous linear maps). Note that for a general topological vector space, the map is not guaranteed to be continuous in (g, f).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) (G : Type u_4) (ι : Type u_5) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F →L[𝕜] G) (f : E [⋀^ι]→L[𝕜] F) : ((compContinuousAlternatingMapCLM 𝕜 E F G ι) g) f = g.compContinuousAlternatingMap f

def ContinuousLinearEquiv.continuousAlternatingMapCongrRight {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G) : E [⋀^ι]→L[𝕜] F ≃L[𝕜] E [⋀^ι]→L[𝕜] G

ContinuousLinearMap.compContinuousAlternatingMap as a bundled continuous linear equiv.

Given a continuous linear equivalence g : F ≃L[𝕜] G, this function returns the equivalence between continuous alternating maps with codomain F and continuous alternating maps with codomain G that acts by composing these maps with g.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongrRight_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G) (a✝ : E [⋀^ι]→L[𝕜] F) : g.continuousAlternatingMapCongrRight a✝ = (↑g).compContinuousAlternatingMap a✝

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G) : g.continuousAlternatingMapCongrRight.symm = g.symm.continuousAlternatingMapCongrRight

def ContinuousLinearEquiv.continuousAlternatingMapCongrLeft {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {ι : Type u_6} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (f : E ≃L[𝕜] E') : E [⋀^ι]→L[𝕜] F ≃L[𝕜] E' [⋀^ι]→L[𝕜] F

Given a continuous linear isomorphism between the domains, generate a continuous linear isomorphism between the spaces of continuous alternating maps.

This is ContinuousAlternatingMap.compContinuousLinearMap as an equivalence, and is the continuous version of AlternatingMap.domLCongr.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongrLeft_apply {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {ι : Type u_6} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (f : E ≃L[𝕜] E') (g : E [⋀^ι]→L[𝕜] F) : f.continuousAlternatingMapCongrLeft g = g.compContinuousLinearMap ↑f.symm

def ContinuousLinearEquiv.continuousAlternatingMapCongr {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (e : E ≃L[𝕜] E') (e' : F ≃L[𝕜] G) : E [⋀^ι]→L[𝕜] F ≃L[𝕜] E' [⋀^ι]→L[𝕜] G

Continuous linear equivalences between the domains and the codomains generate a continuous linear equivalence between the spaces of continuous alternating maps.

Equations

• e.continuousAlternatingMapCongr e' = e.continuousAlternatingMapCongrLeft.trans e'.continuousAlternatingMapCongrRight

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongr_apply {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (e : E ≃L[𝕜] E') (e' : F ≃L[𝕜] G) (a✝ : E [⋀^ι]→L[𝕜] F) : (e.continuousAlternatingMapCongr e') a✝ = (↑e').compContinuousAlternatingMap (a✝.compContinuousLinearMap ↑e.symm)