ExampleConstruction: Literature-sourcedVerification: 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.

Borel-Weil-Bott on the projective line for SL2

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $G = S L_{2} (C)$ with upper triangular Borel $B$ and flag variety $X = G / B ≅ P^{1}$ , and for $m \in Z$ let $L_{m ω_{1}} = G \times^{B} C_{- m ω_{1}} ≅ O (m)$ be the line bundles identified by Flag line-bundle degree on a minimal-parabolic fiber in the rank-one case. Write $L (k ω_{1})$ for the finite-dimensional irreducible ${s l}_{2}$ -module of highest weight $k ω_{1}$ , for $k \geq 0$ . Then: (i) for $m \geq 0$ , $H^{0} (X, L_{m ω_{1}}) ≅ L (m ω_{1})^{*}$ and $H^{1} (X, L_{m ω_{1}}) = 0$ ; (ii) for $m \leq - 2$ , $H^{1} (X, L_{m ω_{1}}) ≅ L ((- m - 2) ω_{1})^{*}$ and $H^{0} (X, L_{m ω_{1}}) = 0$ ; (iii) for $m = - 1$ , $H^{0} (X, L_{- ω_{1}}) = H^{1} (X, L_{- ω_{1}}) = 0$ . The Borel-Weil-Bott degree is $0$ for $m \geq 0$ , $1$ for $m \leq - 2$ , and the weight $m ω_{1}$ is dot-singular exactly for $m = - 1$ .

Facts & Assumptions

Given: The Axiom of Choice, $G = S L_{2} (C)$ with upper triangular Borel, $X = G / B ≅ P^{1}$ , the fundamental weight $ω_{1}$ , $ρ = ω_{1}$ , the simple reflection $s$ , and the bundles $L_{m ω_{1}}$ for $m \in Z$ .

[F1]

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

[F2]

In rank one $ρ = ω_{1}$ , so $m ω_{1} + ρ = (m + 1) ω_{1}$ is regular exactly for $m \neq - 1$ ; for $m \geq 0$ the Weyl element is $v = 1$ with $1 \cdot (m ω_{1}) = m ω_{1}$ , while for $m \leq - 2$ the Weyl element is $s$ and $s (λ + ρ) - ρ$ with $λ = m ω_{1}$ equals $- (m + 2) ω_{1}$ : indeed $s ((m + 1) ω_{1}) = - (m + 1) ω_{1}$ , so $s \cdot (m ω_{1}) = - (m + 1) ω_{1} - ω_{1} = - (m + 2) ω_{1}$ (Fundamental weights for a chosen simple root system, The Weyl vector, Length and longest Weyl-group element).

[F3]

For $G = S L_{2}$ the unique simple root $α$ has $P_{α} = G$ , so the minimal parabolic fibre is all of $X = G / B$ , and under the fixed identification of $X$ with $P^{1}$ the bundle $L_{m ω_{1}}$ restricts to $O (m)$ by the degree computation $⟨ m ω_{1}, α^{\lor} ⟩ = m$ ; the singular boundary case $m = - 1$ has all cohomology vanishing (A minimal-parabolic flag projection is a projective-line bundle, Minimal parabolic from one negative simple root, Flag line-bundle degree on a minimal-parabolic fiber, Two-affine projective line and its twists, The sl2 singular weight has no cohomology).

[F4]

On $P^{1}$ over $C$ : $H^{0} (O (m))$ has dimension $m + 1$ for $m \geq 0$ and vanishes for $m < 0$ ; $H^{1} (O (m))$ vanishes for $m \geq - 1$ and has dimension $- m - 1$ for $m \leq - 2$ ; all other cohomology vanishes (Cohomology of O(d) on projective space). The Weyl dimension formula for ${s l}_{2}$ , whose single positive root pairs with $ρ$ by $1$ , gives $\dim L (k ω_{1}) = k + 1$ for $k \geq 0$ (The Weyl dimension formula).

Verification

technique · direct

1.1F1F2F4given

Case $m \geq 0$ : the weight $m ω_{1}$ is dominant and $m ω_{1} + ρ$ is regular with Weyl element $1$ by [F2], so [F1] gives $H^{0} (X, L_{m ω_{1}}) ≅ L (m ω_{1})^{*}$ and $H^{1} (X, L_{m ω_{1}}) = 0$ . This matches the dimensions of [F4], since $\dim L (m ω_{1})^{*} = m + 1 = \dim H^{0} (O (m))$ .

1.2F1F2F4given

Case $m \leq - 2$ : $m ω_{1} + ρ = (m + 1) ω_{1}$ is regular and the Weyl element is $s$ with $s \cdot (m ω_{1}) = - (m + 2) ω_{1}$ , which is dominant because $- m - 2 \geq 0$ ; by [F1], $H^{1} (X, L_{m ω_{1}}) ≅ L ((- m - 2) ω_{1})^{*}$ and all other cohomology vanishes, in particular $H^{0} = 0$ . The dimensions match those of [F4] because $\dim L ((- m - 2) ω_{1})^{*} = - m - 1 = \dim H^{1} (O (m))$ .

1.3F3given

Case $m = - 1$ : the weight $(- 1) ω_{1} = - ρ$ has $m ω_{1} + ρ = 0$ singular, and by [F3] all cohomology of $L_{- ω_{1}}$ vanishes, so $H^{0} = H^{1} = 0$ .

2.1step 1.1step 1.2step 1.3given∎

The three cases are exhaustive and $m ω_{1} + ρ = (m + 1) ω_{1}$ is singular exactly for $m = - 1$ ; collecting steps 1.1-1.3 gives the asserted Borel-Weil-Bott description on the projective line, with degree $0$ for $m \geq 0$ and degree $1$ for $m \leq - 2$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

89 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

Xiong Rui, Borel-Weil and Borel-Weil-Bott, Lecture 1 (standard reference, not scraped)
Joshua Ng (Hoi Hei Jan Sum), The Borel-Weil-Bott Theorem (Chicago REU 2015) (standard reference, not scraped)