FiniteProductDeterminant.lean

1 import Mathlib.LinearAlgebra.Determinant
2 import Mathlib.LinearAlgebra.Dimension.Constructions
3 import Mathlib.Data.Fintype.Option
4 
5 /-! Determinants of actual finite products with varying coordinate spaces. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.FiniteProductDeterminant
9 open scoped BigOperators Classical
10 
11 universe u v w
12 variable {k : Type w} [Field k]
13 
14 def map {ι : Type u} {V : ι → Type v} [∀ i, AddCommGroup (V i)]
15     [∀ i, Module k (V i)] (f : ∀ i, Module.End k (V i)) :
16     Module.End k (∀ i, V i) :=
17   LinearMap.pi fun i => (f i).comp (LinearMap.proj i)
18 
19 @[simp] theorem map_apply {ι : Type u} {V : ι → Type v}
20     [∀ i, AddCommGroup (V i)] [∀ i, Module k (V i)]
21     (f : ∀ i, Module.End k (V i)) (x : ∀ i, V i) (i : ι) :
22     map f x i = f i (x i) := rfl
23 
24 theorem determinant (ι : Type u) [Fintype ι] (V : ι → Type v)
25     [∀ i, AddCommGroup (V i)] [∀ i, Module k (V i)]
26     [∀ i, FiniteDimensional k (V i)] (f : ∀ i, Module.End k (V i)) :
27     (map f).det = ∏ i, (f i).det := by
28   classical
29   revert V
30   refine Fintype.induction_empty_option
31     (P := fun α _ => ∀ (W : α → Type v) [∀ i, AddCommGroup (W i)]
32       [∀ i, Module k (W i)] [∀ i, FiniteDimensional k (W i)]
33       (a : ∀ i, Module.End k (W i)), (map a).det = ∏ i, (a i).det)
34     ?_ ?_ ?_ ι
35   · intro α β _ e ih V _ _ _ f
36     let : Fintype α := Fintype.ofEquiv β e.symm
37     let E := LinearEquiv.piCongrLeft k V e
38     have hmap : E.toLinearMap ∘ₗ map (fun i => f (e i)) ∘ₗ E.symm.toLinearMap =
39         map f := by
40       apply LinearMap.ext
41       intro x
42       apply E.symm.injective
43       change E.symm (E (map (fun i => f (e i)) (E.symm x))) = E.symm (map f x)
44       rw [E.symm_apply_apply]
45       rfl
46     rw [← hmap, LinearMap.det_conj, ih]
47     exact e.prod_comp (fun i => (f i).det)
48   · intro V _ _ _ f
49     rw [LinearMap.det_eq_one_of_subsingleton]
50     simp
51   · intro α _ ih V _ _ _ f
52     let E := LinearEquiv.piOptionEquivProd k (M := V)
53     have hmap : E.toLinearMap ∘ₗ map f ∘ₗ E.symm.toLinearMap =
54         LinearMap.prodMap (f none) (map (fun i => f (some i))) := by
55       apply LinearMap.ext
56       intro x
57       apply Prod.ext
58       · rfl
59       · rfl
60     have hd := LinearMap.det_conj (map f) E
61     rw [hmap, LinearMap.det_prodMap, ih] at hd
62     rw [← hd, Fintype.prod_option]
63 
64 end PaperXI.FiniteProductDeterminant

Back to source controls