Schubert geometry, Demazure sections and flag K-theory
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremTauCeti.PLPath.lower_eq_some_iff#
Littelmann's root operators are partial inverses: lowering p gives q exactly when raising
q gives p.
TauCeti.PLPath.lower_eq_some_iff.{u_1, u_2} {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜] [AddCommGroup V] [_root_.Module 𝕜 V] {f : Module.Dual 𝕜 V} {x : V}
(hx : f x = 2) {p q : TauCeti.PLPath 𝕜 V} :
TauCeti.PLPath.lower f x p = some q ↔ TauCeti.PLPath.raise f x q = some p
Uses 2
TheoremThe stabilizer of a dominant weight is a standard parabolic subgroup#
the one generated by the simple reflections in the walls through it.
RootPairing.parabolic_wallIndices_eq_stabilizer.{u, v, w, x} {ι : Type u} {R : Type v} {M : Type w}
{N : Type x} [CommRing R] [AddCommGroup M] [_root_.Module R M] [AddCommGroup N]
[_root_.Module R N] (P : RootPairing ι R M N) (b : P.Base) [LinearOrder R] [IsStrictOrderedRing R]
[Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {lam : M}
(hlam : lam ∈ P.dominantChamber b) :
(TauCeti.weylCoxeterSystem P b).parabolic (P.wallIndices b lam) =
MulAction.stabilizer (↥P.weylGroup) lam
Lean
Formalized in Tau Ceti as RootPairing.parabolic_wallIndices_eq_stabilizer.
Sources
TheoremA cover of W / W_λ has a unique positive root label#
If y is covered by x in the
Bruhat order of the minimal coset representatives of the stabilizer of the dominant weight λ,
there is exactly one positive root β with y λ = s_β (x λ).
TauCeti.existsUnique_isPos_reflection_smul_eq_of_minimalCosetRepCovBy.{u, v, w, x} {ι : Type u}
{R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M]
[_root_.Module R M] [AddCommGroup N] [_root_.Module R N] {P : RootPairing ι R M N} {b : P.Base}
[LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced]
[P.flip.IsReduced] {lam : M} (hlam : lam ∈ P.dominantChamber b) {x y : ↥P.weylGroup}
(h : (TauCeti.weylCoxeterSystem P b).MinimalCosetRepCovBy (P.wallIndices b lam) y x) :
∃! β, b.IsPos β ∧ (P.reflection β) (x • lam) = y • lam
Lean
Formalized in Tau Ceti as TauCeti.existsUnique_isPos_reflection_smul_eq_of_minimalCosetRepCovBy.
Sources
- Tau Ceti documentation:
TauCeti.existsUnique_isPos_reflection_smul_eq_of_minimalCosetRepCovBy - Source of
TauCeti.existsUnique_isPos_reflection_smul_eq_of_minimalCosetRepCovByin TauCeti/LinearAlgebra/RootSystem/Weyl/CoverBond.lean - Tau Ceti roadmap status: Schubert geometry, Demazure sections and flag K-theory
Uses 2 · Used by 1
TheoremThe bond of a cover of W / W_λ is a positive integer#
The bond of a cover of W / W_λ is a positive integer when the dominant weight λ is
integral, that is when every simple coroot takes an integer value on λ.
TauCeti.exists_nat_reflectionBond_eq_of_minimalCosetRepCovBy.{u, v, w, x} {ι : Type u} {R : Type v}
{M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [_root_.Module R M]
[AddCommGroup N] [_root_.Module R N] {P : RootPairing ι R M N} {b : P.Base} [LinearOrder R]
[IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced]
{lam : M} (hlam : lam ∈ P.dominantChamber b) (hint : ∀ i ∈ b.support, ∃ z, (P.coroot' i) lam = ↑z)
{x y : ↥P.weylGroup}
(h : (TauCeti.weylCoxeterSystem P b).MinimalCosetRepCovBy (P.wallIndices b lam) y x) :
∃ n, 0 < n ∧ P.reflectionBond b (x • lam) (y • lam) = ↑n
Lean
Formalized in Tau Ceti as TauCeti.exists_nat_reflectionBond_eq_of_minimalCosetRepCovBy.
Sources
TheoremThe localization identity of the Demazure operator#
(1 - e^{-αᵢ}) Dᵢ(f) = f - e^{-αᵢ} sᵢ(f), where sᵢ reindexes ℤ[M] along the reflection of
M. Equivalently, Dᵢ(e^x) = (e^x - e^{-αᵢ} e^{sᵢ x}) / (1 - e^{-αᵢ}).
RootPairing.one_sub_single_neg_root_mul_demazureOperator.{u_1, u_2, u_3} {ι : Type u_1}
{M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι)
(f : AddMonoidAlgebra ℤ M) :
(1 - AddMonoidAlgebra.single (-P.root i) 1) * (P.demazureOperator i) f =
f -
AddMonoidAlgebra.single (-P.root i) 1 *
(AddMonoidAlgebra.mapDomainRingEquiv ℤ (P.reflection i).toAddEquiv) f
Lean
Formalized in Tau Ceti as RootPairing.one_sub_single_neg_root_mul_demazureOperator.
Sources
TheoremThe Demazure operator is idempotent, Dᵢ² = Dᵢ#
RootPairing.demazureOperator_demazureOperator.{u_1, u_2, u_3} {ι : Type u_1} {M : Type u_2}
{N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι)
(f : AddMonoidAlgebra ℤ M) :
(P.demazureOperator i) ((P.demazureOperator i) f) = (P.demazureOperator i) f
Uses 1
TheoremTauCeti.NormalCrystal.tensor_ε_eq_max#
Kashiwara's form of the raising string length of a tensor product:
ε i (x₁ ⊗ x₂) = max (ε i x₁) (ε i x₂ - ⟨wt x₁, α_i^∨⟩).
TauCeti.NormalCrystal.tensor_ε_eq_max.{u, v, w, x₁, x₂} {ι : Type u} {X : Type v} {Y : Type w}
[AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁}
{B₂ : Type x₂} {c : TauCeti.NormalCrystal P b B₁} {d : TauCeti.NormalCrystal P b B₂}
(i : ↥b.support) (x : B₁ × B₂) :
↑((c.tensor d).ε i x) =
max (↑(c.ε i x.1)) (↑(d.ε i x.2) - (P.toLinearMap (c.wt x.1)) (P.coroot ↑i))
Uses 2
StructureTauCeti.NormalCrystal#
A normal crystal over the root datum P with base b: a weight map, partial raising and
lowering operators e i, f i indexed by the simple roots, and natural string lengths ε i,
φ i, satisfying Kashiwara's crystal axioms together with normality (ε i x and φ i x are the
lengths of the e i- and f i-strings through x). The value none of e i or f i stands
for Kashiwara's 0.
TauCeti.NormalCrystal.{u, v, w, x₁} {ι : Type u} {X : Type v} {Y : Type w} [AddCommGroup X]
[AddCommGroup Y] (P : RootDatum ι X Y) (b : RootPairing.Base P) (B : Type x₁) :
Type (max (max u v) x₁)
Used by 2
DefinitionTauCeti.NormalCrystal.tensor#
The tensor product B₁ ⊗ B₂ of two normal crystals, on the product type, with
Kashiwara's tie convention: on a tie φ i x₁ = ε i x₂ the raising operator acts on the left
factor and the lowering operator on the right factor.
TauCeti.NormalCrystal.tensor.{u, v, w, x₁, x₂} {ι : Type u} {X : Type v} {Y : Type w}
[AddCommGroup X] [AddCommGroup Y] {P : RootDatum ι X Y} {b : RootPairing.Base P} {B₁ : Type x₁}
{B₂ : Type x₂} (c : TauCeti.NormalCrystal P b B₁) (d : TauCeti.NormalCrystal P b B₂) :
TauCeti.NormalCrystal P b (B₁ × B₂)
Uses 1 · Used by 1
DefinitionTauCeti.PLPath.lower#
Littelmann's lowering operator f_α on paths, for the root α = x and the coroot pairing
f = ⟨-, α^∨⟩. Let h be the minimal height, t₀ the last time at which the height equals h
and t₁ the first time from which on the height is at least h + 1. Between t₀ and t₁, the
pieces along which the height increases and stays at most every later height are reflected by
Module.preReflection x f, the equal-height excursions are kept, and the rest of the path after
t₁ is translated by -x. It is none when f (π 1) - h < 1.
TauCeti.PLPath.lower.{u_1, u_2} {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜] [AddCommGroup V] [_root_.Module 𝕜 V] (f : Module.Dual 𝕜 V) (x : V)
(p : TauCeti.PLPath 𝕜 V) : Option (TauCeti.PLPath 𝕜 V)
Used by 2
DefinitionTauCeti.PLPath.raise#
Littelmann's raising operator e_α on paths, the conjugate of TauCeti.PLPath.lower by the
reversal of paths. Let h be the minimal height, t₁ the first time at which the height equals
h and t₀ the last time up to which the height is at least h + 1. Between t₀ and t₁, the
pieces along which the height decreases and stays at most every earlier height are reflected by
Module.preReflection x f, the equal-height excursions are kept, and the rest of the path after
t₁ is translated by x. It is none when -1 < h.
TauCeti.PLPath.raise.{u_1, u_2} {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜] [AddCommGroup V] [_root_.Module 𝕜 V] (f : Module.Dual 𝕜 V) (x : V)
(p : TauCeti.PLPath 𝕜 V) : Option (TauCeti.PLPath 𝕜 V)
Uses 1 · Used by 1
DefinitionRootPairing.reflectionBond#
The bond of two weights related by a reflection in a positive root: if y = s_β x for a
positive root β, it is ⟨y, β^∨⟩ = -⟨x, β^∨⟩. For y ≠ x and a reduced root pairing the
positive root β is unique (TauCeti.eq_of_isPos_of_reflection_eq), so the bond is well defined
(RootPairing.reflectionBond_eq_coroot'). If no reflection in a positive root sends x to y, the
bond is 0. For a cover y ⋖ x of the parabolic quotient W / W_λ, the bond of x λ and y λ
is the positive cover bond b_λ(x, y).
RootPairing.reflectionBond.{u, v, w, x} {ι : Type u} {R : Type v} {M : Type w} {N : Type x}
[CommRing R] [CharZero R] [AddCommGroup M] [_root_.Module R M] [AddCommGroup N]
[_root_.Module R N] (P : RootPairing ι R M N) (b : P.Base) (x y : M) : R
Used by 1
StructureCoxeterSystem.MinimalCosetRepCovBy#
y is covered by x in the Bruhat order of the parabolic quotient W / W_J, modelled on
the minimal coset representatives: both are minimal coset representatives, y < x, and no minimal
coset representative lies strictly between them.
CoxeterSystem.MinimalCosetRepCovBy.{u_1, u_2} {B : Type u_1} {W : Type u_2} [Group W]
{M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (y x : W) : Prop
TheoremDemazure's formula on a basis element#
D_{w₀}(e^λ) is Weyl's quotient. For a reduced word
ω of the longest element w₀ and a weight λ,
Δ · D_{w₀}(e^λ) = ∑_{w ∈ W} sgn(w) e^{w λ - (ρ - w ρ)},
the alternating sum over the dot orbit w ⬝ λ = w(λ + ρ) - ρ.
RootPairing.weylDenominator_mul_prod_map_demazureOperator_single.{u_1, u_2, u_3} {ι : Type u_1}
{M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N)
[Finite ι] (b : P.Base) [P.IsReduced] [Fintype ↥P.weylGroup] {ω : List ↥b.support}
(hω : (TauCeti.weylCoxeterSystem P b).IsReduced ω)
(hdesc :
∀ (i : ↥b.support),
(TauCeti.weylCoxeterSystem P b).IsLeftDescent ((TauCeti.weylCoxeterSystem P b).wordProd ω) i)
(lam : M) :
TauCeti.weylDenominator P b *
(List.map (fun m => P.demazureOperator ↑m) ω).prod (AddMonoidAlgebra.single lam 1) =
∑ w,
↑((TauCeti.weylSign P b) w) •
AddMonoidAlgebra.single (w • lam - ∑ i ∈ TauCeti.inversionsFinset P b w⁻¹, P.root i) 1
Lean
Formalized in Tau Ceti as RootPairing.weylDenominator_mul_prod_map_demazureOperator_single.
Other forms
Demazure's formula for the longest element. Formalized in Tau Ceti as RootPairing.weylDenominator_mul_prod_map_demazureOperator.
RootPairing.weylDenominator_mul_prod_map_demazureOperator.{u_1, u_2, u_3} {ι : Type u_1}
{M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N)
[Finite ι] (b : P.Base) [P.IsReduced] [Fintype ↥P.weylGroup] {ω : List ↥b.support}
(hω : (TauCeti.weylCoxeterSystem P b).IsReduced ω)
(hdesc :
∀ (i : ↥b.support),
(TauCeti.weylCoxeterSystem P b).IsLeftDescent ((TauCeti.weylCoxeterSystem P b).wordProd ω) i)
(f : AddMonoidAlgebra ℤ M) :
TauCeti.weylDenominator P b * (List.map (fun m => P.demazureOperator ↑m) ω).prod f =
(P.dotAlternatization b) f
Sources
TheoremThe Weyl dimension formula (TauCeti.sum_coeff_mul_prod_coroot'_weylVector_eq)#
If f · Δ = N(λ) and g · Δ = N(0) in ℤ[M], then the
sums of the coefficients of f and g satisfy
(∑ f) ∏_{α>0} ⟨ρ, α^∨⟩ = (∑ g) ∏_{α>0} ⟨λ+ρ, α^∨⟩.
For the formal character f = ch L(λ) of an irreducible module and g = ch L(0) = 1 this is
dim L(λ) ∏_{α>0} ⟨ρ, α^∨⟩ = ∏_{α>0} ⟨λ+ρ, α^∨⟩, the division-free form of
dim L(λ) = ∏_{α>0} ⟨λ+ρ, α^∨⟩ / ⟨ρ, α^∨⟩. An invariant form on the root pairing is needed for
the proof, though it does not appear in the statement.
TauCeti.sum_coeff_mul_prod_coroot'_weylVector_eq.{u, v, w, x} {ι : Type u} {R : Type v} {M : Type w}
{N : Type x} [CommRing R] [AddCommGroup M] [_root_.Module R M] [AddCommGroup N]
[_root_.Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) [Algebra ℚ R]
[IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup]
(B : P.InvariantForm) {f g : AddMonoidAlgebra ℤ M} {lam : M}
(hf : f * TauCeti.weylDenominator P b = TauCeti.weylNumerator P b lam)
(hg : g * TauCeti.weylDenominator P b = TauCeti.weylNumerator P b 0) :
↑(f.coeff.sum fun x n => n) *
∏ i ∈ TauCeti.posRootsFinset P b, (P.coroot' i) (TauCeti.weylVector P b) =
↑(g.coeff.sum fun x n => n) *
∏ i ∈ TauCeti.posRootsFinset P b, (P.coroot' i) (lam + TauCeti.weylVector P b)
Lean
Formalized in Tau Ceti as TauCeti.sum_coeff_mul_prod_coroot'_weylVector_eq.
Other forms
The Weyl dimension formula, in terms of an invariant form. Formalized in Tau Ceti as TauCeti.sum_coeff_mul_prod_form_weylVector_root_eq.
TauCeti.sum_coeff_mul_prod_form_weylVector_root_eq.{u, v, w, x} {ι : Type u} {R : Type v}
{M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [_root_.Module R M] [AddCommGroup N]
[_root_.Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) [Algebra ℚ R]
[IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup]
(B : P.InvariantForm) {f g : AddMonoidAlgebra ℤ M} {lam : M}
(hf : f * TauCeti.weylDenominator P b = TauCeti.weylNumerator P b lam)
(hg : g * TauCeti.weylDenominator P b = TauCeti.weylNumerator P b 0) :
↑(f.coeff.sum fun x n => n) *
∏ i ∈ TauCeti.posRootsFinset P b, (B.form (TauCeti.weylVector P b)) (P.root i) =
↑(g.coeff.sum fun x n => n) *
∏ i ∈ TauCeti.posRootsFinset P b, (B.form (lam + TauCeti.weylVector P b)) (P.root i)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.