AuxiliaryGroupAlgebra.lean

1 import Mathlib.Algebra.MonoidAlgebra.Basic
2 import Mathlib.RingTheory.Ideal.Quotient.Operations
3 
4 set_option autoImplicit false
5 
6 /-! Paper XII, Proposition 5.1. Actual group-algebra transfer and augmentation.
7 The monoids need not be finite or commutative. -/
8 namespace PaperXII.AuxiliaryGroupAlgebra
9 
10 open scoped MonoidAlgebra
11 
12 variable {R G H K : Type*} [CommRing R] [Monoid G] [Monoid H] [Monoid K]
13 
14 /-- Linear extension of the supplied homomorphism on the group basis. -/
15 noncomputable def transfer (q : G →* H) : R[G] →ₐ[R] R[H] :=
16   MonoidAlgebra.mapDomainAlgHom R R q
17 
18 /-- Transfer on every basis element, including its coefficient. -/
19 theorem transfer_single (q : G →* H) (g : G) (r : R) :
20     transfer q (MonoidAlgebra.single g r) = MonoidAlgebra.single (q g) r := by
21   simp [transfer]
22 
23 /-- The induced transfer is surjective whenever the group map is. -/
24 theorem transfer_surjective (q : G →* H) (hq : Function.Surjective q) :
25     Function.Surjective (transfer (R := R) q) := by
26   intro x
27   obtain ⟨y, hy⟩ := Finsupp.mapDomain_surjective hq x.coeff
28   refine ⟨MonoidAlgebra.ofCoeff y, ?_⟩
29   apply MonoidAlgebra.coeff_injective
30   exact hy
31 
32 /-- Transfer respects identity maps. -/
33 theorem transfer_id : transfer (R := R) (MonoidHom.id G) = AlgHom.id R R[G] := by
34   exact MonoidAlgebra.mapDomainAlgHom_id
35 
36 /-- Transfer respects composition. -/
37 theorem transfer_comp (q : G →* H) (s : H →* K) :
38     transfer (R := R) (s.comp q) = (transfer s).comp (transfer q) := by
39   exact MonoidAlgebra.mapDomainAlgHom_comp q s
40 
41 /-- The actual augmentation sends every group element to one. -/
42 noncomputable def augmentation : R[G] →ₐ[R] R :=
43   MonoidAlgebra.lift R R G 1
44 
45 /-- Augmentation of a basis term is its coefficient. -/
46 theorem augmentation_single (g : G) (r : R) :
47     augmentation (MonoidAlgebra.single g r) = r := by
48   simp [augmentation]
49 
50 /-- Augmentation is split surjective by the coefficient inclusion. -/
51 theorem augmentation_surjective : Function.Surjective (augmentation (R := R) (G := G)) := by
52   intro r
53   exact ⟨MonoidAlgebra.single 1 r, augmentation_single 1 r⟩
54 
55 /-- Augmentation commutes with transfer, as an equality of algebra maps. -/
56 theorem augmentation_transfer (q : G →* H) :
57     (augmentation (R := R)).comp (transfer q) = augmentation := by
58   apply MonoidAlgebra.algHom_ext
59   · intro g
60     simp [AlgHom.comp_apply, transfer_single, augmentation_single]
61   · ext
62 
63 /-- The augmentation ideal is the kernel of the actual augmentation map. -/
64 noncomputable abbrev augmentationIdeal : Ideal (R[G]) :=
65   RingHom.ker (augmentation (R := R) (G := G)).toRingHom
66 
67 /-- Exact quotient identification, valid also for noncommutative group algebras. -/
68 noncomputable def augmentationQuotient :
69     (R[G] ⧸ (augmentationIdeal (R := R) (G := G))) ≃ₐ[R] R :=
70   Ideal.quotientKerAlgEquivOfSurjective (augmentation_surjective (R := R) (G := G))
71 
72 end PaperXII.AuxiliaryGroupAlgebra

Back to source controls