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

Merge remote-tracking branch 'origin/new_lean' into new_lean

Browse source 
# Conflicts:
#	algebra/exactness.hlean
#	homotopy/pushout.hlean
#	move_to_lib.hlean
This commit is contained in:
Steve Awodey 2017-06-16 14:50:55 -04:00
parent a2c4e0858d
commit 89118f2a8e
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 :=
homology (differential EC) (differential_is_differential EC)
print homology
definition derived_couple_i : derived_couple_A →g derived_couple_A :=
(image_lift (exact_couple.i EC)) ∘g (image_incl (exact_couple.i EC))