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

remove uses of homomorphism_comp_compute

Browse source 
making group_fun an abbreviation makes this obsolete
This commit is contained in:
Floris van Doorn 2017-06-14 18:46:54 -04:00
parent 5d57e60a43
commit da95ea0acb
3 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
algebra/graded.hlean
View file

@ -414,10 +414,10 @@ end
definition dirsum : LeftModule R := definition dirsum : LeftModule R :=
LeftModule_of_AddAbGroup (dirsum' N) (λr n, dirsum_smul r n) LeftModule_of_AddAbGroup (dirsum' N) (λr n, dirsum_smul r n)
(λr, homomorphism.addstruct (dirsum_smul r)) proof (λr, homomorphism.addstruct (dirsum_smul r)) qed
dirsum_smul_right_distrib proof dirsum_smul_right_distrib qed
dirsum_mul_smul proof dirsum_mul_smul qed
dirsum_one_smul proof dirsum_one_smul qed
/- graded variants of left-module constructions -/ /- graded variants of left-module constructions -/

12
algebra/seq_colim.hlean
View file

@ -47,16 +47,15 @@ namespace group
end end
definition seq_colim_glue {i : @trunctype.mk 0 ℕ _} {a : A i} : seq_colim_incl i a = seq_colim_incl (succ i) (f i a) := definition seq_colim_glue {i : @trunctype.mk 0 ℕ _} {a : A i} : seq_colim_incl i a = seq_colim_incl (succ i) (f i a) :=
begin begin
refine !homomorphism_comp_compute ⬝ _, refine gqg_eq_of_rel _ _,
refine gqg_eq_of_rel _ _ ⬝ (!homomorphism_comp_compute)⁻¹, exact tr (seq_colim_rel.rmk _ _)
exact tr (seq_colim_rel.rmk _ _) end
end
section section
local abbreviation h (m : seq_colim →g A') : Πi, A i →g A' := λi, m ∘g (seq_colim_incl i) local abbreviation h (m : seq_colim →g A') : Πi, A i →g A' := λi, m ∘g (seq_colim_incl i)
local abbreviation k (m : seq_colim →g A') : Πi a, h m i a = h m (succ i) (f i a) := local abbreviation k (m : seq_colim →g A') : Πi a, h m i a = h m (succ i) (f i a) :=
λ i a, !homomorphism_comp_compute ⬝ ap m (@seq_colim_glue i a) ⬝ !homomorphism_comp_compute⁻¹ λ i a, ap m (@seq_colim_glue i a)
definition seq_colim_unique (m : seq_colim →g A') : definition seq_colim_unique (m : seq_colim →g A') :
Πv, seq_colim_elim (h m) (k m) v = m v := Πv, seq_colim_elim (h m) (k m) v = m v :=
@ -77,7 +76,6 @@ namespace group
seq_colim_elim (λi, seq_colim_incl i ∘g h i) seq_colim_elim (λi, seq_colim_incl i ∘g h i)
begin begin
intro i a, intro i a,
refine !homomorphism_comp_compute ⬝ _ ⬝ !homomorphism_comp_compute⁻¹,
refine _ ⬝ ap (seq_colim_incl (succ i)) (p i a)⁻¹, refine _ ⬝ ap (seq_colim_incl (succ i)) (p i a)⁻¹,
apply seq_colim_glue apply seq_colim_glue
end end

3
algebra/submodule.hlean
View file

@ -277,12 +277,13 @@ begin
end end
variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃} variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃}
definition image_elim [constructor] (θ : M₁ →lm M₃) (h : Π⦃g⦄, φ g = 0 → θ g = 0) : definition image_elim [constructor] (θ : M₁ →lm M₃) (h : Π⦃g⦄, φ g = 0 → θ g = 0) :
image_module φ →lm M₃ := image_module φ →lm M₃ :=
begin begin
refine homomorphism.mk (image_elim (group_homomorphism_of_lm_homomorphism θ) h) _, refine homomorphism.mk (image_elim (group_homomorphism_of_lm_homomorphism θ) h) _,
split, split,
{ apply homomorphism.addstruct }, { exact homomorphism.struct (image_elim (group_homomorphism_of_lm_homomorphism θ) _) },
{ intro r, refine @total_image.rec _ _ _ _ (λx, !is_trunc_eq) _, intro g, { intro r, refine @total_image.rec _ _ _ _ (λx, !is_trunc_eq) _, intro g,
apply to_respect_smul } apply to_respect_smul }
end end