The augmentation ideal and the augmentation sequence

For a group G and a commutative ring k, the augmentation k[G] ⟶ k sends a group ring element to the sum of its coefficients, and its kernel I_G is the augmentation ideal, here taken as a representation of G. The augmentation sequence 0 ⟶ I_G ⟶ k[G] ⟶ k ⟶ 0 is short exact, and stays short exact after restriction along any monoid homomorphism.

Nothing here mentions cohomology: the cohomological consequences live in TauCeti.RepresentationTheory.Homological.TateCohomology.Augmentation, which imports this file.

Main definitions

• Rep.augmentation: the augmentation k[G] ⟶ k.
• Rep.augmentationIdeal: the augmentation ideal I_G, the kernel of the augmentation.
• Rep.augmentationSES: the short exact sequence I_G ⟶ k[G] ⟶ k.
• Rep.augmentationιIsKernel: the augmentation ideal is a kernel of the augmentation.
• Rep.augmentationKerIso: the module-theoretic kernel of the group-ring augmentation is the categorical augmentation ideal.

Main statements

• Rep.augmentationSES_shortExact, Rep.augmentationSES_res_shortExact: the augmentation sequence is short exact, also after restriction along a monoid homomorphism.
• TauCeti.AugmentationIdeal.singleSub, TauCeti.AugmentationIdeal.ι_singleSub: an element mapping to [g] a - [1] a and its image under the inclusion.
• TauCeti.AugmentationIdeal.ρ_singleSub, TauCeti.AugmentationIdeal.singleSub_one: the group action and value at the identity.
• TauCeti.AugmentationIdeal.sum_coeff_augmentationι: the coefficients of an augmentation-ideal element sum to zero.

References

• J. S. Milne, Class Field Theory, Chapter II, proof of Theorem 3.11.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (3.1.4).
• The same construction appears in ClassFieldTheory/Cohomology/AugmentationModule.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0); it is reimplemented here on Mathlib's Rep API rather than copied.

@[reducible, inline]

noncomputable abbrev Rep.augmentation (k G : Type u) [CommRing k] [Group G] : leftRegular k G ⟶ trivial k G k

The augmentation k[G] ⟶ k, the map of representations sending a group ring element to the sum of its coefficients; it is the map out of the left regular representation attached to 1 : k.

theorem Rep.augmentation_hom_apply (k G : Type u) [CommRing k] [Group G] (w : MonoidAlgebra k G) : (Hom.hom (augmentation k G)) w = (TauCeti.MonoidAlgebra.augmentation k G) w

The augmentation of representations is the coefficient sum TauCeti.MonoidAlgebra.augmentation.

instance Rep.augmentation_epi (k G : Type u) [CommRing k] [Group G] : CategoryTheory.Epi (augmentation k G)

The augmentation is surjective.

noncomputable def Rep.augmentationIdeal (k G : Type u) [CommRing k] [Group G] : Rep k G

The augmentation ideal I_G, the kernel of the augmentation k[G] ⟶ k, as a representation of G. The body is exposed because the endpoints of the connecting homomorphism built from augmentationSES appear in downstream statement types.

noncomputable def Rep.augmentationι (k G : Type u) [CommRing k] [Group G] : augmentationIdeal k G ⟶ leftRegular k G

The inclusion of the augmentation ideal into the left regular representation.

instance Rep.augmentationι_mono (k G : Type u) [CommRing k] [Group G] : CategoryTheory.Mono (augmentationι k G)

The inclusion of the augmentation ideal is a monomorphism.

@[simp]

theorem Rep.augmentationι_comp_augmentation (k G : Type u) [CommRing k] [Group G] : CategoryTheory.CategoryStruct.comp (augmentationι k G) (augmentation k G) = 0

The inclusion of the augmentation ideal followed by the augmentation is zero.

@[simp]

theorem Rep.augmentationι_comp_augmentation_assoc (k G : Type u) [CommRing k] [Group G] {Z : Rep k G} (h : trivial k G k ⟶ Z) : CategoryTheory.CategoryStruct.comp (augmentationι k G) (CategoryTheory.CategoryStruct.comp (augmentation k G) h) = CategoryTheory.CategoryStruct.comp 0 h

The inclusion of the augmentation ideal followed by the augmentation is zero.

noncomputable def Rep.augmentationιIsKernel (k G : Type u) [CommRing k] [Group G] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (augmentationι k G) ⋯)

The inclusion of the augmentation ideal is a kernel of the augmentation.

noncomputable def Rep.augmentationSES (k G : Type u) [CommRing k] [Group G] : CategoryTheory.ShortComplex (Rep k G)

The augmentation sequence I_G ⟶ k[G] ⟶ k. The body is exposed for the same reason as augmentationIdeal: downstream statements name the endpoints of its connecting homomorphism.

theorem Rep.augmentationSES_def (k G : Type u) [CommRing k] [Group G] : augmentationSES k G = { X₁ := augmentationIdeal k G, X₂ := leftRegular k G, X₃ := trivial k G k, f := augmentationι k G, g := augmentation k G, zero := ⋯ }

The augmentation sequence has maps the inclusion of the augmentation ideal and the augmentation.

@[simp]

theorem Rep.augmentationSES_X₁ (k G : Type u) [CommRing k] [Group G] : (augmentationSES k G).X₁ = augmentationIdeal k G

The first term of the augmentation sequence is the augmentation ideal.

@[simp]

theorem Rep.augmentationSES_X₂ (k G : Type u) [CommRing k] [Group G] : (augmentationSES k G).X₂ = leftRegular k G

The middle term of the augmentation sequence is the left regular representation.

@[simp]

theorem Rep.augmentationSES_X₃ (k G : Type u) [CommRing k] [Group G] : (augmentationSES k G).X₃ = trivial k G k

The last term of the augmentation sequence is the trivial representation on k.

theorem Rep.augmentationSES_shortExact (k G : Type u) [CommRing k] [Group G] : (augmentationSES k G).ShortExact

The augmentation sequence is short exact.

theorem Rep.augmentationSES_res_shortExact (k G : Type u) [CommRing k] [Group G] {H : Type u_1} [Monoid H] (f : H →* G) : ((augmentationSES k G).map (resFunctor f)).ShortExact

The augmentation sequence stays short exact after restriction along any monoid homomorphism f : H →* G.

noncomputable def Rep.augmentationKerIso (k G : Type u) [CommRing k] [Group G] : ofModuleMonoidAlgebra.obj ↧↥(RingHom.ker (TauCeti.MonoidAlgebra.augmentation k G)) ≅ augmentationIdeal k G

The representation attached to the module-theoretic augmentation kernel of k[G] is the categorical augmentation ideal Rep.augmentationIdeal k G.

@[simp]

theorem Rep.augmentationι_augmentationKerIso_hom_apply (k G : Type u) [CommRing k] [Group G] (x : ↑(ofModuleMonoidAlgebra.obj ↧↥(RingHom.ker (TauCeti.MonoidAlgebra.augmentation k G)))) : (Hom.hom (augmentationι k G)) ((CategoryTheory.ConcreteCategory.hom (augmentationKerIso k G).hom) x) = ↑((RestrictScalars.addEquiv k (MonoidAlgebra k G) ↥(RingHom.ker (TauCeti.MonoidAlgebra.augmentation k G))) x)

The augmentation-kernel isomorphism is compatible with the inclusions into the group ring.

noncomputable def TauCeti.AugmentationIdeal.singleSub (k G : Type u) [CommRing k] [Group G] (a : k) (g : G) : ↑(Rep.augmentationIdeal k G)

The element of the augmentation ideal whose image in k[G] is [g] a - [1] a.

@[simp]

theorem TauCeti.AugmentationIdeal.ι_singleSub (k G : Type u) [CommRing k] [Group G] (a : k) (g : G) : (Rep.Hom.hom (Rep.augmentationι k G)) (singleSub k G a g) = MonoidAlgebra.single g a - MonoidAlgebra.single 1 a

The image of singleSub a g under the inclusion into k[G].

theorem TauCeti.AugmentationIdeal.augmentationι_injective (k G : Type u) [CommRing k] [Group G] : Function.Injective ⇑(Rep.Hom.hom (Rep.augmentationι k G))

The inclusion of the augmentation ideal into k[G] is injective.

theorem TauCeti.AugmentationIdeal.ρ_singleSub (k G : Type u) [CommRing k] [Group G] (a : k) (x y : G) : ((Rep.augmentationIdeal k G).ρ x) (singleSub k G a y) = singleSub k G a (x * y) - singleSub k G a x

The action of G on an augmentation ideal element [g] a - [1] a.

@[simp]

theorem TauCeti.AugmentationIdeal.singleSub_one (k G : Type u) [CommRing k] [Group G] (a : k) : singleSub k G a 1 = 0

The augmentation ideal element [1] a - [1] a is zero.

@[simp]

theorem TauCeti.AugmentationIdeal.sum_coeff_augmentationι (k G : Type u) [CommRing k] [Group G] (x : ↑(Rep.augmentationIdeal k G)) : (((Rep.Hom.hom (Rep.augmentationι k G)) x).coeff.sum fun (x : G) (a : k) => a) = 0

The coefficients of an element of the augmentation ideal sum to zero after inclusion in the group ring.