Affineness of the three group stabilizers

Open

QAlgorithms.Papers.Independent.Intakethird100.P79.lemma_3_1_2

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

prove2quantum

Let $k$ be an algebraically closed field of characteristic zero, let $M$ be an irreducible algebraic monoid with unit group $G$ , and let $e\in M$ satisfy $e^2=e$ . Define $G_e^\ell=\{g\in G:ge=e\}$ , $G_e^r=\{g\in G:eg=e\}$ and $G_e=G_e^\ell\cap G_e^r$ . Then

G_e^\ell,\quad G_e^r,\quad G_e\quad\text{are affine algebraic groups}.

No affineness or normality of $M$ is assumed. This gives affine group stabilizers even for non-affine monoids.

Formalization Note The unit group is represented by the inverse-pair scheme $\{(x,y):xy=yx=1\}$ , and each stabilizer is computed by equalizer equations, rather than supplied as an arbitrary group.

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

/-- Lemma 3.1.2, PDF p. 16: all three group stabilizers are affine.
M is arbitrary irreducible; affineness and normality of M are not hypotheses. -/
theorem lemma_3_1_2 [IsAlgClosed k] [CharZero k]
    (M : KScheme k) [MonObj M] [IsVariety k M] [IrreducibleSpace M.left]
    (e : 𝟙_ (KScheme k) ⟶ M) (he : IsIdempotentPoint M e) :
    ∀ side : Fin 3, IsAffine (groupStabilizer M e side).left := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P79

end

Source

Local structure of algebraic monoids, arXiv:0709.1255v2, PDF p. 16, Lemma 3.1.2

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$ be a rational point satisfying $e^2=e$ . Form the $k$ -scheme $V$ as the equalizer of the morphism $M\times_k M\to M\times_k M$ sending $(a,b)$ to $(ab,ba)$ and the constant morphism with value $(1_M,1_M)$ . For $s=0$ , let $H_s$ be the equalizer on $V$ of $(a,b)\mapsto ae$ and the constant morphism with value $e$ ; for $s=1$ , use $(a,b)\mapsto ea$ and that constant morphism; for $s=2$ , use $(a,b)\mapsto(ae,ea)$ and the constant morphism with value $(e,e)$ . These are scheme-theoretic equalizers, without taking reductions. For every $s\in\{0,1,2\}$ , the underlying scheme of $H_s$ is affine.

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