AlgebraicCurves.Geometry.Sheaves.Proofs.ExteriorPowerDeterminant.AlgebraicGeometry.Scheme.Modules.Ws31H2.alternatingMap_apply_matrix_smul
Source context 19 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ExteriorPowerDeterminant
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace Ws31H2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.OppositeLean source · full declaration
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
rw [h3, h4]
have hdet : b.det (fun j => a.transpose j) = a.det :=
(Pi.basisFun_det_apply (R := A) (fun j i => a i j)).trans (Matrix.det_transpose a)
exact congrArg (fun r : A => r • g f) hdet