Recognizing a second exterior power

An alternating bilinear map ω : M → M → N induces, by the universal property of the exterior power, a linear map ⋀²M → N sending x ∧ y to ω x y. This file records when that map is an isomorphism: if M has a basis b indexed by a linearly ordered type and the values ω (b i) (b j) for i < j form a basis of N, then ⋀²M ≃ N.

This is how a module presented by a basis of "brackets" of basis vectors, such as the degree-one piece of the graded Lie algebra of a free group, is identified with an exterior square without comparing the index set {(i, j) | i < j} with Mathlib's index set of two-element subsets.

Main definitions

• LinearMap.IsAlt.exteriorSquareEquiv: the isomorphism ⋀²M ≃ N induced by an alternating bilinear map carrying the ordered pairs of a basis of M to a basis of N.

Main results

• LinearMap.IsAlt.exteriorSquareEquiv_ιMulti: the isomorphism sends x ∧ y to ω x y.
• LinearMap.IsAlt.exteriorSquareEquiv_symm_apply: its inverse sends the basis vector indexed by i < j to b i ∧ b j.
• exteriorPower.ιMulti_two_add_right and exteriorPower.ιMulti_two_smul_right: the wedge u ∧ w of two vectors is linear in w.
• exteriorPower.ιMulti_two_smul_left: the wedge u ∧ w is homogeneous in u.

theorem exteriorPower.ιMulti_two_add_right {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (u w w' : M) : (ιMulti R 2) ![u, w + w'] = (ιMulti R 2) ![u, w] + (ιMulti R 2) ![u, w']

The wedge u ∧ w is additive in w.

theorem exteriorPower.ιMulti_two_smul_right {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (u w : M) (c : R) : (ιMulti R 2) ![u, c • w] = c • (ιMulti R 2) ![u, w]

The wedge u ∧ w is homogeneous in w.

theorem exteriorPower.ιMulti_two_smul_left {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (u w : M) (c : R) : (ιMulti R 2) ![c • u, w] = c • (ιMulti R 2) ![u, w]

The wedge u ∧ w is homogeneous in u.

noncomputable def LinearMap.IsAlt.exteriorSquareEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [LinearOrder ι] {ω : M →ₗ[R] M →ₗ[R] N} (hω : ω.IsAlt) (b : Module.Basis ι R M) (c : Module.Basis { ij : ι × ι // ij.1 < ij.2 } R N) (hc : ∀ (ij : { ij : ι × ι // ij.1 < ij.2 }), (ω (b (↑ij).1)) (b (↑ij).2) = c ij) : ↥(⋀[R]^2 M) ≃ₗ[R] N

Recognizing an exterior square. Let ω be an alternating bilinear map, b a basis of M indexed by a linearly ordered type, and c a basis of N indexed by the pairs i < j with c (i, j) = ω (b i) (b j). Then the linear map ⋀²M → N induced by ω, which sends x ∧ y to ω x y (LinearMap.IsAlt.exteriorSquareEquiv_ιMulti), is an isomorphism.

@[simp]

theorem LinearMap.IsAlt.exteriorSquareEquiv_ιMulti {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [LinearOrder ι] {ω : M →ₗ[R] M →ₗ[R] N} (hω : ω.IsAlt) (b : Module.Basis ι R M) (c : Module.Basis { ij : ι × ι // ij.1 < ij.2 } R N) (hc : ∀ (ij : { ij : ι × ι // ij.1 < ij.2 }), (ω (b (↑ij).1)) (b (↑ij).2) = c ij) (v : Fin 2 → M) : (hω.exteriorSquareEquiv b c hc) ((exteriorPower.ιMulti R 2) v) = (ω (v 0)) (v 1)

The isomorphism induced by ω sends x ∧ y to ω x y.

@[simp]

theorem LinearMap.IsAlt.exteriorSquareEquiv_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [LinearOrder ι] {ω : M →ₗ[R] M →ₗ[R] N} (hω : ω.IsAlt) (b : Module.Basis ι R M) (c : Module.Basis { ij : ι × ι // ij.1 < ij.2 } R N) (hc : ∀ (ij : { ij : ι × ι // ij.1 < ij.2 }), (ω (b (↑ij).1)) (b (↑ij).2) = c ij) (ij : { ij : ι × ι // ij.1 < ij.2 }) : (hω.exteriorSquareEquiv b c hc).symm (c ij) = (exteriorPower.ιMulti R 2) ![b (↑ij).1, b (↑ij).2]

The inverse isomorphism sends the basis vector of N indexed by i < j to b i ∧ b j.