Mathlib.LinearAlgebra.Alternating.Basic

AlternatingMap structure

extends MultilinearMap R (fun _ : ι => M) N

Full source

/-- An alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→ₗ[R] N`,
is a multilinear map that vanishes when two of its arguments are equal. -/
structure AlternatingMap extends MultilinearMap R (fun _ : ι => M) N where
  /-- The map is alternating: if `v` has two equal coordinates, then `f v = 0`. -/
  map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toFun v = 0

Alternating Map

Informal description

An alternating map from $\iota \to M$ to $N$, denoted $M [\bigwedge^\iota] \to_{R} N$, is a multilinear map that vanishes whenever two of its arguments are equal.

term_[⋀^_]→ₗ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation M " [⋀^" ι "]→ₗ[" R "] " N:100 => AlternatingMap R M N ι

Space of alternating multilinear maps

Informal description

The notation $ M [\bigwedge^\iota] \to_{\ell[R]} N $ represents the space of $ R $-linear alternating maps from $ \iota \to M $ to $ N $, where $ M $ and $ N $ are modules over a commutative semiring $ R $, and $ \iota $ is the index type for the arguments of the map.

AlternatingMap.instFunLike instance

: FunLike (M [⋀^ι]→ₗ[R] N) (ι → M) N

Full source

instance instFunLike : FunLike (M [⋀^ι]→ₗ[R] N) (ι → M) N where
  coe f := f.toFun
  coe_injective' f g h := by
    rcases f with ⟨⟨_, _, _⟩, _⟩
    rcases g with ⟨⟨_, _, _⟩, _⟩
    congr

Function-Like Structure on Alternating Maps

Informal description

The space of $R$-linear alternating maps from $\iota \to M$ to $N$ has a function-like structure, where each alternating map can be viewed as a function from $\iota \to M$ to $N$.

AlternatingMap.toFun_eq_coe theorem

: f.toFun = f

Full source

@[simp]
theorem toFun_eq_coe : f.toFun = f :=
  rfl

Underlying Function Equals Alternating Map

Informal description

For any alternating map $f$, the underlying function `f.toFun` is equal to $f$ itself.

AlternatingMap.coe_mk theorem

(f : MultilinearMap R (fun _ : ι => M) N) (h) : ⇑(⟨f, h⟩ : M [⋀^ι]→ₗ[R] N) = f

Full source

@[simp]
theorem coe_mk (f : MultilinearMap R (fun _ : ι => M) N) (h) :
    ⇑(⟨f, h⟩ : M [⋀^ι]→ₗ[R] N) = f :=
  rfl

Equality of Underlying Function in Alternating Map Construction

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be an index type. Given a multilinear map $f \colon (\iota \to M) \to N$ and a proof $h$ that $f$ is alternating, the underlying function of the constructed alternating map $\langle f, h \rangle \colon M [\bigwedge^\iota] \to_{R} N$ is equal to $f$.

AlternatingMap.congr_fun theorem

{f g : M [⋀^ι]→ₗ[R] N} (h : f = g) (x : ι → M) : f x = g x

Full source

protected theorem congr_fun {f g : M [⋀^ι]→ₗ[R] N} (h : f = g) (x : ι → M) : f x = g x :=
  congr_arg (fun h : M [⋀^ι]→ₗ[R] N => h x) h

Function Equality Implies Pointwise Equality for Alternating Maps

Informal description

For any two $R$-linear alternating maps $f, g \colon M [\bigwedge^\iota] \to_{R} N$ and any vector $x \colon \iota \to M$, if $f = g$, then $f(x) = g(x)$.

AlternatingMap.congr_arg theorem

(f : M [⋀^ι]→ₗ[R] N) {x y : ι → M} (h : x = y) : f x = f y

Full source

protected theorem congr_arg (f : M [⋀^ι]→ₗ[R] N) {x y : ι → M} (h : x = y) : f x = f y :=
  congr_arg (fun x : ι → M => f x) h

Congruence of Alternating Maps under Equal Arguments

Informal description

For any $R$-linear alternating map $f$ from $\iota \to M$ to $N$, and for any two vectors $x, y \colon \iota \to M$ such that $x = y$, the evaluation of $f$ at $x$ equals its evaluation at $y$, i.e., $f(x) = f(y)$.

AlternatingMap.coe_injective theorem

: Injective ((↑) : M [⋀^ι]→ₗ[R] N → (ι → M) → N)

Full source

theorem coe_injective : Injective ((↑) : M [⋀^ι]→ₗ[R] N → (ι → M) → N) :=
  DFunLike.coe_injective

Injectivity of the Canonical Map from Alternating Maps to Functions

Informal description

The canonical map from the space of $R$-linear alternating maps $M [\bigwedge^\iota] \to_{R} N$ to the space of functions $(\iota \to M) \to N$ is injective. That is, if two alternating maps $f$ and $g$ satisfy $f(x) = g(x)$ for all $x \in \iota \to M$, then $f = g$.

AlternatingMap.coe_inj theorem

{f g : M [⋀^ι]→ₗ[R] N} : (f : (ι → M) → N) = g ↔ f = g

Full source

@[norm_cast]
theorem coe_inj {f g : M [⋀^ι]→ₗ[R] N} : (f : (ι → M) → N) = g ↔ f = g :=
  coe_injective.eq_iff

Equality of Alternating Maps via Function Equality

Informal description

For any two $R$-linear alternating maps $f, g \colon M [\bigwedge^\iota] \to_{R} N$, the underlying functions $f$ and $g$ are equal if and only if the maps themselves are equal, i.e., $f = g$ as functions implies $f = g$ as alternating maps and vice versa.

AlternatingMap.ext theorem

{f f' : M [⋀^ι]→ₗ[R] N} (H : ∀ x, f x = f' x) : f = f'

Full source

@[ext]
theorem ext {f f' : M [⋀^ι]→ₗ[R] N} (H : ∀ x, f x = f' x) : f = f' :=
  DFunLike.ext _ _ H

Extensionality of Alternating Maps

Informal description

For any two $R$-linear alternating maps $f, f' \colon M [\bigwedge^\iota] \to_{R} N$, if $f(x) = f'(x)$ for all $x \in \iota \to M$, then $f = f'$.

AlternatingMap.coe instance

: Coe (M [⋀^ι]→ₗ[R] N) (MultilinearMap R (fun _ : ι => M) N)

Full source

instance coe : Coe (M [⋀^ι]→ₗ[R] N) (MultilinearMap R (fun _ : ι => M) N) :=
  ⟨fun x => x.toMultilinearMap⟩

Alternating Maps as Multilinear Maps

Informal description

Every alternating map from $\iota \to M$ to $N$ can be viewed as a multilinear map from $\iota \to M$ to $N$ with the same underlying function.

AlternatingMap.coe_multilinearMap theorem

: ⇑(f : MultilinearMap R (fun _ : ι => M) N) = f

Full source

@[simp, norm_cast]
theorem coe_multilinearMap : ⇑(f : MultilinearMap R (fun _ : ι => M) N) = f :=
  rfl

Coercion of Alternating Map to Multilinear Map Preserves Underlying Function

Informal description

For any $R$-linear alternating map $f$ from $\iota \to M$ to $N$, when viewed as a multilinear map, its underlying function is equal to $f$ itself. In other words, the coercion from alternating maps to multilinear maps preserves the underlying function.

AlternatingMap.coe_multilinearMap_injective theorem

: Function.Injective ((↑) : M [⋀^ι]→ₗ[R] N → MultilinearMap R (fun _ : ι => M) N)

Full source

theorem coe_multilinearMap_injective :
    Function.Injective ((↑) : M [⋀^ι]→ₗ[R] N → MultilinearMap R (fun _ : ι => M) N) :=
  fun _ _ h => ext <| MultilinearMap.congr_fun h

Injectivity of the Alternating-to-Multilinear Map Embedding

Informal description

The canonical embedding from the space of $R$-linear alternating maps $M [\bigwedge^\iota] \to_{R} N$ to the space of $R$-multilinear maps $(\iota \to M) \to N$ is injective. In other words, if two alternating maps induce the same multilinear map, then they are equal.

AlternatingMap.coe_multilinearMap_mk theorem

 (f : (ι → M) → N) (h₁ h₂ h₃) :
  ((⟨⟨f, h₁, h₂⟩, h₃⟩ : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) = ⟨f, @h₁, @h₂⟩

Full source

theorem coe_multilinearMap_mk (f : (ι → M) → N) (h₁ h₂ h₃) :
    ((⟨⟨f, h₁, h₂⟩, h₃⟩ : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) =
      ⟨f, @h₁, @h₂⟩ := by
  simp

Coercion of Constructed Alternating Map to Multilinear Map

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be an index type. For any function $f : (\iota \to M) \to N$ with properties $h₁$ (linearity in each argument), $h₂$ (additivity), and $h₃$ (alternating property), the coercion of the constructed alternating map $\langle \langle f, h₁, h₂ \rangle, h₃ \rangle : M [\bigwedge^\iota] \to_{R} N$ to a multilinear map equals the multilinear map $\langle f, h₁, h₂ \rangle$.

AlternatingMap.map_update_add theorem

[DecidableEq ι] (i : ι) (x y : M) : f (update v i (x + y)) = f (update v i x) + f (update v i y)

Full source

@[simp]
theorem map_update_add [DecidableEq ι] (i : ι) (x y : M) :
    f (update v i (x + y)) = f (update v i x) + f (update v i y) :=
  f.map_update_add' v i x y

Additivity of Alternating Maps Under Function Update

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be an index type with decidable equality. For any $R$-linear alternating map $f : M [\bigwedge^\iota] \to_{R} N$, vector $v : \iota \to M$, index $i \in \iota$, and elements $x, y \in M$, the following holds: \[ f\big(\text{update } v \, i \, (x + y)\big) = f\big(\text{update } v \, i \, x\big) + f\big(\text{update } v \, i \, y\big), \] where $\text{update } v \, i \, z$ denotes the function equal to $v$ everywhere except at $i$, where it takes the value $z$.

AlternatingMap.map_update_sub theorem

[DecidableEq ι] (i : ι) (x y : M') : g' (update v' i (x - y)) = g' (update v' i x) - g' (update v' i y)

Full source

@[simp]
theorem map_update_sub [DecidableEq ι] (i : ι) (x y : M') :
    g' (update v' i (x - y)) = g' (update v' i x) - g' (update v' i y) :=
  g'.toMultilinearMap.map_update_sub v' i x y

Alternating Map Preserves Subtraction Under Function Update

Informal description

Let $R$ be a commutative ring, $M'$ and $N$ be $R$-modules, and $\iota$ be an index type with decidable equality. For any $R$-linear alternating map $g' : M' [\bigwedge^\iota] \to_{R} N$, vector $v' : \iota \to M'$, index $i \in \iota$, and elements $x, y \in M'$, the following holds: \[ g'\big(\text{update } v' \, i \, (x - y)\big) = g'\big(\text{update } v' \, i \, x\big) - g'\big(\text{update } v' \, i \, y\big), \] where $\text{update } v' \, i \, z$ denotes the function equal to $v'$ everywhere except at $i$, where it takes the value $z$.

AlternatingMap.map_update_neg theorem

[DecidableEq ι] (i : ι) (x : M') : g' (update v' i (-x)) = -g' (update v' i x)

Full source

@[simp]
theorem map_update_neg [DecidableEq ι] (i : ι) (x : M') :
    g' (update v' i (-x)) = -g' (update v' i x) :=
  g'.toMultilinearMap.map_update_neg v' i x

Alternating Map Negation Under Function Update

Informal description

Let $R$ be a commutative ring, $M'$ and $N$ be $R$-modules, and $\iota$ be an index type with decidable equality. For any $R$-linear alternating map $g' : M' [\bigwedge^\iota] \to_{R} N$, vector $v' : \iota \to M'$, index $i \in \iota$, and element $x \in M'$, the following holds: \[ g'\big(\text{update } v' \, i \, (-x)\big) = -g'\big(\text{update } v' \, i \, x\big), \] where $\text{update } v' \, i \, z$ denotes the function equal to $v'$ everywhere except at $i$, where it takes the value $z$.

AlternatingMap.map_update_smul theorem

[DecidableEq ι] (i : ι) (r : R) (x : M) : f (update v i (r • x)) = r • f (update v i x)

Full source

@[simp]
theorem map_update_smul [DecidableEq ι] (i : ι) (r : R) (x : M) :
    f (update v i (r • x)) = r • f (update v i x) :=
  f.map_update_smul' v i r x

Alternating Map Preserves Scalar Multiplication Under Function Update

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be an index type with decidable equality. For any $R$-linear alternating map $f : M [\bigwedge^\iota] \to_{R} N$, vector $v : \iota \to M$, index $i \in \iota$, scalar $r \in R$, and element $x \in M$, the following holds: \[ f\big(\text{update } v \, i \, (r \cdot x)\big) = r \cdot f\big(\text{update } v \, i \, x\big), \] where $\text{update } v \, i \, z$ denotes the function equal to $v$ everywhere except at $i$, where it takes the value $z$.

AlternatingMap.map_eq_zero_of_eq theorem

(v : ι → M) {i j : ι} (h : v i = v j) (hij : i ≠ j) : f v = 0

Full source

@[simp]
theorem map_eq_zero_of_eq (v : ι → M) {i j : ι} (h : v i = v j) (hij : i ≠ j) : f v = 0 :=
  f.map_eq_zero_of_eq' v i j h hij

Alternating Maps Vanish on Equal Arguments

Informal description

Let $f$ be an $R$-linear alternating map from $\iota \to M$ to $N$. For any function $v : \iota \to M$ and any distinct indices $i, j \in \iota$ with $v(i) = v(j)$, we have $f(v) = 0$.

AlternatingMap.map_coord_zero theorem

{m : ι → M} (i : ι) (h : m i = 0) : f m = 0

Full source

theorem map_coord_zero {m : ι → M} (i : ι) (h : m i = 0) : f m = 0 :=
  f.toMultilinearMap.map_coord_zero i h

Alternating Maps Vanish on Zero Coordinates

Informal description

Let $f$ be an $R$-linear alternating map from $\iota \to M$ to $N$. For any function $m : \iota \to M$ and any index $i \in \iota$, if $m(i) = 0$, then $f(m) = 0$.

AlternatingMap.map_update_zero theorem

[DecidableEq ι] (m : ι → M) (i : ι) : f (update m i 0) = 0

Full source

@[simp]
theorem map_update_zero [DecidableEq ι] (m : ι → M) (i : ι) : f (update m i 0) = 0 :=
  f.toMultilinearMap.map_update_zero m i

Alternating Maps Vanish on Zero-Updated Functions

Informal description

Let $f$ be an $R$-linear alternating map from $\iota \to M$ to $N$. For any function $m : \iota \to M$ and any index $i \in \iota$, the evaluation of $f$ on the function obtained by setting the $i$-th coordinate of $m$ to zero is zero, i.e., $f(\text{update } m \, i \, 0) = 0$.

AlternatingMap.map_zero theorem

[Nonempty ι] : f 0 = 0

Full source

@[simp]
theorem map_zero [Nonempty ι] : f 0 = 0 :=
  f.toMultilinearMap.map_zero

Alternating Maps Vanish on Zero Function

Informal description

For any nonempty type $\iota$ and any $R$-linear alternating map $f$ from $\iota \to M$ to $N$, the evaluation of $f$ at the zero function is zero, i.e., $f(0) = 0$.

AlternatingMap.map_eq_zero_of_not_injective theorem

(v : ι → M) (hv : ¬Function.Injective v) : f v = 0

Full source

theorem map_eq_zero_of_not_injective (v : ι → M) (hv : ¬Function.Injective v) : f v = 0 := by
  rw [Function.Injective] at hv
  push_neg at hv
  rcases hv with ⟨i₁, i₂, heq, hne⟩
  exact f.map_eq_zero_of_eq v heq hne

Alternating Maps Vanish on Non-Injective Arguments

Informal description

Let $f$ be an $R$-linear alternating map from $\iota \to M$ to $N$. For any function $v : \iota \to M$ that is not injective, we have $f(v) = 0$.

AlternatingMap.smul instance

: SMul S (M [⋀^ι]→ₗ[R] N)

Full source

instance smul : SMul S (M [⋀^ι]→ₗ[R] N) :=
  ⟨fun c f =>
    { c • (f : MultilinearMap R (fun _ : ι => M) N) with
      map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij] }⟩

Scalar Multiplication on Alternating Maps

Informal description

For any commutative semiring $R$, modules $M$ and $N$ over $R$, and type $\iota$, the space of $R$-linear alternating maps from $\iota \to M$ to $N$ has a scalar multiplication structure over any scalar semigroup $S$ acting on $N$.

AlternatingMap.smul_apply theorem

(c : S) (m : ι → M) : (c • f) m = c • f m

Full source

@[simp]
theorem smul_apply (c : S) (m : ι → M) : (c • f) m = c • f m :=
  rfl

Scalar Multiplication Commutes with Evaluation for Alternating Maps

Informal description

For any scalar $c$ in a scalar semigroup $S$ and any tuple $m \in \iota \to M$, the evaluation of the scalar multiple $c \cdot f$ at $m$ equals the scalar multiple of the evaluation of $f$ at $m$, i.e., $(c \cdot f)(m) = c \cdot f(m)$.

AlternatingMap.coe_smul theorem

(c : S) : ↑(c • f) = c • (f : MultilinearMap R (fun _ : ι => M) N)

Full source

@[norm_cast]
theorem coe_smul (c : S) : ↑(c • f) = c • (f : MultilinearMap R (fun _ : ι => M) N) :=
  rfl

Coercion of Scalar Multiple of Alternating Map Equals Scalar Multiple of Coerced Map

Informal description

For any scalar $c$ in a scalar semigroup $S$ and any $R$-linear alternating map $f$ from $\iota \to M$ to $N$, the coercion of the scalar multiple $c \cdot f$ to a multilinear map equals the scalar multiple of the coercion of $f$ to a multilinear map.

AlternatingMap.coeFn_smul theorem

(c : S) (f : M [⋀^ι]→ₗ[R] N) : ⇑(c • f) = c • ⇑f

Full source

theorem coeFn_smul (c : S) (f : M [⋀^ι]→ₗ[R] N) : ⇑(c • f) = c • ⇑f :=
  rfl

Scalar Multiplication Preserves Function Application for Alternating Maps

Informal description

For any scalar $c$ in a scalar semigroup $S$ and any $R$-linear alternating map $f$ from $\iota \to M$ to $N$, the function application of the scalar multiple $c \cdot f$ is equal to the scalar multiple of the function application of $f$, i.e., $(c \cdot f)(m) = c \cdot f(m)$ for all $m \in \iota \to M$.

AlternatingMap.isCentralScalar instance

[DistribMulAction Sᵐᵒᵖ N] [IsCentralScalar S N] : IsCentralScalar S (M [⋀^ι]→ₗ[R] N)

Full source

instance isCentralScalar [DistribMulAction Sᵐᵒᵖ N] [IsCentralScalar S N] :
    IsCentralScalar S (M [⋀^ι]→ₗ[R] N) :=
  ⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Central Scalar Property of Alternating Maps

Informal description

For any commutative semiring $R$, modules $M$ and $N$ over $R$, type $\iota$, and scalar semigroup $S$ acting on $N$ such that $S$ has a distributive multiplicative action on $N$ and $N$ is a central scalar over $S$, the space of $R$-linear alternating maps from $\iota \to M$ to $N$ is also a central scalar over $S$.

AlternatingMap.prod definition

(f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) : M [⋀^ι]→ₗ[R] (N × P)

Full source

/-- The cartesian product of two alternating maps, as an alternating map. -/
@[simps!]
def prod (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) : M [⋀^ι]→ₗ[R] (N × P) :=
  { f.toMultilinearMap.prod g.toMultilinearMap with
    map_eq_zero_of_eq' := fun _ _ _ h hne =>
      Prod.ext (f.map_eq_zero_of_eq _ h hne) (g.map_eq_zero_of_eq _ h hne) }

Cartesian product of alternating maps

Informal description

Given two $R$-linear alternating maps $f \colon M [\bigwedge^\iota] \to_{R} N$ and $g \colon M [\bigwedge^\iota] \to_{R} P$, the function `AlternatingMap.prod f g` constructs their cartesian product as an alternating map from $M [\bigwedge^\iota]$ to $N \times P$. This map sends any tuple of vectors to the pair $(f(\text{tuple}), g(\text{tuple}))$ and inherits the alternating property from $f$ and $g$.

AlternatingMap.coe_prod theorem

 (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) :
  (f.prod g : MultilinearMap R (fun _ : ι => M) (N × P)) = MultilinearMap.prod f g

Full source

@[simp]
theorem coe_prod (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) :
    (f.prod g : MultilinearMap R (fun _ : ι => M) (N × P)) = MultilinearMap.prod f g :=
  rfl

Underlying Multilinear Map of Product of Alternating Maps Equals Product of Underlying Multilinear Maps

Informal description

For any $R$-linear alternating maps $f \colon M [\bigwedge^\iota] \to_{R} N$ and $g \colon M [\bigwedge^\iota] \to_{R} P$, the underlying multilinear map of their product $f.prod\ g$ is equal to the product of the underlying multilinear maps of $f$ and $g$. That is, $(f.prod\ g) = MultilinearMap.prod\ f\ g$ as multilinear maps.

AlternatingMap.pi definition

 {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)] (f : ∀ i, M [⋀^ι]→ₗ[R] N i) :
  M [⋀^ι]→ₗ[R] (∀ i, N i)

Full source

/-- Combine a family of alternating maps with the same domain and codomains `N i` into an
alternating map taking values in the space of functions `Π i, N i`. -/
@[simps!]
def pi {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
    (f : ∀ i, M [⋀^ι]→ₗ[R] N i) : M [⋀^ι]→ₗ[R] (∀ i, N i) :=
  { MultilinearMap.pi fun a => (f a).toMultilinearMap with
    map_eq_zero_of_eq' := fun _ _ _ h hne => funext fun a => (f a).map_eq_zero_of_eq _ h hne }

Combination of alternating maps into a product space

Informal description

Given a family of $R$-linear alternating maps $f_i \colon M [\bigwedge^\iota] \to_{R} N_i$ for each $i$ in some index set $\iota'$, the function `AlternatingMap.pi` combines them into a single $R$-linear alternating map from $M [\bigwedge^\iota]$ to the product space $\prod_{i \in \iota'} N_i$. This map sends a tuple of vectors to the tuple $(f_i(\text{tuple}))_{i \in \iota'}$ and inherits the alternating property from each $f_i$.

AlternatingMap.coe_pi theorem

 {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)] (f : ∀ i, M [⋀^ι]→ₗ[R] N i) :
  (pi f : MultilinearMap R (fun _ : ι => M) (∀ i, N i)) = MultilinearMap.pi fun a => f a

Full source

@[simp]
theorem coe_pi {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
    (f : ∀ i, M [⋀^ι]→ₗ[R] N i) :
    (pi f : MultilinearMap R (fun _ : ι => M) (∀ i, N i)) = MultilinearMap.pi fun a => f a :=
  rfl

Underlying Multilinear Map of Combined Alternating Maps Equals Combined Underlying Multilinear Maps

Informal description

Let $R$ be a commutative semiring, $M$ and $N_i$ (for $i$ in some index set $\iota'$) be $R$-modules. Given a family of $R$-linear alternating maps $f_i \colon M [\bigwedge^\iota] \to_{R} N_i$ for each $i \in \iota'$, the underlying multilinear map of the combined alternating map $\mathrm{pi}\, f$ is equal to the multilinear map obtained by combining the underlying multilinear maps of each $f_i$. That is, $(\mathrm{pi}\, f) = \mathrm{MultilinearMap.pi}\, (\lambda a, f a)$ as multilinear maps.

AlternatingMap.smulRight definition

 {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂]
  (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) : M₁ [⋀^ι]→ₗ[R] M₂

Full source

/-- Given an alternating `R`-multilinear map `f` taking values in `R`, `f.smul_right z` is the map
sending `m` to `f m • z`. -/
@[simps!]
def smulRight {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂]
    [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) : M₁ [⋀^ι]→ₗ[R] M₂ :=
  { f.toMultilinearMap.smulRight z with
    map_eq_zero_of_eq' := fun v i j h hne => by simp [f.map_eq_zero_of_eq v h hne] }

Scalar multiplication of an alternating map by a fixed element

Informal description

Given a commutative semiring $R$, additive commutative monoids $M₁$ and $M₂$ with $R$-module structures, and an $R$-linear alternating map $f$ from $\iota \to M₁$ to $R$, the function `smulRight` constructs an $R$-linear alternating map from $\iota \to M₁$ to $M₂$ by sending a tuple $m$ to $f(m) \cdot z$, where $z$ is a fixed element of $M₂$.

AlternatingMap.coe_smulRight theorem

 {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂]
  (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :
  (f.smulRight z : MultilinearMap R (fun _ : ι => M₁) M₂) = MultilinearMap.smulRight f z

Full source

@[simp]
theorem coe_smulRight {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂]
    [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :
    (f.smulRight z : MultilinearMap R (fun _ : ι => M₁) M₂) = MultilinearMap.smulRight f z :=
  rfl

Coercion of scalar multiplication of alternating maps matches multilinear version

Informal description

Let $R$ be a commutative semiring, $M₁$ and $M₂$ be additive commutative monoids equipped with $R$-module structures, and $\iota$ be an index type. Given an $R$-linear alternating map $f \colon M₁ [\bigwedge^\iota] \to_{R} R$ and an element $z \in M₂$, the underlying multilinear map of the alternating map $f.\text{smulRight}\, z$ is equal to the multilinear map obtained by right scalar multiplication of $f$ by $z$.

AlternatingMap.add instance

: Add (M [⋀^ι]→ₗ[R] N)

Full source

instance add : Add (M [⋀^ι]→ₗ[R] N) :=
  ⟨fun a b =>
    { (a + b : MultilinearMap R (fun _ : ι => M) N) with
      map_eq_zero_of_eq' := fun v i j h hij => by
        simp [a.map_eq_zero_of_eq v h hij, b.map_eq_zero_of_eq v h hij] }⟩

Additive Structure on Alternating Maps

Informal description

The space of $R$-linear alternating maps from $\iota \to M$ to $N$ forms an additive commutative monoid under pointwise addition.

AlternatingMap.add_apply theorem

: (f + f') v = f v + f' v

Full source

@[simp]
theorem add_apply : (f + f') v = f v + f' v :=
  rfl

Additivity of Alternating Map Evaluation

Informal description

For any two alternating maps $f, f' \colon M [\bigwedge^\iota] \to_{R} N$ and any vector $v \in \iota \to M$, the evaluation of their sum at $v$ is equal to the sum of their evaluations, i.e., $(f + f')(v) = f(v) + f'(v)$.

AlternatingMap.coe_add theorem

: (↑(f + f') : MultilinearMap R (fun _ : ι => M) N) = f + f'

Full source

@[norm_cast]
theorem coe_add : (↑(f + f') : MultilinearMap R (fun _ : ι => M) N) = f + f' :=
  rfl

Coercion of Sum of Alternating Maps Equals Sum of Coercions

Informal description

The coercion of the sum of two alternating maps $f$ and $f'$ from $M [\bigwedge^\iota] \to_{R} N$ to multilinear maps is equal to the sum of their coercions, i.e., $\uparrow(f + f') = \uparrow f + \uparrow f'$ as multilinear maps.

AlternatingMap.zero instance

: Zero (M [⋀^ι]→ₗ[R] N)

Full source

instance zero : Zero (M [⋀^ι]→ₗ[R] N) :=
  ⟨{ (0 : MultilinearMap R (fun _ : ι => M) N) with
      map_eq_zero_of_eq' := fun _ _ _ _ _ => by simp }⟩

Zero Element in the Space of Alternating Maps

Informal description

The space of $R$-linear alternating maps from $\iota \to M$ to $N$ has a zero element.

AlternatingMap.zero_apply theorem

: (0 : M [⋀^ι]→ₗ[R] N) v = 0

Full source

@[simp]
theorem zero_apply : (0 : M [⋀^ι]→ₗ[R] N) v = 0 :=
  rfl

Zero Alternating Map Evaluates to Zero

Informal description

For any vector $v$ in $\iota \to M$, the zero alternating map evaluated at $v$ is equal to the zero element in $N$, i.e., $0(v) = 0$.

AlternatingMap.coe_zero theorem

: ((0 : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) = 0

Full source

@[norm_cast]
theorem coe_zero : ((0 : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) = 0 :=
  rfl

Coercion of Zero Alternating Map to Multilinear Map Yields Zero

Informal description

The zero alternating map, when viewed as a multilinear map, is equal to the zero multilinear map. That is, the coercion of the zero element in the space of $R$-linear alternating maps from $\iota \to M$ to $N$ to a multilinear map yields the zero multilinear map.

AlternatingMap.mk_zero theorem

: mk (0 : MultilinearMap R (fun _ : ι ↦ M) N) (0 : M [⋀^ι]→ₗ[R] N).2 = 0

Full source

@[simp]
theorem mk_zero :
    mk (0 : MultilinearMap R (fun _ : ι ↦ M) N) (0 : M [⋀^ι]→ₗ[R] N).2 = 0 :=
  rfl

Construction of Zero Alternating Map Yields Zero Element

Informal description

The construction of the zero alternating map, obtained from the zero multilinear map and the zero alternating property, is equal to the zero element in the space of alternating maps from $\iota \to M$ to $N$.

AlternatingMap.inhabited instance

: Inhabited (M [⋀^ι]→ₗ[R] N)

Full source

instance inhabited : Inhabited (M [⋀^ι]→ₗ[R] N) :=
  ⟨0⟩

Inhabited Space of Alternating Maps

Informal description

For any commutative ring $R$, modules $M$ and $N$ over $R$, and any type $\iota$, the space of $R$-linear alternating maps from $\iota \to M$ to $N$ is inhabited.

AlternatingMap.addCommMonoid instance

: AddCommMonoid (M [⋀^ι]→ₗ[R] N)

Full source

instance addCommMonoid : AddCommMonoid (M [⋀^ι]→ₗ[R] N) :=
  coe_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => coeFn_smul _ _

Additive Commutative Monoid Structure on Alternating Maps

Informal description

The space of $R$-linear alternating maps from $\iota \to M$ to $N$ forms an additive commutative monoid under pointwise addition.

AlternatingMap.neg instance

: Neg (M [⋀^ι]→ₗ[R] N')

Full source

instance neg : Neg (M [⋀^ι]→ₗ[R] N') :=
  ⟨fun f =>
    { -(f : MultilinearMap R (fun _ : ι => M) N') with
      map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij] }⟩

Negation Operation on Alternating Maps

Informal description

For any commutative ring $R$, modules $M$ and $N'$ over $R$, and any type $\iota$, the space of alternating maps $M [\bigwedge^\iota] \to_{R} N'$ is equipped with a negation operation. Specifically, for any alternating map $g$ in this space, the negation $-g$ is defined pointwise as $(-g)(m) = -g(m)$ for all $m \in \iota \to M$.

AlternatingMap.neg_apply theorem

(m : ι → M) : (-g) m = -g m

Full source

@[simp]
theorem neg_apply (m : ι → M) : (-g) m = -g m :=
  rfl

Pointwise Negation of Alternating Maps

Informal description

For any alternating map $g$ from $\iota \to M$ to $N'$ and any input $m \in \iota \to M$, the evaluation of the negated map $-g$ at $m$ equals the negation of the evaluation of $g$ at $m$, i.e., $(-g)(m) = -g(m)$.

AlternatingMap.coe_neg theorem

: ((-g : M [⋀^ι]→ₗ[R] N') : MultilinearMap R (fun _ : ι => M) N') = -g

Full source

@[norm_cast]
theorem coe_neg : ((-g : M [⋀^ι]→ₗ[R] N') : MultilinearMap R (fun _ : ι => M) N') = -g :=
  rfl

Coercion of Negated Alternating Map Equals Negation of Coercion

Informal description

For any $R$-linear alternating map $g$ from $\iota \to M$ to $N'$, the coercion of $-g$ to a multilinear map equals the negation of the coercion of $g$, i.e., $(-g) = -g$ as multilinear maps.

AlternatingMap.sub instance

: Sub (M [⋀^ι]→ₗ[R] N')

Full source

instance sub : Sub (M [⋀^ι]→ₗ[R] N') :=
  ⟨fun f g =>
    { (f - g : MultilinearMap R (fun _ : ι => M) N') with
      map_eq_zero_of_eq' := fun v i j h hij => by
        simp [f.map_eq_zero_of_eq v h hij, g.map_eq_zero_of_eq v h hij] }⟩

Subtraction of Alternating Maps

Informal description

The space of $R$-linear alternating maps from $\iota \to M$ to $N$ has a subtraction operation.

AlternatingMap.sub_apply theorem

(m : ι → M) : (g - g₂) m = g m - g₂ m

Full source

@[simp]
theorem sub_apply (m : ι → M) : (g - g₂) m = g m - g₂ m :=
  rfl

Evaluation of Difference of Alternating Maps Equals Difference of Evaluations

Informal description

For any alternating maps $g$ and $g_2$ from $\iota \to M$ to $N'$ and any input $m : \iota \to M$, the evaluation of their difference at $m$ equals the difference of their evaluations, i.e., $(g - g_2)(m) = g(m) - g_2(m)$.

AlternatingMap.coe_sub theorem

: (↑(g - g₂) : MultilinearMap R (fun _ : ι => M) N') = g - g₂

Full source

@[norm_cast]
theorem coe_sub : (↑(g - g₂) : MultilinearMap R (fun _ : ι => M) N') = g - g₂ :=
  rfl

Coercion of Difference of Alternating Maps Equals Difference of Coercions

Informal description

The coercion of the difference of two alternating maps $g$ and $g_2$ from $M^{[\iota]} \to_R N'$ to multilinear maps equals the difference of their coercions, i.e., $\uparrow(g - g_2) = \uparrow g - \uparrow g_2$.

AlternatingMap.addCommGroup instance

: AddCommGroup (M [⋀^ι]→ₗ[R] N')

Full source

instance addCommGroup : AddCommGroup (M [⋀^ι]→ₗ[R] N') :=
  coe_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => coeFn_smul _ _) fun _ _ => coeFn_smul _ _

Additive Commutative Group Structure on Alternating Maps

Informal description

The space of $R$-linear alternating maps from $\iota \to M$ to $N'$ forms an additive commutative group under pointwise addition and negation.

AlternatingMap.distribMulAction instance

: DistribMulAction S (M [⋀^ι]→ₗ[R] N)

Full source

instance distribMulAction : DistribMulAction S (M [⋀^ι]→ₗ[R] N) where
  one_smul _ := ext fun _ => one_smul _ _
  mul_smul _ _ _ := ext fun _ => mul_smul _ _ _
  smul_zero _ := ext fun _ => smul_zero _
  smul_add _ _ _ := ext fun _ => smul_add _ _ _

Distributive Multiplicative Action on Alternating Maps

Informal description

For any commutative semiring $R$, modules $M$ and $N$ over $R$, type $\iota$, and scalar monoid $S$ acting on $N$, the space of $R$-linear alternating maps from $\iota \to M$ to $N$ forms a distributive multiplicative action over $S$.

AlternatingMap.module instance

: Module S (M [⋀^ι]→ₗ[R] N)

Full source

/-- The space of multilinear maps over an algebra over `R` is a module over `R`, for the pointwise
addition and scalar multiplication. -/
instance module : Module S (M [⋀^ι]→ₗ[R] N) where
  add_smul _ _ _ := ext fun _ => add_smul _ _ _
  zero_smul _ := ext fun _ => zero_smul _ _

Module Structure on Alternating Maps

Informal description

For any commutative semiring $R$, modules $M$ and $N$ over $R$, type $\iota$, and semiring $S$ acting on $N$, the space of $R$-linear alternating maps from $\iota \to M$ to $N$ forms a module over $S$ under pointwise addition and scalar multiplication.

AlternatingMap.noZeroSMulDivisors instance

[NoZeroSMulDivisors S N] : NoZeroSMulDivisors S (M [⋀^ι]→ₗ[R] N)

Full source

instance noZeroSMulDivisors [NoZeroSMulDivisors S N] :
    NoZeroSMulDivisors S (M [⋀^ι]→ₗ[R] N) :=
  coe_injective.noZeroSMulDivisors _ rfl coeFn_smul

No Zero Scalar Divisors in Alternating Maps

Informal description

For any scalar semigroup $S$ acting on a module $N$ over a commutative semiring $R$, if $N$ has no zero scalar divisors with respect to $S$, then the space of $R$-linear alternating maps from $\iota \to M$ to $N$ also has no zero scalar divisors with respect to $S$.

AlternatingMap.ofSubsingleton definition

[Subsingleton ι] (i : ι) : (M →ₗ[R] N) ≃ (M [⋀^ι]→ₗ[R] N)

Full source

/-- The natural equivalence between linear maps from `M` to `N`
and `1`-multilinear alternating maps from `M` to `N`. -/
@[simps!]
def ofSubsingleton [Subsingleton ι] (i : ι) : (M →ₗ[R] N) ≃ (M [⋀^ι]→ₗ[R] N) where
  toFun f := ⟨MultilinearMap.ofSubsingleton R M N i f, fun _ _ _ _ ↦ absurd (Subsingleton.elim _ _)⟩
  invFun f := (MultilinearMap.ofSubsingleton R M N i).symm f
  left_inv _ := rfl
  right_inv _ := coe_multilinearMap_injective <|
    (MultilinearMap.ofSubsingleton R M N i).apply_symm_apply _

Equivalence between linear maps and alternating maps for subsingleton index type

Informal description

Given a subsingleton index type $\iota$ (i.e., all elements of $\iota$ are equal) and an index $i \in \iota$, there is a natural equivalence between linear maps $M \to_{R} N$ and alternating maps $\bigwedge^\iota M \to_{R} N$. Specifically: - The forward direction constructs an alternating map from a linear map by extending it trivially (since all inputs are equal, the alternating property holds vacuously). - The inverse direction restricts an alternating map to its action on the $i$-th component (well-defined because $\iota$ is a subsingleton).

AlternatingMap.constOfIsEmpty definition

[IsEmpty ι] (m : N) : M [⋀^ι]→ₗ[R] N

Full source

/-- The constant map is alternating when `ι` is empty. -/
@[simps -fullyApplied]
def constOfIsEmpty [IsEmpty ι] (m : N) : M [⋀^ι]→ₗ[R] N :=
  { MultilinearMap.constOfIsEmpty R _ m with
    toFun := Function.const _ m
    map_eq_zero_of_eq' := fun _ => isEmptyElim }

Constant alternating map for empty index type

Informal description

Given a module $N$ over a commutative ring $R$ and an index type $\iota$ that is empty, the constant map that sends every element of the empty function space $\iota \to M$ to a fixed element $m \in N$ is an $R$-linear alternating map from $M^{\iota}$ to $N$. This map trivially satisfies the alternating property since there are no elements in $\iota$ to compare.

AlternatingMap.codRestrict definition

(f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h : ∀ v, f v ∈ p) : M [⋀^ι]→ₗ[R] p

Full source

/-- Restrict the codomain of an alternating map to a submodule. -/
@[simps]
def codRestrict (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h : ∀ v, f v ∈ p) :
    M [⋀^ι]→ₗ[R] p :=
  { f.toMultilinearMap.codRestrict p h with
    toFun := fun v => ⟨f v, h v⟩
    map_eq_zero_of_eq' := fun _ _ _ hv hij => Subtype.ext <| map_eq_zero_of_eq _ _ hv hij }

Codomain restriction of an alternating map to a submodule

Informal description

Given an $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to N$ and a submodule $p$ of $N$ such that $f(v) \in p$ for all $v \colon \iota \to M$, the codomain restriction of $f$ to $p$ is an $R$-linear alternating map from $M [\bigwedge^\iota]$ to $p$. This restricted map inherits the alternating property from $f$, meaning it vanishes whenever two of its arguments are equal.

LinearMap.compAlternatingMap definition

(g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι]→ₗ[R] N₂

Full source

/-- Composing an alternating map with a linear map on the left gives again an alternating map. -/
def compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι]→ₗ[R] N₂ where
  __ := g.compMultilinearMap (f : MultilinearMap R (fun _ : ι => M) N)
  map_eq_zero_of_eq' v i j h hij := by simp [f.map_eq_zero_of_eq v h hij]

Composition of a linear map with an alternating map

Informal description

Given a linear map $g : N \to_{R} N_2$ and an alternating map $f : M [\bigwedge^\iota] \to_{R} N$, the composition $g \circ f$ is an alternating map from $M [\bigwedge^\iota]$ to $N_2$. This composition preserves the alternating property, meaning it vanishes whenever two of its arguments are equal.

LinearMap.coe_compAlternatingMap theorem

(g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) : ⇑(g.compAlternatingMap f) = g ∘ f

Full source

@[simp]
theorem coe_compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :
    ⇑(g.compAlternatingMap f) = g ∘ f :=
  rfl

Composition of Linear Map with Alternating Map Preserves Function Application

Informal description

For any $R$-linear map $g \colon N \to N_2$ and any alternating map $f \colon M [\bigwedge^\iota] \to N$, the underlying function of the composition $g \circ f$ is equal to the pointwise composition of $g$ and $f$, i.e., $(g \circ f)(m) = g(f(m))$ for all $m \in \iota \to M$.

LinearMap.compAlternatingMap_apply theorem

(g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (m : ι → M) : g.compAlternatingMap f m = g (f m)

Full source

@[simp]
theorem compAlternatingMap_apply (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (m : ι → M) :
    g.compAlternatingMap f m = g (f m) :=
  rfl

Evaluation of Composition of Linear Map with Alternating Map

Informal description

Given a linear map $g \colon N \to_R N_2$ and an alternating map $f \colon M [\bigwedge^\iota] \to_R N$, the evaluation of their composition at a vector $m \colon \iota \to M$ is equal to $g$ applied to $f(m)$, i.e., $(g \circ f)(m) = g(f(m))$.

LinearMap.compAlternatingMap_zero theorem

(g : N →ₗ[R] N₂) : g.compAlternatingMap (0 : M [⋀^ι]→ₗ[R] N) = 0

Full source

@[simp]
theorem compAlternatingMap_zero (g : N →ₗ[R] N₂) :
    g.compAlternatingMap (0 : M [⋀^ι]→ₗ[R] N) = 0 :=
  AlternatingMap.ext fun _ => map_zero g

Composition with Zero Alternating Map Yields Zero

Informal description

For any $R$-linear map $g \colon N \to N_2$, the composition of $g$ with the zero alternating map from $M [\bigwedge^\iota]$ to $N$ is the zero alternating map from $M [\bigwedge^\iota]$ to $N_2$, i.e., $g \circ 0 = 0$.

LinearMap.zero_compAlternatingMap theorem

(f : M [⋀^ι]→ₗ[R] N) : (0 : N →ₗ[R] N₂).compAlternatingMap f = 0

Full source

@[simp]
theorem zero_compAlternatingMap (f : M [⋀^ι]→ₗ[R] N) :
    (0 : N →ₗ[R] N₂).compAlternatingMap f = 0 := rfl

Composition with Zero Linear Map Yields Zero Alternating Map

Informal description

For any $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to_{R} N$, the composition of the zero linear map $0 \colon N \to_{R} N_2$ with $f$ is the zero alternating map, i.e., $0 \circ f = 0$.

LinearMap.compAlternatingMap_add theorem

 (g : N →ₗ[R] N₂) (f₁ f₂ : M [⋀^ι]→ₗ[R] N) :
  g.compAlternatingMap (f₁ + f₂) = g.compAlternatingMap f₁ + g.compAlternatingMap f₂

Full source

@[simp]
theorem compAlternatingMap_add (g : N →ₗ[R] N₂) (f₁ f₂ : M [⋀^ι]→ₗ[R] N) :
    g.compAlternatingMap (f₁ + f₂) = g.compAlternatingMap f₁ + g.compAlternatingMap f₂ :=
  AlternatingMap.ext fun _ => map_add g _ _

Additivity of Composition with Sum of Alternating Maps

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be an index type. For any $R$-linear map $g : N \to_R N_2$ and any two $R$-linear alternating maps $f_1, f_2 : M [\bigwedge^\iota] \to_R N$, the composition of $g$ with the sum $f_1 + f_2$ equals the sum of the individual compositions, i.e., $g \circ (f_1 + f_2) = g \circ f_1 + g \circ f_2$.

LinearMap.add_compAlternatingMap theorem

 (g₁ g₂ : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :
  (g₁ + g₂).compAlternatingMap f = g₁.compAlternatingMap f + g₂.compAlternatingMap f

Full source

@[simp]
theorem add_compAlternatingMap (g₁ g₂ : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :
    (g₁ + g₂).compAlternatingMap f = g₁.compAlternatingMap f + g₂.compAlternatingMap f := rfl

Additivity of Composition with Alternating Maps

Informal description

For any two $R$-linear maps $g_1, g_2 \colon N \to_R N_2$ and any $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to_R N$, the composition of the sum $g_1 + g_2$ with $f$ equals the sum of the individual compositions, i.e., $(g_1 + g_2) \circ f = g_1 \circ f + g_2 \circ f$.

LinearMap.compAlternatingMap_smul theorem

 [Monoid S] [DistribMulAction S N] [DistribMulAction S N₂] [SMulCommClass R S N] [SMulCommClass R S N₂]
  [CompatibleSMul N N₂ S R] (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
  g.compAlternatingMap (s • f) = s • g.compAlternatingMap f

Full source

@[simp]
theorem compAlternatingMap_smul [Monoid S] [DistribMulAction S N] [DistribMulAction S N₂]
    [SMulCommClass R S N] [SMulCommClass R S N₂] [CompatibleSMul N N₂ S R]
    (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
    g.compAlternatingMap (s • f) = s • g.compAlternatingMap f :=
  AlternatingMap.ext fun _ => g.map_smul_of_tower _ _

Scalar Multiplication Commutes with Composition of Linear and Alternating Maps

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\iota$ be a type. Let $S$ be a monoid with distributive multiplicative actions on $N$ and $N_2$, such that the scalar multiplications of $R$ and $S$ commute on both $N$ and $N_2$. Given an $R$-linear map $g \colon N \to_R N_2$, a scalar $s \in S$, and an $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to_R N$, the composition of $g$ with the scaled alternating map $s \cdot f$ equals the scaling of the composition $g \circ f$ by $s$, i.e., $g \circ (s \cdot f) = s \cdot (g \circ f)$.

LinearMap.smul_compAlternatingMap theorem

 [Monoid S] [DistribMulAction S N₂] [SMulCommClass R S N₂] (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
  (s • g).compAlternatingMap f = s • g.compAlternatingMap f

Full source

@[simp]
theorem smul_compAlternatingMap [Monoid S] [DistribMulAction S N₂] [SMulCommClass R S N₂]
    (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
    (s • g).compAlternatingMap f = s • g.compAlternatingMap f := rfl

Scalar Multiplication Commutes with Composition of Linear and Alternating Maps

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\iota$ be a type. Given a scalar monoid $S$ acting on $N_2$ with $R$ and $S$ commuting, for any linear map $g : N \to_R N_2$, scalar $s \in S$, and alternating map $f : M [\bigwedge^\iota] \to_R N$, the composition of the scaled linear map $s \cdot g$ with $f$ equals the scaling of the composition $g \circ f$ by $s$, i.e., $(s \cdot g) \circ f = s \cdot (g \circ f)$.

LinearMap.compAlternatingMapₗ definition

 [Semiring S] [Module S N] [Module S N₂] [SMulCommClass R S N] [SMulCommClass R S N₂]
  [LinearMap.CompatibleSMul N N₂ S R] (g : N →ₗ[R] N₂) : (M [⋀^ι]→ₗ[R] N) →ₗ[S] (M [⋀^ι]→ₗ[R] N₂)

Full source

/-- `LinearMap.compAlternatingMap` as an `S`-linear map. -/
@[simps]
def compAlternatingMapₗ [Semiring S] [Module S N] [Module S N₂]
    [SMulCommClass R S N] [SMulCommClass R S N₂] [LinearMap.CompatibleSMul N N₂ S R]
    (g : N →ₗ[R] N₂) :
    (M [⋀^ι]→ₗ[R] N) →ₗ[S] (M [⋀^ι]→ₗ[R] N₂) where
  toFun := g.compAlternatingMap
  map_add' := g.compAlternatingMap_add
  map_smul' := g.compAlternatingMap_smul

$S$-linear map induced by composition with a linear map on alternating maps

Informal description

Given a commutative semiring $R$, modules $M$, $N$, and $N_2$ over $R$, a type $\iota$, and a semiring $S$ with compatible scalar multiplication actions on $N$ and $N_2$, the function maps a linear map $g \colon N \to_R N_2$ to an $S$-linear map from the space of $R$-linear alternating maps $M [\bigwedge^\iota] \to_R N$ to the space of $R$-linear alternating maps $M [\bigwedge^\iota] \to_R N_2$. This is achieved by composing $g$ with an alternating map, preserving the $S$-linear structure.

LinearMap.smulRight_eq_comp theorem

 {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂]
  (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) : f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f

Full source

theorem smulRight_eq_comp {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁]
    [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :
    f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f :=
  rfl

Equality between scalar multiplication and composition of alternating maps: $f.\mathrm{smulRight}\, z = (\mathrm{id}.\mathrm{smulRight}\, z) \circ f$

Informal description

Let $R$ be a commutative semiring, $M₁$ and $M₂$ be additive commutative monoids with $R$-module structures, and $\iota$ be a type. For any $R$-linear alternating map $f: M₁ [\bigwedge^\iota] \to_R R$ and any element $z \in M₂$, the alternating map $f.\mathrm{smulRight}\, z$ is equal to the composition of $f$ with the linear map $\mathrm{id}.\mathrm{smulRight}\, z$, where $\mathrm{id}$ is the identity linear map on $R$.

LinearMap.subtype_compAlternatingMap_codRestrict theorem

(f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h) : p.subtype.compAlternatingMap (f.codRestrict p h) = f

Full source

@[simp]
theorem subtype_compAlternatingMap_codRestrict (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N)
    (h) : p.subtype.compAlternatingMap (f.codRestrict p h) = f :=
  AlternatingMap.ext fun _ => rfl

Subtype Composition with Codomain-Restricted Alternating Map Equals Original Map

Informal description

Let $f \colon M [\bigwedge^\iota] \to_R N$ be an $R$-linear alternating map and $p$ be a submodule of $N$ such that $f(v) \in p$ for all $v \colon \iota \to M$. Then the composition of the submodule inclusion map $p \hookrightarrow N$ with the codomain-restricted alternating map $f \colon M [\bigwedge^\iota] \to_R p$ equals the original map $f$.

LinearMap.compAlternatingMap_codRestrict theorem

 (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N₂) (h) :
  (g.codRestrict p h).compAlternatingMap f = (g.compAlternatingMap f).codRestrict p fun v => h (f v)

Full source

@[simp]
theorem compAlternatingMap_codRestrict (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N)
    (p : Submodule R N₂) (h) :
    (g.codRestrict p h).compAlternatingMap f =
      (g.compAlternatingMap f).codRestrict p fun v => h (f v) :=
  AlternatingMap.ext fun _ => rfl

Composition of Codomain-Restricted Linear Map with Alternating Map Equals Codomain-Restricted Composition

Informal description

Let $R$ be a commutative ring, $M$, $N$, and $N_2$ be $R$-modules, and $\iota$ be an index type. Given an $R$-linear map $g \colon N \to N_2$, an $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to N$, and a submodule $p$ of $N_2$ such that $g(f(v)) \in p$ for all $v \colon \iota \to M$, the composition of the codomain-restricted map $g|_{p}$ with $f$ is equal to the codomain restriction of $g \circ f$ to $p$. That is, $$(g|_{p}) \circ f = (g \circ f)|_{p}.$$

AlternatingMap.compLinearMap definition

(f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) : M₂ [⋀^ι]→ₗ[R] N

Full source

/-- Composing an alternating map with the same linear map on each argument gives again an
alternating map. -/
def compLinearMap (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) : M₂ [⋀^ι]→ₗ[R] N :=
  { (f : MultilinearMap R (fun _ : ι => M) N).compLinearMap fun _ => g with
    map_eq_zero_of_eq' := fun _ _ _ h hij => f.map_eq_zero_of_eq _ (LinearMap.congr_arg h) hij }

Composition of an alternating map with a linear map

Informal description

Given an $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to N$ and an $R$-linear map $g \colon M_2 \to M$, the composition $f \circ (g \circ \cdot)$ is an $R$-linear alternating map from $M_2 [\bigwedge^\iota] \to N$. Here, the notation $M [\bigwedge^\iota] \to N$ denotes the space of alternating multilinear maps from $\iota \to M$ to $N$.

AlternatingMap.coe_compLinearMap theorem

(f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) : ⇑(f.compLinearMap g) = f ∘ (g ∘ ·)

Full source

theorem coe_compLinearMap (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :
    ⇑(f.compLinearMap g) = f ∘ (g ∘ ·) :=
  rfl

Composition of Alternating Map with Linear Map Preserves Underlying Function

Informal description

Let $R$ be a commutative ring, $M$, $M_2$, and $N$ be $R$-modules, and $\iota$ be an index type. Given an $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to N$ and an $R$-linear map $g \colon M_2 \to M$, the underlying function of the composition $f \circ g$ is equal to the composition of $f$ with the post-composition by $g$. In other words, for any $v \colon \iota \to M_2$, we have $(f \circ g)(v) = f(g \circ v)$.

AlternatingMap.compLinearMap_apply theorem

(f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) (v : ι → M₂) : f.compLinearMap g v = f fun i => g (v i)

Full source

@[simp]
theorem compLinearMap_apply (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) (v : ι → M₂) :
    f.compLinearMap g v = f fun i => g (v i) :=
  rfl

Evaluation of Composition of Alternating Map with Linear Map

Informal description

Let $R$ be a commutative ring, and let $M$, $M_2$, and $N$ be $R$-modules. Given an $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to N$ and an $R$-linear map $g \colon M_2 \to M$, the evaluation of the composition $f \circ g$ at a vector $v \colon \iota \to M_2$ is equal to $f$ evaluated at the vector obtained by applying $g$ componentwise to $v$, i.e., $$(f \circ g)(v) = f(g \circ v).$$

AlternatingMap.compLinearMap_assoc theorem

 (f : M [⋀^ι]→ₗ[R] N) (g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂) :
  (f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂)

Full source

/-- Composing an alternating map twice with the same linear map in each argument is
the same as composing with their composition. -/
theorem compLinearMap_assoc (f : M [⋀^ι]→ₗ[R] N) (g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂) :
    (f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂) :=
  rfl

Associativity of Composition for Alternating Maps and Linear Maps

Informal description

Let $R$ be a commutative ring, and let $M$, $M_2$, $M_3$, and $N$ be $R$-modules. Given an $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to N$ and $R$-linear maps $g_1 \colon M_2 \to M$ and $g_2 \colon M_3 \to M_2$, the composition of $f$ with $g_1$ followed by $g_2$ is equal to the composition of $f$ with the composite map $g_1 \circ g_2$. In other words, $$(f \circ g_1) \circ g_2 = f \circ (g_1 \circ g_2).$$

AlternatingMap.zero_compLinearMap theorem

(g : M₂ →ₗ[R] M) : (0 : M [⋀^ι]→ₗ[R] N).compLinearMap g = 0

Full source

@[simp]
theorem zero_compLinearMap (g : M₂ →ₗ[R] M) : (0 : M [⋀^ι]→ₗ[R] N).compLinearMap g = 0 := by
  ext
  simp only [compLinearMap_apply, zero_apply]

Composition of Zero Alternating Map with Linear Map Yields Zero Map

Informal description

For any $R$-linear map $g \colon M_2 \to M$, the composition of the zero alternating map $0 \colon M [\bigwedge^\iota] \to N$ with $g$ is equal to the zero alternating map from $M_2 [\bigwedge^\iota] \to N$, i.e., $$0 \circ g = 0.$$

AlternatingMap.add_compLinearMap theorem

 (f₁ f₂ : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) : (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

Full source

@[simp]
theorem add_compLinearMap (f₁ f₂ : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :
    (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g := by
  ext
  simp only [compLinearMap_apply, add_apply]

Linearity of Composition with Sum of Alternating Maps

Informal description

Let $R$ be a commutative ring, and let $M$, $M_2$, and $N$ be $R$-modules. For any two $R$-linear alternating maps $f_1, f_2 \colon M [\bigwedge^\iota] \to N$ and any $R$-linear map $g \colon M_2 \to M$, the composition of the sum $f_1 + f_2$ with $g$ is equal to the sum of the individual compositions, i.e., $$(f_1 + f_2) \circ g = (f_1 \circ g) + (f_2 \circ g).$$

AlternatingMap.compLinearMap_zero theorem

[Nonempty ι] (f : M [⋀^ι]→ₗ[R] N) : f.compLinearMap (0 : M₂ →ₗ[R] M) = 0

Full source

@[simp]
theorem compLinearMap_zero [Nonempty ι] (f : M [⋀^ι]→ₗ[R] N) :
    f.compLinearMap (0 : M₂ →ₗ[R] M) = 0 := by
  ext
  simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]

Composition of Alternating Map with Zero Linear Map Yields Zero Map

Informal description

For any nonempty type $\iota$ and any $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to N$, the composition of $f$ with the zero linear map $0 \colon M_2 \to M$ is the zero alternating map, i.e., $f \circ 0 = 0$.

AlternatingMap.compLinearMap_id theorem

(f : M [⋀^ι]→ₗ[R] N) : f.compLinearMap LinearMap.id = f

Full source

/-- Composing an alternating map with the identity linear map in each argument. -/
@[simp]
theorem compLinearMap_id (f : M [⋀^ι]→ₗ[R] N) : f.compLinearMap LinearMap.id = f :=
  ext fun _ => rfl

Composition with Identity Preserves Alternating Map

Informal description

For any $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to N$, the composition of $f$ with the identity linear map $\text{id} \colon M \to M$ is equal to $f$ itself, i.e., $f \circ \text{id} = f$.

AlternatingMap.compLinearMap_injective theorem

 (f : M₂ →ₗ[R] M) (hf : Function.Surjective f) : Function.Injective fun g : M [⋀^ι]→ₗ[R] N => g.compLinearMap f

Full source

/-- Composing with a surjective linear map is injective. -/
theorem compLinearMap_injective (f : M₂ →ₗ[R] M) (hf : Function.Surjective f) :
    Function.Injective fun g : M [⋀^ι]→ₗ[R] N => g.compLinearMap f := fun g₁ g₂ h =>
  ext fun x => by
    simpa [Function.surjInv_eq hf] using AlternatingMap.ext_iff.mp h (Function.surjInvFunction.surjInv hf ∘ x)

Injectivity of Alternating Map Composition with a Surjective Linear Map

Informal description

Let $R$ be a commutative ring, and let $M$, $M_2$, and $N$ be $R$-modules. Given an $R$-linear surjective map $f \colon M_2 \to M$, the composition map \[ g \mapsto g \circ f \] from the space of $R$-linear alternating maps $\bigwedge^\iota M \to N$ to the space of $R$-linear alternating maps $\bigwedge^\iota M_2 \to N$ is injective.

AlternatingMap.compLinearMap_inj theorem

 (f : M₂ →ₗ[R] M) (hf : Function.Surjective f) (g₁ g₂ : M [⋀^ι]→ₗ[R] N) :
  g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂

Full source

theorem compLinearMap_inj (f : M₂ →ₗ[R] M) (hf : Function.Surjective f)
    (g₁ g₂ : M [⋀^ι]→ₗ[R] N) : g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂ :=
  (compLinearMap_injective _ hf).eq_iff

Injectivity of Alternating Map Composition with Surjective Linear Map

Informal description

Let $R$ be a commutative ring, $M$, $M_2$, and $N$ be $R$-modules, and $f \colon M_2 \to M$ be a surjective $R$-linear map. For any two $R$-linear alternating maps $g_1, g_2 \colon \bigwedge^\iota M \to N$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

AlternatingMap.domLCongr definition

(e : M ≃ₗ[R] M₂) : M [⋀^ι]→ₗ[R] N ≃ₗ[S] (M₂ [⋀^ι]→ₗ[R] N)

Full source

/-- Construct a linear equivalence between maps from a linear equivalence between domains. -/
@[simps apply]
def domLCongr (e : M ≃ₗ[R] M₂) : M [⋀^ι]→ₗ[R] NM [⋀^ι]→ₗ[R] N ≃ₗ[S] (M₂ [⋀^ι]→ₗ[R] N) where
  toFun f := f.compLinearMap e.symm
  invFun g := g.compLinearMap e
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv f := AlternatingMap.ext fun _ => f.congr_arg <| funext fun _ => e.symm_apply_apply _
  right_inv f := AlternatingMap.ext fun _ => f.congr_arg <| funext fun _ => e.apply_symm_apply _

Linear equivalence of alternating maps induced by a module equivalence

Informal description

Given a linear equivalence $e \colon M \simeq_R M_2$ between $R$-modules $M$ and $M_2$, there is an induced $S$-linear equivalence between the spaces of $R$-linear alternating maps from $\iota \to M$ to $N$ and from $\iota \to M_2$ to $N$. This equivalence is constructed by precomposing with $e^{-1}$ in one direction and with $e$ in the other.

AlternatingMap.domLCongr_refl theorem

: domLCongr R N ι S (LinearEquiv.refl R M) = LinearEquiv.refl S _

Full source

@[simp]
theorem domLCongr_refl : domLCongr R N ι S (LinearEquiv.refl R M) = LinearEquiv.refl S _ :=
  LinearEquiv.ext fun _ => AlternatingMap.ext fun _ => rfl

Identity Linear Equivalence Induces Identity on Alternating Maps

Informal description

Given a commutative ring $R$, modules $M$ and $N$ over $R$, a type $\iota$, and a semiring $S$ acting on $N$, the linear equivalence `domLCongr` induced by the identity linear equivalence $\text{refl}_R M$ on $M$ is equal to the identity linear equivalence $\text{refl}_S$ on the space of $R$-linear alternating maps from $\iota \to M$ to $N$.

AlternatingMap.domLCongr_symm theorem

(e : M ≃ₗ[R] M₂) : (domLCongr R N ι S e).symm = domLCongr R N ι S e.symm

Full source

@[simp]
theorem domLCongr_symm (e : M ≃ₗ[R] M₂) : (domLCongr R N ι S e).symm = domLCongr R N ι S e.symm :=
  rfl

Symmetry of Linear Equivalence on Alternating Maps

Informal description

Given a linear equivalence $e \colon M \simeq_R M_2$ between $R$-modules $M$ and $M_2$, the symmetry of the induced linear equivalence on alternating maps states that the inverse of the equivalence $\text{domLCongr}(e)$ is equal to $\text{domLCongr}(e^{-1})$. In other words, $(\text{domLCongr}(e))^{-1} = \text{domLCongr}(e^{-1})$.

AlternatingMap.domLCongr_trans theorem

 (e : M ≃ₗ[R] M₂) (f : M₂ ≃ₗ[R] M₃) : (domLCongr R N ι S e).trans (domLCongr R N ι S f) = domLCongr R N ι S (e.trans f)

Full source

theorem domLCongr_trans (e : M ≃ₗ[R] M₂) (f : M₂ ≃ₗ[R] M₃) :
    (domLCongr R N ι S e).trans (domLCongr R N ι S f) = domLCongr R N ι S (e.trans f) :=
  rfl

Composition of Linear Equivalences on Alternating Maps

Informal description

Given $R$-linear equivalences $e \colon M \simeq_R M_2$ and $f \colon M_2 \simeq_R M_3$, the composition of the induced linear equivalences $\text{domLCongr}(e)$ and $\text{domLCongr}(f)$ on spaces of alternating maps is equal to the linear equivalence induced by the composition $e \circ f$. That is, \[ \text{domLCongr}(e) \circ \text{domLCongr}(f) = \text{domLCongr}(e \circ f). \]

AlternatingMap.compLinearEquiv_eq_zero_iff theorem

(f : M [⋀^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M) : f.compLinearMap (g : M₂ →ₗ[R] M) = 0 ↔ f = 0

Full source

/-- Composing an alternating map with the same linear equiv on each argument gives the zero map
if and only if the alternating map is the zero map. -/
@[simp]
theorem compLinearEquiv_eq_zero_iff (f : M [⋀^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M) :
    f.compLinearMap (g : M₂ →ₗ[R] M) = 0 ↔ f = 0 :=
  (domLCongr R N ι ℕ g.symm).map_eq_zero_iff

Composition with Linear Equivalence Yields Zero Map if and Only if Original Map is Zero

Informal description

Let $f \colon M [\bigwedge^\iota] \to_{R} N$ be an $R$-linear alternating map and let $g \colon M_2 \simeq_R M$ be a linear equivalence between $R$-modules $M_2$ and $M$. Then the composition $f \circ g$ (where $g$ is viewed as a linear map) is the zero map if and only if $f$ is the zero map.

AlternatingMap.map_update_sum theorem

 {α : Type*} [DecidableEq ι] (t : Finset α) (i : ι) (g : α → M) (m : ι → M) :
  f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a))

Full source

theorem map_update_sum {α : Type*} [DecidableEq ι] (t : Finset α) (i : ι) (g : α → M) (m : ι → M) :
    f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a)) :=
  f.toMultilinearMap.map_update_sum t i g m

Linearity of Alternating Maps under Finite Sum Updates

Informal description

Let $f$ be an $R$-linear alternating map from $\iota \to M$ to $N$, and let $\alpha$ be a type with decidable equality on $\iota$. For any finite set $t \subseteq \alpha$, index $i \in \iota$, function $g \colon \alpha \to M$, and vector $m \colon \iota \to M$, the following equality holds: \[ f\left(\text{update } m \, i \left(\sum_{a \in t} g(a)\right)\right) = \sum_{a \in t} f\left(\text{update } m \, i \, (g(a))\right), \] where $\text{update } m \, i \, v$ denotes the function that coincides with $m$ everywhere except at $i$, where it takes the value $v$.

AlternatingMap.map_update_self theorem

[DecidableEq ι] {i j : ι} (hij : i ≠ j) : f (Function.update v i (v j)) = 0

Full source

theorem map_update_self [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
    f (Function.update v i (v j)) = 0 :=
  f.map_eq_zero_of_eq _ (by rw [Function.update_self, Function.update_of_ne hij.symm]) hij

Alternating Maps Vanish on Self-Updated Arguments

Informal description

Let $f$ be an $R$-linear alternating map from $\iota \to M$ to $N$, and let $\iota$ have decidable equality. For any function $v : \iota \to M$ and any distinct indices $i, j \in \iota$ with $i \neq j$, we have $f(\text{update } v \, i \, (v j)) = 0$, where $\text{update } v \, i \, (v j)$ denotes the function that coincides with $v$ everywhere except at $i$, where it takes the value $v(j)$.

AlternatingMap.map_update_update theorem

[DecidableEq ι] {i j : ι} (hij : i ≠ j) (m : M) : f (Function.update (Function.update v i m) j m) = 0

Full source

theorem map_update_update [DecidableEq ι] {i j : ι} (hij : i ≠ j) (m : M) :
    f (Function.update (Function.update v i m) j m) = 0 :=
  f.map_eq_zero_of_eq _
    (by rw [Function.update_self, Function.update_of_ne hij, Function.update_self]) hij

Alternating Maps Vanish on Double-Updated Equal Arguments

Informal description

Let $f$ be an $R$-linear alternating map from $\iota \to M$ to $N$, and let $\iota$ have decidable equality. For any function $v : \iota \to M$, any distinct indices $i, j \in \iota$ with $i \neq j$, and any element $m \in M$, we have: \[ f(\text{update } (\text{update } v \, i \, m) \, j \, m) = 0, \] where $\text{update } v \, i \, m$ denotes the function that coincides with $v$ everywhere except at $i$, where it takes the value $m$.

AlternatingMap.map_swap_add theorem

[DecidableEq ι] {i j : ι} (hij : i ≠ j) : f (v ∘ Equiv.swap i j) + f v = 0

Full source

theorem map_swap_add [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
    f (v ∘ Equiv.swap i j) + f v = 0 := by
  rw [Equiv.comp_swap_eq_update]
  convert f.map_update_update v hij (v i + v j)
  simp [f.map_update_self _ hij, f.map_update_self _ hij.symm,
    Function.update_comm hij (v i + v j) (v _) v, Function.update_comm hij.symm (v i) (v i) v]

Alternating Map Property: $f(v \circ \mathrm{swap}(i,j)) + f(v) = 0$ for Distinct Indices

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be an index type with decidable equality. For any $R$-linear alternating map $f : M [\bigwedge^\iota] \to_{R} N$, any function $v : \iota \to M$, and any distinct indices $i, j \in \iota$ with $i \neq j$, we have: \[ f(v \circ \mathrm{swap}(i,j)) + f(v) = 0, \] where $\mathrm{swap}(i,j)$ denotes the permutation that swaps $i$ and $j$.

AlternatingMap.map_add_swap theorem

[DecidableEq ι] {i j : ι} (hij : i ≠ j) : f v + f (v ∘ Equiv.swap i j) = 0

Full source

theorem map_add_swap [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
    f v + f (v ∘ Equiv.swap i j) = 0 := by
  rw [add_comm]
  exact f.map_swap_add v hij

Alternating Map Property: $f(v) + f(v \circ \mathrm{swap}(i,j)) = 0$ for Distinct Indices

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be an index type with decidable equality. For any $R$-linear alternating map $f : M [\bigwedge^\iota] \to_{R} N$, any function $v : \iota \to M$, and any distinct indices $i, j \in \iota$ with $i \neq j$, we have: \[ f(v) + f(v \circ \mathrm{swap}(i,j)) = 0, \] where $\mathrm{swap}(i,j)$ denotes the permutation that swaps $i$ and $j$.

AlternatingMap.map_swap theorem

[DecidableEq ι] {i j : ι} (hij : i ≠ j) : g (v ∘ Equiv.swap i j) = -g v

Full source

theorem map_swap [DecidableEq ι] {i j : ι} (hij : i ≠ j) : g (v ∘ Equiv.swap i j) = -g v :=
  eq_neg_of_add_eq_zero_left <| g.map_swap_add v hij

Alternating Map Property: $g(v \circ \mathrm{swap}(i,j)) = -g(v)$ for Distinct Indices

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be an index type with decidable equality. For any $R$-linear alternating map $g : M [\bigwedge^\iota] \to_{R} N$, any function $v : \iota \to M$, and any distinct indices $i, j \in \iota$ with $i \neq j$, we have: \[ g(v \circ \mathrm{swap}(i,j)) = -g(v), \] where $\mathrm{swap}(i,j)$ denotes the permutation that swaps $i$ and $j$.

AlternatingMap.map_perm theorem

[DecidableEq ι] [Fintype ι] (v : ι → M) (σ : Equiv.Perm ι) : g (v ∘ σ) = Equiv.Perm.sign σ • g v

Full source

theorem map_perm [DecidableEq ι] [Fintype ι] (v : ι → M) (σ : Equiv.Perm ι) :
    g (v ∘ σ) = Equiv.Perm.sign σ • g v := by
  induction σ using Equiv.Perm.swap_induction_on' with
  | one => simp
  | mul_swap s x y hxy hI => simp_all [← Function.comp_assoc, g.map_swap]

Alternating Map Behavior under Permutation: $g(v \circ \sigma) = \text{sign}(\sigma) \cdot g(v)$

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be a finite index type with decidable equality. For any $R$-linear alternating map $g : M [\bigwedge^\iota] \to_{R} N$, any function $v : \iota \to M$, and any permutation $\sigma$ of $\iota$, we have: \[ g(v \circ \sigma) = \text{sign}(\sigma) \cdot g(v), \] where $\text{sign}(\sigma)$ denotes the sign of the permutation $\sigma$ (which is $1$ for even permutations and $-1$ for odd permutations), and $\cdot$ denotes the scalar multiplication in $N$.

AlternatingMap.map_congr_perm theorem

[DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) : g v = Equiv.Perm.sign σ • g (v ∘ σ)

Full source

theorem map_congr_perm [DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) :
    g v = Equiv.Perm.sign σ • g (v ∘ σ) := by
  rw [g.map_perm, smul_smul]
  simp

Alternating Map Invariance under Permutation: $g(v) = \text{sign}(\sigma) \cdot g(v \circ \sigma)$

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\iota$ be a finite index type with decidable equality. For any $R$-linear alternating map $g : M [\bigwedge^\iota] \to_{R} N$, any function $v : \iota \to M$, and any permutation $\sigma$ of $\iota$, we have: \[ g(v) = \text{sign}(\sigma) \cdot g(v \circ \sigma), \] where $\text{sign}(\sigma)$ denotes the sign of the permutation $\sigma$ (which is $1$ for even permutations and $-1$ for odd permutations), and $\cdot$ denotes the scalar multiplication in $N$.

AlternatingMap.domDomCongr definition

(σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι']→ₗ[R] N

Full source

/-- Transfer the arguments to a map along an equivalence between argument indices.

This is the alternating version of `MultilinearMap.domDomCongr`. -/
@[simps]
def domDomCongr (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι']→ₗ[R] N :=
  { f.toMultilinearMap.domDomCongr σ with
    toFun := fun v => f (v ∘ σ)
    map_eq_zero_of_eq' := fun v i j hv hij =>
      f.map_eq_zero_of_eq (v ∘ σ) (i := σ.symm i) (j := σ.symm j)
        (by simpa using hv) (σ.symm.injective.ne hij) }

Alternating Map Reindexing via Equivalence

Informal description

Given an equivalence $\sigma : \iota \simeq \iota'$ between index types and an $R$-linear alternating map $f : M [\bigwedge^\iota] \to_{R} N$, the operation `domDomCongr` constructs a new alternating map $M [\bigwedge^{\iota'}] \to_{R} N$ by precomposing the input with $\sigma$. Specifically, for any $v : \iota' \to M$, the new map evaluates to $f(v \circ \sigma)$. This operation preserves the alternating property: if two inputs to the new map are equal, the output is zero.

AlternatingMap.domDomCongr_refl theorem

(f : M [⋀^ι]→ₗ[R] N) : f.domDomCongr (Equiv.refl ι) = f

Full source

@[simp]
theorem domDomCongr_refl (f : M [⋀^ι]→ₗ[R] N) : f.domDomCongr (Equiv.refl ι) = f := rfl

Reindexing by Identity Preserves Alternating Map

Informal description

For any $R$-linear alternating map $f : M [\bigwedge^\iota] \to_{R} N$, reindexing the domain by the identity equivalence $\text{refl}_\iota : \iota \simeq \iota$ leaves the map unchanged, i.e., $f.\text{domDomCongr}(\text{refl}_\iota) = f$.

AlternatingMap.domDomCongr_trans theorem

 (σ₁ : ι ≃ ι') (σ₂ : ι' ≃ ι'') (f : M [⋀^ι]→ₗ[R] N) : f.domDomCongr (σ₁.trans σ₂) = (f.domDomCongr σ₁).domDomCongr σ₂

Full source

theorem domDomCongr_trans (σ₁ : ι ≃ ι') (σ₂ : ι' ≃ ι'') (f : M [⋀^ι]→ₗ[R] N) :
    f.domDomCongr (σ₁.trans σ₂) = (f.domDomCongr σ₁).domDomCongr σ₂ :=
  rfl

Composition of Reindexings for Alternating Maps

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\iota$, $\iota'$, $\iota''$ be types. For any equivalences $\sigma_1 : \iota \simeq \iota'$ and $\sigma_2 : \iota' \simeq \iota''$, and any $R$-linear alternating map $f : M [\bigwedge^\iota] \to_{R} N$, the reindexing of $f$ via the composition $\sigma_1 \circ \sigma_2$ is equal to the reindexing of $f.\text{domDomCongr}(\sigma_1)$ via $\sigma_2$. That is, $$f.\text{domDomCongr}(\sigma_1 \circ \sigma_2) = (f.\text{domDomCongr}(\sigma_1)).\text{domDomCongr}(\sigma_2).$$

AlternatingMap.domDomCongr_zero theorem

(σ : ι ≃ ι') : (0 : M [⋀^ι]→ₗ[R] N).domDomCongr σ = 0

Full source

@[simp]
theorem domDomCongr_zero (σ : ι ≃ ι') : (0 : M [⋀^ι]→ₗ[R] N).domDomCongr σ = 0 :=
  rfl

Reindexing Preserves the Zero Alternating Map

Informal description

For any equivalence $\sigma : \iota \simeq \iota'$ between index types, the reindexing of the zero alternating map via $\sigma$ is equal to the zero alternating map. That is, $(0 : M [\bigwedge^\iota] \to_{R} N).\text{domDomCongr} \sigma = 0$.

AlternatingMap.domDomCongr_add theorem

(σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) : (f + g).domDomCongr σ = f.domDomCongr σ + g.domDomCongr σ

Full source

@[simp]
theorem domDomCongr_add (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) :
    (f + g).domDomCongr σ = f.domDomCongr σ + g.domDomCongr σ :=
  rfl

Additivity of Alternating Map Reindexing

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\iota$, $\iota'$ be types. For any equivalence $\sigma : \iota \simeq \iota'$ and any $R$-linear alternating maps $f, g : M [\bigwedge^\iota] \to_{R} N$, the reindexing of the sum $f + g$ via $\sigma$ is equal to the sum of the reindexed maps: $$(f + g).\text{domDomCongr} \sigma = f.\text{domDomCongr} \sigma + g.\text{domDomCongr} \sigma.$$

AlternatingMap.domDomCongr_smul theorem

 {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (σ : ι ≃ ι') (c : S) (f : M [⋀^ι]→ₗ[R] N) :
  (c • f).domDomCongr σ = c • f.domDomCongr σ

Full source

@[simp]
theorem domDomCongr_smul {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N]
    (σ : ι ≃ ι') (c : S) (f : M [⋀^ι]→ₗ[R] N) :
    (c • f).domDomCongr σ = c • f.domDomCongr σ :=
  rfl

Scalar Multiplication Commutes with Alternating Map Reindexing

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\iota$ be a type. Given a monoid $S$ acting distributively on $N$ with $R$ and $S$ having commuting scalar actions, for any equivalence $\sigma : \iota \simeq \iota'$, scalar $c \in S$, and $R$-linear alternating map $f : M [\bigwedge^\iota] \to_{R} N$, we have $$(c \cdot f).\text{domDomCongr} \sigma = c \cdot (f.\text{domDomCongr} \sigma).$$

AlternatingMap.domDomCongrEquiv definition

(σ : ι ≃ ι') : M [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N

Full source

/-- `AlternatingMap.domDomCongr` as an equivalence.

This is declared separately because it does not work with dot notation. -/
@[simps apply symm_apply]
def domDomCongrEquiv (σ : ι ≃ ι') : M [⋀^ι]→ₗ[R] NM [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N where
  toFun := domDomCongr σ
  invFun := domDomCongr σ.symm
  left_inv f := by
    ext
    simp [Function.comp_def]
  right_inv m := by
    ext
    simp [Function.comp_def]
  map_add' := domDomCongr_add σ

Additive equivalence of alternating maps under reindexing

Informal description

Given a commutative semiring $R$, $R$-modules $M$ and $N$, and an equivalence $\sigma : \iota \simeq \iota'$ between index types, the operation `domDomCongrEquiv` defines an additive equivalence between the space of $R$-linear alternating maps $M [\bigwedge^\iota] \to_{R} N$ and $M [\bigwedge^{\iota'}] \to_{R} N$. This equivalence is constructed by reindexing the input via $\sigma$, with the inverse operation given by reindexing via $\sigma^{-1}$. The equivalence preserves addition, meaning that for any two alternating maps $f$ and $g$, we have $$(f + g).\text{domDomCongr} \sigma = f.\text{domDomCongr} \sigma + g.\text{domDomCongr} \sigma.$$

AlternatingMap.domDomCongrₗ definition

(σ : ι ≃ ι') : M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι']→ₗ[R] N

Full source

/-- `AlternatingMap.domDomCongr` as a linear equivalence. -/
@[simps apply symm_apply]
def domDomCongrₗ (σ : ι ≃ ι') : M [⋀^ι]→ₗ[R] NM [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι']→ₗ[R] N where
  toFun := domDomCongr σ
  invFun := domDomCongr σ.symm
  left_inv f := by ext; simp [Function.comp_def]
  right_inv m := by ext; simp [Function.comp_def]
  map_add' := domDomCongr_add σ
  map_smul' := domDomCongr_smul σ

Linear Equivalence of Alternating Maps under Reindexing

Informal description

Given a commutative semiring $R$, $R$-modules $M$ and $N$, a semiring $S$ acting on $N$ with commuting $R$- and $S$-actions, and an equivalence $\sigma : \iota \simeq \iota'$ between index types, the operation `domDomCongrₗ` defines a linear equivalence between the space of $R$-linear alternating maps $M [\bigwedge^\iota] \to_{R} N$ and $M [\bigwedge^{\iota'}] \to_{R} N$. This equivalence is constructed by reindexing the input via $\sigma$, with the inverse operation given by reindexing via $\sigma^{-1}$. The equivalence preserves both addition and scalar multiplication, meaning that for any two alternating maps $f$ and $g$ and scalar $c \in S$, we have $$(f + g).\text{domDomCongr} \sigma = f.\text{domDomCongr} \sigma + g.\text{domDomCongr} \sigma$$ and $$(c \cdot f).\text{domDomCongr} \sigma = c \cdot (f.\text{domDomCongr} \sigma).$$

AlternatingMap.domDomCongrₗ_refl theorem

: (domDomCongrₗ S (Equiv.refl ι) : M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι]→ₗ[R] N) = LinearEquiv.refl _ _

Full source

@[simp]
theorem domDomCongrₗ_refl :
    (domDomCongrₗ S (Equiv.refl ι) : M [⋀^ι]→ₗ[R] NM [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι]→ₗ[R] N) =
      LinearEquiv.refl _ _ :=
  rfl

Identity Reindexing Yields Identity Linear Equivalence for Alternating Maps

Informal description

For any commutative semiring $R$, $R$-modules $M$ and $N$, and semiring $S$ acting on $N$, the linear equivalence obtained by reindexing the arguments of an alternating map via the identity equivalence $\text{Equiv.refl } \iota$ is equal to the identity linear equivalence on the space of $R$-linear alternating maps $M [\bigwedge^\iota] \to_{R} N$.

AlternatingMap.domDomCongrₗ_toAddEquiv theorem

 (σ : ι ≃ ι') : (↑(domDomCongrₗ S σ : M [⋀^ι]→ₗ[R] N ≃ₗ[S] _) : M [⋀^ι]→ₗ[R] N ≃+ _) = domDomCongrEquiv σ

Full source

@[simp]
theorem domDomCongrₗ_toAddEquiv (σ : ι ≃ ι') :
    (↑(domDomCongrₗ S σ : M [⋀^ι]→ₗ[R] NM [⋀^ι]→ₗ[R] N ≃ₗ[S] _) : M [⋀^ι]→ₗ[R] NM [⋀^ι]→ₗ[R] N ≃+ _) =
      domDomCongrEquiv σ :=
  rfl

Additive Equivalence Underlying Linear Equivalence of Reindexed Alternating Maps

Informal description

For any commutative semiring $R$, $R$-modules $M$ and $N$, semiring $S$ acting on $N$ with commuting $R$- and $S$-actions, and equivalence $\sigma : \iota \simeq \iota'$ between index types, the underlying additive equivalence of the linear equivalence $\mathrm{domDomCongr}_S\,\sigma$ between spaces of $R$-linear alternating maps is equal to the additive equivalence $\mathrm{domDomCongrEquiv}\,\sigma$.

AlternatingMap.domDomCongr_eq_iff theorem

(σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) : f.domDomCongr σ = g.domDomCongr σ ↔ f = g

Full source

/-- The results of applying `domDomCongr` to two maps are equal if and only if those maps are. -/
@[simp]
theorem domDomCongr_eq_iff (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) :
    f.domDomCongr σ = g.domDomCongr σ ↔ f = g :=
  (domDomCongrEquiv σ : _ ≃+ M [⋀^ι']→ₗ[R] N).apply_eq_iff_eq

Equality of Reindexed Alternating Maps if and only if Original Maps are Equal

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\sigma : \iota \simeq \iota'$ be an equivalence between index types. For any two $R$-linear alternating maps $f, g : M [\bigwedge^\iota] \to_{R} N$, the reindexed maps $f.\text{domDomCongr} \sigma$ and $g.\text{domDomCongr} \sigma$ are equal if and only if the original maps $f$ and $g$ are equal.

AlternatingMap.domDomCongr_eq_zero_iff theorem

(σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) : f.domDomCongr σ = 0 ↔ f = 0

Full source

@[simp]
theorem domDomCongr_eq_zero_iff (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) :
    f.domDomCongr σ = 0 ↔ f = 0 :=
  (domDomCongrEquiv σ : M [⋀^ι]→ₗ[R] NM [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N).map_eq_zero_iff

Reindexed Alternating Map is Zero if and only if Original is Zero

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\sigma \colon \iota \simeq \iota'$ be an equivalence between index types. For any $R$-linear alternating map $f \colon M [\bigwedge^\iota] \to_R N$, the reindexed alternating map $f.\mathrm{domDomCongr}\,\sigma$ is zero if and only if $f$ is zero.

AlternatingMap.domDomCongr_perm theorem

[Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) : g.domDomCongr σ = Equiv.Perm.sign σ • g

Full source

theorem domDomCongr_perm [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) :
    g.domDomCongr σ = Equiv.Perm.sign σ • g :=
  AlternatingMap.ext fun v => g.map_perm v σ

Reindexed Alternating Map Equals Sign Times Original Under Permutation: $g.\mathrm{domDomCongr}\,\sigma = \mathrm{sign}(\sigma) \cdot g$

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\iota$ be a finite index type with decidable equality. For any $R$-linear alternating map $g : M [\bigwedge^\iota] \to_{R} N$ and any permutation $\sigma$ of $\iota$, the reindexed alternating map $g.\mathrm{domDomCongr}\,\sigma$ equals $\mathrm{sign}(\sigma) \cdot g$, where $\mathrm{sign}(\sigma)$ denotes the sign of the permutation $\sigma$ (which is $1$ for even permutations and $-1$ for odd permutations), and $\cdot$ denotes the scalar multiplication in $N$.

AlternatingMap.coe_domDomCongr theorem

(σ : ι ≃ ι') : ↑(f.domDomCongr σ) = (f : MultilinearMap R (fun _ : ι => M) N).domDomCongr σ

Full source

@[norm_cast]
theorem coe_domDomCongr (σ : ι ≃ ι') :
    ↑(f.domDomCongr σ) = (f : MultilinearMap R (fun _ : ι => M) N).domDomCongr σ :=
  MultilinearMap.ext fun _ => rfl

Coercion Commutes with Reindexing of Alternating Maps

Informal description

For any equivalence $\sigma \colon \iota \simeq \iota'$ between index types, the coercion of the reindexed alternating map $f.\mathrm{domDomCongr}\,\sigma$ to a multilinear map coincides with the reindexing of the coercion of $f$ as a multilinear map via $\sigma$. That is, \[ (f.\mathrm{domDomCongr}\,\sigma) = (f \colon \mathrm{MultilinearMap}_R(\lambda \_, M) N).\mathrm{domDomCongr}\,\sigma. \]

AlternatingMap.map_linearDependent theorem

 {K : Type*} [Ring K] {M : Type*} [AddCommGroup M] [Module K M] {N : Type*} [AddCommGroup N] [Module K N]
  [NoZeroSMulDivisors K N] (f : M [⋀^ι]→ₗ[K] N) (v : ι → M) (h : ¬LinearIndependent K v) : f v = 0

Full source

/-- If the arguments are linearly dependent then the result is `0`. -/
theorem map_linearDependent {K : Type*} [Ring K] {M : Type*} [AddCommGroup M] [Module K M]
    {N : Type*} [AddCommGroup N] [Module K N] [NoZeroSMulDivisors K N] (f : M [⋀^ι]→ₗ[K] N)
    (v : ι → M) (h : ¬LinearIndependent K v) : f v = 0 := by
  obtain ⟨s, g, h, i, hi, hz⟩ := not_linearIndependent_iff.mp h
  letI := Classical.decEq ι
  suffices f (update v i (g i • v i)) = 0 by
    rw [f.map_update_smul, Function.update_eq_self, smul_eq_zero] at this
    exact Or.resolve_left this hz
  rw [← Finset.insert_erase hi, Finset.sum_insert (s.not_mem_erase i), add_eq_zero_iff_eq_neg] at h
  rw [h, f.map_update_neg, f.map_update_sum, neg_eq_zero]
  apply Finset.sum_eq_zero
  intro j hj
  obtain ⟨hij, _⟩ := Finset.mem_erase.mp hj
  rw [f.map_update_smul, f.map_update_self _ hij.symm, smul_zero]

Alternating Maps Vanish on Linearly Dependent Families

Informal description

Let $K$ be a ring, $M$ and $N$ be $K$-modules with $N$ having no zero scalar divisors (i.e., $[NoZeroSMulDivisors K N]$). For any $K$-linear alternating map $f \colon M [\bigwedge^\iota] \to_{K} N$ and any family of vectors $v \colon \iota \to M$ that is linearly dependent over $K$, the evaluation of $f$ at $v$ is zero, i.e., $f(v) = 0$.

AlternatingMap.map_vecCons_add theorem

 {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (x y : M) :
  f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)

Full source

/-- A version of `MultilinearMap.cons_add` for `AlternatingMap`. -/
theorem map_vecCons_add {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (x y : M) :
    f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m) :=
  f.toMultilinearMap.cons_add _ _ _

Additivity of Alternating Maps in First Argument

Informal description

For any natural number $n$, given an $R$-linear alternating map $f \colon M^{\wedge (n+1)} \to N$, a vector $m \in M^n$, and elements $x, y \in M$, we have \[ f(x + y, m) = f(x, m) + f(y, m), \] where $(x + y, m)$ denotes the vector in $M^{n+1}$ obtained by prepending $x + y$ to $m$.

AlternatingMap.map_vecCons_smul theorem

 {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (c : R) (x : M) :
  f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)

Full source

/-- A version of `MultilinearMap.cons_smul` for `AlternatingMap`. -/
theorem map_vecCons_smul {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (c : R)
    (x : M) : f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m) :=
  f.toMultilinearMap.cons_smul _ _ _

Linearity of Alternating Maps in First Argument under Scalar Multiplication

Informal description

For any natural number $n$, given an $R$-linear alternating map $f \colon M^{\wedge (n+1)} \to N$, a vector $m \in M^n$, a scalar $c \in R$, and an element $x \in M$, we have \[ f(c \cdot x, m) = c \cdot f(x, m), \] where $(c \cdot x, m)$ denotes the vector in $M^{n+1}$ obtained by prepending $c \cdot x$ to $m$.

MultilinearMap.alternatization definition

: MultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N'

Full source

/-- Produce an `AlternatingMap` out of a `MultilinearMap`, by summing over all argument
permutations. -/
def alternatization : MultilinearMapMultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N' where
  toFun m :=
    { ∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ with
      toFun := ⇑(∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ)
      map_eq_zero_of_eq' := fun v i j hvij hij =>
        alternization_map_eq_zero_of_eq_aux m v i j hij hvij }
  map_add' a b := by
    ext
    simp only [mk_coe, AlternatingMap.coe_mk, sum_apply, smul_apply, domDomCongr_apply, add_apply,
      smul_add, Finset.sum_add_distrib, AlternatingMap.add_apply]
  map_zero' := by
    ext
    simp only [mk_coe, AlternatingMap.coe_mk, sum_apply, smul_apply, domDomCongr_apply,
      zero_apply, smul_zero, Finset.sum_const_zero, AlternatingMap.zero_apply]

Alternatization of a multilinear map

Informal description

Given a commutative ring $ R $, modules $ M $ and $ N' $ over $ R $, and a type $ \iota $, the function `MultilinearMap.alternatization` constructs an $ R $-linear alternating map from a multilinear map $ m \colon M^\iota \to N' $ by summing over all permutations $ \sigma $ of $ \iota $, with each term weighted by the sign of the permutation. Specifically, the alternating map is defined as: \[ \text{alternatization}(m)(v) = \sum_{\sigma \in \text{Perm}(\iota)} \text{sign}(\sigma) \cdot m(\sigma \cdot v), \] where $ \text{sign}(\sigma) $ is the sign of the permutation $ \sigma $ (1 for even, -1 for odd), and $ \sigma \cdot v $ denotes the action of $ \sigma $ on the vector $ v $.

MultilinearMap.alternatization_def theorem

 (m : MultilinearMap R (fun _ : ι => M) N') :
  ⇑(alternatization m) = (∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ :)

Full source

theorem alternatization_def (m : MultilinearMap R (fun _ : ι => M) N') :
    ⇑(alternatization m) = (∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ :) :=
  rfl

Definition of Alternatization via Permutation Sum

Informal description

Given a commutative ring $R$, modules $M$ and $N'$ over $R$, and a type $\iota$, for any multilinear map $m \colon M^\iota \to N'$, the underlying function of its alternatization is given by: \[ \text{alternatization}(m)(v) = \sum_{\sigma \in \text{Perm}(\iota)} \text{sign}(\sigma) \cdot m(\sigma \cdot v), \] where $\text{sign}(\sigma)$ is the sign of the permutation $\sigma$ (1 for even, -1 for odd), and $\sigma \cdot v$ denotes the action of $\sigma$ on the vector $v$.

MultilinearMap.alternatization_coe theorem

 (m : MultilinearMap R (fun _ : ι => M) N') :
  ↑(alternatization m) = (∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ :)

Full source

theorem alternatization_coe (m : MultilinearMap R (fun _ : ι => M) N') :
    ↑(alternatization m) = (∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ :) :=
  coe_injective rfl

Coefficient Form of Alternatization of a Multilinear Map

Informal description

For any multilinear map $ m $ from $ \iota \to M $ to $ N' $ over a commutative ring $ R $, the underlying multilinear map of its alternatization is equal to the sum over all permutations $ \sigma $ of $ \iota $ of the signed multilinear map obtained by permuting the arguments of $ m $ according to $ \sigma $. That is, \[ \text{alternatization}(m) = \sum_{\sigma \in \text{Perm}(\iota)} \text{sign}(\sigma) \cdot m \circ \sigma, \] where $ \text{sign}(\sigma) $ denotes the sign of the permutation $ \sigma $, and $ m \circ \sigma $ denotes the composition of $ m $ with the permutation $ \sigma $ acting on the arguments.

MultilinearMap.alternatization_apply theorem

 (m : MultilinearMap R (fun _ : ι => M) N') (v : ι → M) :
  alternatization m v = ∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ v

Full source

theorem alternatization_apply (m : MultilinearMap R (fun _ : ι => M) N') (v : ι → M) :
    alternatization m v = ∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ v := by
  simp only [alternatization_def, smul_apply, sum_apply]

Alternatization Formula for Multilinear Maps

Informal description

Let $R$ be a commutative ring, $M$ and $N'$ be $R$-modules, and $\iota$ be a finite type. Given a multilinear map $m \colon M^\iota \to N'$ and a vector $v \in M^\iota$, the alternatization of $m$ evaluated at $v$ is given by: \[ \text{alternatization}(m)(v) = \sum_{\sigma \in \text{Perm}(\iota)} \text{sign}(\sigma) \cdot m(\sigma \cdot v), \] where $\text{sign}(\sigma) \in \{\pm 1\}$ is the sign of the permutation $\sigma$, and $\sigma \cdot v$ denotes the action of $\sigma$ on $v$.

AlternatingMap.coe_alternatization theorem

 [DecidableEq ι] [Fintype ι] (a : M [⋀^ι]→ₗ[R] N') :
  MultilinearMap.alternatization (a : MultilinearMap R (fun _ => M) N') = Nat.factorial (Fintype.card ι) • a

Full source

/-- Alternatizing a multilinear map that is already alternating results in a scale factor of `n!`,
where `n` is the number of inputs. -/
theorem coe_alternatization [DecidableEq ι] [Fintype ι] (a : M [⋀^ι]→ₗ[R] N') :
    MultilinearMap.alternatization (a : MultilinearMap R (fun _ => M) N')
    = Nat.factorial (Fintype.card ι) • a := by
  apply AlternatingMap.coe_injective
  simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]

Alternatization of an Alternating Map Scales by Factorial of Dimension: $\text{alternatization}(a) = n! \cdot a$

Informal description

Let $R$ be a commutative ring, $M$ and $N'$ be $R$-modules, and $\iota$ be a finite type with decidable equality. For any $R$-linear alternating map $a \colon M [\bigwedge^\iota] \to_{R} N'$, the alternatization of $a$ (viewed as a multilinear map) equals $n! \cdot a$, where $n$ is the cardinality of $\iota$. In mathematical notation: \[ \text{alternatization}(a) = n! \cdot a \] where $n = |\iota|$ and $a$ is considered as a multilinear map.

LinearMap.compMultilinearMap_alternatization theorem

 (g : N' →ₗ[R] N'₂) (f : MultilinearMap R (fun _ : ι => M) N') :
  MultilinearMap.alternatization (g.compMultilinearMap f) = g.compAlternatingMap (MultilinearMap.alternatization f)

Full source

/-- Composition with a linear map before and after alternatization are equivalent. -/
theorem compMultilinearMap_alternatization (g : N' →ₗ[R] N'₂)
    (f : MultilinearMap R (fun _ : ι => M) N') :
    MultilinearMap.alternatization (g.compMultilinearMap f)
      = g.compAlternatingMap (MultilinearMap.alternatization f) := by
  ext
  simp [MultilinearMap.alternatization_def]

Commutativity of Alternatization with Linear Map Composition

Informal description

Let $R$ be a commutative ring, $M$ an $R$-module, and $\iota$ a type. For any linear map $g \colon N' \to_R N'_2$ and any multilinear map $f \colon M^\iota \to_R N'$, the alternatization of the composition $g \circ f$ equals the composition of $g$ with the alternatization of $f$. That is, \[ \text{alternatization}(g \circ f) = g \circ \text{alternatization}(f). \]

Basis.ext_alternating theorem

 {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Basis ι₁ R' N₁)
  (h : ∀ v : ι → ι₁, Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)) : f = g

Full source

/-- Two alternating maps indexed by a `Fintype` are equal if they are equal when all arguments
are distinct basis vectors. -/
theorem Basis.ext_alternating {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Basis ι₁ R' N₁)
    (h : ∀ v : ι → ι₁, Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)) :
    f = g := by
  classical
    refine AlternatingMap.coe_multilinearMap_injective (Basis.ext_multilinear e fun v => ?_)
    by_cases hi : Function.Injective v
    · exact h v hi
    · have : ¬Function.Injective fun i => e (v i) := hi.imp Function.Injective.of_comp
      rw [coe_multilinearMap, coe_multilinearMap, f.map_eq_zero_of_not_injective _ this,
        g.map_eq_zero_of_not_injective _ this]

Equality of Alternating Maps via Basis Vectors

Informal description

Let $R'$ be a commutative ring, $N₁$ and $N₂$ be $R'$-modules, and $\iota$, $\iota₁$ be types with $\iota$ finite. Given two $R'$-linear alternating maps $f, g \colon N₁ [\bigwedge^\iota] \to_{R'} N₂$ and a basis $e$ of $N₁$ indexed by $\iota₁$, if for every injective function $v \colon \iota \to \iota₁$ we have \[ f \left( \lambda i \mapsto e(v(i)) \right) = g \left( \lambda i \mapsto e(v(i)) \right), \] then $f = g$.

AlternatingMap.curryLeft definition

{n : ℕ} (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') : M'' →ₗ[R'] M'' [⋀^Fin n]→ₗ[R'] N''

Full source

/-- Given an alternating map `f` in `n+1` variables, split the first variable to obtain
a linear map into alternating maps in `n` variables, given by `x ↦ (m ↦ f (Matrix.vecCons x m))`.
It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.

This is `MultilinearMap.curryLeft` for `AlternatingMap`. See also
`AlternatingMap.curryLeftLinearMap`. -/
@[simps]
def curryLeft {n : ℕ} (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
    M'' →ₗ[R'] M'' [⋀^Fin n]→ₗ[R'] N'' where
  toFun m :=
    { f.toMultilinearMap.curryLeft m with
      toFun := fun v => f (Matrix.vecCons m v)
      map_eq_zero_of_eq' := fun v i j hv hij =>
        f.map_eq_zero_of_eq _ (by
          rwa [Matrix.cons_val_succ, Matrix.cons_val_succ]) ((Fin.succ_injective _).ne hij) }
  map_add' _ _ := ext fun _ => f.map_vecCons_add _ _ _
  map_smul' _ _ := ext fun _ => f.map_vecCons_smul _ _ _

Left currying of an alternating map

Informal description

Given an $R$-linear alternating map $f$ in $n+1$ variables (where the variables are indexed by `Fin n.succ`), the operation `curryLeft` constructs a linear map from $M''$ to the space of alternating maps in $n$ variables (indexed by `Fin n`). Specifically, for each $m \in M''$, the resulting alternating map is defined by $(v_1, \ldots, v_n) \mapsto f(m, v_1, \ldots, v_n)$. This operation effectively binds the leftmost argument of $f$, producing a family of alternating maps parameterized by $m$.

AlternatingMap.curryLeft_zero theorem

{n : ℕ} : curryLeft (0 : M'' [⋀^Fin n.succ]→ₗ[R'] N'') = 0

Full source

@[simp]
theorem curryLeft_zero {n : ℕ} : curryLeft (0 : M'' [⋀^Fin n.succ]→ₗ[R'] N'') = 0 :=
  rfl

Left Currying of Zero Alternating Map Yields Zero Linear Map

Informal description

For any natural number $n$, the left currying of the zero alternating map in $n+1$ variables is equal to the zero linear map from $M''$ to the space of alternating maps in $n$ variables.

AlternatingMap.curryLeft_add theorem

{n : ℕ} (f g : M'' [⋀^Fin n.succ]→ₗ[R'] N'') : curryLeft (f + g) = curryLeft f + curryLeft g

Full source

@[simp]
theorem curryLeft_add {n : ℕ} (f g : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
    curryLeft (f + g) = curryLeft f + curryLeft g :=
  rfl

Additivity of Left Currying for Alternating Maps

Informal description

For any natural number $n$ and $R'$-linear alternating maps $f, g$ in $n+1$ variables (indexed by `Fin n.succ`), the left currying of the sum $f + g$ is equal to the sum of the left currying of $f$ and the left currying of $g$. That is, $\text{curryLeft}(f + g) = \text{curryLeft}(f) + \text{curryLeft}(g)$.

AlternatingMap.curryLeft_smul theorem

{n : ℕ} (r : R') (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') : curryLeft (r • f) = r • curryLeft f

Full source

@[simp]
theorem curryLeft_smul {n : ℕ} (r : R') (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
    curryLeft (r • f) = r • curryLeft f :=
  rfl

Scalar Multiplication Commutes with Left Currying of Alternating Maps

Informal description

For any natural number $n$, scalar $r \in R'$, and $R'$-linear alternating map $f$ from $M''^{n+1}$ to $N''$, the left currying of the scalar multiple $r \cdot f$ equals the scalar multiple $r$ applied to the left currying of $f$. In other words, $\text{curryLeft}(r \cdot f) = r \cdot \text{curryLeft}(f)$.

AlternatingMap.curryLeftLinearMap definition

{n : ℕ} : (M'' [⋀^Fin n.succ]→ₗ[R'] N'') →ₗ[R'] M'' →ₗ[R'] M'' [⋀^Fin n]→ₗ[R'] N''

Full source

/-- `AlternatingMap.curryLeft` as a `LinearMap`. This is a separate definition as dot notation
does not work for this version. -/
@[simps]
def curryLeftLinearMap {n : ℕ} :
    (M'' [⋀^Fin n.succ]→ₗ[R'] N'') →ₗ[R'] M'' →ₗ[R'] M'' [⋀^Fin n]→ₗ[R'] N'' where
  toFun f := f.curryLeft
  map_add' := curryLeft_add
  map_smul' := curryLeft_smul

Linear map version of left currying for alternating maps

Informal description

For any natural number $n$, the linear map `curryLeftLinearMap` takes an $R'$-linear alternating map $f$ from $M''^{n+1}$ to $N''$ (where the variables are indexed by `Fin n.succ`) and returns a linear map from $M''$ to the space of $R'$-linear alternating maps from $M''^n$ to $N''$ (indexed by `Fin n`). Specifically, for each $m \in M''$, the resulting alternating map is $(v_1, \ldots, v_n) \mapsto f(m, v_1, \ldots, v_n)$. This map is linear in $f$, meaning it preserves addition and scalar multiplication: - $\text{curryLeftLinearMap}(f + g) = \text{curryLeftLinearMap}(f) + \text{curryLeftLinearMap}(g)$ - $\text{curryLeftLinearMap}(r \cdot f) = r \cdot \text{curryLeftLinearMap}(f)$ for any scalar $r \in R'$.

AlternatingMap.curryLeft_same theorem

{n : ℕ} (f : M'' [⋀^Fin n.succ.succ]→ₗ[R'] N'') (m : M'') : (f.curryLeft m).curryLeft m = 0

Full source

/-- Currying with the same element twice gives the zero map. -/
@[simp]
theorem curryLeft_same {n : ℕ} (f : M'' [⋀^Fin n.succ.succ]→ₗ[R'] N'') (m : M'') :
    (f.curryLeft m).curryLeft m = 0 :=
  ext fun _ => f.map_eq_zero_of_eq _ (by simp) Fin.zero_ne_one

Double Left Currying of Alternating Map Vanishes

Informal description

Let $R'$ be a commutative ring, $M''$ and $N''$ be $R'$-modules, and $n$ be a natural number. For any $R'$-linear alternating map $f \colon M'' [\bigwedge^{\text{Fin } (n+2)}] \to N''$ and any $m \in M''$, the double left currying of $f$ at $m$ equals zero, i.e., $$(f.\text{curryLeft}(m)).\text{curryLeft}(m) = 0.$$

AlternatingMap.curryLeft_compAlternatingMap theorem

 {n : ℕ} (g : N'' →ₗ[R'] N₂'') (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M'') :
  (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m)

Full source

@[simp]
theorem curryLeft_compAlternatingMap {n : ℕ} (g : N'' →ₗ[R'] N₂'')
    (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M'') :
    (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m) :=
  rfl

Compatibility of Left Currying with Linear Composition of Alternating Maps

Informal description

For any natural number $n$, given a linear map $g : N'' \to_{R'} N_2''$ and an alternating map $f : M'' [\bigwedge^{\text{Fin } n+1}] \to_{R'} N''$, and for any $m \in M''$, the left currying of the composition $g \circ f$ evaluated at $m$ equals the composition of $g$ with the left currying of $f$ evaluated at $m$. In symbols: $$(g \circ f).\text{curryLeft}(m) = g \circ (f.\text{curryLeft}(m))$$

AlternatingMap.curryLeft_compLinearMap theorem

 {n : ℕ} (g : M₂'' →ₗ[R'] M'') (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M₂'') :
  (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g

Full source

@[simp]
theorem curryLeft_compLinearMap {n : ℕ} (g : M₂'' →ₗ[R'] M'')
    (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M₂'') :
    (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g :=
  ext fun v => congr_arg f <| funext <| by
    refine Fin.cases ?_ ?_
    · rfl
    · simp

Compatibility of Left Currying with Linear Map Composition for Alternating Maps

Informal description

Let $R'$ be a commutative ring, $M''$, $M_2''$, and $N''$ be $R'$-modules, and $n$ be a natural number. For any $R'$-linear map $g \colon M_2'' \to M''$, any $R'$-linear alternating map $f \colon M'' [\bigwedge^{\text{Fin } (n+1)}] \to N''$, and any $m \in M_2''$, we have: \[ (f \circ g).\text{curryLeft}(m) = (f.\text{curryLeft}(g(m))) \circ g \] Here, $\text{curryLeft}$ denotes the operation of fixing the first argument of an alternating map, and $\circ$ denotes the composition of alternating maps with linear maps.

AlternatingMap.constLinearEquivOfIsEmpty definition

[IsEmpty ι] : N'' ≃ₗ[R'] (M'' [⋀^ι]→ₗ[R'] N'')

Full source

/-- The space of constant maps is equivalent to the space of maps that are alternating with respect
to an empty family. -/
@[simps]
def constLinearEquivOfIsEmpty [IsEmpty ι] : N'' ≃ₗ[R'] (M'' [⋀^ι]→ₗ[R'] N'') where
  toFun := AlternatingMap.constOfIsEmpty R' M'' ι
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun f := f 0
  left_inv _ := rfl
  right_inv f := ext fun _ => AlternatingMap.congr_arg f <| Subsingleton.elim _ _

Linear equivalence between a module and alternating maps over an empty index type

Informal description

Given a commutative ring $R'$, modules $M''$ and $N''$ over $R'$, and an empty index type $\iota$, there is a linear equivalence between $N''$ and the space of $R'$-linear alternating maps from $\iota \to M''$ to $N''$. The equivalence maps an element $n \in N''$ to the constant alternating map with value $n$, and its inverse evaluates an alternating map at the zero function.

Mathlib.LinearAlgebra.Alternating.Basic

Main definitions

Implementation notes