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

add explanation of universal property of cofiber

Browse source
This commit is contained in:
Floris van Doorn 2017-06-29 15:03:23 +01:00
parent 00d02ecacf
commit 0d48402927
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
homotopy/pushout.hlean
View file

@ -485,6 +485,11 @@ namespace pushout
apply eq_inv_con_of_con_eq, exact (to_homotopy_pt p)⁻¹ } apply eq_inv_con_of_con_eq, exact (to_homotopy_pt p)⁻¹ }
end end
/-
The maps Z^{C_f} --> Z^Y --> Z^X are exact at Z^Y.
Here Y^X means pointed maps from X to Y and C_f is the cofiber of f.
The maps are given by precomposing with (pcod f) and f.
-/
definition cofiber_exact {X Y Z : Type*} (f : X →* Y) : definition cofiber_exact {X Y Z : Type*} (f : X →* Y) :
is_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) := is_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) :=
begin begin