From 8e366e08c37684e6787742e20027fa7ee804fbc3 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 18 Nov 2016 15:20:22 -0500 Subject: [PATCH] Finish the universal property of the direct sum --- algebra/direct_sum.hlean | 26 +++++++++++--------- algebra/free_commutative_group.hlean | 23 +++++++++++------- algebra/quotient_group.hlean | 36 ++++++++++++++++------------ 3 files changed, 51 insertions(+), 34 deletions(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index 3577240..46ea343 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -23,7 +23,7 @@ namespace group variables {A' : CommGroup} definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _) - local abbreviation ι := @free_comm_group_inclusion + local abbreviation ι [constructor] := @free_comm_group_inclusion inductive dirsum_rel : dirsum_carrier → Type := | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹) @@ -35,26 +35,30 @@ namespace group homomorphism.mk (λy, class_of (ι ⟨i, y⟩)) begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end - definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' := + definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier) + (r : ∥dirsum_rel g∥) : free_comm_group_elim (λv, f v.1 v.2) g = 1 := begin - refine homomorphism.mk (gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) _) _, - { intro g r, induction r with r, induction r, - rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul, - rewrite [one_mul], apply ap (free_comm_group_elim (λ v, group_fun (f v.1) v.2)), - exact sorry - }, - { exact sorry } + induction r with r, induction r, + rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul, + rewrite [one_mul, to_respect_mul, ▸*, ↑foldl, +one_mul, to_respect_mul] end + definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' := + gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f) + definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) : dirsum_elim f ∘g dirsum_incl i ~ f i := begin - intro g, exact sorry + intro g, apply one_mul end definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A') (H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f := - sorry + begin + apply gqg_elim_unique, + apply free_comm_group_elim_unique, + intro x, induction x with i y, exact H i y + end end diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean index c9ca0c7..26d9af7 100644 --- a/algebra/free_commutative_group.hlean +++ b/algebra/free_commutative_group.hlean @@ -174,20 +174,27 @@ namespace group definition fn_of_free_comm_group_elim [unfold_full] (φ : free_comm_group X →g A) : X → A := φ ∘ free_comm_group_inclusion + definition free_comm_group_elim_unique [constructor] (f : X → A) (k : free_comm_group X →g A) + (H : k ∘ free_comm_group_inclusion ~ f) : k ~ free_comm_group_elim f := + begin + refine set_quotient.rec_prop _, intro l, esimp, + induction l with s l IH, + { esimp [foldl], exact to_respect_one k}, + { rewrite [foldl_cons, fgh_helper_mul], + refine to_respect_mul k (class_of [s]) (class_of l) ⬝ _, + rewrite [IH], apply ap (λx, x * _), induction s: rewrite [▸*, one_mul, -H a], + apply to_respect_inv } + end + variables (X A) - definition free_comm_group_elim_equiv_fn : (free_comm_group X →g A) ≃ (X → A) := + definition free_comm_group_elim_equiv_fn [constructor] : (free_comm_group X →g A) ≃ (X → A) := begin fapply equiv.MK, { exact fn_of_free_comm_group_elim}, { exact free_comm_group_elim}, { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul}, - { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp, - induction l with s l IH, - { esimp [foldl], symmetry, exact to_respect_one φ}, - { rewrite [foldl_cons, fgh_helper_mul], - refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹, - rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _), - exact !to_respect_inv⁻¹}} + { intro k, symmetry, apply homomorphism_eq, apply free_comm_group_elim_unique, + reflexivity } end end group diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index 82bc746..314ba15 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -37,7 +37,7 @@ namespace group have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc (g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)] ... = g * k⁻¹ : by rewrite inv_mul_cancel_right, - show N (g * k⁻¹), from H2 ▸ H1 + show N (g * k⁻¹), by rewrite [-H2]; exact H1 theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) := is_equivalence.mk quotient_rel_refl @@ -53,7 +53,7 @@ namespace group g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc ... = g⁻¹ * h : inv_mul_cancel_right ... = g⁻¹ * h⁻¹⁻¹ : by rewrite algebra.inv_inv, - show N (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1 + show N (g⁻¹ * h⁻¹⁻¹), by rewrite [-H2]; exact H1 theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h') : quotient_rel N (g * g') (h * h') := @@ -187,26 +187,33 @@ namespace group apply rel_of_eq _ H end - definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := + definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) + (g : quotient_group N) : G' := + begin + refine set_quotient.elim f _ g, + intro g h K, + apply eq_of_mul_inv_eq_one, + have e : f (g * h⁻¹) = f g * (f h)⁻¹, + from calc + f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul + ... = f g * (f h)⁻¹ : to_respect_inv, + rewrite (inverse e), + apply H, exact K + end + + definition quotient_group_elim [constructor] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := begin fapply homomorphism.mk, -- define function - { apply set_quotient.elim f, - intro g h K, - apply eq_of_mul_inv_eq_one, - have e : f (g * h⁻¹) = f g * (f h)⁻¹, - from calc - f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul - ... = f g * (f h)⁻¹ : to_respect_inv, - rewrite (inverse e), - apply H, exact K}, + { exact quotient_group_elim_fun f H }, { intro g h, induction g using set_quotient.rec_prop with g, induction h using set_quotient.rec_prop with h, krewrite (inverse (to_respect_mul (qg_map N) g h)), unfold qg_map, esimp, exact to_respect_mul f g h } end - definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group_elim f H ∘g qg_map N ~ f := + definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : + quotient_group_elim f H ∘g qg_map N ~ f := begin intro g, reflexivity end @@ -215,7 +222,6 @@ namespace group : ( k ∘g qg_map N ~ f ) → k ~ quotient_group_elim f H := begin intro K cg, induction cg using set_quotient.rec_prop with g, - krewrite (quotient_group_compute f), exact K g end @@ -340,7 +346,7 @@ print iff.mpr definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h := eq_of_rel (tr (rincl H)) - definition gqg_elim (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) + definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) : quotient_comm_group_gen →g A₂ := begin apply quotient_group_elim f,