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

seq_colim_elim added

Browse source
This commit is contained in:
Robert Rose 2017-06-07 10:30:32 -06:00
parent 9256bf8861
commit 21a0dcfcfe
1 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
algebra/seq_colim.hlean
View file

@ -18,14 +18,21 @@ namespace group
definition seq_colim_incl [constructor] (i : ℕ) : A i →g seq_colim :=
qg_map _ ∘g dirsum_incl A i
definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (i + 1) (f i a))
definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (succ i) (f i a))
(v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 1 :=
begin
induction r with r, induction r, exact sorry
induction r with r, induction r,
refine !to_respect_mul ⬝ _,
refine ap (λγ, group_fun (dirsum_elim h) (group_fun (dirsum_incl A i) a) * group_fun (dirsum_elim h) γ) (!to_respect_inv)⁻¹ ⬝ _,
refine ap (λγ, γ * group_fun (dirsum_elim h) (group_fun (dirsum_incl A (succ i)) (f i a)⁻¹)) !dirsum_elim_compute ⬝ _,
refine ap (λγ, (h i a) * γ) !dirsum_elim_compute ⬝ _,
refine ap (λγ, γ * group_fun (h (succ i)) (f i a)⁻¹) !k ⬝ _,
refine ap (λγ, group_fun (h (succ i)) (f i a) * γ) (!to_respect_inv) ⬝ _,
exact !mul.right_inv
end
definition seq_colim_elim [constructor] (h : Πi, A i →g A')
(k : Πi a, h i a = h (i + 1) (f i a)) : seq_colim →g A' :=
(k : Πi a, h i a = h (succ i) (f i a)) : seq_colim →g A' :=
gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k)
end