Alphabeta Math
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.

An sl3 weight with cohomology in degree one

Example

Assume the Axiom of Choice (The Axiom of Choice). Let G=SL3(C) with standard Borel, simple roots α1,α2, fundamental weights ω1,ω2 and ρ=ω1+ω2, and put λ=s1⋅ρ=ρ−2α1=−3ω1+3ω2. Then λ+ρ=s1(2ρ) is regular with Weyl element w=s1 and s1⋅λ=ρ, so The Borel-Weil-Bott theorem gives H1(X,Lλ)≅L(ρ)∗ and Hi(X,Lλ)=0 for i≠1. Since L(ρ) is eight-dimensional by the Weyl dimension formula, H1 is eight-dimensional and the Euler-characteristic formula reads ch H0−ch H1=−ch L(ρ).

Facts & Assumptions

Given: The Axiom of Choice, g=sl3(C) with standard Cartan and Borel, simple roots α1,α2, fundamental weights ω1,ω2, ρ=ω1+ω2, the simple reflection s1, the longest element w0 of the Weyl group, and λ=s1⋅ρ=ρ−2α1=−3ω1+3ω2.

[F1]

In A2 the simple roots are α1,α2, the positive roots are α1,α2,α1+α2, and ρ=ω1+ω2 satisfies ⟨ρ,αi∨⟩=1; the simple reflection acts by s1(ν)=ν−⟨ν,α1∨⟩α1, and the dot action is w⋅ν=w(ν+ρ)−ρ with ℓ(s1)=1 (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, Root reflections and the Weyl group action).

[F2]

Borel-Weil-Bott: if ν+ρ is regular with Weyl element v, then Hℓ(v)(X,Lν)≅L(v⋅ν)∗ and all other cohomology vanishes (The Borel-Weil-Bott theorem).

[F3]

The Weyl dimension formula gives dim⁡L(ρ)=∏β∈Φ+(2ρ,β)/(ρ,β)=2∣Φ+∣=23=8, since (2ρ,β)=2(ρ,β) and (ρ,β)>0 for the three positive roots; in particular H1≅L(ρ)∗ is eight-dimensional (The Weyl dimension formula, Root systems of the classical complex Lie algebras, The Weyl vector in fundamental coordinates).

[F4]

Euler-characteristic form of Borel-Weil-Bott: ∑i(−1)ich Hi(X,Lν)=(−1)ℓ(v)ch L(v⋅ν)∗ when ν+ρ is regular with Weyl element v (The Borel-Weil-Bott Euler character is a signed dual Weyl character).

[F5]

For a dominant integral weight ν the dual L(ν)∗ is irreducible of highest weight −w0ν; since w0 maps Φ+ onto Φ−, it sends 2ρ=∑α>0α to −2ρ, so w0ρ=−ρ and −w0ρ=ρ, hence L(ρ)∗ is irreducible of highest weight ρ and therefore L(ρ)∗≅L(ρ) by the classification of finite-dimensional irreducibles, with ch L(ρ)∗=ch L(ρ) (Highest weight of the dual representation, Length and longest Weyl-group element, Highest-weight classification).

Verification

technique · direct
1.1F1givenalgebra

Compute in A2: λ=s1⋅ρ=s1(2ρ)−ρ=2ρ−2α1−ρ=ρ−2α1 by [F1] and ⟨ρ,α1∨⟩=1. Since ρ=ω1+ω2 and α1=2ω1−ω2 (the A2 Cartan entry is ⟨α1,α2∨⟩=−1, read off from the ε-coordinates of [F1], so α1=⟨α1,α1∨⟩ω1+⟨α1,α2∨⟩ω2), this is ω1+ω2−4ω1+2ω2=−3ω1+3ω2. Moreover λ+ρ=s1(2ρ), which is regular because 2ρ is regular and W preserves regularity, and s1⋅λ=s1(λ+ρ)−ρ=2ρ−ρ=ρ, so the Weyl element is w=s1 with ℓ(w)=1.

2.1F2F3step 1.1

By [F2] applied to λ and step 1.1, H1(X,Lλ)≅L(ρ)∗ and Hi(X,Lλ)=0 for i≠1; by [F3] this group is eight-dimensional.

3.1F4F5step 2.1algebra

The Euler-characteristic formula of [F4] at this weight reads ch H0−ch H1=(−1)1ch L(ρ)∗=−ch L(ρ)∗, and by [F5] L(ρ)∗≅L(ρ), so this equals −ch L(ρ); since H0=0 by step 2.1 the formula is precisely the alternating class of the group H1≅L(ρ)∗.

4.1step 1.1step 2.1step 3.1∎

Steps 1.1-3.1 give a weight whose cohomology is concentrated in degree one with H1≅L(ρ)∗≅L(ρ) of dimension eight and whose Euler characteristic is −ch L(ρ), as asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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