Exactness for monoid algebras

The coefficient-sum augmentation ideal of a monoid algebra is generated by the basis differences single k 1 - 1. For a group algebra, the differences indexed by a generating set already generate it as a left ideal, and over a nontrivial ring this characterises generating sets: single x 1 - 1 lies in the left ideal generated by the differences indexed by s exactly when x lies in the subgroup generated by s. More generally, a homomorphism from a group to a monoid induces a monoid-algebra map whose kernel is generated by the corresponding differences for elements in the kernel of the homomorphism.

These descriptions give the ideal-theoretic exactness of monoid algebras associated to an exact pair of monoid homomorphisms whose middle object is a group. They provide the algebraic input for transporting exact character sequences contravariantly to coordinate rings of diagonalizable groups. The description by generators is the surjectivity half of Lyndon's exact sequence for the relation module of a generating family (TauCeti.MonoidAlgebra.relationModule).

Main declarations

• TauCeti.MonoidAlgebra.augmentation: the coefficient-sum augmentation.
• TauCeti.MonoidAlgebra.ker_augmentation_eq_span: its kernel is generated by basis differences.
• MonoidAlgebra.augmentationLinearMap: the augmentation as an R-linear map, and MonoidAlgebra.quotientKerAugmentationEquiv: the quotient R[K] ⧸ I_K by the augmentation ideal is R, so it has rank one (MonoidAlgebra.finrank_quotient_ker_augmentation), and the model R[K]^n × R[K] ⧸ I_K of n regular and one trivial representation has rank n · #K + 1 (MonoidAlgebra.finrank_pi_prod_quotient_ker_augmentation). These live in the root MonoidAlgebra namespace, where dot notation on the monoid algebra finds them.
• TauCeti.MonoidAlgebra.single_sub_one_mem_span_iff: the left ideal generated by the differences indexed by s contains single x 1 - 1 exactly when x ∈ Subgroup.closure s.
• TauCeti.MonoidAlgebra.ker_augmentation_eq_span_of_closure_eq_top, TauCeti.MonoidAlgebra.ker_augmentation_eq_span_iff: the differences indexed by a set generate the augmentation ideal of a group algebra exactly when the set generates the group.
• TauCeti.MonoidAlgebra.single_sub_one_mem_ker_mapDomainRingHom_iff: over a nontrivial ring, a basis difference lies in the kernel of an induced monoid-algebra map exactly when its index lies in the kernel of the homomorphism.
• TauCeti.MonoidAlgebra.ker_mapDomainRingHom_eq_span: the analogous kernel description for a homomorphism out of a group.
• TauCeti.MonoidAlgebra.map_ker_augmentation_eq_ker_mapDomainRingHom: the resulting exactness statement for ideals.

References

Milne, Algebraic Groups, Theorem 12.9(b), gives the corresponding augmentation and quotient description for group algebras of finitely generated commutative groups over a field. The proofs here use finite support directly and apply to arbitrary coefficient rings and the indicated possibly noncommutative monoids.

noncomputable def TauCeti.MonoidAlgebra.augmentation (R : Type u) [Ring R] (K : Type v) [Monoid K] : MonoidAlgebra R K →+* R

The coefficient-sum augmentation of a monoid algebra. It sends every standard basis element to 1 and acts identically on coefficients.

Equations

• TauCeti.MonoidAlgebra.augmentation R K = MonoidAlgebra.liftNCRingHom (RingHom.id R) 1 ⋯

@[simp]

theorem TauCeti.MonoidAlgebra.augmentation_single (R : Type u) [Ring R] {K : Type v} [Monoid K] (k : K) (r : R) : (augmentation R K) (MonoidAlgebra.single k r) = r

The coefficient-sum augmentation sends a singleton to its coefficient.

@[simp]

theorem TauCeti.MonoidAlgebra.augmentation_comp_mapDomainRingHom (R : Type u) [Ring R] {M : Type v} {N : Type w} [Monoid M] [Monoid N] (f : M →* N) : (augmentation R N).comp (MonoidAlgebra.mapDomainRingHom R f) = augmentation R M

The coefficient-sum augmentation is natural with respect to homomorphisms of monoids.

theorem TauCeti.MonoidAlgebra.single_sub_one_mem_ker_mapDomainRingHom_iff (R : Type u) [Ring R] [Nontrivial R] {M : Type v} {N : Type w} [Monoid M] [Monoid N] (f : M →* N) (m : M) : MonoidAlgebra.single m 1 - 1 ∈ RingHom.ker (MonoidAlgebra.mapDomainRingHom R f) ↔ f m = 1

Over a nontrivial ring, the basis difference single m 1 - 1 lies in the kernel of the monoid-algebra map induced by f exactly when m lies in the kernel of f.

theorem TauCeti.MonoidAlgebra.ker_augmentation_eq_span (R : Type u) [Ring R] (K : Type v) [Monoid K] : RingHom.ker (augmentation R K) = Ideal.span (Set.range fun (k : K) => MonoidAlgebra.single k 1 - 1)

The kernel of the coefficient-sum augmentation is generated by the differences between standard basis elements and the unit basis element.

theorem TauCeti.MonoidAlgebra.single_sub_one_mem_span_of_mem_closure (R : Type u) [Ring R] {G : Type v} [Group G] {s : Set G} {x : G} (hx : x ∈ Subgroup.closure s) : MonoidAlgebra.single x 1 - 1 ∈ Ideal.span ((fun (g : G) => MonoidAlgebra.single g 1 - 1) '' s)

The left ideal generated by the basis differences single g 1 - 1, g ∈ s, contains single x 1 - 1 for every x in the subgroup generated by s.

theorem TauCeti.MonoidAlgebra.single_sub_one_mem_span_iff (R : Type u) [Ring R] {G : Type v} [Group G] [Nontrivial R] {s : Set G} {x : G} : MonoidAlgebra.single x 1 - 1 ∈ Ideal.span ((fun (g : G) => MonoidAlgebra.single g 1 - 1) '' s) ↔ x ∈ Subgroup.closure s

Over a nontrivial ring, single x 1 - 1 lies in the left ideal generated by the basis differences single g 1 - 1, g ∈ s, exactly when x lies in the subgroup generated by s.

theorem TauCeti.MonoidAlgebra.ker_augmentation_eq_span_of_closure_eq_top (R : Type u) [Ring R] {G : Type v} [Group G] {s : Set G} (hs : Subgroup.closure s = ⊤) : RingHom.ker (augmentation R G) = Ideal.span ((fun (g : G) => MonoidAlgebra.single g 1 - 1) '' s)

The kernel of the augmentation of a group algebra is generated, as a left ideal, by the basis differences single g 1 - 1 for g running over any generating set of the group.

theorem TauCeti.MonoidAlgebra.ker_augmentation_eq_span_iff (R : Type u) [Ring R] {G : Type v} [Group G] [Nontrivial R] {s : Set G} : RingHom.ker (augmentation R G) = Ideal.span ((fun (g : G) => MonoidAlgebra.single g 1 - 1) '' s) ↔ Subgroup.closure s = ⊤

Over a nontrivial ring, the basis differences single g 1 - 1, g ∈ s, generate the kernel of the augmentation of a group algebra as a left ideal exactly when s generates the group.

theorem TauCeti.MonoidAlgebra.ker_mapDomainRingHom_eq_span (R : Type u) [Ring R] {G : Type v} {H : Type w} [Group G] [Monoid H] (q : G →* H) : RingHom.ker (MonoidAlgebra.mapDomainRingHom R q) = Ideal.span (Set.range fun (k : ↥q.ker) => MonoidAlgebra.single (↑k) 1 - 1)

If q : G → H is a homomorphism from a group to a monoid, the kernel of the induced monoid-algebra map is generated by the basis differences indexed by ker q.

theorem TauCeti.MonoidAlgebra.map_ker_augmentation_eq_ker_mapDomainRingHom (R : Type u) [Ring R] {L : Type v} {G : Type w} {H : Type x} [Monoid L] [Group G] [Monoid H] (p : L →* G) (q : G →* H) (hexact : MonoidHom.mrange p = MonoidHom.mker q) : Ideal.map (MonoidAlgebra.mapDomainRingHom R p) (RingHom.ker (augmentation R L)) = RingHom.ker (MonoidAlgebra.mapDomainRingHom R q)

An exact pair of monoid homomorphisms whose middle object is a group induces an exact ideal sequence on monoid algebras: the extension of the first augmentation ideal is the kernel of the second induced map.

The augmentation as a linear map, and the trivial module R[K] ⧸ I_K

noncomputable def MonoidAlgebra.augmentationLinearMap (R : Type u) [Ring R] (K : Type v) [Monoid K] : MonoidAlgebra R K →ₗ[R] R

The coefficient-sum augmentation as an R-linear map R[K] → R.

Equations

• MonoidAlgebra.augmentationLinearMap R K = { toFun := ⇑(TauCeti.MonoidAlgebra.augmentation R K), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MonoidAlgebra.augmentationLinearMap_apply (R : Type u) [Ring R] (K : Type v) [Monoid K] (x : MonoidAlgebra R K) : (augmentationLinearMap R K) x = (TauCeti.MonoidAlgebra.augmentation R K) x

theorem MonoidAlgebra.augmentationLinearMap_surjective (R : Type u) [Ring R] (K : Type v) [Monoid K] : Function.Surjective ⇑(augmentationLinearMap R K)

theorem MonoidAlgebra.ker_augmentationLinearMap (R : Type u) [Ring R] (K : Type v) [Monoid K] : (augmentationLinearMap R K).ker = Submodule.restrictScalars R (RingHom.ker (TauCeti.MonoidAlgebra.augmentation R K))

The kernel of the linear augmentation is the augmentation ideal, with scalars restricted.

noncomputable def MonoidAlgebra.quotientKerAugmentationEquiv (R : Type u) [Ring R] (K : Type v) [Monoid K] : (MonoidAlgebra R K ⧸ RingHom.ker (TauCeti.MonoidAlgebra.augmentation R K)) ≃ₗ[R] R

The quotient of R[K] by the augmentation ideal is R, the trivial module.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MonoidAlgebra.quotientKerAugmentationEquiv_mk (R : Type u) [Ring R] (K : Type v) [Monoid K] (x : MonoidAlgebra R K) : (quotientKerAugmentationEquiv R K) ((Ideal.Quotient.mk (RingHom.ker (TauCeti.MonoidAlgebra.augmentation R K))) x) = (TauCeti.MonoidAlgebra.augmentation R K) x

theorem MonoidAlgebra.finrank_quotient_ker_augmentation (R : Type u) [Ring R] (K : Type v) [Monoid K] [StrongRankCondition R] : Module.finrank R (MonoidAlgebra R K ⧸ RingHom.ker (TauCeti.MonoidAlgebra.augmentation R K)) = 1

The quotient of R[K] by the augmentation ideal has rank one over R.

theorem MonoidAlgebra.finrank_pi_prod_quotient_ker_augmentation (R : Type u) [Ring R] (K : Type v) [Monoid K] [StrongRankCondition R] [Finite K] (n : ℕ) : Module.finrank R ((Fin n → MonoidAlgebra R K) × MonoidAlgebra R K ⧸ RingHom.ker (TauCeti.MonoidAlgebra.augmentation R K)) = n * Nat.card K + 1

The model R[K]^n × R[K] ⧸ I_K of n copies of the regular representation and one trivial one has rank n · #K + 1 over R.