# Documentation

Mathlib.Topology.Algebra.Module.Alternating

# 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) [] [] [Module R M] [] [] [Module R N] [] extends :
Type (max (max u_2 u_3) u_4)

A continuous alternating map is a continuous map from ι → M to N 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.
Instances For
@[reducible]
abbrev ContinuousAlternatingMap.toAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [] [] [Module R M] [] [] [Module R N] [] (self : M[Λ^ι]→L[R]N) :

Projection to AlternatingMaps.

Instances For
Instances For
theorem ContinuousAlternatingMap.toContinuousMultilinearMap_injective {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] :
Function.Injective ContinuousAlternatingMap.toContinuousMultilinearMap
theorem ContinuousAlternatingMap.range_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] :
Set.range ContinuousAlternatingMap.toContinuousMultilinearMap = {f | ∀ (v : ιM) (i j : ι), v i = v ji jf v = 0}
instance ContinuousAlternatingMap.continuousMapClass {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) :
@[simp]
theorem ContinuousAlternatingMap.coe_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R N] [] (f : ContinuousMultilinearMap R (fun x => M) N) (h : ∀ (v : ιM) (i j : ι), v i = v ji jMultilinearMap.toFun f.toMultilinearMap 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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) :
theorem ContinuousAlternatingMap.ext {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R N] [] :
Set.range ContinuousAlternatingMap.toAlternatingMap = {f | }
@[simp]
theorem ContinuousAlternatingMap.map_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (m : ιM) (i : ι) (x : M) (y : M) :
f (Function.update m i (x + y)) = f () + f ()
@[simp]
theorem ContinuousAlternatingMap.map_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (m : ιM) (i : ι) (c : R) (x : M) :
f (Function.update m i (c x)) = c f ()
theorem ContinuousAlternatingMap.map_coord_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (m : ιM) (i : ι) :
f () = 0
@[simp]
theorem ContinuousAlternatingMap.map_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] :
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} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) (v : ιM) (hv : ) :
f v = 0
@[simp]
theorem ContinuousAlternatingMap.codRestrict_apply_coe {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) (p : ) (h : ∀ (v : ιM), f v p) (v : (i : ι) → (fun x => M) i) :
↑(↑() v) = f v
def ContinuousAlternatingMap.codRestrict {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) (p : ) (h : ∀ (v : ιM), f v p) :
M[Λ^ι]→L[R]{ x // x p }

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

Instances For
instance ContinuousAlternatingMap.instZeroContinuousAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] :
instance ContinuousAlternatingMap.instInhabitedContinuousAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] :
@[simp]
theorem ContinuousAlternatingMap.coe_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] :
0 = 0
@[simp]
theorem ContinuousAlternatingMap.toContinuousMultilinearMap_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] :
0.toContinuousMultilinearMap = 0
@[simp]
theorem ContinuousAlternatingMap.toAlternatingMap_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] :
instance ContinuousAlternatingMap.instSMulContinuousAlternatingMap {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [] [] {R' : Type u_7} {A : Type u_9} [Monoid R'] [] [Module A M] [Module A N] [] [] [SMulCommClass A R' N] :
SMul R' (M[Λ^ι]→L[A]N)
@[simp]
theorem ContinuousAlternatingMap.coe_smul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [] [] {R' : Type u_7} {A : Type u_9} [Monoid R'] [] [Module A M] [Module A 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} [] [] [] [] {R' : Type u_7} {A : Type u_9} [Monoid R'] [] [Module A M] [Module A 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} [] [] [] [] {R' : Type u_7} {A : Type u_9} [Monoid R'] [] [Module A M] [Module A 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} [] [] [] [] {R' : Type u_7} {A : Type u_9} [Monoid R'] [] [Module A M] [Module A N] [] [] [SMulCommClass A R' N] (c : R') (f : M[Λ^ι]→L[A]N) :
instance ContinuousAlternatingMap.instSMulCommClassContinuousAlternatingMapInstSMulContinuousAlternatingMapInstSMulContinuousAlternatingMap {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [] [] {R' : Type u_7} {R'' : Type u_8} {A : Type u_9} [Monoid R'] [Monoid R''] [] [Module A M] [Module A N] [] [] [SMulCommClass A R' N] [DistribMulAction R'' N] [] [SMulCommClass A R'' N] [SMulCommClass R' R'' N] :
instance ContinuousAlternatingMap.instIsScalarTowerContinuousAlternatingMapInstSMulContinuousAlternatingMapInstSMulContinuousAlternatingMap {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [] [] {R' : Type u_7} {R'' : Type u_8} {A : Type u_9} [Monoid R'] [Monoid R''] [] [Module A M] [Module A N] [] [] [SMulCommClass A R' N] [DistribMulAction R'' N] [] [SMulCommClass A R'' N] [SMul R' R''] [IsScalarTower R' R'' N] :
instance ContinuousAlternatingMap.instMulActionContinuousAlternatingMap {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [] [] {R' : Type u_7} {A : Type u_9} [Monoid R'] [] [Module A M] [Module A N] [] [] [SMulCommClass A R' N] :
instance ContinuousAlternatingMap.instAddContinuousAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] :
@[simp]
theorem ContinuousAlternatingMap.coe_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) (g : M[Λ^ι]→L[R]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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) (g : M[Λ^ι]→L[R]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} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R N] [] [] (f : M[Λ^ι]→L[R]N) (g : M[Λ^ι]→L[R]N) :
instance ContinuousAlternatingMap.addCommMonoid {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] :
def ContinuousAlternatingMap.applyAddHom {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] (v : ιM) :

Evaluation of a ContinuousAlternatingMap at a vector as an AddMonoidHom.

Instances For
@[simp]
theorem ContinuousAlternatingMap.sum_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] {α : Type u_7} (f : αM[Λ^ι]→L[R]N) (m : ιM) {s : } :
↑(Finset.sum s fun a => f a) m = Finset.sum s 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} [] [] [Module R M] [] [] [Module R N] [] [] (f : M[Λ^ι]→L[R]N) :
def ContinuousAlternatingMap.toMultilinearAddHom {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] :

Projection to ContinuousMultilinearMaps as a bundled AddMonoidHom.

Instances For
@[simp]
theorem ContinuousAlternatingMap.toContinuousLinearMap_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (m : ιM) (i : ι) (x : M) :
= f ()
def ContinuousAlternatingMap.toContinuousLinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (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.

Instances For
@[simp]
theorem ContinuousAlternatingMap.prod_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] [Module R N'] [] (f : M[Λ^ι]→L[R]N) (g : M[Λ^ι]→L[R]N') (m : (i : ι) → (fun x => M) i) :
↑() 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} [] [] [Module R M] [] [] [Module R N] [] [] [Module R 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.

Instances For
def ContinuousAlternatingMap.pi {R : Type u_1} {M : Type u_2} {ι : Type u_6} [] [] [Module R 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.

Instances For
@[simp]
theorem ContinuousAlternatingMap.coe_pi {R : Type u_1} {M : Type u_2} {ι : Type u_6} [] [] [Module R 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) :
= fun m j => ↑(f j) m
theorem ContinuousAlternatingMap.pi_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [] [] [Module R 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 : ι') :
↑() m j = ↑(f j) m
@[simp]
theorem ContinuousAlternatingMap.ofSubsingleton_toContinuousMultilinearMap (R : Type u_1) (M : Type u_2) {ι : Type u_6} [] [] [Module R M] [] [] (i' : ι) :
().toContinuousMultilinearMap =
@[simp]
theorem ContinuousAlternatingMap.ofSubsingleton_apply (R : Type u_1) (M : Type u_2) {ι : Type u_6} [] [] [Module R M] [] [] (i' : ι) (f : ιM) :
↑() f = f i'
def ContinuousAlternatingMap.ofSubsingleton (R : Type u_1) (M : Type u_2) {ι : Type u_6} [] [] [Module R M] [] [] (i' : ι) :

The evaluation map from ι → M to M is alternating at a given i when ι is subsingleton.

Instances For
@[simp]
theorem ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap (R : Type u_1) (M : Type u_2) {ι : Type u_6} [] [] [Module R M] [] [] (i' : ι) :
@[simp]
theorem ContinuousAlternatingMap.constOfIsEmpty_apply (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [] [] [Module R M] [] [] [Module R N] [] [] (m : N) :
∀ (a : (i : ι) → (fun x => M) i), ↑() a = m
@[simp]
theorem ContinuousAlternatingMap.constOfIsEmpty_toContinuousMultilinearMap (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [] [] [Module R M] [] [] [Module R N] [] [] (m : N) :
().toContinuousMultilinearMap = ContinuousMultilinearMap.constOfIsEmpty R (fun x => M) m
def ContinuousAlternatingMap.constOfIsEmpty (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [] [] [Module R M] [] [] [Module R N] [] [] (m : N) :

The constant map is alternating when ι is empty.

Instances For
@[simp]
theorem ContinuousAlternatingMap.constOfIsEmpty_toAlternatingMap (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [] [] [Module R M] [] [] [Module R N] [] [] (m : N) :
def ContinuousAlternatingMap.compContinuousLinearMap {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R M'] [] [] [Module R N] [] (g : M[Λ^ι]→L[R]N) (f : M' →L[R] M) :

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.

Instances For
@[simp]
theorem ContinuousAlternatingMap.compContinuousLinearMap_apply {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R M'] [] [] [Module R N] [] (g : M[Λ^ι]→L[R]N) (f : M' →L[R] M) (m : ι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} [] [] [Module R M] [] [] [Module R N] [] [] [Module R N'] [] (g : N →L[R] N') (f : M[Λ^ι]→L[R]N) :

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

Instances For
@[simp]
theorem ContinuousLinearMap.compContinuousAlternatingMap_coe {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] [Module R N'] [] (g : N →L[R] N') (f : M[Λ^ι]→L[R]N) :
= g f
def ContinuousLinearEquiv.continuousAlternatingMapComp {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R M'] [] [] [Module R N] [] (e : M ≃L[R] M') :

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

Instances For
def ContinuousLinearEquiv.compContinuousAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] [Module R N'] [] (e : N ≃L[R] N') :

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

Instances For
@[simp]
theorem ContinuousLinearEquiv.compContinuousAlternatingMap_coe {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] [Module R N'] [] (e : N ≃L[R] N') (f : M[Λ^ι]→L[R]N) :
= 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} [] [] [Module R M] [] [] [Module R M'] [] [] [Module R N] [] [] [Module R N'] [] (e : M ≃L[R] M') (e' : N ≃L[R] N') :

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

Instances For
@[simp]
theorem ContinuousAlternatingMap.piEquiv_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [] [] [Module R 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 =
@[simp]
theorem ContinuousAlternatingMap.piEquiv_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [] [] [Module R 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 =
def ContinuousAlternatingMap.piEquiv {R : Type u_1} {M : Type u_2} {ι : Type u_6} [] [] [Module R 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.

Instances For
theorem ContinuousAlternatingMap.cons_add {R : Type u_1} {M : Type u_2} {N : Type u_4} [] [] [Module R M] [] [] [Module R N] [] {n : } (f : M[Λ^Fin (n + 1)]→L[R]N) (m : Fin nM) (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} [] [] [Module R M] [] [] [Module R N] [] {n : } (f : M[Λ^Fin (n + 1)]→L[R]N) (m : Fin nM) (x : M) (y : M) :
f (Matrix.vecCons (x + y) m) = f () + f ()

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} [] [] [Module R M] [] [] [Module R 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} [] [] [Module R M] [] [] [Module R 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 ()

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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (m : ιM) (m' : ιM) (t : ) :
f (Finset.piecewise t (m + m') m') = Finset.sum () fun s => f (Finset.piecewise s m m')
theorem ContinuousAlternatingMap.map_add_univ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] [] (m : ιM) (m' : ιM) :
f (m + m') = Finset.sum Finset.univ fun s => f (Finset.piecewise s 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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) {α : ιType u_7} [] [] (g' : (i : ι) → α iM) (A : (i : ι) → Finset (α i)) :
(f fun i => Finset.sum (A i) fun j => g' i j) = Finset.sum () fun r => 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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) {α : ιType u_7} [] [] (g' : (i : ι) → α iM) [(i : ι) → Fintype (α i)] :
(f fun i => Finset.sum Finset.univ fun j => g' i j) = Finset.sum Finset.univ fun r => 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} [] [] [Module R M] [] [] [Module R N] [] {A : Type u_7} [] [SMul R A] [Module A M] [Module 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.

Instances For
@[simp]
theorem ContinuousAlternatingMap.coe_restrictScalars (R : Type u_1) {M : Type u_2} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] {A : Type u_7} [] [SMul R A] [Module A M] [Module A N] [] [] (f : M[Λ^ι]→L[A]N) :
@[simp]
theorem ContinuousAlternatingMap.map_sub {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (m : ιM) (i : ι) (x : M) (y : M) :
f (Function.update m i (x - y)) = f () - f ()
@[simp]
theorem ContinuousAlternatingMap.coe_neg {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) :
↑(-f) = -f
theorem ContinuousAlternatingMap.neg_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) (m : ιM) :
↑(-f) m = -f m
@[simp]
theorem ContinuousAlternatingMap.coe_sub {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) (g : M[Λ^ι]→L[R]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] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) (g : M[Λ^ι]→L[R]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_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (c : ιR) (m : ιM) (s : ) :
f (Finset.piecewise s (fun i => c i m i) m) = (Finset.prod s 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} [] [] [Module R M] [] [] [Module R N] [] (f : M[Λ^ι]→L[R]N) [] (c : ιR) (m : ιM) :
(f fun i => c i m i) = (Finset.prod Finset.univ fun i => c i) f m

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

instance ContinuousAlternatingMap.instDistribMulActionContinuousAlternatingMapToAddMonoidAddCommMonoid {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [] [] [] [] [] [] [Module A M] [Module A N] [] [] [] [] :
instance ContinuousAlternatingMap.instModuleContinuousAlternatingMapAddCommMonoid {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [] [] [] [] [] [] [] [Module A M] [Module A N] [Module R N] [] [] :

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

@[simp]
theorem ContinuousAlternatingMap.toContinuousMultilinearMapLinear_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [] [] [] [] [] [] [] [Module A M] [Module A N] [Module 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} [] [] [] [] [] [] [] [Module A M] [Module A N] [Module R N] [] [] :

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

Instances For
@[simp]
theorem ContinuousAlternatingMap.piLinearEquiv_symm_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [] [] [] [] [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 : ι'), ↑(LinearEquiv.symm ContinuousAlternatingMap.piLinearEquiv) a i =
@[simp]
theorem ContinuousAlternatingMap.piLinearEquiv_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [] [] [] [] [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 =
def ContinuousAlternatingMap.piLinearEquiv {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [] [] [] [] [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.

Instances For
@[simp]
theorem ContinuousAlternatingMap.smulRight_toContinuousMultilinearMap {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [] [] [] [Module R M] [Module R N] [] [] [] [] (f : M[Λ^ι]→L[R]R) (z : N) :
().toContinuousMultilinearMap = ContinuousMultilinearMap.smulRight f.toContinuousMultilinearMap z
@[simp]
theorem ContinuousAlternatingMap.smulRight_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [] [] [] [Module R M] [Module R N] [] [] [] [] (f : M[Λ^ι]→L[R]R) (z : N) :
∀ (a : (i : ι) → (fun x => M) i), = f a z
def ContinuousAlternatingMap.smulRight {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [] [] [] [Module R M] [Module 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.

Instances For
@[simp]
theorem ContinuousAlternatingMap.compContinuousLinearMapₗ_apply {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R M'] [] [] [Module R N] [] [] [] (f : M →L[R] M') (g : M'[Λ^ι]→L[R]N) :
def ContinuousAlternatingMap.compContinuousLinearMapₗ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [] [] [Module R M] [] [] [Module R M'] [] [] [Module R N] [] [] [] (f : M →L[R] M') :

ContinuousAlternatingMap.compContinuousLinearMap as a bundled LinearMap.

Instances For
def ContinuousLinearMap.compContinuousAlternatingMapₗ (R : Type u_1) (M : Type u_2) (N : Type u_4) (N' : Type u_5) {ι : Type u_6} [] [] [Module R M] [] [] [Module R N] [] [] [] [] [Module R N'] [] [] [] :

ContinuousLinearMap.compContinuousAlternatingMap as a bundled bilinear map.

Instances For
theorem ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [] [] [Module R M] [] [] [Module R N] [] [] [] (f : ContinuousMultilinearMap R (fun x => M) N) :
(ContinuousMultilinearMap.alternatization f).toContinuousMultilinearMap = Finset.sum Finset.univ fun σ => Equiv.Perm.sign σ
def ContinuousMultilinearMap.alternatization {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [] [] [Module R M] [] [] [Module R N] [] [] [] :

Alternatization of a continuous multilinear map.

Instances For
theorem ContinuousMultilinearMap.alternatization_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [] [] [Module R M] [] [] [Module R N] [] [] [] (f : ContinuousMultilinearMap R (fun x => M) N) (v : ιM) :
↑(ContinuousMultilinearMap.alternatization f) v = Finset.sum Finset.univ fun σ => 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} [] [] [Module R M] [] [] [Module R N] [] [] [] (f : ContinuousMultilinearMap R (fun x => M) N) :
ContinuousAlternatingMap.toAlternatingMap (ContinuousMultilinearMap.alternatization f) = MultilinearMap.alternatization f.toMultilinearMap