exteriorPower_iotaMulti_comp_eq_det_smul.lean

lemma alternatingMap_apply_matrix_smul {A : Type*} [CommRing A] {M N : Type*} [AddCommGroup M]
    [Module A M] [AddCommGroup N] [Module A N] {n : ℕ} (g : M [⋀^Fin n]→ₗ[A] N) (f : Fin n → M)
    (a : Matrix (Fin n) (Fin n) A) :
    g (fun j => ∑ i, a i j • f i) = a.det • g f := by
  classical
  let L : (Fin n → A) →ₗ[A] M := Fintype.linearCombination A f
  let b : Module.Basis (Fin n) A (Fin n → A) := Pi.basisFun A (Fin n)
  have hL : ∀ i, L (b i) = f i := fun i => by
    simp [L, b, Fintype.linearCombination_apply_single]
  have key : g.compLinearMap L = b.det.smulRight (g f) := by
    refine Module.Basis.ext_alternating b fun v hv => ?_
    let σ : Equiv.Perm (Fin n) := Equiv.ofBijective v (Finite.injective_iff_bijective.1 hv)
    have h1 : (fun i => L (b (v i))) = f ∘ σ := funext fun i => hL (v i)
    have h2 : (fun i => b (v i)) = b ∘ σ := rfl
    rw [AlternatingMap.compLinearMap_apply, h1, AlternatingMap.map_perm,
      AlternatingMap.smulRight_apply,
      h2, AlternatingMap.map_perm, Module.Basis.det_self]
    simp [Units.smul_def, Int.cast_smul_eq_zsmul]
  have h3 : (fun j => ∑ i, a i j • f i) = fun j => L (a.transpose j) := by
    funext j
    simp [L, Fintype.linearCombination_apply, Matrix.transpose_apply]
  have h4 := congrArg (fun G : (Fin n → A) [⋀^Fin n]→ₗ[A] N => G (fun j => a.transpose j)) key
  simp only [AlternatingMap.compLinearMap_apply, AlternatingMap.smulRight_apply] at h4
  calc
    g (fun j => ∑ i, a i j • f i) = (b.det (fun j => a.transpose j)) • g f :=
      (congrArg g h3).trans h4
    _ = a.transpose.det • g f :=
      congrArg (fun r : A => r • g f) (Pi.basisFun_det_apply (fun j k => a k j))
    _ = a.det • g f := congrArg (fun r : A => r • g f) (Matrix.det_transpose a)

lemma ιMulti_matrix_smul {A : Type*} [CommRing A] {M : Type*} [AddCommGroup M] [Module A M]
    {n : ℕ} (f : Fin n → M) (a : Matrix (Fin n) (Fin n) A) :
    exteriorPower.ιMulti A n (fun j => ∑ i, a i j • f i) = a.det • exteriorPower.ιMulti A n f :=
  alternatingMap_apply_matrix_smul (exteriorPower.ιMulti A n) f a

theorem _root_.exteriorPower.iotaMulti_comp_eq_det_smul {A : Type*} [CommRing A] {M : Type*}
  [AddCommGroup M]
    [Module A M] {n : ℕ} (b : Module.Basis (Fin n) A M) (f : M →ₗ[A] M) (m : Fin n → M) :
    exteriorPower.ιMulti A n (f ∘ m) = LinearMap.det f • exteriorPower.ιMulti A n m