Quasi-projectivity of irreducible algebraic monoids

Open

QAlgorithms.Papers.Independent.Intakethird100.P79.corollary_3_3_1

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 a separated reduced $k$ -scheme of finite type which is irreducible and carries an associative regular multiplication with an identity. Then

\exists n\in\mathbb N,\quad\exists i:M\longrightarrow\mathbb P_k^n,\qquad i\text{ is a locally closed immersion over }k.

Thus every irreducible algebraic monoid is quasi-projective, including non-affine and non-normal monoids. Quasi-projectivity is a conclusion, not part of the standing definition of variety.

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.3.1, PDF p. 20: every irreducible algebraic monoid is
quasi-projective. No affine, normal, or reductive assumption is imposed. -/
theorem corollary_3_3_1 [IsAlgClosed k] [CharZero k]
    (M : KScheme k) [MonObj M] [IsVariety k M] [IrreducibleSpace M.left] :
    IsQuasiProjective M := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P79

end

Source

Local structure of algebraic monoids, arXiv:0709.1255v2, PDF p. 20, Corollary 3.3.1

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. There exist a natural number $n$ and an immersion of schemes

i:M\longrightarrow \operatorname{Proj}k[X_0,\ldots,X_n]

such that composing $i$ with the morphism from this projective scheme to the spectrum of its degree-zero ring, and then with the morphism to $\operatorname{Spec}k$ induced by inclusion of constants into that degree-zero ring, gives exactly the structure morphism of $M$ . Here the polynomial ring has its total-degree grading, and $n=0$ is included.

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