feat(RingTheory): homotopy of Koszul complex and cocomplex - #40932

Closed

Thmoas-Guan wants to merge 145 commits into

leanprover-community:masterfrom

Thmoas-Guan:Koszul-Complex-homotopy

Commits on Jun 23, 2026

definition of Koszul complex
Thmoas-Guan
committed
60df0ed
definition of Koszul cocomplex
Thmoas-Guan
committed
deb1c7a
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
e39a890
add homotopy
Thmoas-Guan
committed
b231cdf
exterior power map lemma
Thmoas-Guan
committed
1827789
vanishing of exterior power
Thmoas-Guan
committed
387c8d8
Merge branch 'exterior-power-map-lemma' into Koszul-Complex-def
Thmoas-Guan
committed
e5fdd27
Merge branch 'exterior-power-vanish-lemma' into Koszul-Complex-def
Thmoas-Guan
committed
7b0d0c8
Merge branch 'exterior-power-map-lemma' into Koszul-Cocomplex-def
Thmoas-Guan
committed
0d25080
Merge branch 'exterior-power-vanish-lemma' into Koszul-Cocomplex-def
Thmoas-Guan
committed
b715c93
fix
Thmoas-Guan
committed
19d855f
fix
Thmoas-Guan
committed
8d0f6ff
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
56f3a63
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
d3a8b88
golf
Thmoas-Guan
committed
0f000ea
fix indentation
Thmoas-Guan
committed
f0ee036
Merge branch 'exterior-power-map-lemma' into Koszul-Complex-def
Thmoas-Guan
committed
f66fa75
Merge branch 'exterior-power-vanish-lemma' into Koszul-Complex-def
Thmoas-Guan
committed
bc91ff0
Merge branch 'exterior-power-map-lemma' into Koszul-Cocomplex-def
Thmoas-Guan
committed
78b6305
Merge branch 'exterior-power-vanish-lemma' into Koszul-Cocomplex-def
Thmoas-Guan
committed
600c69d
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
7c8407b
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
1221928
fix naming
Thmoas-Guan
committed
438165b
fix naming
Thmoas-Guan
committed
c0a0720
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
35a85bf
Update Cocomplex.lean
Thmoas-Guan
committed
321abc7
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
36e0154
add doc and golf
Thmoas-Guan
committed
78bb265
add doc and golf
Thmoas-Guan
committed
168bf73
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
7ae4c79
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
ace6525
add doc and golf
Thmoas-Guan
committed
253cfc9
golf
Thmoas-Guan
committed
06475ee
add lemma
Thmoas-Guan
committed
8d56550
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
65f211f
fix
Thmoas-Guan
committed
7263260
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
88e368c
fix
Thmoas-Guan
committed
dd54938

Commits on Jun 25, 2026

Commits on Jul 12, 2026

Commits on Jul 20, 2026

Merge branch 'master' into exterior-power-map-lemma
Thmoas-Guan
committed
5661022
Merge branch 'master' into exterior-power-vanish-lemma
Thmoas-Guan
committed
3da8944
Merge branch 'exterior-power-map-lemma' into Koszul-Complex-def
Thmoas-Guan
committed
12df59b
Merge branch 'exterior-power-vanish-lemma' into Koszul-Complex-def
Thmoas-Guan
committed
5ef899e
Merge branch 'exterior-power-map-lemma' into Koszul-Cocomplex-def
Thmoas-Guan
committed
b7345cd
Merge branch 'exterior-power-vanish-lemma' into Koszul-Cocomplex-def
Thmoas-Guan
committed
425bf6c
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
9150d19
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
e16cda1
fix
Thmoas-Guan
committed
0edbdb7
fix
Thmoas-Guan
committed
f75f951
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
a5f2490
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
6a9fd06

Commits on Aug 27, 2026

Commits on Sep 3, 2026

minimize imports

Thmoas-Guan
and
kbuzzard
authored
1c7ea21
add module doc

Thmoas-Guan
and
kbuzzard
authored
895f2a0
Merge branch 'master' into Koszul-Complex-def
Thmoas-Guan
committed
e86402f
fix
Thmoas-Guan
committed
50e5d0f
fix layout
Thmoas-Guan
committed
6df3579
golf
Thmoas-Guan
committed
6c60183
fix naming
Thmoas-Guan
committed
a965975
refactor API
Thmoas-Guan
committed
a381120
Merge branch 'master' into Koszul-Cocomplex-def
Thmoas-Guan
committed
8c5292a
minimize imports
Thmoas-Guan
committed
bb5889f
refactor API
Thmoas-Guan
committed
0422494
add module doc
Thmoas-Guan
committed
abfb537
fix doc
Thmoas-Guan
committed
df41621
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
a3b98eb
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
61fb5a2
adapt changes
Thmoas-Guan
committed
893412c
add stacks attr
Thmoas-Guan
committed
06727c3
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
8f390d8
add stacks attr
Thmoas-Guan
committed
bb1e164
fix layout
Thmoas-Guan
committed
b990165
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
3104941

Commits on Sep 8, 2026

Merge branch 'master' into Koszul-Complex-def
Thmoas-Guan
committed
f1747ce
fix naming
Thmoas-Guan
committed
00bab40
add map lemma
Thmoas-Guan
committed
a42a2ac
fix linear order
Thmoas-Guan
committed
9523cd7
golf
Thmoas-Guan
committed
95f3b30
fix naming
Thmoas-Guan
committed
4ba69a8
refine layout
Thmoas-Guan
committed
6691417
update docs
Thmoas-Guan
committed
9412a4e
open ModuleCat
Thmoas-Guan
committed
79b610d
Merge branch 'master' into Koszul-Cocomplex-def
Thmoas-Guan
committed
3755ca3
fix LinearOrder
Thmoas-Guan
committed
57d9309
rearrrange lemmas
Thmoas-Guan
committed
bbf9d6f
golf
Thmoas-Guan
committed
15a81a7
open ModuleCat
Thmoas-Guan
committed
ccb1756
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
16d9a9d
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
2eee710
fix
Thmoas-Guan
committed
33cf50a
Merge branch 'master' into Koszul-Complex-def
Thmoas-Guan
committed
e9b31a5
use implicit reducible
Thmoas-Guan
committed
7eba21e
golf by adding lemma
Thmoas-Guan
committed
31be294
Merge branch 'master' into Koszul-Cocomplex-def
Thmoas-Guan
committed
f1f09ff
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
76bf6f1
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
d5b8623
a temp fix to remove X_def
Thmoas-Guan
committed
fbba2ca
remove set_option
Thmoas-Guan
committed
b627087
use grind

Thmoas-Guan
and
Whysoserioushah
authored
d1dc204
use grind
Thmoas-Guan
committed
463170e
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
8c9c68c
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
f48181e
fix
Thmoas-Guan
committed
92449eb

Commits on Sep 9, 2026

try make ChainComplex.of implicit reducible
Thmoas-Guan
committed
adece79
fix another lemma
Thmoas-Guan
committed
ad20d65
a temp fix
Thmoas-Guan
committed
8b41024
fix more
Thmoas-Guan
committed
022f810
fix more
Thmoas-Guan
committed
c83535d
fix layout
Thmoas-Guan
committed
0c6c848
remove .of.d
Thmoas-Guan
committed
7b07362
fix
Thmoas-Guan
committed
9ee7708
remove usage of of_X in Group hom
Thmoas-Guan
committed
c6451e7
fix comment
Thmoas-Guan
committed
64193f7
add comment on attempts
Thmoas-Guan
committed
f20cf6d
remove an of_X
Thmoas-Guan
committed
270c620
final fix
Thmoas-Guan
committed
95b9c5a
fix
Thmoas-Guan
committed
00802f6
fix simpNF
Thmoas-Guan
committed
fa72d0d

Commits on Sep 10, 2026

remove some simp rw problem
Thmoas-Guan
committed
fe0f042
remove simp rw problem
Thmoas-Guan
committed
e96e3c6
Merge branch 'fix-chain-complex-of' into Koszul-Complex-def
Thmoas-Guan
committed
3f3d415
fix
Thmoas-Guan
committed
a8770bd
Merge branch 'fix-chain-complex-of' into Koszul-Cocomplex-def
Thmoas-Guan
committed
7c1a5d8
Merge branch 'Koszul-Complex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
f05e938
golf
Thmoas-Guan
committed
6ff67be
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
f072723
Revert "Merge branch 'fix-chain-complex-of' into Koszul-Cocomplex-def"
Thmoas-Guan
committed
9be0e0b
Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy
Thmoas-Guan
committed
903e155
Revert "Merge branch 'Koszul-Cocomplex-def' into Koszul-Complex-homotopy"
Thmoas-Guan
committed
8653ea1