Skip to content
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

Jump to bottom

Prove Proposition 4.5.2 in Bourbaki about life map to monoid hom for a coxeter system #6

Open
jiajunma opened this issue Mar 24, 2024 · 0 comments
Open

Prove Proposition 4.5.2 in Bourbaki about life map to monoid hom for a coxeter system #6

jiajunma opened this issue Mar 24, 2024 · 0 comments

Comments

@jiajunma
Copy link
Collaborator

coxeter/Coxeter/StrongExchange.lean

Line 48 in c4f1e53

def mapLift {f : S → M} (h : ∀ s s', (f s * f s')^orderOf ((s :G) * s') = 1) :

One may need to develop some basic properties for dihedral subgroup (S4.2 Bourbaki) and state and prove Prop 5.4
slashbade pushed a commit that referenced this issue Apr 18, 2024
@HaotianLiu123
update ASC (#6)
35c9b7e 
* update ASC

* update ASC
JQChong pushed a commit that referenced this issue Apr 19, 2024
@XintaoYu @timechess
@zzsj2001 @Hennessyyyyy @Prowler99 @HaotianLiu123 @hcWang942 @slashbade
PosetChain (#37)
428bc98 
* Fix unsolved goal

* test pr

* Update PosetChain.lean

* Update PosetChain.lean

* chain_nodup & chain_singleton_of_head_eq_tail

* Update PosetChain.lean

* maximal_chain'₂_iff_ledot & maximal_chain_iff_cover

* small improve

* maximal_chain'_cons

* Update PosetChain.lean

* prove 2 6

* Update PosetChain.lean

* tmp

* prove 8th lemma

* Update PosetChain.lean

* poset

* max_chain_mem_edge & new lemma mem_adjPairs_iff

* mem_adjPairs_iff

* Update PosetChain.lean

* PosetGraded && change of PosetChain (#12)

* Update AbstractSimplicialComplex.lean

Make all comments docComments

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Update ASCShelling.lean

Fix a mispelling

* update ASC

* change `simp` to `simp only`

* i love coxeter groups(bushi
)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC

* Update AbstractSimplicialComplex.lean

change `\U i\in s` to `\U i : s`

* Update AbstractSimplicialComplex.lean

* change rank to finite version

* PosetGraded

---------

Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>

* Develop (#13)

* Sync with NUS && fmt (#14)

* Update AbstractSimplicialComplex.lean

Make all comments docComments

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Update ASCShelling.lean

Fix a mispelling

* update ASC

* change `simp` to `simp only`

* i love coxeter groups(bushi
)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC

* Update AbstractSimplicialComplex.lean

change `\U i\in s` to `\U i : s`

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC (#5)

* fmt

* update ASC (#6)

* update ASC

* update ASC

* Update AbstractSimplicialComplex.lean

* Prove `closure_eq_iSup`

1. prove that taking supremum commutes with taking closure
2. prove `closure_eq_iSup`

* Update AbstractSimplicialComplex.lean (#7)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Revert "Update AbstractSimplicialComplex.lean (#7)" (#8)

This reverts commit 512d8fe.

---------

Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: slashbade <[email protected]>

---------

Co-authored-by: timechess <[email protected]>
Co-authored-by: zsj <[email protected]>
Co-authored-by: zzsj2001 <[email protected]>
Co-authored-by: Hennessy <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: slashbade <[email protected]>
slashbade pushed a commit that referenced this issue Apr 19, 2024
@HaotianLiu123 @slashbade
update ASC (#6)
342127c 
* update ASC

* update ASC
slashbade added a commit that referenced this issue Apr 19, 2024
@XintaoYu @timechess
@zzsj2001 @Hennessyyyyy @Prowler99 @HaotianLiu123 @hcWang942 @slashbade
PosetChain (#37)
012f7ff 
* Fix unsolved goal

* test pr

* Update PosetChain.lean

* Update PosetChain.lean

* chain_nodup & chain_singleton_of_head_eq_tail

* Update PosetChain.lean

* maximal_chain'₂_iff_ledot & maximal_chain_iff_cover

* small improve

* maximal_chain'_cons

* Update PosetChain.lean

* prove 2 6

* Update PosetChain.lean

* tmp

* prove 8th lemma

* Update PosetChain.lean

* poset

* max_chain_mem_edge & new lemma mem_adjPairs_iff

* mem_adjPairs_iff

* Update PosetChain.lean

* PosetGraded && change of PosetChain (#12)

* Update AbstractSimplicialComplex.lean

Make all comments docComments

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Update ASCShelling.lean

Fix a mispelling

* update ASC

* change `simp` to `simp only`

* i love coxeter groups(bushi
)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC

* Update AbstractSimplicialComplex.lean

change `\U i\in s` to `\U i : s`

* Update AbstractSimplicialComplex.lean

* change rank to finite version

* PosetGraded

---------

Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>

* Develop (#13)

* Sync with NUS && fmt (#14)

* Update AbstractSimplicialComplex.lean

Make all comments docComments

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Update ASCShelling.lean

Fix a mispelling

* update ASC

* change `simp` to `simp only`

* i love coxeter groups(bushi
)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC

* Update AbstractSimplicialComplex.lean

change `\U i\in s` to `\U i : s`

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC (#5)

* fmt

* update ASC (#6)

* update ASC

* update ASC

* Update AbstractSimplicialComplex.lean

* Prove `closure_eq_iSup`

1. prove that taking supremum commutes with taking closure
2. prove `closure_eq_iSup`

* Update AbstractSimplicialComplex.lean (#7)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Revert "Update AbstractSimplicialComplex.lean (#7)" (#8)

This reverts commit 512d8fe.

---------

Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: slashbade <[email protected]>

---------

Co-authored-by: timechess <[email protected]>
Co-authored-by: zsj <[email protected]>
Co-authored-by: zzsj2001 <[email protected]>
Co-authored-by: Hennessy <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: slashbade <[email protected]>
JQChong added a commit that referenced this issue Apr 21, 2024
@XintaoYu @timechess
@zzsj2001 @Hennessyyyyy @Prowler99 @HaotianLiu123 @hcWang942 @slashbade @jjdishere @ampan98 @JQChong
PosetASC (#53)
ea8eb1d 
* Fix unsolved goal

* test pr

* Update PosetChain.lean

* Update PosetChain.lean

* chain_nodup & chain_singleton_of_head_eq_tail

* Update PosetChain.lean

* maximal_chain'₂_iff_ledot & maximal_chain_iff_cover

* small improve

* maximal_chain'_cons

* Update PosetChain.lean

* prove 2 6

* Update PosetChain.lean

* tmp

* prove 8th lemma

* Update PosetChain.lean

* poset

* max_chain_mem_edge & new lemma mem_adjPairs_iff

* mem_adjPairs_iff

* Update PosetChain.lean

* PosetGraded && change of PosetChain (#12)

* Update AbstractSimplicialComplex.lean

Make all comments docComments

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Update ASCShelling.lean

Fix a mispelling

* update ASC

* change `simp` to `simp only`

* i love coxeter groups(bushi
)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC

* Update AbstractSimplicialComplex.lean

change `\U i\in s` to `\U i : s`

* Update AbstractSimplicialComplex.lean

* change rank to finite version

* PosetGraded

---------

Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>

* Develop (#13)

* Sync with NUS && fmt (#14)

* Update AbstractSimplicialComplex.lean

Make all comments docComments

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Update ASCShelling.lean

Fix a mispelling

* update ASC

* change `simp` to `simp only`

* i love coxeter groups(bushi
)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC

* Update AbstractSimplicialComplex.lean

change `\U i\in s` to `\U i : s`

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* update ASC (#5)

* fmt

* update ASC (#6)

* update ASC

* update ASC

* Update AbstractSimplicialComplex.lean

* Prove `closure_eq_iSup`

1. prove that taking supremum commutes with taking closure
2. prove `closure_eq_iSup`

* Update AbstractSimplicialComplex.lean (#7)

* Update AbstractSimplicialComplex.lean

* Update AbstractSimplicialComplex.lean

* Revert "Update AbstractSimplicialComplex.lean (#7)" (#8)

This reverts commit 512d8fe.

---------

Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: slashbade <[email protected]>

* Develop (#15)

* PosetASC aux sorries (#16)

* fmt

* fmt

* aux for PosetASC

* Update PosetChain.lean (#17)

* prove Delta using List.filter (#18)

* Develop (#20)

* Create ReflectionOrder.lean

* ReflectionOrder init

* Update ReflectionOrder.lean

* fix Hecke

* Update Defs.lean

* Update Defs.lean

* redef

* reflAlg init

* Update GraphSearchAux.lean

* Update GraphSearchAux.lean

* fix refl

* Update InitialSectionsOfRelf.lean

* bruhat order locally finite

* try to define h

* Update PosetChain.lean

* Update PosetASC.lean

* Prove length_diff_one and dependent lemmas.

* fix

* fix Hecke

* fix Rpoly

* 000

---------

Co-authored-by: jjdishere <[email protected]>
Co-authored-by: ampan98 <[email protected]>
Co-authored-by: slashbade <[email protected]>
Co-authored-by: Chong Jing Quan <[email protected]>

* PosetASC Pure (#19)

* Update PosetChain.lean

* Update PosetASC.lean

* 000

* PosetASC

* Clear

* sync

---------

Co-authored-by: XintaoYu <[email protected]>
Co-authored-by: XintaoYu <[email protected]>

---------

Co-authored-by: timechess <[email protected]>
Co-authored-by: zsj <[email protected]>
Co-authored-by: zzsj2001 <[email protected]>
Co-authored-by: Hennessy <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Lei Bichang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: lpya942 <[email protected]>
Co-authored-by: Haocheng Wang <[email protected]>
Co-authored-by: Haotian Liu <[email protected]>
Co-authored-by: slashbade <[email protected]>
Co-authored-by: jjdishere <[email protected]>
Co-authored-by: ampan98 <[email protected]>
Co-authored-by: Chong Jing Quan <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@jiajunma