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 R (fun (x : ι) => M) N, M [⋀^ι]→ₗ[R] N : 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_update_add' [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_update_smul' [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

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

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 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 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 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 toAlternatingMap = {f : M [⋀^ι]→ₗ[R] N | Continuous ⇑f}

@[simp]

theorem ContinuousAlternatingMap.map_update_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 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_update_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

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 = { toContinuousMultilinearMap := f.codRestrict p h, map_eq_zero_of_eq' := ⋯ }

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

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] : 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] : 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)

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)

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)

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 = { toSMul := ContinuousAlternatingMap.instSMul, one_smul := ⋯, mul_smul := ⋯ }

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

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

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 α} : (∑ a ∈ s, f a) m = ∑ a ∈ s, (f a) m

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.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) : toMultilinearAddHom f = f.toContinuousMultilinearMap

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

@[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.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) : ⇑(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 : ι') : (pi f) m j = (f j) m

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_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) : ((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) : ((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) : ((ofSubsingleton R M N i).symm f) x = f fun (x_1 : ι) => x

@[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) : ((ofSubsingleton R M N i) f).toAlternatingMap = (AlternatingMap.ofSubsingleton R M N i) ↑f

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

• ContinuousAlternatingMap.constOfIsEmpty R M ι m = { toContinuousMultilinearMap := ContinuousMultilinearMap.constOfIsEmpty R (fun (x : ι) => M) m, map_eq_zero_of_eq' := ⋯ }

@[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) : (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) : (constOfIsEmpty R M ι m) a✝ = m

@[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) : (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 = { 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

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

@[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.continuousAlternatingMapCongrLeftEquiv {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.

This is available as a continuous linear isomorphism at ContinuousLinearEquiv.continuousAlternatingMapCongrLeft.

This is ContinuousAlternatingMap.compContinuousLinearMap as an equivalence.

Equations

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

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv_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] (e : M ≃L[R] M') : ⇑e.continuousAlternatingMapCongrLeftEquiv = fun (f : M [⋀^ι]→L[R] N) => f.compContinuousLinearMap ↑e.symm

def ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv {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.continuousAlternatingMapCongrRightEquiv = { toFun := (↑e).compContinuousAlternatingMap, invFun := (↑e.symm).compContinuousAlternatingMap, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv_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'] (e : N ≃L[R] N') : ⇑e.continuousAlternatingMapCongrRightEquiv = (↑e).compContinuousAlternatingMap

@[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.continuousAlternatingMapCongrRightEquiv f) = ⇑e ∘ ⇑f

def ContinuousLinearEquiv.continuousAlternatingMapCongrEquiv {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.continuousAlternatingMapCongrEquiv e' = e.continuousAlternatingMapCongrLeftEquiv.trans e'.continuousAlternatingMapCongrRightEquiv

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.

@[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 : ι') : 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) : piEquiv f = pi f

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 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 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) (t : Finset ι) : f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, 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) : f (m + m') = ∑ 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 : ι) => ∑ j ∈ A i, g' i j) = ∑ r ∈ Fintype.piFinset 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 : ι) => ∑ j : α i, g' i j) = ∑ 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) : ⇑(restrictScalars R f) = ⇑f

@[simp]

theorem ContinuousAlternatingMap.map_update_sub {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [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 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_3} {ι : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [IsTopologicalAddGroup 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_3} {ι : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [IsTopologicalAddGroup N] : ⇑(-f) = -⇑f

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

instance ContinuousAlternatingMap.instSub {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [IsTopologicalAddGroup 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_3} {ι : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f g : M [⋀^ι]→L[R] N) [IsTopologicalAddGroup N] : ⇑(f - g) = ⇑f - ⇑g

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

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

Equations

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

theorem ContinuousAlternatingMap.map_piecewise_smul {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [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) = (∏ i ∈ s, c i) • f m

theorem ContinuousAlternatingMap.map_smul_univ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [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) = (∏ 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.

theorem ContinuousAlternatingMap.ext_ring {R : Type u_1} {M : Type u_2} {ι : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [Finite ι] [TopologicalSpace R] ⦃f g : R [⋀^ι]→L[R] M⦄ (h : (f fun (x : ι) => 1) = g fun (x : ι) => 1) : f = g

If two continuous R-alternating maps from R are equal on 1, then they are equal.

This is the alternating version of ContinuousLinearMap.ext_ring.

theorem ContinuousAlternatingMap.ext_ring_iff {R : Type u_1} {M : Type u_2} {ι : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [Finite ι] [TopologicalSpace R] {f g : R [⋀^ι]→L[R] M} : f = g ↔ (f fun (x : ι) => 1) = g fun (x : ι) => 1

instance ContinuousAlternatingMap.uniqueOfCommRing {R : Type u_1} {N : Type u_3} {ι : Type u_4} [CommSemiring R] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Finite ι] [Nontrivial ι] [TopologicalSpace R] : Unique (R [⋀^ι]→L[R] N)

The only continuous R-alternating map from two or more copies of R is the zero map.

Equations

• ContinuousAlternatingMap.uniqueOfCommRing = { toInhabited := ContinuousAlternatingMap.instInhabited, uniq := ⋯ }

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 = { toMulAction := ContinuousAlternatingMap.instMulAction, smul_zero := ⋯, smul_add := ⋯ }

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 = { toDistribMulAction := ContinuousAlternatingMap.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

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.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) : toContinuousMultilinearMapLinear self = self.toContinuousMultilinearMap

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.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] : ⇑toAlternatingMapLinear = toAlternatingMap

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.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 : ι') : piLinearEquiv.symm a✝ i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap a✝

@[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) : piLinearEquiv a✝ = pi a✝

def ContinuousAlternatingMap.smulRight {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [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 = { toContinuousMultilinearMap := f.smulRight z, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.smulRight_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [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

@[simp]

theorem ContinuousAlternatingMap.smulRight_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [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

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

@[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) : (compContinuousLinearMapₗ f) g = g.compContinuousLinearMap f

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 ⋯ ⋯ ⋯ ⋯

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] [IsTopologicalAddGroup 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_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] [IsTopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) : (alternatization f).toContinuousMultilinearMap = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • domDomCongr σ f

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] [IsTopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) (v : ι → M) : (alternatization f) v = ∑ σ : 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] [IsTopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) : (alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap