WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Borel–Weil–Bott theorem

Revision #1047 → #2468 · back to history

modifiedBorel–Weil–Bott theorem (overview)28cbfe4ecd95
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Borel–Weil–Bott theorem or its sheaf-cohomology apparatus for flag varieties appears in Mathlib (grep for `Borel.Weil`, `BorelWeil`, `Bott` finds nothing relevant).
status—not_formalized
modifiedSetup: G, T, B, integral weight and associated line bundleae9da7b54868
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has semisimple Lie algebras and root systems but no Borel subgroup, integral weight lattice, or line bundle L_λ on G/B.
status—not_formalized
modifiedDot action of the Weyl group centered at ρ84dbd40d4e40
FieldFrom #1047To #2468
mathlib.decl—RootPairing.weylGroup
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.RootSystem.WeylGroup
note—The linear Weyl-group action on a root pairing exists (`RootPairing.weylGroup`), but the ρ-shifted dot action w·λ = w(λ+ρ)−ρ is not defined in Mathlib.
status—partial
modifiedDominant weightc3e552a3a15e
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No definition of dominant integral weight (μ with ⟨μ,α∨⟩ ≥ 0 for all simple coroots) exists in Mathlib's root-system or Lie-algebra files.
status—not_formalized
modifiedDichotomy for integral weights under dot action1c31af332191
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The dichotomy (either some w·λ is dominant with trivial stabilizer, or λ is fixed by a nontrivial reflection under the dot action) is not formalized.
status—not_formalized
modifiedBorel–Weil–Bott theorem (statement)f7a160e9f31e
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The precise cohomology-shifting statement H^ℓ(w)(G/B, L_λ) ≅ H^0(G/B, L_{w·λ}) with vanishing in other degrees is absent from Mathlib.
status—not_formalized
modifiedCharacterization of case (1) and recovery of Borel–Weilf5ecb34cd09a
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The identification of case (1) with λ dominant integral (w = e) recovering Borel–Weil is not formalized in Mathlib.
status—not_formalized
modifiedSL_2(C): sections of L_n as symmetric powers119118a80737
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not have the identification H^0(P^1, O(n)) ≅ Sym^n((C^2)*) as an SL_2(C)-representation.
status—not_formalized
modifiedRepresentation theory of sl_2 via Riemann sphere6e12afdf88ab
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The full classification of finite-dimensional irreducible sl_2-representations via cohomology of line bundles on the Riemann sphere is not in Mathlib.
status—not_formalized
modifiedKempf vanishing theorem7951a565ec4f
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no formalization of Kempf's vanishing theorem (grep for `Kempf` returns no results).
status—not_formalized
modifiedFailure of simplicity in positive characteristic; Mumford's example48665c71afd0
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mumford's example demonstrating non-simplicity of H^0(G/B, L_λ) in positive characteristic is not in Mathlib.
status—not_formalized
modifiedBorel–Weil theorem (overview)aca023428456
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formalization of the Borel–Weil model for irreducible representations of compact/complex semisimple Lie groups exists in Mathlib.
status—not_formalized
modifiedFlag variety and equivariant line bundle L_λe15e28ce245b
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The flag variety G/B and the equivariant line bundle L_λ associated to a character of B are not constructed in Mathlib.
status—not_formalized
modifiedBorel–Weil theorem (precise statement)9bda6a415233
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The isomorphism H^0(G/B, L_λ) ≅ V_λ* as G-representations for λ dominant integral is not formalized in Mathlib.
status—not_formalized
modifiedCharacter χ_λ and concrete description of sections of L_λc497e279d950
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No construction of the character χ_λ of B or the concrete description of sections of L_λ as B-equivariant holomorphic functions G → C is present.
status—not_formalized
modifiedAction of G on holomorphic sections569c45ed4631
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The G-action by left translation on B-equivariant holomorphic sections is not formalized in Mathlib.
status—not_formalized
modifiedSL(2,C): characters, sections on CP^1 and weight vectors11409399b9da
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The concrete SL(2,C) computation of characters of the upper-triangular Borel, sections on CP^1, and weight vectors as monomials is not formalized.
status—not_formalized
modifiedWeight vectors as monomials of weight 2i−ndb5b011c65d5
FieldFrom #1047To #2468
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Identification of weight vectors in H^0(CP^1, O(n)) with monomials z^i (weight 2i−n) is not formalized in Mathlib.
status—not_formalized