Affine connected stabilizers with dense unit groups

Open

QAlgorithms.Papers.Independent.Intakethird100.P79.lemma_3_1_4

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 with unit group $G$ , and let $e\in M$ be idempotent. Give $M_e^\ell=\{x\in M:xe=e\}$ , $M_e^r=\{x\in M:ex=e\}$ and $M_e=M_e^\ell\cap M_e^r$ their reduced closed-subscheme structures. For $s\in\{\ell,r,\mathrm{two}\}$ , write $S_s$ for the respective stabilizer and $G_s=G\cap S_s$ for its unit group. Then

\forall s\in\{\ell,r,\mathrm{two}\},\qquad S_s\text{ is affine and connected},\qquad\overline{G_s}^{\,M}=S_s.

The closure formula states density of each actual unit group in its own stabilizer. It does not assert irreducibility, and requires neither affineness nor normality of $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

/-- Lemma 3.1.4, PDF p. 17: the three reduced stabilizers are affine and
connected, and their actual unit groups are dense. Closure is taken inside M,
and is compared with the canonical stabilizer inclusion, so density is not input. -/
theorem lemma_3_1_4 [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 (stabilizer M e side).left ∧
      ConnectedSpace (stabilizer M e side).left ∧
      closure (Set.range (groupStabilizerInclusion M e side).left) =
        Set.range (stabilizerInclusion M e side).left := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P79

end

Source

Local structure of algebraic monoids, arXiv:0709.1255v2, PDF p. 17, Lemma 3.1.4

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$ . For $s\in\{0,1,2\}$ , define $E_s$ scheme-theoretically by the equalizer equation $xe=e$ when $s=0$ , $ex=e$ when $s=1$ , and $(xe,ex)=(e,e)$ when $s=2$ ; let $Z_s$ be its reduction, namely the closed subscheme defined by its nilradical, with its induced morphism $j_s:Z_s\to M$ . Let $V\subseteq M\times_k M$ be the equalizer imposing $ab=ba=1_M$ , and let $H_s$ be the equalizer inside $V$ imposing the same respective equations on the first coordinate $a$ : $ae=e$ , $ea=e$ , or both. Let $h_s:H_s\to M$ be its morphism given by the first coordinate. For every $s\in\{0,1,2\}$ , the underlying scheme of $Z_s$ is affine, its underlying topological space is nonempty and connected, and

\overline{\operatorname{im}(|h_s|)} =\operatorname{im}(|j_s|),

where both images and the closure are taken in the underlying topological space $|M|$ , over all scheme points rather than only rational points.

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