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 :
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.
Instances For
    @[reducible]
    abbrev ContinuousAlternatingMap.toAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (self : M [⋀^ι]→L[R] N) :

    Projection to AlternatingMaps.

    Equations
    • self.toAlternatingMap = { toMultilinearMap := self.toMultilinearMap, map_eq_zero_of_eq' := }
    Instances For

      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.
      Instances For
        theorem ContinuousAlternatingMap.toContinuousMultilinearMap_injective {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] :
        Function.Injective ContinuousAlternatingMap.toContinuousMultilinearMap
        theorem ContinuousAlternatingMap.range_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] :
        Set.range ContinuousAlternatingMap.toContinuousMultilinearMap = {f : ContinuousMultilinearMap R (fun (x : ι) => M) N | ∀ (v : ιM) (i j : ι), v i = v 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
        • ContinuousAlternatingMap.funLike = { coe := fun (f : M [⋀^ι]→L[R] N) => f.toFun, coe_injective' := }
        instance ContinuousAlternatingMap.continuousMapClass {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] :
        ContinuousMapClass (M [⋀^ι]→L[R] N) (ιM) N
        Equations
        • =
        theorem ContinuousAlternatingMap.coe_continuous {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) :
        @[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 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) :
        f.toAlternatingMap = f
        theorem ContinuousAlternatingMap.ext {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {f : M [⋀^ι]→L[R] N} {g : M [⋀^ι]→L[R] N} (H : ∀ (x : ιM), f x = g x) :
        f = g
        theorem ContinuousAlternatingMap.ext_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {f : M [⋀^ι]→L[R] N} {g : M [⋀^ι]→L[R] N} :
        f = g ∀ (x : ιM), f x = g x
        theorem ContinuousAlternatingMap.toAlternatingMap_injective {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] :
        Function.Injective ContinuousAlternatingMap.toAlternatingMap
        @[simp]
        theorem ContinuousAlternatingMap.range_toAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] :
        Set.range ContinuousAlternatingMap.toAlternatingMap = {f : M [⋀^ι]→ₗ[R] N | Continuous f}
        @[simp]
        theorem ContinuousAlternatingMap.map_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ιM) (i : ι) (x : M) (y : M) :
        f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
        @[simp]
        theorem ContinuousAlternatingMap.map_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ιM) (i : ι) (c : R) (x : M) :
        f (Function.update m i (c x)) = c f (Function.update m i x)
        theorem ContinuousAlternatingMap.map_coord_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {m : ιM} (i : ι) (h : m i = 0) :
        f m = 0
        @[simp]
        theorem ContinuousAlternatingMap.map_update_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ιM) (i : ι) :
        f (Function.update m i 0) = 0
        @[simp]
        theorem ContinuousAlternatingMap.map_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [Nonempty ι] :
        f 0 = 0
        theorem ContinuousAlternatingMap.map_eq_zero_of_eq {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (v : ιM) {i : ι} {j : ι} (h : v i = v j) (hij : i j) :
        f v = 0
        theorem ContinuousAlternatingMap.map_eq_zero_of_not_injective {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (v : ιM) (hv : ¬Function.Injective v) :
        f v = 0
        @[simp]
        theorem ContinuousAlternatingMap.codRestrict_apply_coe {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (p : Submodule R N) (h : ∀ (v : ιM), f v p) (v : (i : ι) → (fun (x : ι) => M) i) :
        ((f.codRestrict p h) v) = f v
        def ContinuousAlternatingMap.codRestrict {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (p : Submodule R N) (h : ∀ (v : ιM), f v p) :
        M [⋀^ι]→L[R] p

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

        Equations
        • f.codRestrict p h = let __src := f.toAlternatingMap.codRestrict p h; { toContinuousMultilinearMap := f.codRestrict p h, map_eq_zero_of_eq' := }
        Instances For
          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
          • 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] :
          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
          instance ContinuousAlternatingMap.instSMul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] :
          SMul R' (M [⋀^ι]→L[A] N)
          Equations
          • ContinuousAlternatingMap.instSMul = { smul := fun (c : R') (f : M [⋀^ι]→L[A] N) => { toContinuousMultilinearMap := c f.toContinuousMultilinearMap, map_eq_zero_of_eq' := } }
          @[simp]
          theorem ContinuousAlternatingMap.coe_smul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] (f : M [⋀^ι]→L[A] N) (c : R') :
          (c f) = c f
          theorem ContinuousAlternatingMap.smul_apply {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] (f : M [⋀^ι]→L[A] N) (c : R') (v : ιM) :
          (c f) v = c f v
          @[simp]
          theorem ContinuousAlternatingMap.toContinuousMultilinearMap_smul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] (c : R') (f : M [⋀^ι]→L[A] N) :
          (c f).toContinuousMultilinearMap = c f.toContinuousMultilinearMap
          @[simp]
          theorem ContinuousAlternatingMap.toAlternatingMap_smul {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] (c : R') (f : M [⋀^ι]→L[A] N) :
          (c f).toAlternatingMap = c f.toAlternatingMap
          instance ContinuousAlternatingMap.instSMulCommClass {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {R'' : Type u_8} {A : Type u_9} [Monoid R'] [Monoid R''] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] [DistribMulAction R'' N] [ContinuousConstSMul R'' N] [SMulCommClass A R'' N] [SMulCommClass R' R'' N] :
          SMulCommClass R' R'' (M [⋀^ι]→L[A] N)
          Equations
          • =
          instance ContinuousAlternatingMap.instIsScalarTower {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {R'' : Type u_8} {A : Type u_9} [Monoid R'] [Monoid R''] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] [DistribMulAction R'' N] [ContinuousConstSMul R'' N] [SMulCommClass A R'' N] [SMul R' R''] [IsScalarTower R' R'' N] :
          IsScalarTower R' R'' (M [⋀^ι]→L[A] N)
          Equations
          • =
          Equations
          • =
          instance ContinuousAlternatingMap.instMulAction {M : Type u_2} {N : Type u_4} {ι : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [Monoid R'] [Semiring A] [Module A M] [Module A N] [DistribMulAction R' N] [ContinuousConstSMul R' N] [SMulCommClass A R' N] :
          Equations
          instance ContinuousAlternatingMap.instAdd {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] :
          Add (M [⋀^ι]→L[R] N)
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem ContinuousAlternatingMap.coe_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) [ContinuousAdd N] :
          (f + g) = f + g
          @[simp]
          theorem ContinuousAlternatingMap.add_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) [ContinuousAdd N] (v : ιM) :
          (f + g) v = f v + g v
          @[simp]
          theorem ContinuousAlternatingMap.toContinuousMultilinearMap_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) :
          (f + g).toContinuousMultilinearMap = f.toContinuousMultilinearMap + g.toContinuousMultilinearMap
          @[simp]
          theorem ContinuousAlternatingMap.toAlternatingMap_add {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) :
          (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap
          Equations
          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
          Instances For
            @[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
            @[simp]
            theorem ContinuousAlternatingMap.toMultilinearAddHom_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] (f : M [⋀^ι]→L[R] N) :
            ContinuousAlternatingMap.toMultilinearAddHom f = f.toContinuousMultilinearMap
            def ContinuousAlternatingMap.toMultilinearAddHom {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] :
            M [⋀^ι]→L[R] N →+ ContinuousMultilinearMap R (fun (x : ι) => M) N

            Projection to ContinuousMultilinearMaps as a bundled AddMonoidHom.

            Equations
            • ContinuousAlternatingMap.toMultilinearAddHom = { toFun := fun (f : M [⋀^ι]→L[R] N) => f.toContinuousMultilinearMap, map_zero' := , map_add' := }
            Instances For
              @[simp]
              theorem ContinuousAlternatingMap.toContinuousLinearMap_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ιM) (i : ι) (x : M) :
              (f.toContinuousLinearMap m i) x = f (Function.update m i x)
              def ContinuousAlternatingMap.toContinuousLinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ιM) (i : ι) :
              M →L[R] N

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

              Equations
              • f.toContinuousLinearMap m i = f.toContinuousLinearMap m i
              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} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N') (m : (i : ι) → (fun (x : ι) => M) i) :
                (f.prod g) m = (f m, g m)
                def ContinuousAlternatingMap.prod {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N') :
                M [⋀^ι]→L[R] (N × N')

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

                Equations
                • f.prod g = { toContinuousMultilinearMap := f.prod g.toContinuousMultilinearMap, map_eq_zero_of_eq' := }
                Instances For
                  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
                  Instances For
                    @[simp]
                    theorem ContinuousAlternatingMap.coe_pi {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {M' : ι'Type u_8} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → M [⋀^ι]→L[R] M' i) :
                    (ContinuousAlternatingMap.pi f) = fun (m : ιM) (j : ι') => (f j) m
                    theorem ContinuousAlternatingMap.pi_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {M' : ι'Type u_8} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → M [⋀^ι]→L[R] M' i) (m : ιM) (j : ι') :
                    @[simp]
                    theorem ContinuousAlternatingMap.ofSubsingleton_apply_toContinuousMultilinearMap (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) (f : M →L[R] N) :
                    ((ContinuousAlternatingMap.ofSubsingleton R M N i) f).toContinuousMultilinearMap = (ContinuousMultilinearMap.ofSubsingleton R M N i) f
                    @[simp]
                    theorem ContinuousAlternatingMap.ofSubsingleton_apply_apply (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) (f : M →L[R] N) (x : ιM) :
                    @[simp]
                    theorem ContinuousAlternatingMap.ofSubsingleton_symm_apply_apply (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) (f : M [⋀^ι]→L[R] N) (x : M) :
                    ((ContinuousAlternatingMap.ofSubsingleton R M N i).symm f) x = f fun (x_1 : ι) => x
                    def ContinuousAlternatingMap.ofSubsingleton (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) :
                    (M →L[R] N) M [⋀^ι]→L[R] N

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [Subsingleton ι] (i : ι) (f : M →L[R] N) :
                      ((ContinuousAlternatingMap.ofSubsingleton R M N i) f).toAlternatingMap = (AlternatingMap.ofSubsingleton R M N i) f
                      @[simp]
                      theorem ContinuousAlternatingMap.constOfIsEmpty_toContinuousMultilinearMap (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsEmpty ι] (m : N) :
                      (ContinuousAlternatingMap.constOfIsEmpty R M ι m).toContinuousMultilinearMap = ContinuousMultilinearMap.constOfIsEmpty R (fun (x : ι) => M) m
                      @[simp]
                      theorem ContinuousAlternatingMap.constOfIsEmpty_apply (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsEmpty ι] (m : N) :
                      ∀ (a : (i : ι) → (fun (x : ι) => M) i), (ContinuousAlternatingMap.constOfIsEmpty R M ι m) a = m
                      def ContinuousAlternatingMap.constOfIsEmpty (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsEmpty ι] (m : N) :

                      The constant map is alternating when ι is empty.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        def ContinuousAlternatingMap.compContinuousLinearMap {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (g : M [⋀^ι]→L[R] N) (f : M' →L[R] M) :
                        M' [⋀^ι]→L[R] N

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

                        Equations
                        • g.compContinuousLinearMap f = let __src := g.toAlternatingMap.compLinearMap f; { toContinuousMultilinearMap := g.compContinuousLinearMap fun (x : ι) => f, map_eq_zero_of_eq' := }
                        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} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (g : M [⋀^ι]→L[R] N) (f : M' →L[R] M) (m : ιM') :
                          (g.compContinuousLinearMap f) m = g (f m)
                          def ContinuousLinearMap.compContinuousAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (g : N →L[R] N') (f : M [⋀^ι]→L[R] N) :
                          M [⋀^ι]→L[R] N'

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          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} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (g : N →L[R] N') (f : M [⋀^ι]→L[R] N) :
                            (g.compContinuousAlternatingMap f) = g f
                            def ContinuousLinearEquiv.continuousAlternatingMapComp {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (e : M ≃L[R] M') :

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              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') :

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

                              Equations
                              • e.compContinuousAlternatingMap = { toFun := (e).compContinuousAlternatingMap, invFun := (e.symm).compContinuousAlternatingMap, left_inv := , right_inv := }
                              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} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (e : N ≃L[R] N') (f : M [⋀^ι]→L[R] N) :
                                (e.compContinuousAlternatingMap f) = e f
                                def ContinuousLinearEquiv.continuousAlternatingMapCongr {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (e : M ≃L[R] M') (e' : N ≃L[R] N') :
                                M [⋀^ι]→L[R] N M' [⋀^ι]→L[R] N'

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

                                Equations
                                • e.continuousAlternatingMapCongr e' = e.continuousAlternatingMapComp.trans e'.compContinuousAlternatingMap
                                Instances For
                                  @[simp]
                                  theorem ContinuousAlternatingMap.piEquiv_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {N : ι'Type u_8} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → TopologicalSpace (N i)] [(i : ι') → Module R (N i)] (f : M [⋀^ι]→L[R] ((i : ι') → N i)) (i : ι') :
                                  ContinuousAlternatingMap.piEquiv.symm f i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap f
                                  @[simp]
                                  theorem ContinuousAlternatingMap.piEquiv_apply {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {N : ι'Type u_8} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → TopologicalSpace (N i)] [(i : ι') → Module R (N i)] (f : (i : ι') → M [⋀^ι]→L[R] N i) :
                                  ContinuousAlternatingMap.piEquiv f = ContinuousAlternatingMap.pi f
                                  def ContinuousAlternatingMap.piEquiv {R : Type u_1} {M : Type u_2} {ι : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {ι' : Type u_7} {N : ι'Type u_8} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → TopologicalSpace (N i)] [(i : ι') → Module R (N i)] :
                                  ((i : ι') → M [⋀^ι]→L[R] N i) M [⋀^ι]→L[R] ((i : ι') → N i)

                                  ContinuousAlternatingMap.pi as an Equiv.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    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 : M) (y : M) :
                                    f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)

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

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

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

                                    theorem ContinuousAlternatingMap.cons_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {n : } (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin 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' : ι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' : ι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
                                    Instances For
                                      @[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) :
                                      @[simp]
                                      theorem ContinuousAlternatingMap.map_sub {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (m : ιM) (i : ι) (x : M) (y : M) :
                                      f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
                                      instance ContinuousAlternatingMap.instNeg {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] :
                                      Neg (M [⋀^ι]→L[R] N)
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      @[simp]
                                      theorem ContinuousAlternatingMap.coe_neg {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [TopologicalAddGroup N] :
                                      (-f) = -f
                                      theorem ContinuousAlternatingMap.neg_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [TopologicalAddGroup N] (m : ιM) :
                                      (-f) m = -f m
                                      instance ContinuousAlternatingMap.instSub {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] :
                                      Sub (M [⋀^ι]→L[R] N)
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      @[simp]
                                      theorem ContinuousAlternatingMap.coe_sub {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) [TopologicalAddGroup N] :
                                      (f - g) = f - g
                                      theorem ContinuousAlternatingMap.sub_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N) [TopologicalAddGroup N] (m : ιM) :
                                      (f - g) m = f m - g m
                                      Equations
                                      theorem ContinuousAlternatingMap.map_piecewise_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [DecidableEq ι] (c : ιR) (m : ιM) (s : Finset ι) :
                                      f (s.piecewise (fun (i : ι) => c i m i) m) = (is, c i) f m
                                      theorem ContinuousAlternatingMap.map_smul_univ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [Fintype ι] (c : ιR) (m : ιM) :
                                      (f fun (i : ι) => c i m i) = (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.

                                      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
                                      @[simp]
                                      theorem ContinuousAlternatingMap.toContinuousMultilinearMapLinear_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] [Module A M] [Module A N] [Module R N] [ContinuousConstSMul R N] [SMulCommClass A R N] (self : M [⋀^ι]→L[A] N) :
                                      ContinuousAlternatingMap.toContinuousMultilinearMapLinear self = self.toContinuousMultilinearMap

                                      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' := }
                                      Instances For
                                        @[simp]
                                        theorem ContinuousAlternatingMap.toAlternatingMapLinear_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] [Module A M] [Module A N] [Module R N] [ContinuousConstSMul R N] [SMulCommClass A R N] :
                                        ContinuousAlternatingMap.toAlternatingMapLinear = ContinuousAlternatingMap.toAlternatingMap

                                        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' := }
                                        Instances For
                                          @[simp]
                                          theorem ContinuousAlternatingMap.piLinearEquiv_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [TopologicalSpace M] [Module A M] {ι' : Type u_6} {M' : ι'Type u_7} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R (M' i)] [∀ (i : ι'), ContinuousConstSMul R (M' i)] :
                                          ∀ (a : (i : ι') → M [⋀^ι]→L[A] M' i), ContinuousAlternatingMap.piLinearEquiv a = ContinuousAlternatingMap.pi a
                                          @[simp]
                                          theorem ContinuousAlternatingMap.piLinearEquiv_symm_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [TopologicalSpace M] [Module A M] {ι' : Type u_6} {M' : ι'Type u_7} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R (M' i)] [∀ (i : ι'), ContinuousConstSMul R (M' i)] :
                                          ∀ (a : M [⋀^ι]→L[A] ((i : ι') → M' i)) (i : ι'), ContinuousAlternatingMap.piLinearEquiv.symm a i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap a
                                          def ContinuousAlternatingMap.piLinearEquiv {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_5} [Semiring R] [Semiring A] [AddCommMonoid M] [TopologicalSpace M] [Module A M] {ι' : Type u_6} {M' : ι'Type u_7} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R (M' i)] [∀ (i : ι'), ContinuousConstSMul R (M' i)] :
                                          ((i : ι') → M [⋀^ι]→L[A] M' i) ≃ₗ[R] M [⋀^ι]→L[A] ((i : ι') → M' i)

                                          ContinuousAlternatingMap.pi as a LinearEquiv.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem ContinuousAlternatingMap.smulRight_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [TopologicalSpace R] [TopologicalSpace M] [TopologicalSpace N] [ContinuousSMul R N] (f : M [⋀^ι]→L[R] R) (z : N) :
                                            ∀ (a : (i : ι) → (fun (x : ι) => M) i), (f.smulRight z) a = f a z
                                            @[simp]
                                            theorem ContinuousAlternatingMap.smulRight_toContinuousMultilinearMap {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [TopologicalSpace R] [TopologicalSpace M] [TopologicalSpace N] [ContinuousSMul R N] (f : M [⋀^ι]→L[R] R) (z : N) :
                                            (f.smulRight z).toContinuousMultilinearMap = f.smulRight z
                                            def ContinuousAlternatingMap.smulRight {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [TopologicalSpace R] [TopologicalSpace M] [TopologicalSpace N] [ContinuousSMul R N] (f : M [⋀^ι]→L[R] R) (z : N) :

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

                                            Equations
                                            • f.smulRight z = let __src := f.toAlternatingMap.smulRight z; { toContinuousMultilinearMap := f.smulRight z, map_eq_zero_of_eq' := }
                                            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} [CommSemiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousConstSMul R N] (f : M →L[R] M') (g : M' [⋀^ι]→L[R] N) :
                                              (ContinuousAlternatingMap.compContinuousLinearMapₗ f) g = g.compContinuousLinearMap f

                                              ContinuousAlternatingMap.compContinuousLinearMap as a bundled LinearMap.

                                              Equations
                                              Instances For

                                                ContinuousLinearMap.compContinuousAlternatingMap as a bundled bilinear map.

                                                Equations
                                                Instances For
                                                  theorem ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) :
                                                  (ContinuousMultilinearMap.alternatization f).toContinuousMultilinearMap = σ : Equiv.Perm ι, Equiv.Perm.sign σ ContinuousMultilinearMap.domDomCongr σ f
                                                  def ContinuousMultilinearMap.alternatization {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] :
                                                  ContinuousMultilinearMap R (fun (x : ι) => M) N →+ M [⋀^ι]→L[R] N

                                                  Alternatization of a continuous multilinear map.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    theorem ContinuousMultilinearMap.alternatization_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) (v : ιM) :
                                                    (ContinuousMultilinearMap.alternatization f) v = σ : Equiv.Perm ι, Equiv.Perm.sign σ f (v σ)
                                                    @[simp]
                                                    theorem ContinuousMultilinearMap.alternatization_apply_toAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [TopologicalAddGroup N] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap R (fun (x : ι) => M) N) :
                                                    (ContinuousMultilinearMap.alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap