The spectrum of a group algebra functor

We show that, for a field k, G ↦ Spec k[G] forms a fully faithful functor from commutative groups to group schemes over Spec k.

@[reducible, inline]

noncomputable abbrev specCommGrpAlgebra (R : CommRingCat) : CategoryTheory.Functor CommGrpᵒᵖ (Grp_ (CategoryTheory.Over (AlgebraicGeometry.Spec R)))

The diagonalizable group scheme functor.

Equations

• specCommGrpAlgebra R = (commGrpAlgebra ↑R).comp (hopfSpec R)

noncomputable def specCommGrpAlgebra.fullyFaithful {k : Type u_1} [Field k] : (specCommGrpAlgebra (CommRingCat.of k)).FullyFaithful

The diagonalizable group scheme functor over a field is fully faithful.

Equations

• specCommGrpAlgebra.fullyFaithful = commGrpAlgebra.fullyFaithful.comp hopfSpec.fullyFaithful

instance specCommGrpAlgebra.instFull {k : Type u_1} [Field k] : (specCommGrpAlgebra (CommRingCat.of k)).Full

instance specCommGrpAlgebra.instFaithful {k : Type u_1} [Field k] : (specCommGrpAlgebra (CommRingCat.of k)).Faithful