feat(LinearAlgebra/ExteriorAlgebra/Basic): adds multiplication lemmas for ExteriorAlgebra (leanprover-community#35433)

This adds lemmas for dealing with multiplication of elements in the `ExteriorAlgebra`:
* `ιMulti_eq_zero_of_not_inj` : a product containing duplicates is zero
* `ιMulti_mul_ιMulti` : `ιMulti R m a * ιMulti R n b = ιMulti R (m+n) (Fin.append a b)`
* `ιMulti_family_mul_of_not_disjoint` : if two sets of elements are not disjoint their product is zero
* `ιMulti_perm` : the permutation corresponding to adjoining two sets of elements and sorting the result
* `ιMulti_family_mul_of_disjoint` : the product of two elements of the form `ιMulti_family` is of the form `ιMulti_family` up to sign

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

Author: morrison-daniel

Mathlib/Data/Finset/Basic.lean

@@ -601,6 +601,33 @@ theorem Finset.union_symm_right (h : Disjoint s t) {i : α} (hi : i ∈ t)
     (hi' : i ∈ s ∪ t) : (Equiv.Finset.union s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩ := by
   simp [Equiv.symm_apply_eq]
 
+/-- The disjoint union of finsets is a sum -/
+def Finset.disjUnionEquiv (s t : Finset α) (h : Disjoint s t) :
+    s ⊕ t ≃ s.disjUnion t h :=
+  Equiv.setCongr (coe_disjUnion h) |>.trans (Equiv.Set.union (disjoint_coe.mpr h)) |>.symm
+
+@[simp]
+theorem Finset.disjUnionEquiv_inl (h : Disjoint s t) (x : s) :
+    Equiv.Finset.disjUnionEquiv s t h (Sum.inl x) = ⟨x, Finset.mem_disjUnion.mpr <| Or.inl x.2⟩ :=
+  rfl
+
+@[simp]
+theorem Finset.disjUnionEquiv_inr (h : Disjoint s t) (y : t) :
+    Equiv.Finset.disjUnionEquiv s t h (Sum.inr y) = ⟨y, Finset.mem_disjUnion.mpr <| Or.inr y.2⟩ :=
+  rfl
+
+@[simp]
+theorem Finset.disjUnionEquiv_symm_left (h : Disjoint s t) {i : α} (hi : i ∈ s)
+    (hi' : i ∈ s.disjUnion t h) :
+    (Equiv.Finset.disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩ := by
+  simp [Equiv.symm_apply_eq]
+
+@[simp]
+theorem Finset.disjUnionEquiv_symm_right (h : Disjoint s t) {i : α} (hi : i ∈ t)
+    (hi' : i ∈ s.disjUnion t h) :
+    (Equiv.Finset.disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩ := by
+  simp [Equiv.symm_apply_eq]
+
 /-- The type of dependent functions on the disjoint union of finsets `s ∪ t` is equivalent to the
   type of pairs of functions on `s` and on `t`. This is similar to `Equiv.sumPiEquivProdPi`. -/
 def piFinsetUnion {ι} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι} (h : Disjoint s t) :

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

@@ -316,6 +316,18 @@ theorem ιMulti_succ_curryLeft {n : ℕ} (m : M) :
       (LinearMap.mulLeft R (ι R m)).compAlternatingMap (ιMulti R n) := by
   ext; simp
 
+lemma ιMulti_eq_zero_of_not_inj {n : ℕ} {v : Fin n → M} (hv : ¬Function.Injective v) :
+    ιMulti R n v = 0 :=
+  (ιMulti R n).map_eq_zero_of_not_injective v hv
+
+lemma ιMulti_mul_ιMulti {m n : ℕ} (a : Fin m → M) (b : Fin n → M) :
+    ιMulti R m a * ιMulti R n b = ιMulti R (m + n) (Fin.append a b) := by
+  simp only [ιMulti_apply]
+  change _ = (List.ofFn ((ι R) ∘ Fin.append a b)).prod
+  rw [← List.map_ofFn, List.ofFn_fin_append, List.map_append, List.prod_append]
+  simp only [List.map_ofFn]
+  congr
+
 variable (R)
 
 /-- The image of `ExteriorAlgebra.ιMulti R n` is contained in the `n`th exterior power. -/
@@ -350,6 +362,39 @@ abbrev ιMulti_family (n : ℕ) {I : Type*} [LinearOrder I] (v : I → M)
     (s : Set.powersetCard I n) : ExteriorAlgebra R M :=
   ιMulti R n (v ∘ (Set.powersetCard.ofFinEmbEquiv.symm s))
 
+open Set Set.powersetCard
+
+lemma ιMulti_family_mul_of_not_disjoint {m n : ℕ} {I : Type*} [LinearOrder I] (v : I → M)
+    (s : powersetCard I m) (t : powersetCard I n) (h : ¬Disjoint s.val t.val) :
+    ιMulti_family R m v s * ιMulti_family R n v t = 0 := by
+  rw [Finset.not_disjoint_iff] at h
+  obtain ⟨i, his, hit⟩ := h
+  obtain ⟨j, hj⟩ := (mem_range_ofFinEmbEquiv_symm_iff_mem s i).mpr his
+  obtain ⟨k, hk⟩ := (mem_range_ofFinEmbEquiv_symm_iff_mem t i).mpr hit
+  simp only [ιMulti_family, ιMulti_mul_ιMulti]
+  apply AlternatingMap.map_eq_zero_of_eq (i := Fin.castAdd n j) (j := Fin.natAdd m k)
+  · simp [hj, hk]
+  · apply ne_of_lt
+    apply lt_of_lt_of_le (b := m) <;> simp
+
+lemma ιMulti_family_mul_of_disjoint {m n : ℕ} {I : Type*} [LinearOrder I] (v : I → M)
+    (s : powersetCard I m) (t : powersetCard I n) (h : Disjoint s.val t.val) :
+    ιMulti_family R m v s * ιMulti_family R n v t =
+      (permOfDisjoint h).sign • ιMulti_family R (m + n) v (disjUnion h) := by
+  simp only [ιMulti_family, ιMulti_mul_ιMulti]
+  rw [← AlternatingMap.map_perm, permOfDisjoint]
+  congr
+  ext i
+  let e := powersetCard.orderIsoOfFin (powersetCard.disjUnion h)
+  change _ = v (e (e.symm _))
+  by_cases! hi : i < m
+  · rw [← Fin.castAdd_castLT n i hi, Fin.append_left, OrderIso.apply_symm_apply,
+      finSumFinEquiv_symm_apply_castAdd]
+    aesop
+  · rw [← Fin.natAdd_subNat_cast hi, Fin.append_right, OrderIso.apply_symm_apply,
+      finSumFinEquiv_symm_apply_natAdd]
+    aesop
+
 variable {R}
 
 /-- An `ExteriorAlgebra` over a nontrivial ring is nontrivial. -/

Mathlib/Order/Hom/PowersetCard.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Set.PowersetCard
 public import Mathlib.Data.Finset.Sort
+public import Mathlib.Logic.Equiv.Fin.Basic
 
 /-!
 # Finite sets of an ordered type
@@ -55,6 +56,24 @@ lemma mem_range_ofFinEmbEquiv_symm_iff_mem (s : powersetCard I n) (i : I) :
     i ∈ range (ofFinEmbEquiv.symm s) ↔ i ∈ s := by
   simp [ofFinEmbEquiv_symm_apply]
 
+/-- The natural enumeration of the elements of linearly-ordered type. -/
+@[simps!] def orderIsoOfFin {n : ℕ} {I : Type*} [LinearOrder I] (s : powersetCard I n) :
+    Fin n ≃o s.val :=
+  s.val.orderIsoOfFin s.prop
+
+/-- The permutation of `Fin (m + n)` corresponding to adjoining a `Finset` of card `m`
+to a `Finset` of card `n` and sorting the resulting set. In other words, given `s₁ < s₂ < ⋯ < sₘ`
+and `t₁ < t₂ < ⋯ < tₙ` (disjoint) this is the permutation obtained by sorting
+`s₁, s₂, …, sₘ, t₁, t₂, …, tₙ`. -/
+def permOfDisjoint {m n : ℕ} {I : Type*} [LinearOrder I]
+    {s : powersetCard I m} {t : powersetCard I n} (h : Disjoint s.val t.val) :
+    Equiv.Perm (Fin (m + n)) :=
+  letI e₁ : Fin (m + n) ≃ Fin m ⊕ Fin n := finSumFinEquiv.symm
+  letI e₂ : Fin m ⊕ Fin n ≃ s.val ⊕ t.val := (orderIsoOfFin s).sumCongr (orderIsoOfFin t)
+  letI e₃ : s.val ⊕ t.val ≃ disjUnion h := Equiv.Finset.disjUnionEquiv _ _ h
+  letI e₄ : disjUnion h ≃o Fin (m + n) := (orderIsoOfFin (disjUnion h)).symm
+  e₁.trans <| e₂.trans <| e₃.trans <| e₄
+
 end order
 
 end Set.powersetCard