Smoothness at an idempotent and affine-space stabilizers

Open

QAlgorithms.Papers.Independent.Intakethird100.P79.corollary_3_1_5

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $k$ be algebraically closed of characteristic zero, let $M$ be an irreducible algebraic monoid, and let $e\in M$ be idempotent. Let $M_e=\{x\in M:xe=ex=e\}$ with its reduced closed-subscheme structure. Then

e\text{ is a smooth point of }M\quad\Longleftrightarrow\quad\exists n\in\mathbb N,\ M_e\cong_k\mathbb A_k^n.

The isomorphism is one of varieties, with no compatibility with monoid multiplication required. Dimension zero is allowed. This criterion detects smoothness without a normality or affineness assumption on $M$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P79

Formal statement

noncomputable section

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

open CategoryTheory.MonoidalCategory CategoryTheory.CartesianMonoidalCategory

open CategoryTheory.MonObj

open scoped CategoryTheory.MonObj Pointwise

universe u

namespace QAlgorithms.Papers.Independent.Intakethird100.P79

variable (k : Type u) [Field k]

variable {k}

attribute [local instance] MvPolynomial.gradedAlgebra

/-- Corollary 3.1.5, PDF p. 17: e is smooth in M exactly when the two-sided
stabilizer is isomorphic as a k-variety to affine space. Dimension zero is allowed;
the isomorphism is not required to preserve the monoid multiplication. -/
theorem corollary_3_1_5 [IsAlgClosed k] [CharZero k]
    (M : KScheme k) [MonObj M] [IsVariety k M] [IrreducibleSpace M.left]
    (e : 𝟙_ (KScheme k) ⟶ M) (he : IsIdempotentPoint M e) :
    IsSmoothPoint M e ↔
      ∃ n : ℕ, Nonempty (stabilizer M e 2 ≅ affineSpace (k := k) n) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P79

end

Source

Local structure of algebraic monoids, arXiv:0709.1255v2, PDF p. 17, Corollary 3.1.5

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $k$ be an algebraically closed field of characteristic zero, and let $M$ be a monoid scheme over $k$ whose structure morphism is locally of finite type, quasi-compact, and separated, and whose underlying scheme is reduced and irreducible. Let $e:\operatorname{Spec}k\to M$ satisfy $e^2=e$ . There exists an open subset $W\subseteq |M|$ containing the image under $e$ of the unique point of $\operatorname{Spec}k$ , such that the structure morphism of the corresponding open subscheme $W\to\operatorname{Spec}k$ is smooth, if and only if there exists a natural number $n$ and an isomorphism of $k$ -schemes between the reduction of the scheme-theoretic equalizer of $x\mapsto(xe,ex)$ and the constant morphism with value $(e,e)$ , and

\operatorname{Spec}k[t_0,\ldots,t_{n-1}],

whose structure morphism is induced by inclusion of constants. The reduction is the closed subscheme defined by the equalizer’s nilradical; $n=0$ is allowed and gives $\operatorname{Spec}k$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph