The spectrum of a group algebra functor

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

@[reducible, inline]

noncomputable abbrev specCommMonAlg (R : CommRingCat) : CategoryTheory.Functor CommMonCatᵒᵖ (Mon_ (CategoryTheory.Over (AlgebraicGeometry.Spec R)))

The diagonalizable monoid scheme functor.

Equations

• specCommMonAlg R = (commMonAlg ↑R).comp (bialgSpec R)

@[reducible, inline]

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

The diagonalizable group scheme functor.

Equations

• specCommGrpAlg R = (commGrpAlg ↑R).comp (hopfSpec R)

noncomputable def specCommGrpAlg.fullyFaithful {R : CommRingCat} [IsDomain ↑R] : (specCommGrpAlg (CommRingCat.of ↑R)).FullyFaithful

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

Equations

• specCommGrpAlg.fullyFaithful = commGrpAlg.fullyFaithful.comp hopfSpec.fullyFaithful

instance specCommGrpAlg.instFull {R : CommRingCat} [IsDomain ↑R] : (specCommGrpAlg (CommRingCat.of ↑R)).Full

instance specCommGrpAlg.instFaithful {R : CommRingCat} [IsDomain ↑R] : (specCommGrpAlg (CommRingCat.of ↑R)).Faithful