AugmentationCoinvariants.lean

1 import PaperXII.AuxiliaryGroupAlgebra
2 import Mathlib.LinearAlgebra.Basis.Basic
3 import Mathlib.LinearAlgebra.Quotient.Basic
4 import Mathlib.LinearAlgebra.Isomorphisms
5 import Mathlib.LinearAlgebra.StdBasis
6 import Mathlib.LinearAlgebra.TensorProduct.Basic
7 
8 set_option autoImplicit false
9 
10 /-! Actual augmentation relations and free coinvariants for an augmented algebra.
11 The algebra may be noncommutative. All quotients are coefficient modules. -/
12 namespace PaperXII.AugmentationCoinvariants
13 
14 open scoped TensorProduct
15 open Module
16 
17 variable {R A M : Type*} [CommRing R] [Ring A] [Algebra R A]
18   [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
19 
20 /-- The module generated by the actual balancing relations. -/
21 def relations (ε : A →ₐ[R] R) : Submodule R M :=
22   Submodule.span R (Set.range fun am : A × M => am.1 • am.2 - ε am.1 • am.2)
23 
24 /-- The actual augmentation ideal acting on the module, with finite linear sums. -/
25 def augmentationSMul (ε : A →ₐ[R] R) : Submodule R M :=
26   Submodule.span R {v | ∃ a : A, ε a = 0 ∧ ∃ m : M, a • m = v}
27 
28 omit [IsScalarTower R A M] in
29 /-- Each balancing difference belongs to the relation submodule. -/
30 theorem relation_mem (ε : A →ₐ[R] R) (a : A) (m : M) :
31     a • m - ε a • m ∈ relations ε :=
32   Submodule.subset_span (Set.mem_range_self (a, m))
33 
34 /-- Balancing relations are exactly the augmentation ideal times the module. -/
35 theorem relations_eq_augmentationSMul (ε : A →ₐ[R] R) :
36     relations (M := M) ε = augmentationSMul ε := by
37   apply le_antisymm
38   · apply Submodule.span_le.mpr
39     rintro v ⟨⟨a,m⟩,rfl⟩
40     apply Submodule.subset_span
41     refine ⟨a - algebraMap R A (ε a), by simp, m, ?_⟩
42     simp [sub_smul]
43   · apply Submodule.span_le.mpr
44     rintro v ⟨a,ha,m,rfl⟩
45     simpa [ha] using relation_mem ε a m
46 
47 /-- Coinvariants as the actual quotient by balancing relations. -/
48 abbrev Coinvariants (ε : A →ₐ[R] R) := M ⧸ relations (M := M) ε
49 
50 /-- The quotient map. -/
51 def mk (ε : A →ₐ[R] R) : M →ₗ[R] Coinvariants (M := M) ε :=
52   (relations ε).mkQ
53 
54 omit [IsScalarTower R A M] in
55 /-- Augmented scalar multiplication becomes coefficient scalar multiplication. -/
56 theorem mk_smul (ε : A →ₐ[R] R) (a : A) (m : M) :
57     mk ε (a • m) = ε a • mk ε m := by
58   rw [← map_smul]
59   exact (Submodule.Quotient.eq _).mpr (relation_mem ε a m)
60 
61 variable {ι : Type*} [Fintype ι]
62 
63 /-- Apply augmentation to every coordinate of a supplied free basis. -/
64 noncomputable def coordinateMap (ε : A →ₐ[R] R) (b : Basis ι A M) :
65     M →ₗ[R] (ι → R) :=
66   (LinearMap.pi fun i => ε.toLinearMap.comp
67     ((LinearMap.proj i).comp (b.equivFun.restrictScalars R).toLinearMap))
68 
69 /-- The coordinate map on an element. -/
70 theorem coordinateMap_apply (ε : A →ₐ[R] R) (b : Basis ι A M) (m : M) (i : ι) :
71     coordinateMap ε b m i = ε (b.equivFun m i) := rfl
72 
73 /-- The coordinate map has the augmented scalar action. -/
74 theorem coordinateMap_smul (ε : A →ₐ[R] R) (b : Basis ι A M) (a : A) (m : M) :
75     coordinateMap ε b (a • m) = ε a • coordinateMap ε b m := by
76   ext i
77   simp [coordinateMap_apply, map_smul, smul_eq_mul]
78 
79 /-- The relation module is exactly the kernel of augmentation on free coordinates. -/
80 theorem ker_coordinateMap (ε : A →ₐ[R] R) (b : Basis ι A M) :
81     LinearMap.ker (coordinateMap ε b) = relations ε := by
82   apply le_antisymm
83   · intro m hm
84     have hz : ∀ i, ε (b.equivFun m i) = 0 := fun i => congrFun hm i
85     rw [← b.sum_equivFun m]
86     apply Submodule.sum_mem
87     intro i _
88     simpa only [hz i, zero_smul, sub_zero] using relation_mem ε (b.equivFun m i) (b i)
89   · apply Submodule.span_le.mpr
90     rintro v ⟨⟨a,m⟩,rfl⟩
91     change coordinateMap ε b (a • m - ε a • m) = 0
92     simp only [map_sub, coordinateMap_smul, map_smul, sub_self]
93 
94 /-- Free coordinate augmentation is onto, including for the empty basis. -/
95 theorem coordinateMap_surjective (ε : A →ₐ[R] R) (b : Basis ι A M) :
96     Function.Surjective (coordinateMap ε b) := by
97   intro y
98   refine ⟨b.equivFun.symm (fun i => algebraMap R A (y i)), ?_⟩
99   ext i
100   change ε (b.equivFun (b.equivFun.symm (fun i => algebraMap R A (y i))) i) = y i
101   rw [b.equivFun.apply_symm_apply]
102   exact ε.commutes (y i)
103 
104 /-- Free coinvariants recover exactly one coefficient coordinate per basis vector. -/
105 noncomputable def freeEquiv (ε : A →ₐ[R] R) (b : Basis ι A M) :
106     Coinvariants (M := M) ε ≃ₗ[R] (ι → R) :=
107   (Submodule.quotEquivOfEq _ _ (ker_coordinateMap ε b).symm).trans
108     ((coordinateMap ε b).quotKerEquivOfSurjective (coordinateMap_surjective ε b))
109 
110 /-- Recovery agrees with augmentation of the original coordinates. -/
111 theorem freeEquiv_mk (ε : A →ₐ[R] R) (b : Basis ι A M) (m : M) :
112     freeEquiv ε b (mk ε m) = coordinateMap ε b m := by
113   simp [freeEquiv, mk]
114 
115 /-- The recovered coefficient module has a basis indexed by the original basis. -/
116 noncomputable def recoveredBasis (ε : A →ₐ[R] R) (b : Basis ι A M) :
117     Basis ι R (Coinvariants (M := M) ε) :=
118   (Pi.basisFun R ι).map (freeEquiv ε b).symm
119 
120 end PaperXII.AugmentationCoinvariants

Back to source controls