ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The top-degree Borel-Weil-Bott case and Serre duality

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $G = S L_{3} (C)$ with $ρ = ω_{1} + ω_{2}$ , let $N = 3 = ∣ Φ^{+} ∣$ and put $λ = w_{0} \cdot ρ = - 3 ρ$ , so that $λ + ρ = - 2 ρ$ is regular with Weyl element $w_{0}$ and $w_{0} \cdot λ = ρ$ . Then The Borel-Weil-Bott theorem gives $H^{3} (X, L_{- 3 ρ}) ≅ L (ρ)^{*}, H^{i} (X, L_{- 3 ρ}) = 0 (i \neq 3),$ and the Serre pairing $H^{3} (X, L_{- 3 ρ}) \times H^{0} (X, L_{ρ}) ⟶ H^{3} (X, K_{X}) ≅ C$ is perfect; both sides are eight-dimensional. This is the $w = w_{0}$ , top-degree case of Borel-Weil-Bott is compatible with Serre duality with $μ = - λ - 2 ρ = ρ$ and $u = w_{0} w_{0} = 1$ .

Facts & Assumptions

Given: The Axiom of Choice, $g = {s l}_{3} (C)$ with its standard Cartan, simple roots $α_{1}, α_{2}$ , fundamental weights $ω_{1}, ω_{2}$ , $ρ = ω_{1} + ω_{2}$ , the flag variety $X = G / B$ of dimension $N = 3$ , the longest element $w_{0}$ and the weight $λ = - 3 ρ$ .

[F1]

In $A_{2}$ the simple roots are $α_{1}, α_{2}$ , the positive roots are $α_{1}, α_{2}, α_{1} + α_{2}$ , and the Weyl vector is $ρ = ω_{1} + ω_{2}$ with $⟨ ρ, α_{i}^{\lor} ⟩ = 1$ ; the longest element satisfies $w_{0} Φ^{+} = Φ^{-}$ , hence $w_{0} ρ = - ρ$ , and $ℓ (w_{0}) = N = 3 = ∣ Φ^{+} ∣$ , while the dot action is $w \cdot ν = w (ν + ρ) - ρ$ (Classical complex matrix Lie algebras, Root systems of the classical complex Lie algebras, Fundamental weights for a chosen simple root system, The Weyl vector in fundamental coordinates, The Weyl vector, Length and longest Weyl-group element).

[F2]

Borel-Weil-Bott: for regular $ν + ρ$ with Weyl element $v$ , $H^{ℓ (v)} (X, L_{ν}) ≅ L (v \cdot ν)^{*}$ and all other cohomology vanishes (The Borel-Weil-Bott theorem).

[F3]

Compatibility with Serre duality: for regular $λ$ with Weyl element $w$ and $μ = - λ - 2 ρ$ , the Weyl element of $μ$ is $w_{0} w$ and the Serre pairing identifies $H^{ℓ (w)} (X, L_{λ})^{\lor}$ with $H^{N - ℓ (w)} (X, L_{μ})$ , matching $L (w \cdot λ)^{*}$ with $L (w \cdot λ)$ (Borel-Weil-Bott is compatible with Serre duality).

[F4]

$ω_{X} = K_{X} ≅ L_{- 2 ρ}$ and Serre duality gives a perfect pairing $H^{3} (X, L_{- 3 ρ}) \times H^{0} (X, L_{ρ}) \to H^{3} (X, K_{X}) ≅ C$ ; moreover $\dim L (ρ) = 8$ : the Weyl dimension formula is $\dim L (ρ) = \prod_{β \in Φ^{+}} (2 ρ, β) / (ρ, β) = 2^{∣ Φ^{+} ∣} = 2^{3}$ , since $(2 ρ, β) = 2 (ρ, β)$ and $(ρ, β) > 0$ for the three positive roots (Canonical weight of a flag variety, Serre duality for locally free sheaves on a smooth projective variety, The Weyl dimension formula, Root systems of the classical complex Lie algebras, The Weyl vector in fundamental coordinates).

Verification

technique · direct

1.1F1givenalgebra

By [F1], $λ = w_{0} \cdot ρ = w_{0} (2 ρ) - ρ = - 2 ρ - ρ = - 3 ρ$ ; then $λ + ρ = - 2 ρ$ , and $w_{0} (λ + ρ) = 2 ρ$ is dominant, so the Weyl element of $λ$ is $w = w_{0}$ with $ℓ (w) = 3 = N$ , while $w_{0} \cdot λ = w_{0} (- 2 ρ) - ρ = 2 ρ - ρ = ρ$ .

2.1F2step 1.1

Applying [F2] to $λ$ by step 1.1 gives $H^{3} (X, L_{- 3 ρ}) ≅ L (ρ)^{*}$ and $H^{i} (X, L_{- 3 ρ}) = 0$ for $i \neq 3$ .

3.1F3F4step 1.1step 2.1algebra

For the pairing, $μ = - λ - 2 ρ = 3 ρ - 2 ρ = ρ$ and $u = w_{0} w = w_{0} w_{0} = 1$ with $ℓ (u) = 0 = N - 3$ , so [F3] identifies $H^{3} (X, L_{- 3 ρ})^{\lor}$ with $H^{0} (X, L_{ρ})$ and matches its two sides as $L (ρ)^{*}$ and $L (ρ)$ ; [F4] supplies the perfect Serre pairing to $H^{3} (X, K_{X}) ≅ C$ . Both $L (ρ)$ and its dual are eight-dimensional by [F4], so both sides of the pairing are eight-dimensional.

4.1step 2.1step 3.1∎

Collecting steps 2.1 and 3.1 gives the asserted top-degree Borel-Weil-Bott computation and the perfect eight-dimensional Serre pairing.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

58 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jacob Lurie, A Proof of the Borel-Weil-Bott Theorem (standard reference, not scraped)
George Boxer and Vincent Pilloni, Notes on Higher Coleman Theory (Montreal 2020) (standard reference, not scraped)