Skip to content

Import demazureoperatorslean formalization #89

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Vilin97 merged 11 commits into from
May 20, 2026
Merged

Import demazureoperatorslean formalization #89

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
f478f34
Vendor DemazureOperatorsLean core
Vilin97 May 17, 2026
ce8359f
Merge branch 'main' into import/demazureoperatorslean
Vilin97 May 18, 2026
772af98
Add Demazure operator source citation
Vilin97 May 18, 2026
9ea20e5
Regenerate project card
Vilin97 May 18, 2026
e699d58
Complete Demazure Coxeter theory import
Vilin97 May 19, 2026
0014fcf
Merge origin/main into import/demazureoperatorslean
Vilin97 May 19, 2026
fe95201
Restore Demazure strong exchange and Matsumoto checks
Vilin97 May 19, 2026
9e469ca
Clarify conditional Matsumoto result
Vilin97 May 19, 2026
ce54d83
Add Coxeter source metadata for Demazure import
Vilin97 May 19, 2026
a38d9f2
Clarify Demazure auxiliary theorem framing
Vilin97 May 19, 2026
891ad0b
Merge origin/main into import/demazureoperatorslean
Vilin97 May 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions LeanPool.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,13 @@ import LeanPool.DeadEnds.PrimeTail
import LeanPool.DeadEnds.RelevantPrimes
import LeanPool.DeadEnds.Solution
import LeanPool.DeadEnds.TailEstimates
import LeanPool.DemazureOperatorsLean
import LeanPool.DemazureOperatorsLean.Demazure
import LeanPool.DemazureOperatorsLean.DemazureAux
import LeanPool.DemazureOperatorsLean.DemazureAuxRelations
import LeanPool.DemazureOperatorsLean.DemazureRelations
import LeanPool.DemazureOperatorsLean.Matsumoto
import LeanPool.DemazureOperatorsLean.StrongExchange
import LeanPool.DirectedTopologyLean4
import LeanPool.DirectedTopologyLean4.Constructions
import LeanPool.DirectedTopologyLean4.CoverLemma
Expand Down
32 changes: 32 additions & 0 deletions LeanPool/DemazureOperatorsLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
/-
Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Óscar Álvarez Sánchez
-/

import LeanPool.DemazureOperatorsLean.Demazure
import LeanPool.DemazureOperatorsLean.DemazureAux
import LeanPool.DemazureOperatorsLean.DemazureRelations
import LeanPool.DemazureOperatorsLean.DemazureAuxRelations
import LeanPool.DemazureOperatorsLean.StrongExchange
import LeanPool.DemazureOperatorsLean.Matsumoto

/-!
# Demazure Operators and Lean

Source: doi:10.1070/RM1973v028n03ABEH001549
Authors: Óscar Álvarez Sánchez
Status: verified
Main declarations: `Demazure.Dem`, `CoxeterSystem.strongExchangeProperty`
Tags: algebraic-combinatorics, demazure-operators, polynomials, representation-theory
MSC: 05E05, 13P10, 20F55
-/

/-!
The Demazure-operator declarations are sourced to the BGG Schubert-cells paper
listed in the project card. The strong-exchange declaration is included as
supporting Coxeter theory with source metadata from Humphreys' *Reflection Groups
and Coxeter Groups*. The Matsumoto development is retained as conditional
auxiliary infrastructure because `CoxeterSystem.matsumoto_reduced` assumes the
extra `MatsumotoCondition` hypothesis.
-/
Loading
Loading