Exactness of the diagonalizable-group functor

A short exact sequence 1 → L → M → N → 1 of commutative groups induces, contravariantly, a short exact sequence of diagonalizable groups

1 → D(N) → D(M) → D(L) → 1,

whose coordinate maps are the group-algebra maps R[L] → R[M] → R[N]. Over a nonzero commutative base ring the converse holds as well, so D reflects exactness (TauCeti.DiagonalizableGroup.isShortExact_mapDomainBialgHom_iff). Neither group needs to be finitely generated, and there is no hypothesis on the characteristic: for instance, for n ≥ 1 the sequence 1 → μₙ → 𝔾ₘ → 𝔾ₘ → 1 given by the n-th power map is the image of 0 → ℤ → ℤ → ℤ/n → 0, so it is short exact also when n is divisible by the characteristic.

The inputs are the faithful flatness of R[L] → R[M] for injective L → M (TauCeti.MonoidAlgebra.faithfullyFlat_mapDomainRingHom_iff) and the ideal-theoretic exactness of group algebras (TauCeti.MonoidAlgebra.map_ker_augmentation_eq_ker_mapDomainRingHom).

Main declarations

• TauCeti.DiagonalizableGroup.isShortExact_mapDomainBialgHom: exact character sequences give short exact sequences of diagonalizable groups.
• TauCeti.DiagonalizableGroup.isShortExact_mapDomainBialgHom_iff: the converse over a nonzero base ring.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.9.

theorem TauCeti.DiagonalizableGroup.isShortExact_mapDomainBialgHom (R : Type u) [CommRing R] {L M N : Type v} [CommGroup L] [CommGroup M] [CommGroup N] (p : L →* M) (q : M →* N) (hp : Function.Injective ⇑p) (hq : Function.Surjective ⇑q) (hpq : p.range = q.ker) : CommHopfAlgCat.IsShortExact (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom R p)) (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom R q))

A short exact sequence 1 → L → M → N → 1 of commutative groups induces a short exact sequence 1 → D(N) → D(M) → D(L) → 1 of diagonalizable groups over every commutative ring.

@[simp]

theorem TauCeti.DiagonalizableGroup.isShortExact_mapDomainBialgHom_iff (R : Type u) [CommRing R] {L M N : Type v} [CommGroup L] [CommGroup M] [CommGroup N] (p : L →* M) (q : M →* N) [Nontrivial R] : CommHopfAlgCat.IsShortExact (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom R p)) (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom R q)) ↔ Function.Injective ⇑p ∧ Function.Surjective ⇑q ∧ p.range = q.ker

Over a nonzero commutative ring, the diagonalizable groups D(N) → D(M) → D(L) form a short exact sequence exactly when 1 → L → M → N → 1 is a short exact sequence of commutative groups.