A finite free group scheme of rank four that is not killed by four

Grothendieck asked whether a finite locally free group scheme of order n is killed by n; Deligne proved that this holds for commutative group schemes. This file formalizes a counterexample in the non-commutative case: an affine group scheme, finite free of rank four over the base ring R = ℤ[a, b] / (a³, b³, a²b + 2), whose fourth power map is not trivial. Note that R is a finite ring of size 2^9 satisfying 4 = 0 but 2 ≠ 0.

The coordinate Hopf algebra of the counterexample is A = R[U, V] / (U² - abU + b²V, V² - a²V), built as a QuadraticAlgebra over the QuadraticAlgebra B := R[V] / (V² - a²V). It is finite free of rank four over R. With lambda = (1 + aU) * (1 + bV), the comultiplication is determined by

• Δ(U) = U ⊗ 1 + lambda ⊗ U,
• Δ(V) = V ⊗ lambda + 1 ⊗ V,

and lambda is group-like (that is, Δ(lambda) = lambda ⊗ lambda). The counit sends both U and V to zero. The nth convolution power of the identity — the coordinate map of the pointwise nth power x ↦ xⁿ of the group scheme — sends U to (1 + lambda + ⋯ + lambdaⁿ⁻¹) · U. For n = 4 this is 2bUV ≠ 0, while the eighth convolution power is the convolution unit (the composite of the counit with the unit map of A) and in particular sends U to 0. In particular the seventh convolution power supplies an antipode, so A is a Hopf algebra, and the associated group scheme has order four but is not killed by four.

Main definitions

• Counterexample.GrothendieckPower.R: the base ring ℤ[a, b] / (a³, b³, a²b + 2).
• Counterexample.GrothendieckPower.A: the coordinate algebra, finite free of rank four over R.
• Counterexample.GrothendieckPower.instHopfAlgebra: the Hopf algebra structure on A.
• Counterexample.GrothendieckPower.powerMap: the n-th convolution power of the identity of A, i.e. the coordinate map of the pointwise n-th power of the group scheme.
• Counterexample.GrothendieckPower.affineGroupScheme: the counterexample as a group object in the opposite of the category of commutative R-algebras, through Mathlib's antiequivalence with commutative Hopf algebras.

Main results

• Counterexample.GrothendieckPower.finrank_A: A has rank four over R. Note that A is also finite and free over R, so A ≅ R⁴ as an R-module.
• Counterexample.GrothendieckPower.powerMap_four_U_ne_zero: the fourth power map is not the convolution unit, since it sends U to 2bUV ≠ 0.
• Counterexample.GrothendieckPower.powerMap_eight: the eighth power map is the convolution unit.
• Counterexample.GrothendieckPower.counterexample: the combined statement: over the nontrivial ring R, the algebra A is finite free of rank four and its fourth power map is not the convolution unit.
• Counterexample.GrothendieckPower.exists_hopfAlgebra_not_killed_by_finrank: the negative answer to Grothendieck's question, spelled out as an existence statement: there is a nontrivial commutative ring and a commutative Hopf algebra, free of finite rank over it, whose convolution power map at the exponent equal to its rank is not the convolution unit.
• Counterexample.GrothendieckPower.orderOf_universalPoint: the universal A-valued point of the group scheme has order exactly eight.
• Counterexample.GrothendieckPower.not_isCocomm: A is not cocommutative, i.e. the group scheme is noncommutative, as forced by Deligne's theorem for commutative group schemes.
• Counterexample.GrothendieckPower.id_pow_affineGroupScheme_four_ne_one: the group-scheme formulation, through Mathlib's antiequivalence between commutative Hopf algebras and affine group schemes: on the corresponding group object in (CommAlgCat R)ᵒᵖ, the pointwise fourth power map — the fourth power 𝟙 _ ^ 4 of the identity in the convolution monoid of endomorphisms — is not the constant-unit endomorphism.

Implementation notes

Nontriviality of the base ring (concretely, 2b ≠ 0 in R) is certified by an explicit model: the regular representation of R on M = ℤ/4 × ℤ/4 × (ℤ/2)⁵, with the actions of a and b given by explicit additive endomorphisms and all relations checked by decide +kernel.

The polynomial identities underlying the comultiplication and the power-map computations are proved once in an arbitrary commutative ring satisfying the relations of R (law_relations_generic, law_lambda_generic, theta_identities_generic) using linear_combination, and then transported along algebra maps.

The generators are given short names in each successive algebra (aB, bB, aA, bA) and in the tensor square (a₁, b₁, u₁, v₁, u₂, v₂, l₁, l₂). These are abbrevs, so that they unfold definitionally; their only purpose is to keep the statements of the polynomial certificates and of the coproduct construction readable.

The construction of this group scheme as well as its formalization were carried out by the AI assistants Codex (OpenAI) and Claude (Anthropic).

References

• F. Oort, J. Tate, Group schemes of prime order: Deligne's proof that a commutative finite locally free group scheme is killed by its order is reproduced in §1, and the question for possibly non-commutative group schemes is raised on p. 5.
• J. Tate, Finite flat group schemes: records the question as open in §3.8.

Tags

group scheme, Hopf algebra, counterexample

An explicit faithful model of the base ring

The base ring R = ℤ[a, b] / (a³, b³, a²b + 2) is nontrivial, but this is not syntactically obvious from its presentation. We certify it by exhibiting an explicit R-module: the regular representation of R on ℤ/4 × ℤ/4 × (ℤ/2)⁵, with a and b acting through explicit commuting additive endomorphisms. All required relations are closed by decide +kernel.

def Counterexample.GrothendieckPower.reduce : ZMod 4 →+* ZMod 2

Reduction modulo 2, as a ring homomorphism ℤ/4 → ℤ/2.

Equations

• Counterexample.GrothendieckPower.reduce = ZMod.castHom Counterexample.GrothendieckPower.reduce._proof_1 (ZMod 2)

def Counterexample.GrothendieckPower.double : ZMod 2 →+ ZMod 4

The additive map ℤ/2 → ℤ/4 sending 1 to 2.

Equations

• Counterexample.GrothendieckPower.double = (ZMod.lift 2) ⟨2 • Int.castAddHom (ZMod 4), Counterexample.GrothendieckPower.double._proof_1⟩

@[simp]

theorem Counterexample.GrothendieckPower.reduce_double (x : ZMod 2) : reduce (double x) = 0

@[simp]

theorem Counterexample.GrothendieckPower.double_reduce (x : ZMod 4) : double (reduce x) = 2 * x

@[reducible, inline]

abbrev Counterexample.GrothendieckPower.M : Type

The additive group ℤ/4 × ℤ/4 × (ℤ/2)⁵, carrier of the regular representation of the base ring R := ℤ[a, b] / (a³, b³, a²b + 2) (and in particular isomorphic to R as an additive group).

Equations

• Counterexample.GrothendieckPower.M = (ZMod 4 × ZMod 4 × (Fin 5 → ZMod 2))

def Counterexample.GrothendieckPower.aEnd : AddMonoid.End M

The additive endomorphism of M realizing multiplication by the generator a (the class of the first variable) of the base ring R = ℤ[a, b] / (a³, b³, a²b + 2), in its regular representation.

Equations

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

def Counterexample.GrothendieckPower.bEnd : AddMonoid.End M

The additive endomorphism of M realizing multiplication by the generator b (the class of the second variable) of the base ring R = ℤ[a, b] / (a³, b³, a²b + 2), in its regular representation.

Equations

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

theorem Counterexample.GrothendieckPower.aEnd_bEnd_comm : aEnd * bEnd = bEnd * aEnd

theorem Counterexample.GrothendieckPower.aEnd_cube : aEnd ^ 3 = 0

theorem Counterexample.GrothendieckPower.bEnd_cube : bEnd ^ 3 = 0

theorem Counterexample.GrothendieckPower.aEnd_sq_mul_bEnd : aEnd ^ 2 * bEnd + 2 = 0

theorem Counterexample.GrothendieckPower.two_mul_bEnd_ne_zero : 2 * bEnd ≠ 0

def Counterexample.GrothendieckPower.WitnessRing : Subring (AddMonoid.End M)

The commutative subring of AddMonoid.End M generated by aEnd and bEnd.

Equations

• Counterexample.GrothendieckPower.WitnessRing = Subring.closure {Counterexample.GrothendieckPower.aEnd, Counterexample.GrothendieckPower.bEnd}

instance Counterexample.GrothendieckPower.instIsMulCommutativeSubtypeEndMMemSubringWitnessRing : IsMulCommutative ↥WitnessRing

def Counterexample.GrothendieckPower.aw : ↥WitnessRing

The element aEnd, as an element of WitnessRing.

Equations

• Counterexample.GrothendieckPower.aw = ⟨Counterexample.GrothendieckPower.aEnd, Counterexample.GrothendieckPower.aw._proof_1⟩

def Counterexample.GrothendieckPower.bw : ↥WitnessRing

The element bEnd, as an element of WitnessRing.

Equations

• Counterexample.GrothendieckPower.bw = ⟨Counterexample.GrothendieckPower.bEnd, Counterexample.GrothendieckPower.bw._proof_1⟩

@[simp]

theorem Counterexample.GrothendieckPower.aw_cube : aw ^ 3 = 0

@[simp]

theorem Counterexample.GrothendieckPower.bw_cube : bw ^ 3 = 0

@[simp]

theorem Counterexample.GrothendieckPower.witness_relation : aw ^ 2 * bw + 2 = 0

theorem Counterexample.GrothendieckPower.two_bw_ne_zero : 2 * bw ≠ 0

instance Counterexample.GrothendieckPower.instNontrivialSubtypeEndMMemSubringWitnessRing : Nontrivial ↥WitnessRing

The base ring R = ℤ[a, b] / (a³, b³, a²b + 2)

@[reducible, inline]

abbrev Counterexample.GrothendieckPower.P : Type

The polynomial ring ℤ[a, b].

Equations

• Counterexample.GrothendieckPower.P = MvPolynomial (Fin 2) ℤ

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.ap : P

The polynomial variable a.

Equations

• Counterexample.GrothendieckPower.ap = MvPolynomial.X 0

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.bp : P

The polynomial variable b.

Equations

• Counterexample.GrothendieckPower.bp = MvPolynomial.X 1

noncomputable def Counterexample.GrothendieckPower.baseIdeal : Ideal P

The ideal (a³, b³, a²b + 2) of ℤ[a, b].

Equations

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

@[reducible, inline]

abbrev Counterexample.GrothendieckPower.R : Type

The base ring R = ℤ[a, b] / (a³, b³, a²b + 2).

Equations

• Counterexample.GrothendieckPower.R = (Counterexample.GrothendieckPower.P ⧸ Counterexample.GrothendieckPower.baseIdeal)

noncomputable def Counterexample.GrothendieckPower.a : R

The class of the variable a in the base ring R.

Equations

• Counterexample.GrothendieckPower.a = (Ideal.Quotient.mk Counterexample.GrothendieckPower.baseIdeal) Counterexample.GrothendieckPower.ap

noncomputable def Counterexample.GrothendieckPower.b : R

The class of the variable b in the base ring R.

Equations

• Counterexample.GrothendieckPower.b = (Ideal.Quotient.mk Counterexample.GrothendieckPower.baseIdeal) Counterexample.GrothendieckPower.bp

@[simp]

theorem Counterexample.GrothendieckPower.a_cube : a ^ 3 = 0

@[simp]

theorem Counterexample.GrothendieckPower.b_cube : b ^ 3 = 0

@[simp]

theorem Counterexample.GrothendieckPower.base_relation : a ^ 2 * b + 2 = 0

def Counterexample.GrothendieckPower.evalWitness : P →+* ↥WitnessRing

Evaluation of integer polynomials at (aw, bw) in WitnessRing.

Equations

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

theorem Counterexample.GrothendieckPower.baseIdeal_le_ker_evalWitness : baseIdeal ≤ RingHom.ker evalWitness

noncomputable def Counterexample.GrothendieckPower.witnessHom : R →+* ↥WitnessRing

The ring map R → WitnessRing, giving an action of R on M.

Equations

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

@[simp]

theorem Counterexample.GrothendieckPower.witnessHom_b : witnessHom b = bw

theorem Counterexample.GrothendieckPower.two_b_ne_zero : 2 * b ≠ 0

instance Counterexample.GrothendieckPower.instNontrivialR : Nontrivial R

The coordinate algebra A = R[U, V] / (U² - abU + b²V, V² - a²V)

The algebra A is realized as two nested QuadraticAlgebras, so that its finite freeness of rank four over R follows from the corresponding facts for each step of the tower.

@[reducible, inline]

abbrev Counterexample.GrothendieckPower.B : Type

The intermediate quadratic algebra B = R[V] / (V² - a²V).

Equations

• Counterexample.GrothendieckPower.B = QuadraticAlgebra Counterexample.GrothendieckPower.R 0 (Counterexample.GrothendieckPower.a ^ 2)

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.VB : B

The generator VB of B, satisfying VB² = a²·VB.

Equations

• Counterexample.GrothendieckPower.VB = QuadraticAlgebra.omega

@[simp]

theorem Counterexample.GrothendieckPower.VB_relation : VB ^ 2 = (algebraMap R B) (a ^ 2) * VB

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.aB : B

The image of a in B.

Equations

• Counterexample.GrothendieckPower.aB = (algebraMap Counterexample.GrothendieckPower.R Counterexample.GrothendieckPower.B) Counterexample.GrothendieckPower.a

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.bB : B

The image of b in B.

Equations

• Counterexample.GrothendieckPower.bB = (algebraMap Counterexample.GrothendieckPower.R Counterexample.GrothendieckPower.B) Counterexample.GrothendieckPower.b

@[reducible, inline]

abbrev Counterexample.GrothendieckPower.A : Type

The coordinate algebra A = B[U] / (U² - abU + b²V) = R[U, V] / (U² - abU + b²V, V² - a²V), finite free of rank four over the base ring R.

Equations

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

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.U : A

The generator U of A, satisfying U² = abU - b²V.

Equations

• Counterexample.GrothendieckPower.U = QuadraticAlgebra.omega

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.V : A

The image V of VB in A.

Equations

• Counterexample.GrothendieckPower.V = (algebraMap Counterexample.GrothendieckPower.B Counterexample.GrothendieckPower.A) Counterexample.GrothendieckPower.VB

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.aA : A

The image aA of a in A.

Equations

• Counterexample.GrothendieckPower.aA = (algebraMap Counterexample.GrothendieckPower.R Counterexample.GrothendieckPower.A) Counterexample.GrothendieckPower.a

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.bA : A

The image bA of b in A.

Equations

• Counterexample.GrothendieckPower.bA = (algebraMap Counterexample.GrothendieckPower.R Counterexample.GrothendieckPower.A) Counterexample.GrothendieckPower.b

@[simp]

theorem Counterexample.GrothendieckPower.U_relation : U ^ 2 = (algebraMap R A) (a * b) * U - (algebraMap R A) (b ^ 2) * V

@[simp]

theorem Counterexample.GrothendieckPower.V_relation : V ^ 2 = (algebraMap R A) (a ^ 2) * V

instance Counterexample.GrothendieckPower.instFreeRA : Module.Free R A

instance Counterexample.GrothendieckPower.instFiniteRA : Module.Finite R A

theorem Counterexample.GrothendieckPower.finrank_B : Module.finrank R B = 2

theorem Counterexample.GrothendieckPower.finrank_A_over_B : Module.finrank B A = 2

theorem Counterexample.GrothendieckPower.finrank_A : Module.finrank R A = 4

The universal property of A

An R-algebra map out of A = R[U, V] / (U² - abU + b²V, V² - a²V) amounts to a pair of elements of the target satisfying the two defining relations. The construction goes through the tower R → B → A: the image of V determines an R-algebra map out of B = R[V] / (V² - a²V), which makes the target a B-algebra, and the image of U then determines a quadratic lift out of A. The B-algebra structure depends on the chosen image of V, so it is kept local to the construction and never becomes an instance: the coproduct below, for example, uses a B-algebra structure on A ⊗[R] A different from the canonical one through the left tensor factor.

noncomputable def Counterexample.GrothendieckPower.mkAlgHomB {S : Type u_1} [CommRing S] [Algebra R S] (v : S) (hv : v ^ 2 = (algebraMap R S) (a ^ 2) * v) : B →ₐ[R] S

The R-algebra map B →ₐ[R] S sending VB to a root of X² - a²X.

Equations

• Counterexample.GrothendieckPower.mkAlgHomB v hv = QuadraticAlgebra.lift ⟨v, ⋯⟩

theorem Counterexample.GrothendieckPower.mkAlgHomB_VB {S : Type u_1} [CommRing S] [Algebra R S] (v : S) (hv : v ^ 2 = (algebraMap R S) (a ^ 2) * v) : (mkAlgHomB v hv) VB = v

noncomputable def Counterexample.GrothendieckPower.mkAlgHom {S : Type u_1} [CommRing S] [Algebra R S] (u v : S) (hv : v ^ 2 = (algebraMap R S) (a ^ 2) * v) (hu : u ^ 2 = (algebraMap R S) (a * b) * u - (algebraMap R S) (b ^ 2) * v) : A →ₐ[R] S

If S is an arbitrary R-algebra, then to give an R-algebra map A →ₐ[R] S it suffices to give a pair of elements u and v in S satisfying the equations v²=a²v and u²=abu-b²v.

Equations

• Counterexample.GrothendieckPower.mkAlgHom u v hv hu = AlgHom.restrictScalars Counterexample.GrothendieckPower.R (QuadraticAlgebra.lift ⟨u, ⋯⟩)

theorem Counterexample.GrothendieckPower.mkAlgHom_U {S : Type u_1} [CommRing S] [Algebra R S] {u v : S} (hv : v ^ 2 = (algebraMap R S) (a ^ 2) * v) (hu : u ^ 2 = (algebraMap R S) (a * b) * u - (algebraMap R S) (b ^ 2) * v) : (mkAlgHom u v hv hu) U = u

theorem Counterexample.GrothendieckPower.mkAlgHom_V {S : Type u_1} [CommRing S] [Algebra R S] {u v : S} (hv : v ^ 2 = (algebraMap R S) (a ^ 2) * v) (hu : u ^ 2 = (algebraMap R S) (a * b) * u - (algebraMap R S) (b ^ 2) * v) : (mkAlgHom u v hv hu) V = v

The comultiplication

The polynomial identities behind the coproduct are proved once, in an arbitrary commutative ring whose distinguished elements satisfy the relations of R, by linear_combination certificates; they are then transported to the tensor square along the two inclusions.

noncomputable def Counterexample.GrothendieckPower.lambda : A

The group-like unit (1+aU)(1+bV) of A controlling the semidirect-product law.

Equations

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

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.left : A →ₐ[R] TensorProduct R A A

The inclusion of the left tensor factor A → A ⊗[R] A.

Equations

• Counterexample.GrothendieckPower.left = Algebra.TensorProduct.includeLeft

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.right : A →ₐ[R] TensorProduct R A A

The inclusion of the right tensor factor A → A ⊗[R] A.

Equations

• Counterexample.GrothendieckPower.right = Algebra.TensorProduct.includeRight

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.a₁ : TensorProduct R A A

The image of a in A ⊗[R] A.

Equations

• Counterexample.GrothendieckPower.a₁ = Counterexample.GrothendieckPower.left Counterexample.GrothendieckPower.aA

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.b₁ : TensorProduct R A A

The image of b in A ⊗[R] A.

Equations

• Counterexample.GrothendieckPower.b₁ = Counterexample.GrothendieckPower.left Counterexample.GrothendieckPower.bA

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.u₁ : TensorProduct R A A

The element U ⊗ₜ 1 in A ⊗ A.

Equations

• Counterexample.GrothendieckPower.u₁ = Counterexample.GrothendieckPower.left Counterexample.GrothendieckPower.U

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.v₁ : TensorProduct R A A

The element V ⊗ₜ 1 in A ⊗ A.

Equations

• Counterexample.GrothendieckPower.v₁ = Counterexample.GrothendieckPower.left Counterexample.GrothendieckPower.V

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.u₂ : TensorProduct R A A

The element 1 ⊗ₜ U in A ⊗ A.

Equations

• Counterexample.GrothendieckPower.u₂ = Counterexample.GrothendieckPower.right Counterexample.GrothendieckPower.U

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.v₂ : TensorProduct R A A

The element 1 ⊗ₜ V in A ⊗ A.

Equations

• Counterexample.GrothendieckPower.v₂ = Counterexample.GrothendieckPower.right Counterexample.GrothendieckPower.V

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.l₁ : TensorProduct R A A

The element λ ⊗ₜ 1 = (1+aU)(1+bV) ⊗ₜ 1 in A ⊗ A.

Equations

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

@[reducible, inline]

noncomputable abbrev Counterexample.GrothendieckPower.l₂ : TensorProduct R A A

The element 1 ⊗ₜ λ = 1 ⊗ₜ (1+aU)(1+bV) in A ⊗ A.

Equations

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

noncomputable def Counterexample.GrothendieckPower.deltaV : TensorProduct R A A

The element δ_V := V ⊗ₜ λ + 1 ⊗ₜ V which will be the image of V under the comultiplication on A.

Equations

• Counterexample.GrothendieckPower.deltaV = Counterexample.GrothendieckPower.v₁ * Counterexample.GrothendieckPower.l₂ + Counterexample.GrothendieckPower.v₂

noncomputable def Counterexample.GrothendieckPower.deltaU : TensorProduct R A A

The element δ_U := U ⊗ₜ 1 + λ ⊗ₜ U which will be the image of U under the comultiplication on A.

Equations

• Counterexample.GrothendieckPower.deltaU = Counterexample.GrothendieckPower.u₁ + Counterexample.GrothendieckPower.l₁ * Counterexample.GrothendieckPower.u₂

noncomputable def Counterexample.GrothendieckPower.comul : A →ₐ[R] TensorProduct R A A

The coproduct algebra homomorphism, sending U to δ_U and V to δ_V.

Equations

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

theorem Counterexample.GrothendieckPower.comul_U : comul U = deltaU

theorem Counterexample.GrothendieckPower.comul_V : comul V = deltaV

theorem Counterexample.GrothendieckPower.comul_aA : comul aA = a₁

theorem Counterexample.GrothendieckPower.comul_bA : comul bA = b₁

theorem Counterexample.GrothendieckPower.left_lambda : left lambda = l₁

theorem Counterexample.GrothendieckPower.right_lambda : right lambda = l₂

@[simp]

theorem Counterexample.GrothendieckPower.comul_lambda : comul lambda = left lambda * right lambda

@[simp]

theorem Counterexample.GrothendieckPower.comul_U_formula : comul U = left U + left lambda * right U

@[simp]

theorem Counterexample.GrothendieckPower.comul_V_formula : comul V = left V * right lambda + right V

theorem Counterexample.GrothendieckPower.algHom_ext {S : Type u_1} [Semiring S] [Algebra R S] {f g : A →ₐ[R] S} (hU : f U = g U) (hv : f V = g V) : f = g

Two R-algebra maps out of A agree if they agree on U and V.

The counit and the bialgebra structure

noncomputable def Counterexample.GrothendieckPower.counit : A →ₐ[R] R

The counit algebra homomorphism, sending U and V to zero.

Equations

• Counterexample.GrothendieckPower.counit = Counterexample.GrothendieckPower.mkAlgHom 0 0 Counterexample.GrothendieckPower.counit._proof_1 Counterexample.GrothendieckPower.counit._proof_2

@[simp]

theorem Counterexample.GrothendieckPower.counit_V : counit V = 0

@[simp]

theorem Counterexample.GrothendieckPower.counit_U : counit U = 0

@[simp]

theorem Counterexample.GrothendieckPower.counit_lambda : counit lambda = 1

theorem Counterexample.GrothendieckPower.comul_coassoc : (↑(Algebra.TensorProduct.assoc R R R A A A)).comp ((Algebra.TensorProduct.map comul (AlgHom.id R A)).comp comul) = (Algebra.TensorProduct.map (AlgHom.id R A) comul).comp comul

theorem Counterexample.GrothendieckPower.counit_left : (Algebra.TensorProduct.map counit (AlgHom.id R A)).comp comul = ↑(Algebra.TensorProduct.lid R A).symm

theorem Counterexample.GrothendieckPower.counit_right : (Algebra.TensorProduct.map (AlgHom.id R A) counit).comp comul = ↑(Algebra.TensorProduct.rid R R A).symm

@[instance_reducible]

noncomputable instance Counterexample.GrothendieckPower.instBialgebra : Bialgebra R A

The bialgebra structure underlying the counterexample.

Equations

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

theorem Counterexample.GrothendieckPower.isGroupLikeElem_lambda : IsGroupLikeElem R lambda

The coordinate lambda is a group-like element of A.

The convolution power maps

The n-th power map of the group scheme (pointwise x ↦ xⁿ) corresponds, on coordinate rings, to the nth convolution power of the identity of A. On the skew-primitive coordinates it is controlled by the geometric sum 1 + lambda + ⋯ + lambdaⁿ⁻¹, which we compute from the square-zero element theta = lambda - 1.

noncomputable def Counterexample.GrothendieckPower.theta : A

The square-zero part of the group-like coordinate.

Equations

• Counterexample.GrothendieckPower.theta = Counterexample.GrothendieckPower.lambda - 1

theorem Counterexample.GrothendieckPower.theta_sq : theta ^ 2 = 0

theorem Counterexample.GrothendieckPower.two_theta : 2 * theta = 2 * bA * V

noncomputable def Counterexample.GrothendieckPower.universalPoint : WithConv (A →ₐ[R] A)

The universal point, in the convolution monoid of R-algebra endomorphisms.

Equations

• Counterexample.GrothendieckPower.universalPoint = WithConv.toConv (AlgHom.id Counterexample.GrothendieckPower.R Counterexample.GrothendieckPower.A)

noncomputable def Counterexample.GrothendieckPower.powerMap (n : ℕ) : A →ₐ[R] A

The nth convolution power of the identity of A: the coordinate ring map of the pointwise nth power map of the group scheme.

Equations

• Counterexample.GrothendieckPower.powerMap n = (Counterexample.GrothendieckPower.universalPoint ^ n).ofConv

@[simp]

theorem Counterexample.GrothendieckPower.powerMap_zero_apply (x : A) : (powerMap 0) x = (algebraMap R A) (counit x)

@[simp]

theorem Counterexample.GrothendieckPower.powerMap_one_apply (x : A) : (powerMap 1) x = x

theorem Counterexample.GrothendieckPower.powerMap_succ_U (n : ℕ) : (powerMap (n + 1)) U = (powerMap n) U + (powerMap n) lambda * U

theorem Counterexample.GrothendieckPower.powerMap_succ_V (n : ℕ) : (powerMap (n + 1)) V = (powerMap n) V * lambda + V

theorem Counterexample.GrothendieckPower.powerMap_succ_lambda (n : ℕ) : (powerMap (n + 1)) lambda = (powerMap n) lambda * lambda

theorem Counterexample.GrothendieckPower.four_eq_zero : 4 = 0

theorem Counterexample.GrothendieckPower.lambda_eq_one_add_theta : lambda = 1 + theta

theorem Counterexample.GrothendieckPower.lambda_pow_four : lambda ^ 4 = 1

theorem Counterexample.GrothendieckPower.powerMap_lambda (n : ℕ) : (powerMap n) lambda = lambda ^ n

theorem Counterexample.GrothendieckPower.powerMap_U (n : ℕ) : (powerMap n) U = (∑ i ∈ Finset.range n, lambda ^ i) * U

theorem Counterexample.GrothendieckPower.powerMap_V (n : ℕ) : (powerMap n) V = V * ∑ i ∈ Finset.range n, lambda ^ i

theorem Counterexample.GrothendieckPower.geom_sum_four : ∑ i ∈ Finset.range 4, lambda ^ i = 2 * bA * V

theorem Counterexample.GrothendieckPower.powerMap_four_U : (powerMap 4) U = 2 * bA * U * V

theorem Counterexample.GrothendieckPower.two_b_U_V_ne_zero : 2 * bA * U * V ≠ 0

theorem Counterexample.GrothendieckPower.powerMap_four_U_ne_zero : (powerMap 4) U ≠ 0

theorem Counterexample.GrothendieckPower.powerMap_four_V : (powerMap 4) V = 0

theorem Counterexample.GrothendieckPower.geom_sum_eight : ∑ i ∈ Finset.range 8, lambda ^ i = 0

theorem Counterexample.GrothendieckPower.powerMap_eight_U : (powerMap 8) U = 0

theorem Counterexample.GrothendieckPower.powerMap_eight_V : (powerMap 8) V = 0

theorem Counterexample.GrothendieckPower.powerMap_eight : powerMap 8 = (Algebra.ofId R A).comp counit

theorem Counterexample.GrothendieckPower.universalPoint_pow_eight : universalPoint ^ 8 = 1

theorem Counterexample.GrothendieckPower.universalPoint_pow_four_ne_one : universalPoint ^ 4 ≠ 1

theorem Counterexample.GrothendieckPower.orderOf_universalPoint : orderOf universalPoint = 8

In the group of A-valued points of the group scheme, the universal point has order exactly eight: an element of order eight on a group scheme of order four.

The Hopf algebra structure and the main statement

Since the eighth convolution power of the identity is the convolution unit, the seventh convolution power is a two-sided convolution inverse of the identity, that is, an antipode.

theorem Counterexample.GrothendieckPower.antipode_right_identity : (Algebra.TensorProduct.lift (powerMap 7) (AlgHom.id R A) ⋯).comp (Bialgebra.comulAlgHom R A) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A)

theorem Counterexample.GrothendieckPower.antipode_left_identity : (Algebra.TensorProduct.lift (AlgHom.id R A) (powerMap 7) ⋯).comp (Bialgebra.comulAlgHom R A) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A)

@[instance_reducible]

noncomputable instance Counterexample.GrothendieckPower.instHopfAlgebra : HopfAlgebra R A

The Hopf R-algebra structure on A.

Equations

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

noncomputable def Counterexample.GrothendieckPower.coordinateHopfAlgebra : CommHopfAlgCat R

The bundled commutative Hopf algebra representing the affine group scheme.

Equations

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

theorem Counterexample.GrothendieckPower.counterexample : Nontrivial R ∧ Module.Free R A ∧ Module.Finite R A ∧ Module.finrank R A = 4 ∧ powerMap 4 ≠ (Algebra.ofId R A).comp counit

The formal counterexample: over the nontrivial base ring R, the commutative Hopf algebra A is finite free of rank four, and its fourth power map is not the convolution unit.

The freeness and finiteness conjuncts guarantee that the Module.finrank conjunct expresses the honest rank of A over R.

theorem Counterexample.GrothendieckPower.exists_hopfAlgebra_not_killed_by_finrank : ∃ (S : Type) (x : CommRing S) (_ : Nontrivial S) (H : Type) (x_2 : CommRing H) (x_3 : HopfAlgebra S H) (_ : Module.Free S H) (_ : Module.Finite S H), 0 < Module.finrank S H ∧ WithConv.toConv (AlgHom.id S H) ^ Module.finrank S H ≠ 1

Grothendieck's question has a negative answer. Grothendieck asked whether every finite locally free group scheme of order n is killed by n — equivalently, whether the n-th convolution power of the identity of a commutative Hopf algebra that is free of rank n over the base ring is always the convolution unit 1 (the composite of the counit with the unit). This is false: there is a nontrivial commutative ring S and a commutative S-Hopf algebra H, free of finite rank over S, whose (Module.finrank S H)-th convolution power of the identity is not the convolution unit. The witness is the rank-four Hopf algebra A over R; see counterexample.

Non-cocommutativity

By Deligne's theorem, a commutative finite locally free group scheme is killed by its order, so the group scheme represented by A is necessarily noncommutative; equivalently, A is not cocommutative. We verify this directly: the coefficient functional of U distinguishes Δ(U) from its swap.

theorem Counterexample.GrothendieckPower.not_isCocomm : ¬Coalgebra.IsCocomm R A

The Hopf algebra A is not cocommutative; equivalently, the affine group scheme it represents is noncommutative. This is forced by Deligne's theorem, which affirms Grothendieck's question for commutative group schemes.

The group-scheme formulation

Mathlib's antiequivalence commHopfAlgCatEquivCogrpCommAlgCat identifies commutative Hopf algebras over R with group objects in (CommAlgCat R)ᵒᵖ, the opposite of the category of commutative R-algebras. This opposite category is the category of affine schemes over R (via the Spec antiequivalence), so these group objects are exactly the affine group schemes over R; here the group object is op A, the algebraic incarnation of Spec A. We work entirely on the algebra side and do not use AlgebraicGeometry.Spec, as Mathlib does not yet connect commutative Hopf algebras to group objects in AlgebraicGeometry.Scheme. This section transports the counterexample across that equivalence: the pointwise fourth power map of the resulting group object is not the constant-unit endomorphism.

theorem Counterexample.GrothendieckPower.id_pow_op_unop_hom (n : ℕ) : CommAlgCat.Hom.hom (CategoryTheory.CategoryStruct.id (Opposite.op (CommAlgCat.of R A)) ^ n).unop = powerMap n

On the group object op A in (CommAlgCat R)ᵒᵖ — the affine group scheme corresponding to A — the pointwise n-th power map 𝟙 _ ^ n (the n-th power of the identity in the convolution monoid CategoryTheory.Hom.monoid of endomorphisms; for a group scheme, the morphism x ↦ xⁿ, which is not in general a homomorphism) corresponds to the n-th convolution power of the identity of A.

theorem Counterexample.GrothendieckPower.id_pow_op_four_ne_one : CategoryTheory.CategoryStruct.id (Opposite.op (CommAlgCat.of R A)) ^ 4 ≠ 1

The pointwise fourth power map of the group object op A in (CommAlgCat R)ᵒᵖ — the affine group scheme corresponding to A — is not the constant-unit endomorphism 1.

noncomputable def Counterexample.GrothendieckPower.affineGroupScheme : CategoryTheory.Grp (CommAlgCat R)ᵒᵖ

The rank-four counterexample as an affine group scheme: the group object in the opposite of the category of commutative R-algebras corresponding to coordinateHopfAlgebra under Mathlib's antiequivalence commHopfAlgCatEquivCogrpCommAlgCat.

Equations

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

theorem Counterexample.GrothendieckPower.affineGroupScheme_X : affineGroupScheme.X = Opposite.op (CommAlgCat.of R A)

theorem Counterexample.GrothendieckPower.id_pow_affineGroupScheme_four_ne_one : CategoryTheory.CategoryStruct.id affineGroupScheme.X ^ 4 ≠ 1

The order-four affine group scheme corresponding to A (the group object in (CommAlgCat R)ᵒᵖ) is not killed by four: its pointwise fourth power map — the fourth power of the identity in the convolution monoid of endomorphisms — is not the constant-unit endomorphism 1.