michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge branch 'master' of https://github.com/cmu-phil/Spectral

Browse source
This commit is contained in:
Egbert Rijke 2017-05-18 17:24:14 -04:00
commit f35158874a
1 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
algebra/exact_couple.hlean
View file

@ -108,6 +108,13 @@ definition differential_is_differential {A B : AbGroup} (EC : exact_couple A B)
section derived_couple section derived_couple
/-
A - i -> A
k ^ |
| v j
B ====== B
-/
parameters {A B : AbGroup} (EC : exact_couple A B) parameters {A B : AbGroup} (EC : exact_couple A B)
local abbreviation i := exact_couple.i EC local abbreviation i := exact_couple.i EC
local abbreviation j := exact_couple.j EC local abbreviation j := exact_couple.j EC
@ -132,9 +139,7 @@ definition SES_of_exact_couple_at_i : SES (ab_kernel i) A (ab_image i) :=
end end
definition kj_zero (a : A) : k (j a) = 1 := definition kj_zero (a : A) : k (j a) = 1 :=
begin is_exact.im_in_ker (exact_couple.exact_jk EC) a
exact sorry
end
definition j_factor : A →g (ab_kernel d) := definition j_factor : A →g (ab_kernel d) :=
begin begin
@ -147,7 +152,6 @@ begin
... = 1 : to_respect_one, ... = 1 : to_respect_one,
end end
definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC := definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC :=
begin begin
exact sorry, exact sorry,