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-06-16 15:41:15 -04:00
commit a1e01456f1
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
algebra/exact_couple.hlean
View file

@ -129,6 +129,9 @@ definition derived_couple_A : AbGroup :=
definition derived_couple_B : AbGroup := definition derived_couple_B : AbGroup :=
homology (differential EC) (differential_is_differential EC) homology (differential EC) (differential_is_differential EC)
print homology
definition derived_couple_i : derived_couple_A →g derived_couple_A := definition derived_couple_i : derived_couple_A →g derived_couple_A :=
(image_lift (exact_couple.i EC)) ∘g (image_incl (exact_couple.i EC)) (image_lift (exact_couple.i EC)) ∘g (image_incl (exact_couple.i EC))