feat(Counterexamples): a finite free group scheme of order four not killed by four#41748
Conversation
…illed by four Add a counterexample to Grothendieck's question of whether a finite locally free group scheme of order n is killed by n. Deligne proved this holds for commutative group schemes; this file gives a non-commutative counterexample. Over R = ℤ[a,b]/(a³,b³,a²b+2), the rank-four free Hopf algebra A = R[U,V]/(U²-abU+b²V, V²-a²V) has a group scheme of order four whose fourth convolution power map is not the convolution unit (it sends U to 2bUV ≠ 0), while the eighth power map is the unit. Disclosure: the construction of this group scheme and its formalization were carried out with the AI assistants Codex (OpenAI) and Claude (Anthropic), under the direction of the author. This is also stated in the module docstring.
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary d223a56548Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
metakunt
added
the
LLM-generated
|
I'm surprised that you are neither using https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/AffineScheme.html#AlgebraicGeometry.AffineScheme or https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/Scheme.html#AlgebraicGeometry.Scheme. Can this be proven using the API already in mathlib? |
Address review feedback: the docstrings referred to `Spec A`, but the file works entirely on the algebra side and never uses `AlgebraicGeometry.Spec`. Reword them to name the actual object (the group object `op A` in `(CommAlgCat R)ᵒᵖ`) and explain the identification with the affine group scheme, noting that Mathlib does not yet connect commutative Hopf algebras to group objects in `AlgebraicGeometry.Scheme`.
| noncomputable instance : IsScalarTower R B B where | ||
| smul_assoc r x y := by | ||
| change (r • x) * y = r • (x * y) | ||
| rw [Algebra.smul_def r x, Algebra.smul_def r (x * y)] | ||
| exact mul_assoc _ _ _ |
Address review feedback: the hand-written `IsScalarTower R B B` (and, it turns out, three more) are already provided by Mathlib. The `R B B` and `R A A` towers follow from the general `IsScalarTower.right`, and the `R B A` tower and `SMulCommClass R A A` follow from `QuadraticAlgebra`'s component-wise instances. Only the explicit `Algebra R A` construction is kept.
riccardobrasca
left a comment
riccardobrasca
left a comment
There was a problem hiding this comment.
I think you can ask your LLM to try to use grind as much as possible, it should simplify a couple of proofs.
| change (algebraMap B A V) ^ 2 = algebraMap R A (a ^ 2) * algebraMap B A V | ||
| rw [← map_pow, V_relation, map_mul, IsScalarTower.algebraMap_apply R B A] | ||
|
|
||
| instance : Nontrivial B := |
There was a problem hiding this comment.
Various instances about QuadraticAlgebra should be available in general. For example we have QuadraticAlgebra.instNontrivial, so it is enough enough to add Nontrivial R.
| simp only [hu₁, hu₂, hv₁, hb, h4] | ||
| ring_nf | ||
| simp only [hv₁, ha, hb, h4] | ||
| linear_combination |
|
I think it makes sense to wait for #40500 to be merged, as then one can probably write a cleaner statement. Maybe making this PR depending on #40500 is a good idea? cc @YaelDillies |
Add `exists_hopfAlgebra_not_killed_by_finrank`, an existence statement that spells out the negative answer to Grothendieck's question directly: there is a nontrivial commutative ring and a commutative Hopf algebra, free of finite rank, whose convolution power map at the exponent equal to its rank is not the convolution unit. Also address reviewer feedback: * `reduce` is now a `RingHom` (`ZMod.castHom` directly) rather than an `AddMonoidHom`; * clarify in the `aEnd`/`bEnd` docstrings that `a`, `b` are the two generators of the base ring; * state `aEnd_bEnd_comm` as `Commute`; * use hypothesis binders instead of `∀ ∈` in `generators_commute`; * drop the hand-written `Nontrivial B`/`Nontrivial A` instances, which follow from `QuadraticAlgebra.instNontrivial` and `Nontrivial R`; * make `ap`, `bp` abbreviations.
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on:
|
|
@j2d9w5xtjn-png can you please mark "resolved" the comments that are taken into account? Thanks! |
Following riccardobrasca's review: definitions that are just an existing object (`QuadraticAlgebra.omega`, an `algebraMap` image) are turned into `abbrev`s, so no unfolding is needed. `a` and `b` are kept as `def`, since making them reducible unfolds them to `Ideal.Quotient.mk baseIdeal _` and prevents the `a_cube`/`b_cube`/`base_relation` simp lemmas from matching. The now-redundant `rfl` in `algHom_ext` is removed.
riccardobrasca
left a comment
riccardobrasca
left a comment
There was a problem hiding this comment.
I have to stop now, I will finish the review later.
I am also thinking about a generalization of your construction, there is maybe a nice little construction here.
| private theorem r_smul_mul (r : R) (x y : A) : r • x * y = r • (x * y) := by | ||
| ext <;> simp [V, aB, bB, pow_two] | ||
|
|
||
| noncomputable instance : Algebra R A := |
There was a problem hiding this comment.
This is already in mathlib as QuadraticAlgebra.instAlgebra. Having it here creates a diamond. I think you can just remove it and add
instance : IsScalarTower R B A :=
IsScalarTower.of_algebraMap_eq (R := R) (S := B) (A := A) fun _ ↦ rfl|
|
||
| /-- The pointwise `n`-th power map of a monoid object in a cartesian monoidal category. For | ||
| a group scheme, this is the morphism `x ↦ xⁿ`, which is not in general a homomorphism. -/ | ||
| def monPowMap {C : Type*} [Category C] [CartesianMonoidalCategory C] (M : C) [MonObj M] : |
There was a problem hiding this comment.
You can just use CategoryTheory.Hom.monoid and the usual power.
| calc | ||
| comulB aB = algebraMap R (A ⊗[R] A) a := comulB.commutes a | ||
| _ = a • (1 : A ⊗[R] A) := Algebra.algebraMap_eq_smul_one a | ||
| _ = aaT := aaT_smul.symm |
There was a problem hiding this comment.
| calc | |
| comulB aB = algebraMap R (A ⊗[R] A) a := comulB.commutes a | |
| _ = a • (1 : A ⊗[R] A) := Algebra.algebraMap_eq_smul_one a | |
| _ = aaT := aaT_smul.symm | |
| rw [comulB.commutes, Algebra.algebraMap_eq_smul_one, ← aaT_smul] |
| calc | ||
| comulB bB = algebraMap R (A ⊗[R] A) b := comulB.commutes b | ||
| _ = b • (1 : A ⊗[R] A) := Algebra.algebraMap_eq_smul_one b | ||
| _ = bbT := bbT_smul.symm |
There was a problem hiding this comment.
| calc | |
| comulB bB = algebraMap R (A ⊗[R] A) b := comulB.commutes b | |
| _ = b • (1 : A ⊗[R] A) := Algebra.algebraMap_eq_smul_one b | |
| _ = bbT := bbT_smul.symm | |
| rw [comulB.commutes, Algebra.algebraMap_eq_smul_one, ← bbT_smul] |
| have hc : comulB (-(bB ^ 2) * V) = -(bbT ^ 2) * deltaV := by | ||
| have hn : comulB (-(bB ^ 2)) = -(comulB bB ^ 2) := by | ||
| calc | ||
| comulB (-(bB ^ 2)) = -comulB (bB ^ 2) := comulB_neg _ | ||
| _ = -(comulB bB ^ 2) := congr_arg Neg.neg comulB_bB_sq | ||
| calc | ||
| comulB (-(bB ^ 2) * V) = comulB (-(bB ^ 2)) * comulB V := comulB.map_mul _ _ | ||
| _ = -(comulB bB ^ 2) * comulB V := by rw [hn] | ||
| _ = -(bbT ^ 2) * deltaV := by rw [comulB_bB, comulB_V] | ||
| have hl : comulB (aB * bB) = aaT * bbT := by | ||
| calc | ||
| comulB (aB * bB) = comulB aB * comulB bB := comulB.map_mul _ _ | ||
| _ = aaT * bbT := by rw [comulB_aB, comulB_bB] | ||
| rw [hc, hl] |
There was a problem hiding this comment.
| have hc : comulB (-(bB ^ 2) * V) = -(bbT ^ 2) * deltaV := by | |
| have hn : comulB (-(bB ^ 2)) = -(comulB bB ^ 2) := by | |
| calc | |
| comulB (-(bB ^ 2)) = -comulB (bB ^ 2) := comulB_neg _ | |
| _ = -(comulB bB ^ 2) := congr_arg Neg.neg comulB_bB_sq | |
| calc | |
| comulB (-(bB ^ 2) * V) = comulB (-(bB ^ 2)) * comulB V := comulB.map_mul _ _ | |
| _ = -(comulB bB ^ 2) * comulB V := by rw [hn] | |
| _ = -(bbT ^ 2) * deltaV := by rw [comulB_bB, comulB_V] | |
| have hl : comulB (aB * bB) = aaT * bbT := by | |
| calc | |
| comulB (aB * bB) = comulB aB * comulB bB := comulB.map_mul _ _ | |
| _ = aaT * bbT := by rw [comulB_aB, comulB_bB] | |
| rw [hc, hl] | |
| rw [map_mul, map_neg, map_pow, map_mul, comulB_aB, comulB_bB, comulB_V] |
| calc | ||
| comul bA = algebraMap R (A ⊗[R] A) b := comul.commutes b | ||
| _ = b • (1 : A ⊗[R] A) := Algebra.algebraMap_eq_smul_one b | ||
| _ = bbT := bbT_smul.symm |
There was a problem hiding this comment.
| calc | |
| comul bA = algebraMap R (A ⊗[R] A) b := comul.commutes b | |
| _ = b • (1 : A ⊗[R] A) := Algebra.algebraMap_eq_smul_one b | |
| _ = bbT := bbT_smul.symm | |
| rw [comul.commutes, Algebra.algebraMap_eq_smul_one, ← bbT_smul] |
| have hone : left (1 : A) = 1 := left.map_one | ||
| unfold lambda l₁ | ||
| simp only [map_mul, map_add] | ||
| rw [hone] |
There was a problem hiding this comment.
| have hone : left (1 : A) = 1 := left.map_one | |
| unfold lambda l₁ | |
| simp only [map_mul, map_add] | |
| rw [hone] | |
| simp only [lambda, map_mul, map_add, map_one] |
| have hone : right (1 : A) = 1 := right.map_one | ||
| unfold lambda l₂ | ||
| simp only [map_mul, map_add] | ||
| rw [hone, right_aA, right_bA] |
There was a problem hiding this comment.
| have hone : right (1 : A) = 1 := right.map_one | |
| unfold lambda l₂ | |
| simp only [map_mul, map_add] | |
| rw [hone, right_aA, right_bA] | |
| simp only [lambda, map_mul, map_add, map_one, right_aA, right_bA] |
| rw [left_lambda, right_lambda] | ||
| have hone : comul (1 : A) = 1 := comul.map_one | ||
| unfold lambda | ||
| simp only [map_mul, map_add] | ||
| rw [hone, comul_aA, comul_bA, comul_U, comul_v] | ||
| exact delta_lambda |
There was a problem hiding this comment.
| rw [left_lambda, right_lambda] | |
| have hone : comul (1 : A) = 1 := comul.map_one | |
| unfold lambda | |
| simp only [map_mul, map_add] | |
| rw [hone, comul_aA, comul_bA, comul_U, comul_v] | |
| exact delta_lambda | |
| rw [left_lambda, right_lambda] | |
| simpa [lambda, map_mul, map_add, comul_aA, comul_bA, comul_U, comul_v] using delta_lambda |
| @[simp] theorem powerMap_one_apply (x : A) : powerMap 1 x = x := by | ||
| calc | ||
| powerMap 1 x = universalPoint.ofConv x := | ||
| congr_arg (fun f : WithConv (A →ₐ[R] A) ↦ f.ofConv x) (pow_one universalPoint) | ||
| _ = x := rfl |
There was a problem hiding this comment.
| @[simp] theorem powerMap_one_apply (x : A) : powerMap 1 x = x := by | |
| calc | |
| powerMap 1 x = universalPoint.ofConv x := | |
| congr_arg (fun f : WithConv (A →ₐ[R] A) ↦ f.ofConv x) (pow_one universalPoint) | |
| _ = x := rfl | |
| @[simp] theorem powerMap_one_apply (x : A) : powerMap 1 x = x := | |
| congr_arg (fun f : WithConv (A →ₐ[R] A) ↦ f.ofConv x) (pow_one universalPoint) |
5 participants
Once #40500 (affine group scheme ↔ Hopf algebra correspondence) lands, the group-scheme formulation can be restated through that API for a cleaner statement.
This PR adds a
Counterexamples/file resolving a question of Grothendieck in the negative.Statement
Grothendieck asked whether a finite locally free group scheme of order
nis killed byn. Deligne proved this holds for commutative group schemes. This file gives a counterexample in the non-commutative case.Over the base ring
R = ℤ[a, b] / (a³, b³, a²b + 2), the coordinate algebrais a Hopf algebra, finite free of rank four over
R, whose associated affine group scheme has order four but is not killed by four. Concretely, the fourth convolution power of the identity is not the convolution unit:Background
nkilled byn? (Recorded as open in Tate, Finite flat group schemes, §3.8.)Proof sketch
Rhas2b ≠ 0; this is certified by an explicit faithfulR-moduleM = ℤ/4 × ℤ/4 × (ℤ/2)⁵witha,bacting by explicit additive endomorphisms.Ais built as two nestedQuadraticAlgebras, hence finite free of rank four.lambda = (1 + aU)(1 + bV), one checkslambdais group-like and the givenΔ(U),Δ(V)extend to a bialgebra comultiplication.powerMap nsendsUto(1 + lambda + ⋯ + lambdaⁿ⁻¹)·U; atn = 4this is2bUV ≠ 0.Ais a Hopf algebra of order four not killed by four. (Consistency with Deligne:Ais not cocommutative —not_isCocomm.)Disclosure
As stated in the module docstring, and per mathlib policy: the construction of this group scheme and its formalization were carried out with the AI assistants Codex (OpenAI) and Claude (Anthropic), under the direction of the author, who takes responsibility for the contribution.