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

fix explicit arguments of dirsum_functor_homotopy

Browse source
This commit is contained in:
Floris van Doorn 2017-06-09 14:28:52 -04:00
parent c8043a6f9f
commit f93fc153d4
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
algebra/graded.hlean
View file

@ -391,14 +391,14 @@ dirsum_functor (λi, smul_homomorphism (N i) r)
definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) : definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) :
dirsum_smul (r + s) n = dirsum_smul r n + dirsum_smul s n := dirsum_smul (r + s) n = dirsum_smul r n + dirsum_smul s n :=
begin begin
refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_mul⁻¹, refine dirsum_functor_homotopy _ _ _ n ⬝ !dirsum_functor_mul⁻¹,
intro i ni, exact to_smul_right_distrib r s ni intro i ni, exact to_smul_right_distrib r s ni
end end
definition dirsum_mul_smul' (r s : R) (n : dirsum' N) : definition dirsum_mul_smul' (r s : R) (n : dirsum' N) :
dirsum_smul (r * s) n = (dirsum_smul r ∘a dirsum_smul s) n := dirsum_smul (r * s) n = (dirsum_smul r ∘a dirsum_smul s) n :=
begin begin
refine dirsum_functor_homotopy _ n ⬝ (dirsum_functor_compose _ _ n)⁻¹ᵖ, refine dirsum_functor_homotopy _ _ _ n ⬝ (dirsum_functor_compose _ _ n)⁻¹ᵖ,
intro i ni, exact to_mul_smul r s ni intro i ni, exact to_mul_smul r s ni
end end
@ -408,7 +408,7 @@ proof dirsum_mul_smul' r s n qed
definition dirsum_one_smul (n : dirsum' N) : dirsum_smul 1 n = n := definition dirsum_one_smul (n : dirsum' N) : dirsum_smul 1 n = n :=
begin begin
refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_gid, refine dirsum_functor_homotopy _ _ _ n ⬝ !dirsum_functor_gid,
intro i ni, exact to_one_smul ni intro i ni, exact to_one_smul ni
end end