Documentation

Mathlib.Topology.Algebra.Module.Alternating.Basic

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.

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.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 ji jf 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
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) :
@[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 ji jf.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) :
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
@[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)
@[deprecated ContinuousAlternatingMap.map_update_add (since := "2024-11-03")]
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 y : M) :
f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)

Alias of ContinuousAlternatingMap.map_update_add.

@[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)
@[deprecated ContinuousAlternatingMap.map_update_smul (since := "2024-11-03")]
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)

Alias of ContinuousAlternatingMap.map_update_smul.

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
@[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] :
Equations
@[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
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
@[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.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) :
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.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
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) :

Evaluation of a ContinuousAlternatingMap at a vector as an AddMonoidHom.

Equations
@[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 α} :
(∑ as, f a) m = as, (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
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
@[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) :
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
@[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
@[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_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_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_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) :
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) :

The constant map is alternating when ι is empty.

Equations
@[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
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
@[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
@[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) :
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') :

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.
@[deprecated ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv (since := "2025-04-16")]
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') :

Alias of ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv.


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

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

Equations
@[deprecated ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv (since := "2025-04-16")]
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') :

Alias of ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv.


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

Equations
@[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) :
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
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_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) :
@[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 : ι') :
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 nM) (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 nM) (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 nM) (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 nM) (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') = st.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 : ι) → α iM) (A : (i : ι) → Finset (α i)) :
(f fun (i : ι) => jA i, g' i j) = rFintype.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 : ι) → α iM) [(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) :

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
@[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)
@[deprecated ContinuousAlternatingMap.map_update_sub (since := "2024-11-03")]
theorem ContinuousAlternatingMap.map_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)

Alias of ContinuousAlternatingMap.map_update_sub.

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
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) = (∏ is, 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

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

Equations
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

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

Equations

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

Equations
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_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✝
@[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 : ι') :
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) :

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

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