Continuous alternating multilinear maps

In this file we define bundled continuous alternating maps and develop basic API about these maps, by reusing API about continuous multilinear maps and alternating maps.

Notation

M [⋀^ι]→L[R] N: notation for R-linear continuous alternating maps from M to N; the arguments are indexed by i : ι.

Keywords

multilinear map, alternating map, continuous

structure ContinuousAlternatingMap (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] extends ContinuousMultilinearMap : Type (max (max u_2 u_3) u_4)

A continuous alternating map from ι → M to N, denoted M [⋀^ι]→L[R] N, is a continuous map that is

• multilinear : f (update m i (c • x)) = c • f (update m i x) and f (update m i (x + y)) = f (update m i x) + f (update m i y);
• alternating : f v = 0 whenever v has two equal coordinates.

• toFun : (ι → M) → N
• map_add' : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M), self.toFun (Function.update m i (x + y)) = self.toFun (Function.update m i x) + self.toFun (Function.update m i y)
• map_smul' : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), self.toFun (Function.update m i (c • x)) = c • self.toFun (Function.update m i x)
• cont : Continuous self.toFun
• map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → self.toFun v = 0

  The map is alternating: if v has two equal coordinates, then f v = 0.

@[reducible]

abbrev ContinuousAlternatingMap.toAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (self : M [⋀^ι]→L[R] N) : M [⋀^ι]→ₗ[R] N

Projection to AlternatingMaps.

Equations

• self.toAlternatingMap = { toMultilinearMap := self.toMultilinearMap, map_eq_zero_of_eq' := ⋯ }

def «term_[⋀^_]→L[_]_» : Lean.TrailingParserDescr

A continuous alternating map from ι → M to N, denoted M [⋀^ι]→L[R] N, is a continuous map that is

• multilinear : f (update m i (c • x)) = c • f (update m i x) and f (update m i (x + y)) = f (update m i x) + f (update m i y);
• alternating : f v = 0 whenever v has two equal coordinates.

Equations

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

theorem ContinuousAlternatingMap.toContinuousMultilinearMap_injective {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : Function.Injective ContinuousAlternatingMap.toContinuousMultilinearMap

theorem ContinuousAlternatingMap.range_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : Set.range ContinuousAlternatingMap.toContinuousMultilinearMap = {f : ContinuousMultilinearMap R (fun (x : ι) => M) N | ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f v = 0}

instance ContinuousAlternatingMap.funLike {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : FunLike (M [⋀^ι]→L[R] N) (ι → M) N

Equations

• ContinuousAlternatingMap.funLike = { coe := fun (f : M [⋀^ι]→L[R] N) => f.toFun, coe_injective' := ⋯ }

instance ContinuousAlternatingMap.continuousMapClass {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : ContinuousMapClass (M [⋀^ι]→L[R] N) (ι → M) N

Equations

• ⋯ = ⋯

theorem ContinuousAlternatingMap.coe_continuous {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) : Continuous ⇑f

@[simp]

theorem ContinuousAlternatingMap.coe_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) : ⇑f.toContinuousMultilinearMap = ⇑f

@[simp]

theorem ContinuousAlternatingMap.coe_mk {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) (h : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f.toFun v = 0) : ⇑{ toContinuousMultilinearMap := f, map_eq_zero_of_eq' := h } = ⇑f

theorem ContinuousAlternatingMap.coe_toAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) : ⇑f.toAlternatingMap = ⇑f

theorem ContinuousAlternatingMap.ext {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {f : M [⋀^ι]→L[R] N} {g : M [⋀^ι]→L[R] N} (H : ∀ (x : ι → M), f x = g x) : f = g

theorem ContinuousAlternatingMap.ext_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {f : M [⋀^ι]→L[R] N} {g : M [⋀^ι]→L[R] N} : f = g ↔ ∀ (x : ι → M), f x = g x

theorem ContinuousAlternatingMap.toAlternatingMap_injective {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : Function.Injective ContinuousAlternatingMap.toAlternatingMap

@[simp]

theorem ContinuousAlternatingMap.range_toAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : Set.range ContinuousAlternatingMap.toAlternatingMap = {f : M [⋀^ι]→ₗ[R] N | Continuous ⇑f}

@[simp]

theorem ContinuousAlternatingMap.map_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ι → M) (i : ι) (x : M) (y : M) : f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)

@[simp]

theorem ContinuousAlternatingMap.map_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M) : f (Function.update m i (c • x)) = c • f (Function.update m i x)

theorem ContinuousAlternatingMap.map_coord_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {m : ι → M} (i : ι) (h : m i = 0) : f m = 0

@[simp]

theorem ContinuousAlternatingMap.map_update_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ι → M) (i : ι) : f (Function.update m i 0) = 0

@[simp]

theorem ContinuousAlternatingMap.map_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [Nonempty ι] : f 0 = 0

theorem ContinuousAlternatingMap.map_eq_zero_of_eq {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (v : ι → M) {i : ι} {j : ι} (h : v i = v j) (hij : i ≠ j) : f v = 0

theorem ContinuousAlternatingMap.map_eq_zero_of_not_injective {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (v : ι → M) (hv : ¬Function.Injective v) : f v = 0

@[simp]

theorem ContinuousAlternatingMap.codRestrict_apply_coe {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (p : Submodule R N) (h : ∀ (v : ι → M), f v ∈ p) (v : (i : ι) → (fun (x : ι) => M) i) : ↑((f.codRestrict p h) v) = f v

def ContinuousAlternatingMap.codRestrict {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (p : Submodule R N) (h : ∀ (v : ι → M), f v ∈ p) : M [⋀^ι]→L[R] ↥p

Restrict the codomain of a continuous alternating map to a submodule.

Equations

• f.codRestrict p h = let __src := f.toAlternatingMap.codRestrict p h; { toContinuousMultilinearMap := f.codRestrict p h, map_eq_zero_of_eq' := ⋯ }

instance ContinuousAlternatingMap.instZero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : Zero (M [⋀^ι]→L[R] N)

Equations

• ContinuousAlternatingMap.instZero = { zero := { toContinuousMultilinearMap := 0, map_eq_zero_of_eq' := ⋯ } }

instance ContinuousAlternatingMap.instInhabited {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : Inhabited (M [⋀^ι]→L[R] N)

Equations

• ContinuousAlternatingMap.instInhabited = { default := 0 }

@[simp]

theorem ContinuousAlternatingMap.coe_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : ⇑0 = 0

@[simp]

theorem ContinuousAlternatingMap.toContinuousMultilinearMap_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : ContinuousAlternatingMap.toContinuousMultilinearMap 0 = 0

@[simp]

theorem ContinuousAlternatingMap.toAlternatingMap_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] : ContinuousAlternatingMap.toAlternatingMap 0 = 0

instance ContinuousAlternatingMap.instSMul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] : SMul R' (M [⋀^ι]→L[A] N)

Equations

• ContinuousAlternatingMap.instSMul = { smul := fun (c : R') (f : M [⋀^ι]→L[A] N) => { toContinuousMultilinearMap := c • f.toContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ } }

@[simp]

theorem ContinuousAlternatingMap.coe_smul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] (f : M [⋀^ι]→L[A] N) (c : R') : ⇑(c • f) = c • ⇑f

theorem ContinuousAlternatingMap.smul_apply {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] (f : M [⋀^ι]→L[A] N) (c : R') (v : ι → M) : (c • f) v = c • f v

@[simp]

theorem ContinuousAlternatingMap.toContinuousMultilinearMap_smul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] (c : R') (f : M [⋀^ι]→L[A] N) : (c • f).toContinuousMultilinearMap = c • f.toContinuousMultilinearMap

@[simp]

theorem ContinuousAlternatingMap.toAlternatingMap_smul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] (c : R') (f : M [⋀^ι]→L[A] N) : (c • f).toAlternatingMap = c • f.toAlternatingMap

instance ContinuousAlternatingMap.instSMulCommClass {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {R'' : Type u_8} {A : Type u_9} [Monoid R'] [Monoid R''] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] [DistribMulAction R'' N] [ContinuousConstSMul R'' N] [SMulCommClass A R'' N] [SMulCommClass R' R'' N] : SMulCommClass R' R'' (M [⋀^ι]→L[A] N)

Equations

• ⋯ = ⋯

instance ContinuousAlternatingMap.instIsScalarTower {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {R'' : Type u_8} {A : Type u_9} [Monoid R'] [Monoid R''] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] [DistribMulAction R'' N] [ContinuousConstSMul R'' N] [SMulCommClass A R'' N] [SMul R' R''] [IsScalarTower R' R'' N] : IsScalarTower R' R'' (M [⋀^ι]→L[A] N)

Equations

• ⋯ = ⋯

instance ContinuousAlternatingMap.instIsCentralScalar {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] [DistribMulAction R'ᵐᵒᵖ N] [IsCentralScalar R' N] : IsCentralScalar R' (M [⋀^ι]→L[A] N)

Equations

• ⋯ = ⋯

instance ContinuousAlternatingMap.instMulAction {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] : MulAction R' (M [⋀^ι]→L[A] N)

Equations

• ContinuousAlternatingMap.instMulAction = Function.Injective.mulAction ContinuousAlternatingMap.toContinuousMultilinearMap ⋯ ⋯

instance ContinuousAlternatingMap.instAdd {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] : Add (M [⋀^ι]→L[R] N)

Equations

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

@[simp]

theorem ContinuousAlternatingMap.coe_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) [ContinuousAdd N] : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem ContinuousAlternatingMap.add_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) [ContinuousAdd N] (v : ι → M) : (f + g) v = f v + g v

@[simp]

theorem ContinuousAlternatingMap.toContinuousMultilinearMap_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) : (f + g).toContinuousMultilinearMap = f.toContinuousMultilinearMap + g.toContinuousMultilinearMap

@[simp]

theorem ContinuousAlternatingMap.toAlternatingMap_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) : (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap

instance ContinuousAlternatingMap.addCommMonoid {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] : AddCommMonoid (M [⋀^ι]→L[R] N)

Equations

• ContinuousAlternatingMap.addCommMonoid = Function.Injective.addCommMonoid ContinuousAlternatingMap.toContinuousMultilinearMap ⋯ ⋯ ⋯ ⋯

def ContinuousAlternatingMap.applyAddHom {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] (v : ι → M) : M [⋀^ι]→L[R] N →+ N

Evaluation of a ContinuousAlternatingMap at a vector as an AddMonoidHom.

Equations

• ContinuousAlternatingMap.applyAddHom v = { toFun := fun (f : M [⋀^ι]→L[R] N) => f v, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.sum_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] {α : Type u_7} (f : α → M [⋀^ι]→L[R] N) (m : ι → M) {s : Finset α} : (s.sum fun (a : α) => f a) m = s.sum fun (a : α) => (f a) m

@[simp]

theorem ContinuousAlternatingMap.toMultilinearAddHom_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] (f : M [⋀^ι]→L[R] N) : ContinuousAlternatingMap.toMultilinearAddHom f = f.toContinuousMultilinearMap

def ContinuousAlternatingMap.toMultilinearAddHom {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] : M [⋀^ι]→L[R] N →+ ContinuousMultilinearMap R (fun (x : ι) => M) N

Projection to ContinuousMultilinearMaps as a bundled AddMonoidHom.

Equations

• ContinuousAlternatingMap.toMultilinearAddHom = { toFun := fun (f : M [⋀^ι]→L[R] N) => f.toContinuousMultilinearMap, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.toContinuousLinearMap_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ι → M) (i : ι) (x : M) : (f.toContinuousLinearMap m i) x = f (Function.update m i x)

def ContinuousAlternatingMap.toContinuousLinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ι → M) (i : ι) : M →L[R] N

If f is a continuous alternating map, then f.toContinuousLinearMap m i is the continuous linear map obtained by fixing all coordinates but i equal to those of m, and varying the i-th coordinate.

Equations

• f.toContinuousLinearMap m i = f.toContinuousLinearMap m i

@[simp]

theorem ContinuousAlternatingMap.prod_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N') (m : (i : ι) → (fun (x : ι) => M) i) : (f.prod g) m = (f m, g m)

def ContinuousAlternatingMap.prod {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N') : M [⋀^ι]→L[R] (N × N')

The cartesian product of two continuous alternating maps, as a continuous alternating map.

Equations

• f.prod g = { toContinuousMultilinearMap := f.prod g.toContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }

def ContinuousAlternatingMap.pi {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {M' : ι' → Type u_8} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → M [⋀^ι]→L[R] M' i) : M [⋀^ι]→L[R] ((i : ι') → M' i)

Combine a family of continuous alternating maps with the same domain and codomains M' i into a continuous alternating map taking values in the space of functions Π i, M' i.

Equations

• ContinuousAlternatingMap.pi f = { toContinuousMultilinearMap := ContinuousMultilinearMap.pi fun (i : ι') => (f i).toContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.coe_pi {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {M' : ι' → Type u_8} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → M [⋀^ι]→L[R] M' i) : ⇑(ContinuousAlternatingMap.pi f) = fun (m : ι → M) (j : ι') => (f j) m

theorem ContinuousAlternatingMap.pi_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {M' : ι' → Type u_8} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → M [⋀^ι]→L[R] M' i) (m : ι → M) (j : ι') : (ContinuousAlternatingMap.pi f) m j = (f j) m

@[simp]

theorem ContinuousAlternatingMap.ofSubsingleton_apply_toContinuousMultilinearMap (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) (f : M →L[R] N) : ((ContinuousAlternatingMap.ofSubsingleton R M N i) f).toContinuousMultilinearMap = (ContinuousMultilinearMap.ofSubsingleton R M N i) f

@[simp]

theorem ContinuousAlternatingMap.ofSubsingleton_apply_apply (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) (f : M →L[R] N) (x : ι → M) : ((ContinuousAlternatingMap.ofSubsingleton R M N i) f) x = f (x i)

@[simp]

theorem ContinuousAlternatingMap.ofSubsingleton_symm_apply_apply (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) (f : M [⋀^ι]→L[R] N) (x : M) : ((ContinuousAlternatingMap.ofSubsingleton R M N i).symm f) x = f fun (x_1 : ι) => x

def ContinuousAlternatingMap.ofSubsingleton (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) : (M →L[R] N) ≃ M [⋀^ι]→L[R] N

The natural equivalence between continuous linear maps from M to N and continuous 1-multilinear alternating maps from M to N.

Equations

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

@[simp]

theorem ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) (f : M →L[R] N) : ((ContinuousAlternatingMap.ofSubsingleton R M N i) f).toAlternatingMap = (AlternatingMap.ofSubsingleton R M N i) ↑f

@[simp]

theorem ContinuousAlternatingMap.constOfIsEmpty_toContinuousMultilinearMap (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsEmpty ι] (m : N) : (ContinuousAlternatingMap.constOfIsEmpty R M ι m).toContinuousMultilinearMap = ContinuousMultilinearMap.constOfIsEmpty R (fun (x : ι) => M) m

@[simp]

theorem ContinuousAlternatingMap.constOfIsEmpty_apply (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsEmpty ι] (m : N) : ∀ (a : (i : ι) → (fun (x : ι) => M) i), (ContinuousAlternatingMap.constOfIsEmpty R M ι m) a = m

def ContinuousAlternatingMap.constOfIsEmpty (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsEmpty ι] (m : N) : M [⋀^ι]→L[R] N

The constant map is alternating when ι is empty.

Equations

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

@[simp]

theorem ContinuousAlternatingMap.constOfIsEmpty_toAlternatingMap (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsEmpty ι] (m : N) : (ContinuousAlternatingMap.constOfIsEmpty R M ι m).toAlternatingMap = AlternatingMap.constOfIsEmpty R M ι m

def ContinuousAlternatingMap.compContinuousLinearMap {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (g : M [⋀^ι]→L[R] N) (f : M' →L[R] M) : M' [⋀^ι]→L[R] N

If g is continuous alternating and f is a continuous linear map, then g (f m₁, ..., f mₙ) is again a continuous alternating map, that we call g.compContinuousLinearMap f.

Equations

• g.compContinuousLinearMap f = let __src := g.toAlternatingMap.compLinearMap ↑f; { toContinuousMultilinearMap := g.compContinuousLinearMap fun (x : ι) => f, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.compContinuousLinearMap_apply {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (g : M [⋀^ι]→L[R] N) (f : M' →L[R] M) (m : ι → M') : (g.compContinuousLinearMap f) m = g (⇑f ∘ m)

def ContinuousLinearMap.compContinuousAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (g : N →L[R] N') (f : M [⋀^ι]→L[R] N) : M [⋀^ι]→L[R] N'

Composing a continuous alternating map with a continuous linear map gives again a continuous alternating map.

Equations

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

@[simp]

theorem ContinuousLinearMap.compContinuousAlternatingMap_coe {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (g : N →L[R] N') (f : M [⋀^ι]→L[R] N) : ⇑(g.compContinuousAlternatingMap f) = ⇑g ∘ ⇑f

def ContinuousLinearEquiv.continuousAlternatingMapComp {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (e : M ≃L[R] M') : M [⋀^ι]→L[R] N ≃ M' [⋀^ι]→L[R] N

A continuous linear equivalence of domains defines an equivalence between continuous alternating maps.

Equations

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

def ContinuousLinearEquiv.compContinuousAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (e : N ≃L[R] N') : M [⋀^ι]→L[R] N ≃ M [⋀^ι]→L[R] N'

A continuous linear equivalence of codomains defines an equivalence between continuous alternating maps.

Equations

• e.compContinuousAlternatingMap = { toFun := (↑e).compContinuousAlternatingMap, invFun := (↑e.symm).compContinuousAlternatingMap, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.compContinuousAlternatingMap_coe {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (e : N ≃L[R] N') (f : M [⋀^ι]→L[R] N) : ⇑(e.compContinuousAlternatingMap f) = ⇑e ∘ ⇑f

def ContinuousLinearEquiv.continuousAlternatingMapCongr {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (e : M ≃L[R] M') (e' : N ≃L[R] N') : M [⋀^ι]→L[R] N ≃ M' [⋀^ι]→L[R] N'

Continuous linear equivalences between domains and codomains define an equivalence between the spaces of continuous alternating maps.

Equations

• e.continuousAlternatingMapCongr e' = e.continuousAlternatingMapComp.trans e'.compContinuousAlternatingMap

@[simp]

theorem ContinuousAlternatingMap.piEquiv_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {N : ι' → Type u_8} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → TopologicalSpace (N i)] [(i : ι') → Module R (N i)] (f : M [⋀^ι]→L[R] ((i : ι') → N i)) (i : ι') : ContinuousAlternatingMap.piEquiv.symm f i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap f

@[simp]

theorem ContinuousAlternatingMap.piEquiv_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {N : ι' → Type u_8} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → TopologicalSpace (N i)] [(i : ι') → Module R (N i)] (f : (i : ι') → M [⋀^ι]→L[R] N i) : ContinuousAlternatingMap.piEquiv f = ContinuousAlternatingMap.pi f

def ContinuousAlternatingMap.piEquiv {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {N : ι' → Type u_8} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → TopologicalSpace (N i)] [(i : ι') → Module R (N i)] : ((i : ι') → M [⋀^ι]→L[R] N i) ≃ M [⋀^ι]→L[R] ((i : ι') → N i)

ContinuousAlternatingMap.pi as an Equiv.

Equations

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

theorem ContinuousAlternatingMap.cons_add {R : Type u_1} {M : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (x : M) (y : M) : f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)

In the specific case of continuous alternating maps on spaces indexed by Fin (n+1), where one can build an element of Π(i : Fin (n+1)), M i using cons, one can express directly the additivity of an alternating map along the first variable.

theorem ContinuousAlternatingMap.vecCons_add {R : Type u_1} {M : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (x : M) (y : M) : f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)

In the specific case of continuous alternating maps on spaces indexed by Fin (n+1), where one can build an element of Π(i : Fin (n+1)), M i using cons, one can express directly the additivity of an alternating map along the first variable.

theorem ContinuousAlternatingMap.cons_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (c : R) (x : M) : f (Fin.cons (c • x) m) = c • f (Fin.cons x m)

In the specific case of continuous alternating maps on spaces indexed by Fin (n+1), where one can build an element of Π(i : Fin (n+1)), M i using cons, one can express directly the multiplicativity of an alternating map along the first variable.

theorem ContinuousAlternatingMap.vecCons_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (c : R) (x : M) : f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)

In the specific case of continuous alternating maps on spaces indexed by Fin (n+1), where one can build an element of Π(i : Fin (n+1)), M i using cons, one can express directly the multiplicativity of an alternating map along the first variable.

theorem ContinuousAlternatingMap.map_piecewise_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ι → M) (m' : ι → M) (t : Finset ι) : f (t.piecewise (m + m') m') = t.powerset.sum fun (s : Finset ι) => f (s.piecewise m m')

theorem ContinuousAlternatingMap.map_add_univ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] [Fintype ι] (m : ι → M) (m' : ι → M) : f (m + m') = Finset.univ.sum fun (s : Finset ι) => f (s.piecewise m m')

Additivity of a continuous alternating map along all coordinates at the same time, writing f (m + m') as the sum of f (s.piecewise m m') over all sets s.

theorem ContinuousAlternatingMap.map_sum_finset {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {α : ι → Type u_7} [Fintype ι] [DecidableEq ι] (g' : (i : ι) → α i → M) (A : (i : ι) → Finset (α i)) : (f fun (i : ι) => (A i).sum fun (j : α i) => g' i j) = (Fintype.piFinset A).sum fun (r : (a : ι) → α a) => f fun (i : ι) => g' i (r i)

If f is continuous alternating, then f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ) is the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions with r 1 ∈ A₁, ..., r n ∈ Aₙ. This follows from multilinearity by expanding successively with respect to each coordinate.

theorem ContinuousAlternatingMap.map_sum {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {α : ι → Type u_7} [Fintype ι] [DecidableEq ι] (g' : (i : ι) → α i → M) [(i : ι) → Fintype (α i)] : (f fun (i : ι) => Finset.univ.sum fun (j : α i) => g' i j) = Finset.univ.sum fun (r : (i : ι) → α i) => f fun (i : ι) => g' i (r i)

If f is continuous alternating, then f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ) is the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions r. This follows from multilinearity by expanding successively with respect to each coordinate.

def ContinuousAlternatingMap.restrictScalars (R : Type u_1) {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {A : Type u_7} [Semiring A] [SMul R A] [Module A M] [Module A N] [IsScalarTower R A M] [IsScalarTower R A N] (f : M [⋀^ι]→L[A] N) : M [⋀^ι]→L[R] N

Reinterpret a continuous A-alternating map as a continuous R-alternating map, if A is an algebra over R and their actions on all involved modules agree with the action of R on A.

Equations

• ContinuousAlternatingMap.restrictScalars R f = { toContinuousMultilinearMap := ContinuousMultilinearMap.restrictScalars R f.toContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.coe_restrictScalars (R : Type u_1) {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {A : Type u_7} [Semiring A] [SMul R A] [Module A M] [Module A N] [IsScalarTower R A M] [IsScalarTower R A N] (f : M [⋀^ι]→L[A] N) : ⇑(ContinuousAlternatingMap.restrictScalars R f) = ⇑f

@[simp]

theorem ContinuousAlternatingMap.map_sub {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ι → M) (i : ι) (x : M) (y : M) : f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)

instance ContinuousAlternatingMap.instNeg {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] : Neg (M [⋀^ι]→L[R] N)

Equations

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

@[simp]

theorem ContinuousAlternatingMap.coe_neg {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [TopologicalAddGroup N] : ⇑(-f) = -⇑f

theorem ContinuousAlternatingMap.neg_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [TopologicalAddGroup N] (m : ι → M) : (-f) m = -f m

instance ContinuousAlternatingMap.instSub {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] : Sub (M [⋀^ι]→L[R] N)

Equations

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

@[simp]

theorem ContinuousAlternatingMap.coe_sub {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) [TopologicalAddGroup N] : ⇑(f - g) = ⇑f - ⇑g

theorem ContinuousAlternatingMap.sub_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) [TopologicalAddGroup N] (m : ι → M) : (f - g) m = f m - g m

instance ContinuousAlternatingMap.instAddCommGroup {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] : AddCommGroup (M [⋀^ι]→L[R] N)

Equations

• ContinuousAlternatingMap.instAddCommGroup = Function.Injective.addCommGroup ContinuousAlternatingMap.toContinuousMultilinearMap ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem ContinuousAlternatingMap.map_piecewise_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (c : ι → R) (m : ι → M) (s : Finset ι) : f (s.piecewise (fun (i : ι) => c i • m i) m) = (s.prod fun (i : ι) => c i) • f m

theorem ContinuousAlternatingMap.map_smul_univ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [Fintype ι] (c : ι → R) (m : ι → M) : (f fun (i : ι) => c i • m i) = (Finset.univ.prod fun (i : ι) => c i) • f m

Multiplicativity of a continuous alternating map along all coordinates at the same time, writing f (fun i ↦ c i • m i) as (∏ i, c i) • f m.

instance ContinuousAlternatingMap.instDistribMulAction {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Monoid R] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [TopologicalSpace M] [TopologicalSpace N] [Module A M] [Module A N] [DistribMulAction R N] [ContinuousConstSMul R N] [SMulCommClass A R N] [ContinuousAdd N] : DistribMulAction R (M [⋀^ι]→L[A] N)

Equations

• ContinuousAlternatingMap.instDistribMulAction = Function.Injective.distribMulAction ContinuousAlternatingMap.toMultilinearAddHom ⋯ ⋯

instance ContinuousAlternatingMap.instModule {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] [Module A M] [Module A N] [Module R N] [ContinuousConstSMul R N] [SMulCommClass A R N] : Module R (M [⋀^ι]→L[A] N)

The space of continuous alternating maps over an algebra over R is a module over R, for the pointwise addition and scalar multiplication.

Equations

• ContinuousAlternatingMap.instModule = Function.Injective.module R ContinuousAlternatingMap.toMultilinearAddHom ⋯ ⋯

@[simp]

theorem ContinuousAlternatingMap.toContinuousMultilinearMapLinear_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] [Module A M] [Module A N] [Module R N] [ContinuousConstSMul R N] [SMulCommClass A R N] (self : M [⋀^ι]→L[A] N) : ContinuousAlternatingMap.toContinuousMultilinearMapLinear self = self.toContinuousMultilinearMap

def ContinuousAlternatingMap.toContinuousMultilinearMapLinear {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] [Module A M] [Module A N] [Module R N] [ContinuousConstSMul R N] [SMulCommClass A R N] : M [⋀^ι]→L[A] N →ₗ[R] ContinuousMultilinearMap A (fun (x : ι) => M) N

Linear map version of the map toMultilinearMap associating to a continuous alternating map the corresponding multilinear map.

Equations

• ContinuousAlternatingMap.toContinuousMultilinearMapLinear = { toFun := ContinuousAlternatingMap.toContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.toAlternatingMapLinear_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] [Module A M] [Module A N] [Module R N] [ContinuousConstSMul R N] [SMulCommClass A R N] : ⇑ContinuousAlternatingMap.toAlternatingMapLinear = ContinuousAlternatingMap.toAlternatingMap

def ContinuousAlternatingMap.toAlternatingMapLinear {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] [Module A M] [Module A N] [Module R N] [ContinuousConstSMul R N] [SMulCommClass A R N] : M [⋀^ι]→L[A] N →ₗ[R] M [⋀^ι]→ₗ[A] N

Linear map version of the map toAlternatingMap associating to a continuous alternating map the corresponding alternating map.

Equations

• ContinuousAlternatingMap.toAlternatingMapLinear = { toFun := ContinuousAlternatingMap.toAlternatingMap, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.piLinearEquiv_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [TopologicalSpace M] [Module A M] {ι' : Type u_6} {M' : ι' → Type u_7} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R (M' i)] [∀ (i : ι'), ContinuousConstSMul R (M' i)] : ∀ (a : (i : ι') → M [⋀^ι]→L[A] M' i), ContinuousAlternatingMap.piLinearEquiv a = ContinuousAlternatingMap.pi a

@[simp]

theorem ContinuousAlternatingMap.piLinearEquiv_symm_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [TopologicalSpace M] [Module A M] {ι' : Type u_6} {M' : ι' → Type u_7} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R (M' i)] [∀ (i : ι'), ContinuousConstSMul R (M' i)] : ∀ (a : M [⋀^ι]→L[A] ((i : ι') → M' i)) (i : ι'), ContinuousAlternatingMap.piLinearEquiv.symm a i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap a

def ContinuousAlternatingMap.piLinearEquiv {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [TopologicalSpace M] [Module A M] {ι' : Type u_6} {M' : ι' → Type u_7} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R (M' i)] [∀ (i : ι'), ContinuousConstSMul R (M' i)] : ((i : ι') → M [⋀^ι]→L[A] M' i) ≃ₗ[R] M [⋀^ι]→L[A] ((i : ι') → M' i)

ContinuousAlternatingMap.pi as a LinearEquiv.

Equations

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

@[simp]

theorem ContinuousAlternatingMap.smulRight_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [TopologicalSpace R] [TopologicalSpace M] [TopologicalSpace N] [ContinuousSMul R N] (f : M [⋀^ι]→L[R] R) (z : N) : ∀ (a : (i : ι) → (fun (x : ι) => M) i), (f.smulRight z) a = f a • z

@[simp]

theorem ContinuousAlternatingMap.smulRight_toContinuousMultilinearMap {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [TopologicalSpace R] [TopologicalSpace M] [TopologicalSpace N] [ContinuousSMul R N] (f : M [⋀^ι]→L[R] R) (z : N) : (f.smulRight z).toContinuousMultilinearMap = f.smulRight z

def ContinuousAlternatingMap.smulRight {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [TopologicalSpace R] [TopologicalSpace M] [TopologicalSpace N] [ContinuousSMul R N] (f : M [⋀^ι]→L[R] R) (z : N) : M [⋀^ι]→L[R] N

Given a continuous R-alternating map f taking values in R, f.smulRight z is the continuous alternating map sending m to f m • z.

Equations

• f.smulRight z = let __src := f.toAlternatingMap.smulRight z; { toContinuousMultilinearMap := f.smulRight z, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.compContinuousLinearMapₗ_apply {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] (f : M →L[R] M') (g : M' [⋀^ι]→L[R] N) : (ContinuousAlternatingMap.compContinuousLinearMapₗ f) g = g.compContinuousLinearMap f

def ContinuousAlternatingMap.compContinuousLinearMapₗ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] (f : M →L[R] M') : M' [⋀^ι]→L[R] N →ₗ[R] M [⋀^ι]→L[R] N

ContinuousAlternatingMap.compContinuousLinearMap as a bundled LinearMap.

Equations

• ContinuousAlternatingMap.compContinuousLinearMapₗ f = { toFun := fun (g : M' [⋀^ι]→L[R] N) => g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }

def ContinuousLinearMap.compContinuousAlternatingMapₗ (R : Type u_1) (M : Type u_2) (N : Type u_4) (N' : Type u_5) {ι : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] [ContinuousAdd N'] [ContinuousConstSMul R N'] : (N →L[R] N') →ₗ[R] M [⋀^ι]→L[R] N →ₗ[R] M [⋀^ι]→L[R] N'

ContinuousLinearMap.compContinuousAlternatingMap as a bundled bilinear map.

Equations

• ContinuousLinearMap.compContinuousAlternatingMapₗ R M N N' = LinearMap.mk₂ R ContinuousLinearMap.compContinuousAlternatingMap ⋯ ⋯ ⋯ ⋯

theorem ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) : (ContinuousMultilinearMap.alternatization f).toContinuousMultilinearMap = Finset.univ.sum fun (σ : Equiv.Perm ι) => Equiv.Perm.sign σ • ContinuousMultilinearMap.domDomCongr σ f

def ContinuousMultilinearMap.alternatization {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] : ContinuousMultilinearMap R (fun (x : ι) => M) N →+ M [⋀^ι]→L[R] N

Alternatization of a continuous multilinear map.

Equations

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

theorem ContinuousMultilinearMap.alternatization_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) (v : ι → M) : (ContinuousMultilinearMap.alternatization f) v = Finset.univ.sum fun (σ : Equiv.Perm ι) => Equiv.Perm.sign σ • f (v ∘ ⇑σ)

@[simp]

theorem ContinuousMultilinearMap.alternatization_apply_toAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) : (ContinuousMultilinearMap.alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap