diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index d90f763..cfaa89e 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -21,12 +21,12 @@ namespace group definition Group_arrow (A : Type) (G : Group) : Group := Group.mk (A → G) _ - definition comm_group_arrow [instance] (A B : Type) [comm_group B] : comm_group (A → B) := - ⦃comm_group, group_arrow A B, + definition ab_group_arrow [instance] (A B : Type) [ab_group B] : ab_group (A → B) := + ⦃ab_group, group_arrow A B, mul_comm := by intros; apply eq_of_homotopy; intro a; apply mul.comm⦄ - definition CommGroup_arrow (A : Type) (G : CommGroup) : CommGroup := - CommGroup.mk (A → G) _ + definition AbGroup_arrow (A : Type) (G : AbGroup) : AbGroup := + AbGroup.mk (A → G) _ definition pgroup_ppmap [instance] (A B : Type*) [pgroup B] : pgroup (ppmap A B) := begin @@ -44,12 +44,12 @@ namespace group definition Group_pmap (A : Type*) (G : Group) : Group := Group_of_pgroup (ppmap A (pType_of_Group G)) - definition CommGroup_pmap (A : Type*) (G : CommGroup) : CommGroup := - CommGroup.mk (A →* pType_of_Group G) - ⦃ comm_group, Group.struct (Group_pmap A G), + definition AbGroup_pmap (A : Type*) (G : AbGroup) : AbGroup := + AbGroup.mk (A →* pType_of_Group G) + ⦃ ab_group, Group.struct (Group_pmap A G), mul_comm := by intro f g; apply pmap_eq_of_homotopy; intro a; apply mul.comm ⦄ - definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : CommGroup) : + definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : AbGroup) : Group_pmap A G →g Group_pmap A' G := begin fapply homomorphism.mk, diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index 3577240..074d1d1 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -13,21 +13,21 @@ open eq algebra is_trunc set_quotient relation sigma prod sum list trunc functio namespace group variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - {A B : CommGroup} + {A B : AbGroup} variables (X : Set) {l l' : list (X ⊎ X)} section - parameters {I : Set} (Y : I → CommGroup) - variables {A' : CommGroup} + parameters {I : Set} (Y : I → AbGroup) + variables {A' : AbGroup} - definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _) - local abbreviation ι := @free_comm_group_inclusion + definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _) + local abbreviation ι [constructor] := @free_ab_group_inclusion inductive dirsum_rel : dirsum_carrier → Type := | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹) - definition dirsum : CommGroup := quotient_comm_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥) + definition dirsum : AbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥) -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier := @@ -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_ab_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_ab_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_ab_group_elim_unique, + intro x, induction x with i y, exact H i y + end end diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 68507ce..78f14a5 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -11,50 +11,50 @@ import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .q open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc equiv -structure is_exact {A B C : CommGroup} (f : A →g B) (g : B →g C) := +structure is_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) := ( im_in_ker : Π(a:A), g (f a) = 1) - ( ker_in_im : Π(b:B), (g b = 1) → ∃(a:A), f a = b) + ( ker_in_im : Π(b:B), (g b = 1) → ∃(a:A), f a = b) -definition is_differential {B : CommGroup} (d : B →g B) := Π(b:B), d (d b) = 1 +definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1 -definition image_subgroup_of_diff {B : CommGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (comm_kernel d) := +definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (ab_kernel d) := subgroup_rel_of_subgroup (image_subgroup d) (kernel_subgroup d) begin - intro g p, + intro g p, induction p with f, induction f with h p, - rewrite [p⁻¹], + rewrite [p⁻¹], esimp, - exact H h + exact H h end -definition homology {B : CommGroup} (d : B →g B) (H : is_differential d) : CommGroup := - @quotient_comm_group (comm_kernel d) (image_subgroup_of_diff d H) +definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup := + @quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H) -structure exact_couple (A B : CommGroup) : Type := +structure exact_couple (A B : AbGroup) : Type := ( i : A →g A) (j : A →g B) (k : B →g A) ( exact_ij : is_exact i j) ( exact_jk : is_exact j k) ( exact_ki : is_exact k i) -definition differential {A B : CommGroup} (EC : exact_couple A B) : B →g B := +definition differential {A B : AbGroup} (EC : exact_couple A B) : B →g B := (exact_couple.j EC) ∘g (exact_couple.k EC) -definition differential_is_differential {A B : CommGroup} (EC : exact_couple A B) : is_differential (differential EC) := +definition differential_is_differential {A B : AbGroup} (EC : exact_couple A B) : is_differential (differential EC) := begin - induction EC, - induction exact_jk, + induction EC, + induction exact_jk, intro b, exact (ap (group_fun j) (im_in_ker (group_fun k b))) ⬝ (respect_one j) end section derived_couple - variables {A B : CommGroup} (EC : exact_couple A B) + variables {A B : AbGroup} (EC : exact_couple A B) -definition derived_couple_A : CommGroup := - comm_subgroup (image_subgroup (exact_couple.i EC)) +definition derived_couple_A : AbGroup := + ab_subgroup (image_subgroup (exact_couple.i EC)) -definition derived_couple_B : CommGroup := +definition derived_couple_B : AbGroup := homology (differential EC) (differential_is_differential EC) definition derived_couple_i : derived_couple_A EC →g derived_couple_A EC := diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean index c9ca0c7..a459968 100644 --- a/algebra/free_commutative_group.hlean +++ b/algebra/free_commutative_group.hlean @@ -12,12 +12,12 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list tru namespace group - variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup} + variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup} variables (X : Set) {l l' : list (X ⊎ X)} - /- Free Commutative Group of a set -/ - namespace free_comm_group + /- Free Abelian Group of a set -/ + namespace free_ab_group inductive fcg_rel : list (X ⊎ X) → list (X ⊎ X) → Type := | rrefl : Πl, fcg_rel l l @@ -133,22 +133,22 @@ namespace group rewrite [-append_concat], apply IH} end end - end free_comm_group open free_comm_group + end free_ab_group open free_ab_group variables (X) - definition group_free_comm_group [constructor] : comm_group (fcg_carrier X) := - comm_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one + definition group_free_ab_group [constructor] : ab_group (fcg_carrier X) := + ab_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one fcg_inv fcg_mul_left_inv fcg_mul_comm - definition free_comm_group [constructor] : CommGroup := - CommGroup.mk _ (group_free_comm_group X) + definition free_ab_group [constructor] : AbGroup := + AbGroup.mk _ (group_free_ab_group X) /- The universal property of the free commutative group -/ variables {X A} - definition free_comm_group_inclusion [constructor] (x : X) : free_comm_group X := + definition free_ab_group_inclusion [constructor] (x : X) : free_ab_group X := class_of [inl x] - theorem fgh_helper_respect_comm_rel (f : X → A) (r : fcg_rel X l l') + theorem fgh_helper_respect_fcg_rel (f : X → A) (r : fcg_rel X l l') : Π(g : A), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' := begin induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g, @@ -160,34 +160,41 @@ namespace group { exact !IH₁ ⬝ !IH₂} end - definition free_comm_group_elim [constructor] (f : X → A) : free_comm_group X →g A := + definition free_ab_group_elim [constructor] (f : X → A) : free_ab_group X →g A := begin fapply homomorphism.mk, { intro g, refine set_quotient.elim _ _ g, { intro l, exact foldl (fgh_helper f) 1 l}, { intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r, - exact fgh_helper_respect_comm_rel f r 1}}, + exact fgh_helper_respect_fcg_rel f r 1}}, { refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l', esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul} end - definition fn_of_free_comm_group_elim [unfold_full] (φ : free_comm_group X →g A) : X → A := - φ ∘ free_comm_group_inclusion + definition fn_of_free_ab_group_elim [unfold_full] (φ : free_ab_group X →g A) : X → A := + φ ∘ free_ab_group_inclusion + + definition free_ab_group_elim_unique [constructor] (f : X → A) (k : free_ab_group X →g A) + (H : k ∘ free_ab_group_inclusion ~ f) : k ~ free_ab_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_ab_group_elim_equiv_fn [constructor] : (free_ab_group X →g A) ≃ (X → A) := begin fapply equiv.MK, - { exact fn_of_free_comm_group_elim}, - { exact free_comm_group_elim}, + { exact fn_of_free_ab_group_elim}, + { exact free_ab_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_ab_group_elim_unique, + reflexivity } end end group diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean index d502b69..c46d923 100644 --- a/algebra/free_group.hlean +++ b/algebra/free_group.hlean @@ -12,7 +12,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list tru namespace group - variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup} + variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup} /- Free Group of a set -/ variables (X : Set) {l l' : list (X ⊎ X)} diff --git a/algebra/group_constructions.hlean b/algebra/group_constructions.hlean index f768db1..d7c9a36 100644 --- a/algebra/group_constructions.hlean +++ b/algebra/group_constructions.hlean @@ -11,29 +11,29 @@ import .free_commutative_group open eq algebra is_trunc sigma sigma.ops prod trunc function equiv namespace group - variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup} + variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup} /- Tensor group (WIP) -/ /- namespace tensor_group variables {A B} - local abbreviation ι := @free_comm_group_inclusion + local abbreviation ι := @free_ab_group_inclusion - inductive tensor_rel_type : free_comm_group (Set_of_Group A ×t Set_of_Group B) → Type := + inductive tensor_rel_type : free_ab_group (Set_of_Group A ×t Set_of_Group B) → Type := | mul_left : Π(a₁ a₂ : A) (b : B), tensor_rel_type (ι (a₁, b) * ι (a₂, b) * (ι (a₁ * a₂, b))⁻¹) | mul_right : Π(a : A) (b₁ b₂ : B), tensor_rel_type (ι (a, b₁) * ι (a, b₂) * (ι (a, b₁ * b₂))⁻¹) open tensor_rel_type - definition tensor_rel' (x : free_comm_group (Set_of_Group A ×t Set_of_Group B)) : Prop := + definition tensor_rel' (x : free_ab_group (Set_of_Group A ×t Set_of_Group B)) : Prop := ∥ tensor_rel_type x ∥ - definition tensor_group_rel (A B : CommGroup) - : normal_subgroup_rel (free_comm_group (Set_of_Group A ×t Set_of_Group B)) := + definition tensor_group_rel (A B : AbGroup) + : normal_subgroup_rel (free_ab_group (Set_of_Group A ×t Set_of_Group B)) := sorry /- relation generated by tensor_rel'-/ - definition tensor_group [constructor] : CommGroup := - quotient_comm_group (tensor_group_rel A B) + definition tensor_group [constructor] : AbGroup := + quotient_ab_group (tensor_group_rel A B) end tensor_group-/ diff --git a/algebra/module.hlean b/algebra/module.hlean index f6496d2..7475fb7 100644 --- a/algebra/module.hlean +++ b/algebra/module.hlean @@ -17,7 +17,7 @@ infixl ` • `:73 := has_scalar.smul /- modules over a ring -/ -structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, comm_group M renaming +structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, ab_group M renaming mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg mul_left_inv→add_left_inv mul_comm→add_comm := (smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y))) @@ -26,12 +26,12 @@ structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, comm (one_smul : Π x, smul one x = x) /- we make it a class now (and not as part of the structure) to avoid - left_module.to_comm_group to be an instance -/ + left_module.to_ab_group to be an instance -/ attribute left_module [class] -definition add_comm_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R] - [H : left_module R M] : add_comm_group M := -@left_module.to_comm_group R M K H +definition add_ab_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R] + [H : left_module R M] : add_ab_group M := +@left_module.to_ab_group R M K H definition has_scalar_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R] [H : left_module R M] : has_scalar R M := diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean index c585007..800650f 100644 --- a/algebra/product_group.hlean +++ b/algebra/product_group.hlean @@ -13,7 +13,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum namespace group variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - {A B : CommGroup} + {A B : AbGroup} /- Binary products (direct product) of Groups -/ definition product_one [constructor] : G × G' := (one, one) @@ -39,7 +39,7 @@ namespace group theorem product_mul_left_inv (g : G × G') : g⁻¹ * g = 1 := prod_eq !mul.left_inv !mul.left_inv - theorem product_mul_comm {G G' : CommGroup} (g h : G × G') : g * h = h * g := + theorem product_mul_comm {G G' : AbGroup} (g h : G × G') : g * h = h * g := prod_eq !mul.comm !mul.comm end @@ -52,11 +52,11 @@ namespace group definition product [constructor] : Group := Group.mk _ (group_prod G G') - definition comm_group_prod [constructor] (G G' : CommGroup) : comm_group (G × G') := - ⦃comm_group, group_prod G G', mul_comm := product_mul_comm⦄ + definition ab_group_prod [constructor] (G G' : AbGroup) : ab_group (G × G') := + ⦃ab_group, group_prod G G', mul_comm := product_mul_comm⦄ - definition comm_product [constructor] (G G' : CommGroup) : CommGroup := - CommGroup.mk _ (comm_group_prod G G') + definition ab_product [constructor] (G G' : AbGroup) : AbGroup := + AbGroup.mk _ (ab_group_prod G G') infix ` ×g `:30 := group.product diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index d98f5da..a3d87f0 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -13,7 +13,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod trunc functi namespace group variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - variables {A B : CommGroup} + variables {A B : AbGroup} /- Quotient Group -/ @@ -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') := @@ -113,7 +113,7 @@ namespace group exact ap class_of !mul.left_inv end - theorem quotient_mul_comm {G : CommGroup} {N : normal_subgroup_rel G} (g h : qg N) + theorem quotient_mul_comm {G : AbGroup} {N : normal_subgroup_rel G} (g h : qg N) : g * h = h * g := begin refine set_quotient.rec_prop _ g, clear g, intro g, @@ -131,18 +131,18 @@ namespace group definition quotient_group [constructor] : Group := Group.mk _ (group_qg N) - definition comm_group_qg [constructor] {G : CommGroup} (N : normal_subgroup_rel G) - : comm_group (qg N) := - ⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄ + definition ab_group_qg [constructor] {G : AbGroup} (N : normal_subgroup_rel G) + : ab_group (qg N) := + ⦃ab_group, group_qg N, mul_comm := quotient_mul_comm⦄ - definition quotient_comm_group [constructor] {G : CommGroup} (N : subgroup_rel G) - : CommGroup := - CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N)) + definition quotient_ab_group [constructor] {G : AbGroup} (N : subgroup_rel G) + : AbGroup := + AbGroup.mk _ (ab_group_qg (normal_subgroup_rel_ab N)) definition qg_map [constructor] : G →g quotient_group N := homomorphism.mk class_of (λ g h, idp) - definition comm_gq_map {G : CommGroup} (N : subgroup_rel G) : G →g quotient_comm_group N := + definition ab_gq_map {G : AbGroup} (N : subgroup_rel G) : G →g quotient_ab_group N := begin fapply homomorphism.mk, exact class_of, @@ -166,7 +166,7 @@ namespace group unfold quotient_rel, rewrite e, exact H end - definition comm_gq_map_eq_one {K : subgroup_rel A} (g :A) (H : K g) : comm_gq_map K g = 1 := + definition ab_gq_map_eq_one {K : subgroup_rel A} (g :A) (H : K g) : ab_gq_map K g = 1 := begin apply eq_of_rel, have e : (g * 1⁻¹ = g), @@ -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 @@ -231,17 +237,17 @@ namespace group {fapply is_prop.elimo} } end -definition comm_group_quotient_homomorphism (A B : CommGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B) - (p : Π(a:A), K(a) → L(f a)) : quotient_comm_group K →g quotient_comm_group L := +definition ab_group_quotient_homomorphism (A B : AbGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B) + (p : Π(a:A), K(a) → L(f a)) : quotient_ab_group K →g quotient_ab_group L := begin fapply quotient_group_elim, - exact (comm_gq_map L) ∘g f, + exact (ab_gq_map L) ∘g f, intro a, intro k, - exact @comm_gq_map_eq_one B L (f a) (p a k), + exact @ab_gq_map_eq_one B L (f a) (p a k), end -definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_comm_group (kernel_subgroup f) ≃g comm_image f := +definition ab_group_first_iso_thm (A B : AbGroup) (f : A →g B) : quotient_ab_group (kernel_subgroup f) ≃g ab_image f := begin fapply isomorphism.mk, fapply quotient_group_elim, @@ -254,12 +260,60 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_ -- show that the above map is injective and surjective. end +definition ab_group_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g ) + : Π a:A , kernel_subgroup(g)(a) → kernel_subgroup(f)(a) := + begin + intro a, + intro p, + exact calc + f a = i (g a) : homotopy_of_eq (ap group_fun H) a + ... = i 1 : ap i p + ... = 1 : respect_one i + end + +definition ab_group_kernel_equivalent {A B : AbGroup} (C : AbGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i) + : Π a:A , kernel_subgroup(g)(a) ↔ kernel_subgroup(f)(a) := +begin + intro a, + fapply iff.intro, + exact ab_group_kernel_factor f g H a, + intro p, + apply @is_injective_of_is_embedding _ _ i _ (g a) 1, + exact calc + i (g a) = f a : (homotopy_of_eq (ap group_fun H) a)⁻¹ + ... = 1 : p + ... = i 1 : (respect_one i)⁻¹ +end + +definition ab_group_kernel_image_lift (A B : AbGroup) (f : A →g B) + : Π a : A, kernel_subgroup(image_lift(f))(a) ↔ kernel_subgroup(f)(a) := + begin + fapply ab_group_kernel_equivalent (ab_image f) (f) (image_lift(f)) (image_incl(f)), + exact image_factor f, + exact is_embedding_of_is_injective (image_incl_injective(f)), + end + +definition ab_group_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) + : quotient_ab_group (kernel_subgroup f) →g ab_image (f) := +begin +fapply quotient_group_elim (image_lift f), intro a, intro p, +apply iff.mpr (ab_group_kernel_image_lift _ _ f a) p +end + +definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) + : is_surjective (ab_group_kernel_quotient_to_image f) := + begin + intro b, exact sorry + -- have H : is_surjective (image_lift f) + end + +print iff.mpr /- set generating normal subgroup -/ section - parameters {A₁ : CommGroup} (S : A₁ → Prop) - variable {A₂ : CommGroup} + parameters {A₁ : AbGroup} (S : A₁ → Prop) + variable {A₂ : AbGroup} inductive generating_relation' : A₁ → Type := | rincl : Π{g}, S g → generating_relation' g @@ -283,17 +337,17 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_ Rmul := gr_mul⦄ parameter (A₁) - definition quotient_comm_group_gen : CommGroup := quotient_comm_group normal_generating_relation + definition quotient_ab_group_gen : AbGroup := quotient_ab_group normal_generating_relation - definition gqg_map [constructor] : A₁ →g quotient_comm_group_gen := + definition gqg_map [constructor] : A₁ →g quotient_ab_group_gen := qg_map _ parameter {A₁} 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) - : quotient_comm_group_gen →g A₂ := + definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) + : quotient_ab_group_gen →g A₂ := begin apply quotient_group_elim f, intro g r, induction r with r, @@ -311,7 +365,7 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_ end definition gqg_elim_unique (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) - (k : quotient_comm_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H := + (k : quotient_ab_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H := !gelim_unique end diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index 78d66b6..1d00fac 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -130,12 +130,12 @@ namespace group abbreviation is_normal_subgroup [unfold 2] := @normal_subgroup_rel.is_normal_subgroup variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - {A B : CommGroup} + {A B : AbGroup} theorem is_normal_subgroup' (h : G) (r : N g) : N (h⁻¹ * g * h) := inv_inv h ▸ is_normal_subgroup N h⁻¹ r - definition normal_subgroup_rel_comm.{u} [constructor] (R : subgroup_rel.{_ u} A) + definition normal_subgroup_rel_ab.{u} [constructor] (R : subgroup_rel.{_ u} A) : normal_subgroup_rel.{_ u} A := ⦃normal_subgroup_rel, R, is_normal_subgroup := abstract begin @@ -209,7 +209,7 @@ namespace group theorem subgroup_mul_left_inv (g : sg H) : g⁻¹ * g = 1 := subtype_eq !mul.left_inv - theorem subgroup_mul_comm {G : CommGroup} {H : subgroup_rel G} (g h : sg H) + theorem subgroup_mul_comm {G : AbGroup} {H : subgroup_rel G} (g h : sg H) : g * h = h * g := subtype_eq !mul.comm @@ -223,17 +223,17 @@ namespace group definition subgroup [constructor] : Group := Group.mk _ (group_sg H) - definition comm_group_sg [constructor] {G : CommGroup} (H : subgroup_rel G) - : comm_group (sg H) := - ⦃comm_group, group_sg H, mul_comm := subgroup_mul_comm⦄ + definition ab_group_sg [constructor] {G : AbGroup} (H : subgroup_rel G) + : ab_group (sg H) := + ⦃ab_group, group_sg H, mul_comm := subgroup_mul_comm⦄ - definition comm_subgroup [constructor] {G : CommGroup} (H : subgroup_rel G) - : CommGroup := - CommGroup.mk _ (comm_group_sg H) + definition ab_subgroup [constructor] {G : AbGroup} (H : subgroup_rel G) + : AbGroup := + AbGroup.mk _ (ab_group_sg H) definition kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel_subgroup f) - definition comm_kernel {G H : CommGroup} (f : G →g H) : CommGroup := comm_subgroup (kernel_subgroup f) + definition ab_kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel_subgroup f) definition incl_of_subgroup [constructor] {G : Group} (H : subgroup_rel G) : subgroup H →g G := begin @@ -258,24 +258,24 @@ namespace group definition image {G H : Group} (f : G →g H) : Group := subgroup (image_subgroup f) - definition CommGroup_of_Group.{u} (G : Group.{u}) (H : Π (g h : G), mul g h = mul h g) : CommGroup.{u} := + definition AbGroup_of_Group.{u} (G : Group.{u}) (H : Π (g h : G), mul g h = mul h g) : AbGroup.{u} := begin induction G, induction struct, - fapply CommGroup.mk, + fapply AbGroup.mk, exact carrier, - fapply comm_group.mk, - repeat assumption, + fapply ab_group.mk, + repeat assumption, exact H end - definition comm_image {G : CommGroup} {H : Group} (f : G →g H) : CommGroup := - CommGroup_of_Group (image f) + definition ab_image {G : AbGroup} {H : Group} (f : G →g H) : AbGroup := + AbGroup_of_Group (image f) begin intro g h, induction g with x t, induction h with y s, fapply subtype_eq, - induction t with p, induction s with q, induction p with g p, induction q with h q, induction p, induction q, + induction t with p, induction s with q, induction p with g p, induction q with h q, induction p, induction q, refine (((respect_mul f g h)⁻¹ ⬝ _) ⬝ (respect_mul f h g)), apply (ap f), induction G, induction struct, apply mul_comm @@ -299,9 +299,9 @@ namespace group definition image_lift {G H : Group} (f : G →g H) : G →g image f := begin fapply hom_lift f, - intro g, + intro g, apply tr, - fapply fiber.mk, + fapply fiber.mk, exact g, reflexivity end @@ -317,7 +317,7 @@ namespace group intro p, fapply subtype_eq, exact p - end + end definition image_incl_eq_one {G H : Group} (f : G →g H) : Π (x : image f), (image_incl f x = 1) → x = 1 := begin diff --git a/colim.hlean b/colim.hlean index ee761ee..0d9cd8f 100644 --- a/colim.hlean +++ b/colim.hlean @@ -389,7 +389,7 @@ namespace seq_colim rewrite [▸*, +ap_con, ap_inv, +succ_add_tr_rep_succ, con_inv, inv_con_inv_right, +con.assoc], apply whisker_left, rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'], - note s := (eq_top_of_square (natural_square + note s := (eq_top_of_square (natural_square_tr (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹, rewrite [inv_con_inv_right at s, -con.assoc at s], exact s end diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean deleted file mode 100644 index e7e5de8..0000000 --- a/homotopy/EM.hlean +++ /dev/null @@ -1,279 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Authors: Floris van Doorn - -Eilenberg MacLane spaces --/ - -import homotopy.EM .spectrum - -open eq is_equiv equiv is_conn is_trunc unit function pointed nat group algebra trunc trunc_index - fiber prod pointed susp EM.ops - -namespace EM - - /- Functorial action of Eilenberg-Maclane spaces -/ - - definition pEM1_functor [constructor] {G H : Group} (φ : G →g H) : pEM1 G →* pEM1 H := - begin - fconstructor, - { intro g, induction g, - { exact base }, - { exact pth (φ g) }, - { exact ap pth (respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }}, - { reflexivity } - end - - definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) : - EMadd1 G n →* EMadd1 H n := - begin - apply ptrunc_functor, - apply iterate_psusp_functor, - apply pEM1_functor, - exact φ - end - - definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) : - K G n →* K H n := - begin - cases n with n, - { exact pmap_of_homomorphism φ }, - { exact EMadd1_functor φ n } - end - - -- TODO: (K G n →* K H n) ≃ (G →g H) - - /- Equivalence of Groups and pointed connected 1-truncated types -/ - - definition pEM1_pequiv_ptruncconntype (X : 1-Type*[0]) : pEM1 (π₁ X) ≃* X := - pEM1_pequiv_type - - definition Group_equiv_ptruncconntype [constructor] : Group ≃ 1-Type*[0] := - equiv.MK (λG, ptruncconntype.mk (pEM1 G) _ pt !is_conn_pEM1) - (λX, π₁ X) - begin intro X, apply ptruncconntype_eq, esimp, exact pEM1_pequiv_type end - begin intro G, apply eq_of_isomorphism, apply fundamental_group_pEM1 end - - /- Higher EM-spaces -/ - - /- K(G, 2) is unique (see below for general case) -/ - definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : Ω[succ n] (EMadd1 G n) ≃* pType_of_Group G := - begin - refine _ ⬝e* loop_pEM1 G, - cases n with n, - { refine !loop_ptrunc_pequiv ⬝e* _, refine ptrunc_pequiv _ _ _, - apply is_trunc_eq, apply is_trunc_EM1}, - induction n with n IH, - { exact loop_pequiv_loop (loop_EM2 G)}, - refine _ ⬝e* IH, - refine !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* ⬝e* _ ⬝e* !homotopy_group_pequiv_loop_ptrunc, - apply iterate_psusp_stability_pequiv, - rexact add_mul_le_mul_add n 1 1 - end - - definition EM2_map [unfold 7] {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G) - (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q) - [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 → X := - begin - change trunc 2 (susp (EM1 G)) → X, intro x, - induction x with x, induction x with x, - { exact pt}, - { exact pt}, - { change carrier (Ω X), refine EM1_map e r x} - end - - definition pEM2_pmap [constructor] {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G) - (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q) - [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 →* X := - pmap.mk (EM2_map e r) idp - - definition loop_pEM2_pmap {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G) - (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q) - [is_conn 1 X] [is_trunc 2 X] : - Ω→[2](pEM2_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G 1 := - begin - exact sorry - end - - -- TODO: make arguments in trivial_homotopy_group_of_is_trunc implicit - attribute is_conn_EMadd1 is_trunc_EMadd1 [instance] - definition pEM2_pequiv' {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G) - (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q) - [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 ≃* X := - begin - apply pequiv_of_pmap (pEM2_pmap e r), - have is_conn 0 (EMadd1 G 1), from !is_conn_of_is_conn_succ, - have is_trunc 2 (EMadd1 G 1), from !is_trunc_EMadd1, - refine whitehead_principle_pointed 2 _ _, - intro k, apply @nat.lt_by_cases k 2: intro H, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, - { cases H, esimp, apply is_equiv_trunc_functor, esimp, - apply is_equiv.homotopy_closed, rotate 1, - { symmetry, exact loop_pEM2_pmap _ _}, - apply is_equiv_compose, apply pequiv.to_is_equiv, apply to_is_equiv}, - { apply @is_equiv_of_is_contr, - exact trivial_homotopy_group_of_is_trunc _ H, - apply @trivial_homotopy_group_of_is_trunc, rotate 1, exact H, exact _inst_2} - end - - definition pEM2_pequiv {G : CommGroup} {X : Type*} (e : πg[1+1] X ≃g G) - [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 ≃* X := - begin - have is_set (Ω[2] X), from !is_trunc_eq, - apply pEM2_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e), - intro p q, esimp, exact to_respect_mul e (tr p) (tr q) - end - - -- general case - definition EMadd1_map [unfold 8] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - (r : Π(p q : Ω (Ω[n] X)), e (p ⬝ q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n → X := - begin - revert X e r H1 H2, induction n with n f: intro X e r H1 H2, - { change trunc 1 (EM1 G) → X, intro x, induction x with x, exact EM1_map e r x}, - change trunc (n.+2) (susp (iterate_psusp n (pEM1 G))) → X, intro x, - induction x with x, induction x with x, - { exact pt}, - { exact pt}, - change carrier (Ω X), refine f _ _ _ _ _ (tr x), - { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in}, - exact abstract begin - intro p q, refine _ ⬝ !r, apply ap e, esimp, - apply inv_eq_of_eq, - refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, - exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q - end end - end - - definition pEMadd1_pmap [constructor] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := - pmap.mk (EMadd1_map e r) begin cases n with n: reflexivity end - - definition loop_pEMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : - Ω→[succ n](pEMadd1_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G n := - begin - apply homotopy_of_inv_homotopy_pre (loopn_EMadd1 G n), - intro g, esimp at *, - revert X e r H1 H2, induction n with n IH: intro X e r H1 H2, - { refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _, apply elim_pth}, - { replace (succ (succ n)) with ((succ n) + 1), rewrite [apn_succ], - exact sorry} - -- exact !idp_con ⬝ !elim_pth - end - - -- definition is_conn_of_le (n : ℕ₋₂) (A : Type) [is_conn (n.+1) A] : - -- is_conn n A := - -- is_trunc_trunc_of_le A -2 (trunc_index.self_le_succ n) - -- attribute is_conn_EMadd1 is_trunc_EMadd1 [instance] - - definition pEMadd1_pequiv' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := - begin - apply pequiv_of_pmap (pEMadd1_pmap e r), - have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n), - have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1, - refine whitehead_principle_pointed (n.+1) _ _, - intro k, apply @nat.lt_by_cases k (succ n): intro H, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, - { cases H, esimp, apply is_equiv_trunc_functor, esimp, - apply is_equiv.homotopy_closed, rotate 1, - { symmetry, exact loop_pEMadd1_pmap _ _}, - apply is_equiv_compose, apply pequiv.to_is_equiv}, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_trunc _ H} - end - - definition pEMadd1_pequiv {G : CommGroup} {X : Type*} {n : ℕ} (e : πg[n+1] X ≃g G) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := - begin - have is_set (Ω[succ n] X), from !is_set_loopn, - apply pEMadd1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e), - intro p q, esimp, exact to_respect_mul e (tr p) (tr q) - end - - definition EM_pequiv_succ {G : CommGroup} {X : Type*} {n : ℕ} (e : πg[n+1] X ≃g G) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EM G (succ n) ≃* X := - pEMadd1_pequiv e - - definition EM_pequiv_zero {G : CommGroup} {X : Type*} (e : X ≃* pType_of_Group G) : EM G 0 ≃* X := - proof e⁻¹ᵉ* qed - - definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum := - spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) - - /- uniqueness of K(G,n), method 2: -/ - --- definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) --- : π*[k + 1] (psusp A) ≃* π*[k] A := --- calc --- π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (homotopy_group_succ_in (psusp A) k) --- ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) --- ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) --- ... ≃* π*[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* - - definition iterate_psusp_succ_pequiv (n : ℕ) (A : Type*) : - iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := - begin - induction n with n IH, - { reflexivity}, - { exact psusp_equiv IH} - end - - definition is_conn_psusp [instance] (n : trunc_index) (A : Type*) - [H : is_conn n A] : is_conn (n .+1) (psusp A) := - is_conn_susp n A - - definition iterated_freudenthal_pequiv (A : Type*) {n k m : ℕ} [HA : is_conn n A] (H : k ≤ 2 * n) - : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_psusp m A)) := - begin - revert A n k HA H, induction m with m IH: intro A n k HA H, - { reflexivity}, - { have H2 : succ k ≤ 2 * succ n, - from calc - succ k ≤ succ (2 * n) : succ_le_succ H - ... ≤ 2 * succ n : self_le_succ, - exact calc - ptrunc k A ≃* ptrunc k (Ω (psusp A)) : freudenthal_pequiv A H - ... ≃* Ω (ptrunc (succ k) (psusp A)) : loop_ptrunc_pequiv - ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_psusp m (psusp A)))) : - loop_pequiv_loop (IH (psusp A) (succ n) (succ k) _ H2) - ... ≃* ptrunc k (Ω[succ m] (iterate_psusp m (psusp A))) : loop_ptrunc_pequiv - ... ≃* ptrunc k (Ω[succ m] (iterate_psusp (succ m) A)) : - ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_psusp_succ_pequiv)} - end - - definition pmap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : f = g := - pmap_eq (to_homotopy p) (to_homotopy_pt p)⁻¹ - - definition pmap_equiv_pmap_right {A B : Type*} (C : Type*) (f : A ≃* B) : C →* A ≃ C →* B := - begin - fapply equiv.MK, - { exact pcompose f}, - { exact pcompose f⁻¹ᵉ*}, - { intro f, apply pmap_eq_of_phomotopy, - exact !passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose}, - { intro f, apply pmap_eq_of_phomotopy, - exact !passoc⁻¹* ⬝* pwhisker_right _ !pleft_inv ⬝* !pid_pcompose} - end - - definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) : - iterate_psusp n X →* Y ≃ X →* Ω[n] Y := - begin - revert X Y, induction n with n IH: intro X Y, - { reflexivity}, - { refine !susp_adjoint_loop ⬝e !IH ⬝e _, apply pmap_equiv_pmap_right, - symmetry, apply loopn_succ_in} - end - -end EM --- cohomology ∥ X → K(G,n) ∥ --- reduced cohomology ∥ X →* K(G,n) ∥ --- but we probably want to do this for any spectrum diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index c8fce49..a0ea060 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -6,26 +6,29 @@ Authors: Floris van Doorn Reduced cohomology -/ -import .EM algebra.arrow_group +import algebra.arrow_group .spectrum homotopy.EM -open eq spectrum int trunc pointed EM group algebra circle sphere nat +open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops -definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : CommGroup := -CommGroup_pmap X (πag[2] (Y (2+n))) +definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := +spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) -definition ordinary_cohomology [reducible] (X : Type*) (G : CommGroup) (n : ℤ) : CommGroup := +definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup := +AbGroup_pmap X (πag[2] (Y (2+n))) + +definition ordinary_cohomology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup := cohomology X (EM_spectrum G) n -definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : CommGroup := +definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup := ordinary_cohomology X agℤ n notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n -check H^3[S¹*,EM_spectrum agℤ] -check H^3[S¹*] +-- check H^3[S¹*,EM_spectrum agℤ] +-- check H^3[S¹*] -definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : CommGroup := +definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup := cohomology X₊ Y n definition cohomology_homomorphism [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum) diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 5d3d2e2..7d44180 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -51,11 +51,11 @@ namespace sphere end definition deg {n : ℕ} [H : is_succ n] (f : S* n →* S* n) : ℤ := - by induction H with n; exact πnSn n ((π→g[n+1] f) (tr surf)) + by induction H with n; exact πnSn n (π→g[n+1] f (tr surf)) definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) := by induction H with n; - exact ap (πnSn n) (phomotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n + exact ap (πnSn n) (homotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S* n →* S* n} (p : f ~* g) : deg f = deg g := @@ -94,7 +94,7 @@ namespace sphere apply eq_one_or_eq_neg_one_of_mul_eq_one (deg f⁻¹ᵉ*), refine !deg_compose⁻¹ ⬝ _, refine deg_phomotopy (pright_inv f) ⬝ _, - apply deg_id, + apply deg_id end end sphere diff --git a/homotopy/sample.hlean b/homotopy/sample.hlean index b53cc0d..54a787c 100644 --- a/homotopy/sample.hlean +++ b/homotopy/sample.hlean @@ -175,7 +175,7 @@ namespace homotopy apply trunc.rec, intro a', apply pathover_of_tr_eq, - rewrite [transport_eq_Fr,idp_con], + rewrite [eq_transport_Fr,idp_con], revert H, induction n with [n, IH], { intro H, apply is_prop.elim }, { intros H, diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 5667b40..a8a26eb 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -1,179 +1,9 @@ -- Authors: Floris van Doorn -/- - In this file we define the smash type. This is the cofiber of the map - wedge A B → A × B - However, we define it (equivalently) as the pushout of the maps A + B → 2 and A + B → A × B. --/ - -import homotopy.circle homotopy.join types.pointed homotopy.cofiber ..move_to_lib +import homotopy.smash open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge -namespace smash - - variables {A B : Type*} - - section - open pushout - - definition prod_of_sum [unfold 3] (u : A + B) : A × B := - by induction u with a b; exact (a, pt); exact (pt, b) - - definition bool_of_sum [unfold 3] (u : A + B) : bool := - by induction u; exact ff; exact tt - - definition smash' (A B : Type*) : Type := pushout (@prod_of_sum A B) (@bool_of_sum A B) - protected definition mk (a : A) (b : B) : smash' A B := inl (a, b) - - definition smash [constructor] (A B : Type*) : Type* := - pointed.MK (smash' A B) (smash.mk pt pt) - - definition auxl : smash A B := inr ff - definition auxr : smash A B := inr tt - definition gluel (a : A) : smash.mk a pt = auxl :> smash A B := glue (inl a) - definition gluer (b : B) : smash.mk pt b = auxr :> smash A B := glue (inr b) - - end - - definition gluel' (a a' : A) : smash.mk a pt = smash.mk a' pt :> smash A B := - gluel a ⬝ (gluel a')⁻¹ - definition gluer' (b b' : B) : smash.mk pt b = smash.mk pt b' :> smash A B := - gluer b ⬝ (gluer b')⁻¹ - definition glue (a : A) (b : B) : smash.mk a pt = smash.mk pt b := - gluel' a pt ⬝ gluer' pt b - - definition glue_pt_left (b : B) : glue (Point A) b = gluer' pt b := - whisker_right !con.right_inv _ ⬝ !idp_con - - definition glue_pt_right (a : A) : glue a (Point B) = gluel' a pt := - proof whisker_left _ !con.right_inv qed - - definition ap_mk_left {a a' : A} (p : a = a') : ap (λa, smash.mk a (Point B)) p = gluel' a a' := - by induction p; exact !con.right_inv⁻¹ - - definition ap_mk_right {b b' : B} (p : b = b') : ap (smash.mk (Point A)) p = gluer' b b' := - by induction p; exact !con.right_inv⁻¹ - - protected definition rec {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b)) - (Pl : P auxl) (Pr : P auxr) (Pgl : Πa, Pmk a pt =[gluel a] Pl) - (Pgr : Πb, Pmk pt b =[gluer b] Pr) (x : smash' A B) : P x := - begin - induction x with x b u, - { induction x with a b, exact Pmk a b }, - { induction b, exact Pl, exact Pr }, - { induction u: esimp, - { apply Pgl }, - { apply Pgr }} - end - - -- a rec which is easier to prove, but with worse computational properties - protected definition rec' {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b)) - (Pg : Πa b, Pmk a pt =[glue a b] Pmk pt b) (x : smash' A B) : P x := - begin - induction x using smash.rec, - { apply Pmk }, - { exact gluel pt ▸ Pmk pt pt }, - { exact gluer pt ▸ Pmk pt pt }, - { refine change_path _ (Pg a pt ⬝o !pathover_tr), - refine whisker_right !glue_pt_right _ ⬝ _, esimp, refine !con.assoc ⬝ _, - apply whisker_left, apply con.left_inv }, - { refine change_path _ ((Pg pt b)⁻¹ᵒ ⬝o !pathover_tr), - refine whisker_right !glue_pt_left⁻² _ ⬝ _, - refine whisker_right !inv_con_inv_right _ ⬝ _, refine !con.assoc ⬝ _, - apply whisker_left, apply con.left_inv } - end - - theorem rec_gluel {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)} - {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) - (Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) : - apd (smash.rec Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a := - !pushout.rec_glue - - theorem rec_gluer {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)} - {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) - (Pgr : Πb, Pmk pt b =[gluer b] Pr) (b : B) : - apd (smash.rec Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b := - !pushout.rec_glue - - theorem rec_glue {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)} - {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) - (Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) (b : B) : - apd (smash.rec Pmk Pl Pr Pgl Pgr) (glue a b) = - (Pgl a ⬝o (Pgl pt)⁻¹ᵒ) ⬝o (Pgr pt ⬝o (Pgr b)⁻¹ᵒ) := - by rewrite [↑glue, ↑gluel', ↑gluer', +apd_con, +apd_inv, +rec_gluel, +rec_gluer] - - protected definition elim {P : Type} (Pmk : Πa b, P) (Pl Pr : P) - (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (x : smash' A B) : P := - smash.rec Pmk Pl Pr (λa, pathover_of_eq _ (Pgl a)) (λb, pathover_of_eq _ (Pgr b)) x - - -- an elim which is easier to prove, but with worse computational properties - protected definition elim' {P : Type} (Pmk : Πa b, P) (Pg : Πa b, Pmk a pt = Pmk pt b) - (x : smash' A B) : P := - smash.rec' Pmk (λa b, pathover_of_eq _ (Pg a b)) x - - theorem elim_gluel {P : Type} {Pmk : Πa b, P} {Pl Pr : P} - (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) : - ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a := - begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluel A B a)), - rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluel], - end - - theorem elim_gluer {P : Type} {Pmk : Πa b, P} {Pl Pr : P} - (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b : B) : - ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b := - begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluer A B b)), - rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluer], - end - - theorem elim_glue {P : Type} {Pmk : Πa b, P} {Pl Pr : P} - (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) (b : B) : - ap (smash.elim Pmk Pl Pr Pgl Pgr) (glue a b) = (Pgl a ⬝ (Pgl pt)⁻¹) ⬝ (Pgr pt ⬝ (Pgr b)⁻¹) := - by rewrite [↑glue, ↑gluel', ↑gluer', +ap_con, +ap_inv, +elim_gluel, +elim_gluer] - -end smash -open smash -attribute smash.mk auxl auxr [constructor] -attribute smash.rec smash.elim [unfold 9] [recursor 9] -attribute smash.rec' smash.elim' [unfold 6] - -namespace smash - - variables {A B : Type*} - - definition of_smash_pbool [unfold 2] (x : smash A pbool) : A := - begin - induction x, - { induction b, exact pt, exact a }, - { exact pt }, - { exact pt }, - { reflexivity }, - { induction b: reflexivity } - end - - definition smash_pbool_equiv [constructor] (A : Type*) : smash A pbool ≃* A := - begin - fapply pequiv_of_equiv, - { fapply equiv.MK, - { exact of_smash_pbool }, - { intro a, exact smash.mk a tt }, - { intro a, reflexivity }, - { exact abstract begin intro x, induction x using smash.rec', - { induction b, exact (glue a tt)⁻¹, reflexivity }, - { apply eq_pathover_id_right, induction b: esimp, - { refine ap02 _ !glue_pt_right ⬝ph _, - refine ap_compose (λx, smash.mk x _) _ _ ⬝ph _, - refine ap02 _ (!ap_con ⬝ (!elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻²))) ⬝ph _, - apply hinverse, apply square_of_eq, - esimp, refine (!glue_pt_right ◾ !glue_pt_left)⁻¹ }, - { apply square_of_eq, refine !con.left_inv ⬝ _, esimp, symmetry, - refine ap_compose (λx, smash.mk x _) _ _ ⬝ _, - exact ap02 _ !elim_glue }} end end }}, - { reflexivity } - end - /- smash A (susp B) = susp (smash A B) <- this follows from associativity and smash with S¹-/ /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash), @@ -183,7 +13,11 @@ namespace smash /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/ - definition prod_of_pwedge [unfold 3] (v : pwedge' A B) : A × B := +namespace smash + + variables {A B : Type*} + + definition prod_of_wedge [unfold 3] (v : pwedge A B) : A × B := begin induction v with a b , { exact (a, pt) }, @@ -191,18 +25,17 @@ namespace smash { reflexivity } end - definition pprod_of_pwedge [constructor] : pwedge' A B →* A ×* B := + variables (A B) + definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B := begin fconstructor, - { intro v, induction v with a b , - { exact (a, pt) }, - { exact (pt, b) }, - { reflexivity }}, + { exact prod_of_wedge }, { reflexivity } end + variables {A B} attribute pcofiber [constructor] - definition pcofiber_of_smash (x : smash A B) : pcofiber' (@pprod_of_pwedge A B) := + definition pcofiber_of_smash [unfold 3] (x : smash A B) : pcofiber (@pprod_of_pwedge A B) := begin induction x, { exact pushout.inr (a, b) }, @@ -212,26 +45,72 @@ namespace smash { symmetry, exact pushout.glue (pushout.inr b) } end + -- move definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X} (p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) := by induction p; reflexivity - definition smash_of_pcofiber (x : pcofiber' (@pprod_of_pwedge A B)) : smash A B := + definition smash_of_pcofiber_glue [unfold 3] (x : pwedge A B) : + Point (smash A B) = smash.mk (prod_of_wedge x).1 (prod_of_wedge x).2 := + begin + induction x with a b: esimp, + { apply gluel' }, + { apply gluer' }, + { apply eq_pathover_constant_left, refine _ ⬝hp (ap_eq_ap011 smash.mk _ _ _)⁻¹, + rewrite [ap_compose' prod.pr1, ap_compose' prod.pr2], + -- TODO: define elim_glue for wedges and remove k in krewrite + krewrite [pushout.elim_glue], esimp, apply vdeg_square, + exact !con.right_inv ⬝ !con.right_inv⁻¹ } + end + + definition smash_of_pcofiber [unfold 3] (x : pcofiber (pprod_of_pwedge A B)) : smash A B := begin induction x with x x, { exact smash.mk pt pt }, { exact smash.mk x.1 x.2 }, - { induction x with a b: esimp, - { apply gluel' }, - { apply gluer' }, - { apply eq_pathover_constant_left, refine _ ⬝hp (ap_eq_ap011 smash.mk _ _ _)⁻¹, - unfold [wedge.elim], - rewrite [ap_compose' prod.pr1, ap_compose' prod.pr2], - -- TODO: define elim_glue for wedges and remove krewrite - krewrite [pushout.elim_glue], esimp, apply vdeg_square, - exact !con.right_inv ⬝ !con.right_inv⁻¹ }} + { exact smash_of_pcofiber_glue x } end + definition pcofiber_of_smash_of_pcofiber (x : pcofiber (pprod_of_pwedge A B)) : + pcofiber_of_smash (smash_of_pcofiber x) = x := + begin + induction x with x x, + { refine (pushout.glue pt)⁻¹ }, + { exact sorry }, + { exact sorry } + end + + definition smash_of_pcofiber_of_smash (x : smash A B) : + smash_of_pcofiber (pcofiber_of_smash x) = x := + begin + induction x, + { reflexivity }, + { apply gluel }, + { apply gluer }, + { apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _, + refine ap02 _ !elim_gluel ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _, + esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right _ !inv_con_inv_right⁻¹, + exact !inv_con_cancel_right⁻¹ }, + { apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _, + refine ap02 _ !elim_gluer ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _, + esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right _ !inv_con_inv_right⁻¹, + exact !inv_con_cancel_right⁻¹ }, + end + + variables (A B) + definition smash_pequiv_pcofiber : smash A B ≃* pcofiber (pprod_of_pwedge A B) := + begin + fapply pequiv_of_equiv, + { fapply equiv.MK, + { apply pcofiber_of_smash }, + { apply smash_of_pcofiber }, + { exact pcofiber_of_smash_of_pcofiber }, + { exact smash_of_pcofiber_of_smash }}, + { esimp, symmetry, apply pushout.glue pt } + end + + variables {A B} + /- smash A S¹ = susp A -/ open susp @@ -268,7 +147,7 @@ exit -- the definitions below compile, but take a long time to do so and have so apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left, symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv, refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc, - refine _ ⬝ whisker_right !inv_con_cancel_right⁻¹ _, refine _ ⬝ !con.right_inv⁻¹, + refine _ ⬝ whisker_right _ !inv_con_cancel_right⁻¹, refine _ ⬝ !con.right_inv⁻¹, refine !con.right_inv ◾ _, refine _ ◾ !con.right_inv, refine !ap_mk_right ⬝ !con.right_inv end end } end @@ -281,7 +160,7 @@ exit -- the definitions below compile, but take a long time to do so and have so begin refine ap02 _ !elim_gluer ⬝ph _, induction b, - { apply square_of_eq, exact whisker_right !con.right_inv _ }, + { apply square_of_eq, exact whisker_right _ !con.right_inv }, { apply square_pathover', exact sorry } end @@ -314,7 +193,7 @@ exit -- the definitions below compile, but take a long time to do so and have so refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _, refine ap02 _ !elim_gluer ⬝ph _, induction b, - { apply square_of_eq, exact whisker_right !con.right_inv _ }, + { apply square_of_eq, exact whisker_right _ !con.right_inv }, { exact sorry} }}}, { reflexivity } diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 88be0b1..63dc0db 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -6,6 +6,7 @@ Authors: Michael Shulman, Floris van Doorn -/ import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim + ..pointed_pi open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group seq_colim @@ -190,7 +191,7 @@ namespace spectrum -- Suspension prespectra are one that's naturally indexed on the natural numbers definition psp_susp (X : Type*) : gen_prespectrum +ℕ := - gen_prespectrum.mk (λn, psuspn n X) (λn, loop_susp_unit (psuspn n X)) + gen_prespectrum.mk (λn, psuspn n X) (λn, loop_psusp_unit (psuspn n X)) /- Truncations -/ @@ -210,7 +211,7 @@ namespace spectrum -- read off the homotopy groups without any tedious case-analysis of -- n. We increment by 2 in order to ensure that they are all -- automatically abelian groups. - definition shomotopy_group [constructor] (n : ℤ) (E : spectrum) : CommGroup := πag[0+2] (E (2 - n)) + definition shomotopy_group [constructor] (n : ℤ) (E : spectrum) : AbGroup := πag[0+2] (E (2 - n)) notation `πₛ[`:95 n:0 `]`:0 := shomotopy_group n @@ -234,9 +235,10 @@ namespace spectrum -- Sections of parametrized spectra ---------------------------------------- - definition spi {N : succ_str} (A : Type) (E : A -> gen_spectrum N) : gen_spectrum N := - spectrum.MK (λn, ppi (λa, E a n)) - (λn, (loop_ppi_commute (λa, E a (S n)))⁻¹ᵉ* ∘*ᵉ equiv_ppi_right (λa, equiv_glue (E a) n)) + -- this definition must be changed to use dependent maps respecting the basepoint, presumably + -- definition spi {N : succ_str} (A : Type) (E : A -> gen_spectrum N) : gen_spectrum N := + -- spectrum.MK (λn, ppi (λa, E a n)) + -- (λn, (loop_ppi_commute (λa, E a (S n)))⁻¹ᵉ* ∘*ᵉ equiv_ppi_right (λa, equiv_glue (E a) n)) /----------------------------------------- Fibers and long exact sequences @@ -311,12 +313,12 @@ namespace spectrum example (n : ℤ) : cc_to_fn LES_of_shomotopy_groups (n, 1) = πₛ→[n] (spoint f) := idp -- the maps are ugly for (n, 2) - definition comm_group_LES_of_shomotopy_groups : Π(v : +3ℤ), comm_group (LES_of_shomotopy_groups v) - | (n, fin.mk 0 H) := proof CommGroup.struct (πₛ[n] Y) qed - | (n, fin.mk 1 H) := proof CommGroup.struct (πₛ[n] X) qed - | (n, fin.mk 2 H) := proof CommGroup.struct (πₛ[n] (sfiber f)) qed + definition ab_group_LES_of_shomotopy_groups : Π(v : +3ℤ), ab_group (LES_of_shomotopy_groups v) + | (n, fin.mk 0 H) := proof AbGroup.struct (πₛ[n] Y) qed + | (n, fin.mk 1 H) := proof AbGroup.struct (πₛ[n] X) qed + | (n, fin.mk 2 H) := proof AbGroup.struct (πₛ[n] (sfiber f)) qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - local attribute comm_group_LES_of_shomotopy_groups [instance] + local attribute ab_group_LES_of_shomotopy_groups [instance] definition is_homomorphism_LES_of_shomotopy_groups : Π(v : +3ℤ), is_homomorphism (cc_to_fn LES_of_shomotopy_groups v) @@ -330,7 +332,7 @@ namespace spectrum -- In the comments below is a start on an explicit description of the LES for spectra -- Maybe it's slightly nicer to work with than the above version --- definition shomotopy_groups [reducible] : -3ℤ → CommGroup +-- definition shomotopy_groups [reducible] : -3ℤ → AbGroup -- | (n, fin.mk 0 H) := πₛ[n] Y -- | (n, fin.mk 1 H) := πₛ[n] X -- | (n, fin.mk k H) := πₛ[n] (sfiber f) diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean index 288b9f5..a53c6ea 100644 --- a/homotopy/spherical_fibrations.hlean +++ b/homotopy/spherical_fibrations.hlean @@ -90,7 +90,7 @@ namespace spherical_fibrations definition BF_mul {n m : ℕ} (X : BF n) (Y : BF m) : BF (n + m) := begin cases X with X hX, cases Y with Y hY, - apply sigma.mk (psmash X Y), + apply sigma.mk (smash X Y), induction hX with fX, induction hY with fY, apply tr, exact sorry -- needs smash.spheres : psmash (S. n) (S. m) ≃ S. (n + m) end diff --git a/move_to_lib.hlean b/move_to_lib.hlean index c978b6d..fe4027c 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -5,80 +5,27 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group is_trunc function sphere -attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose - fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in - isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv int.equiv_succ - [constructor] -attribute is_equiv.eq_of_fn_eq_fn' [unfold 3] -attribute isomorphism._trans_of_to_hom [unfold 3] -attribute homomorphism.struct [unfold 3] -attribute pequiv.trans pequiv.symm [constructor] - -namespace sigma - - definition sigma_equiv_sigma_left' [constructor] {A A' : Type} {B : A' → Type} (Hf : A ≃ A') : (Σa, B (Hf a)) ≃ (Σa', B a') := - sigma_equiv_sigma Hf (λa, erfl) - -end sigma -open sigma - namespace group open is_trunc -- some extra instances for type class inference - definition is_homomorphism_comm_homomorphism [instance] {G G' : CommGroup} (φ : G →g G') - : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G)) - (@comm_group.to_group _ (CommGroup.struct G')) φ := - homomorphism.struct φ + -- definition is_homomorphism_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) + -- (@ab_group.to_group _ (AbGroup.struct G')) φ := + -- homomorphism.struct φ - definition is_homomorphism_comm_homomorphism1 [instance] {G G' : CommGroup} (φ : G →g G') - : @is_homomorphism G G' _ - (@comm_group.to_group _ (CommGroup.struct G')) φ := - homomorphism.struct φ + -- definition is_homomorphism_comm_homomorphism1 [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_homomorphism G G' _ + -- (@ab_group.to_group _ (AbGroup.struct G')) φ := + -- homomorphism.struct φ - definition is_homomorphism_comm_homomorphism2 [instance] {G G' : CommGroup} (φ : G →g G') - : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G)) _ φ := - homomorphism.struct φ - - theorem inv_eq_one {A : Type} [group A] {a : A} (H : a = 1) : a⁻¹ = 1 := - iff.mpr (inv_eq_one_iff_eq_one a) H - - definition pSet_of_Group (G : Group) : Set* := ptrunctype.mk G _ 1 - - definition pmap_of_isomorphism [constructor] {G₁ : Group} {G₂ : Group} - (φ : G₁ ≃g G₂) : pType_of_Group G₁ →* pType_of_Group G₂ := - pequiv_of_isomorphism φ - - definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) : - pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) := - begin - induction p, - apply pequiv_eq, - fapply pmap_eq, - { intro g, reflexivity}, - { apply is_prop.elim} - end - - definition homomorphism_change_fun [constructor] {G₁ G₂ : Group} - (φ : G₁ →g G₂) (f : G₁ → G₂) (p : φ ~ f) : G₁ →g G₂ := - homomorphism.mk f (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul φ g h ⬝ ap011 mul (p g) (p h)) - - definition Group_of_pgroup (G : Type*) [pgroup G] : Group := - Group.mk G _ - - definition pgroup_pType_of_Group [instance] (G : Group) : pgroup (pType_of_Group G) := - ⦃ pgroup, Group.struct G, - pt_mul := one_mul, - mul_pt := mul_one, - mul_left_inv_pt := mul.left_inv ⦄ - - definition comm_group_pType_of_Group [instance] (G : CommGroup) : comm_group (pType_of_Group G) := - CommGroup.struct G - - abbreviation gid [constructor] := @homomorphism_id + -- definition is_homomorphism_comm_homomorphism2 [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ := + -- homomorphism.struct φ end group open group + namespace pi -- move to types.arrow definition pmap_eq_idp {X Y : Type*} (f : X →* Y) : @@ -110,335 +57,30 @@ end pi open pi namespace eq - -- types.eq - definition loop_equiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a') - : (a = a) ≃ (a' = a') := - eq_equiv_eq_closed p p - - -- init.path - definition tr_ap {A B : Type} {x y : A} (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) : - transport P (ap f p) z = transport (P ∘ f) p z := - (tr_compose P f p z)⁻¹ - - - definition pathover_eq_Fl' {A B : Type} {f : A → B} {a₁ a₂ : A} {b : B} (p : a₁ = a₂) (q : f a₂ = b) : (ap f p) ⬝ q =[p] q := - by induction p; induction q; exact idpo - - -- this should be renamed square_pathover. The one in cubical.cube should be renamed - definition square_pathover' {A B : Type} {a a' : A} {b₁ b₂ b₃ b₄ : A → B} - {f₁ : b₁ ~ b₂} {f₂ : b₃ ~ b₄} {f₃ : b₁ ~ b₃} {f₄ : b₂ ~ b₄} {p : a = a'} - {q : square (f₁ a) (f₂ a) (f₃ a) (f₄ a)} - {r : square (f₁ a') (f₂ a') (f₃ a') (f₄ a')} - (s : cube (natural_square_tr f₁ p) (natural_square_tr f₂ p) - (natural_square_tr f₃ p) (natural_square_tr f₄ p) q r) : q =[p] r := - by induction p; apply pathover_idp_of_eq; exact eq_of_deg12_cube s - - -- define natural_square_tr this way. Also, natural_square_tr and natural_square should swap names - definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B} - (p : f ~ g) (q : a = a') : natural_square_tr p q = square_of_pathover (apd p q) := - by induction q; reflexivity - - section - variables {A : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ : A} - {p₁₀₀ : a₀₀₀ = a₂₀₀} {p₀₁₀ : a₀₀₀ = a₀₂₀} {p₀₀₁ : a₀₀₀ = a₀₀₂} - {p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂} - {p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂} - {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂} - {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} - {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂} - {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} - {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁} - {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} - {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} - - -- move to cubical.cube - definition eq_concat1 {s₀₁₁' : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} (r : s₀₁₁' = s₀₁₁) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁' s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ := - by induction r; exact c - - definition concat1_eq {s₂₁₁' : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁} - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₂₁₁ = s₂₁₁') - : cube s₀₁₁ s₂₁₁' s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ := - by induction r; exact c - - definition eq_concat2 {s₁₀₁' : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} (r : s₁₀₁' = s₁₀₁) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ s₂₁₁ s₁₀₁' s₁₂₁ s₁₁₀ s₁₁₂ := - by induction r; exact c - - definition concat2_eq {s₁₂₁' : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₁₂₁ = s₁₂₁') - : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁' s₁₁₀ s₁₁₂ := - by induction r; exact c - - definition eq_concat3 {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} (r : s₁₁₀' = s₁₁₀) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀' s₁₁₂ := - by induction r; exact c - - definition concat3_eq {s₁₁₂' : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂} - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₁₁₂ = s₁₁₂') - : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂' := - by induction r; exact c - - end - - infix ` ⬝1 `:75 := cube_concat1 - infix ` ⬝2 `:75 := cube_concat2 - infix ` ⬝3 `:75 := cube_concat3 - infix ` ⬝p1 `:75 := eq_concat1 - infix ` ⬝1p `:75 := concat1_eq - infix ` ⬝p2 `:75 := eq_concat3 - infix ` ⬝2p `:75 := concat2_eq - infix ` ⬝p3 `:75 := eq_concat3 - infix ` ⬝3p `:75 := concat3_eq + -- definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B} + -- (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) := + -- idp end eq open eq namespace pointed - -- in init.pointed `pointed_carrier` should be [unfold 1] instead of [constructor] - definition ptransport [constructor] {A : Type} (B : A → Type*) {a a' : A} (p : a = a') - : B a →* B a' := - pmap.mk (transport B p) (apdt (λa, Point (B a)) p) + -- /- the pointed type of (unpointed) dependent maps -/ + -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* := + -- pointed.mk' (Πa, P a) - definition ptransport_change_eq [constructor] {A : Type} (B : A → Type*) {a a' : A} {p q : a = a'} - (r : p = q) : ptransport B p ~* ptransport B q := - phomotopy.mk (λb, ap (λp, transport B p b) r) begin induction r, exact !idp_con end + -- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) := + -- pequiv_of_equiv eq_equiv_homotopy rfl - definition pnatural_square {A B : Type} (X : B → Type*) {f g : A → B} - (h : Πa, X (f a) →* X (g a)) {a a' : A} (p : a = a') : - h a' ∘* ptransport X (ap f p) ~* ptransport X (ap g p) ∘* h a := - by induction p; exact !pcompose_pid ⬝* !pid_pcompose⁻¹* - - definition pequiv_ap [constructor] {A : Type} (B : A → Type*) {a a' : A} (p : a = a') - : B a ≃* B a' := - pequiv_of_pmap (ptransport B p) !is_equiv_tr - - definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C := - pequiv_of_pmap (g ∘* f) (is_equiv_compose g f) - - infixr ` ∘*ᵉ `:60 := pequiv_compose - - definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt := - begin - fapply equiv.MK : intros f, - { exact ⟨to_fun f , resp_pt f⟩ }, - all_goals cases f with f p, - { exact pmap.mk f p }, - all_goals reflexivity - end - - definition is_trunc_pmap [instance] (n : ℕ₋₂) (A B : Type*) [is_trunc n B] : is_trunc n (A →* B) := - is_trunc_equiv_closed_rev _ !pmap.sigma_char - - definition is_trunc_ppmap [instance] (n : ℕ₋₂) {A B : Type*} [is_trunc n B] : - is_trunc n (ppmap A B) := - !is_trunc_pmap - - definition pmap_eq_of_homotopy {A B : Type*} {f g : A →* B} [is_set B] (p : f ~ g) : f = g := - pmap_eq p !is_set.elim - - definition phomotopy.sigma_char [constructor] {A B : Type*} (f g : A →* B) : (f ~* g) ≃ Σ(p : f ~ g), p pt ⬝ resp_pt g = resp_pt f := - begin - fapply equiv.MK : intros h, - { exact ⟨h , to_homotopy_pt h⟩ }, - all_goals cases h with h p, - { exact phomotopy.mk h p }, - all_goals reflexivity - end - - definition pmap_eq_equiv {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) := - calc (f = g) ≃ pmap.sigma_char f = pmap.sigma_char g - : eq_equiv_fn_eq pmap.sigma_char f g - ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), pathover (λh, h pt = pt) (resp_pt f) p (resp_pt g) - : sigma_eq_equiv _ _ - ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), resp_pt f = ap (λh, h pt) p ⬝ resp_pt g - : sigma_equiv_sigma_right (λp, pathover_eq_equiv_Fl p (resp_pt f) (resp_pt g)) - ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), resp_pt f = ap10 p pt ⬝ resp_pt g - : sigma_equiv_sigma_right (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _)) - ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), resp_pt f = p pt ⬝ resp_pt g - : sigma_equiv_sigma_left' eq_equiv_homotopy - ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), p pt ⬝ resp_pt g = resp_pt f - : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) - ... ≃ (f ~* g) : phomotopy.sigma_char f g - - definition loop_pmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) := - pequiv_of_equiv - (calc Ω(ppmap A B) /- ≃ (pconst A B = pconst A B) : erfl - ... -/ ≃ (pconst A B ~* pconst A B) : pmap_eq_equiv _ _ - ... ≃ Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl : phomotopy.sigma_char - ... /- ≃ Σ(f : A → Ω B), f pt = pt : erfl - ... -/ ≃ (A →* Ω B) : pmap.sigma_char) - (by reflexivity) - - -- definition ppcompose_left {A B C : Type*} (g : B →* C) : ppmap A B →* ppmap A C := - -- pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, resp_pt g) (idp_con _)⁻¹)) - - -- definition is_equiv_ppcompose_left [instance] {A B C : Type*} (g : B →* C) [H : is_equiv g] : is_equiv (@ppcompose_left A B C g) := - -- begin - -- fapply is_equiv.adjointify, - -- { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) }, - -- all_goals (intros f; esimp; apply eq_of_phomotopy), - -- { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc - -- ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H)) - -- ... ~* f : pid_pcompose f }, - -- { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc - -- ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H)) - -- ... ~* f : pid_pcompose f } - -- end - - -- definition pequiv_ppcompose_left {A B C : Type*} (g : B ≃* C) : ppmap A B ≃* ppmap A C := - -- pequiv_of_pmap (ppcompose_left g) _ - - -- definition pcompose_pconst {A B C : Type*} (f : B →* C) : f ∘* pconst A B ~* pconst A C := - -- phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ - - -- definition pconst_pcompose {A B C : Type*} (f : A →* B) : pconst B C ∘* f ~* pconst A C := - -- phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ - - definition ap1_pconst (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) := - phomotopy.mk (λp, idp_con _ ⬝ ap_constant p pt) rfl - - definition apn_pconst (A B : Type*) (n : ℕ) : - apn n (pconst A B) ~* pconst (Ω[n] A) (Ω[n] B) := - begin - induction n with n IH, - { reflexivity }, - { exact ap1_phomotopy IH ⬝* !ap1_pconst } - end - - definition loop_ppi_commute {A : Type} (B : A → Type*) : Ω(ppi B) ≃* Π*a, Ω (B a) := - pequiv_of_equiv eq_equiv_homotopy rfl - - definition equiv_ppi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a) - : (Π*a, P a) ≃* (Π*a, Q a) := - pequiv_of_equiv (pi_equiv_pi_right g) - begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end - - definition pcast_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) - {a₁ a₂ : A} (p : a₁ = a₂) : pcast (ap C p) ∘* f a₁ ~* f a₂ ∘* pcast (ap B p) := - phomotopy.mk - begin induction p, reflexivity end - begin induction p, esimp, refine !idp_con ⬝ !idp_con ⬝ !ap_id⁻¹ end - - definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) - {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) := - pcast_commute f p - - definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := - pmap.mk (λ(f : A →* B), f a) idp - - definition papply_pcompose [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := - pmap.mk (λ(f : A →* B), f a) idp - - open bool --also rename pmap_bool_equiv -> pmap_pbool_equiv - - definition pbool_pmap [constructor] {A : Type*} (a : A) : pbool →* A := - pmap.mk (bool.rec pt a) idp - - definition pmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B := - begin - fapply pequiv.MK, - { exact papply B tt }, - { exact pbool_pmap }, - { intro f, fapply pmap_eq, - { intro b, cases b, exact !respect_pt⁻¹, reflexivity }, - { exact !con.left_inv⁻¹ }}, - { intro b, reflexivity }, - end - - definition papn_pt [constructor] (n : ℕ) (A B : Type*) : ppmap A B →* ppmap (Ω[n] A) (Ω[n] B) := - pmap.mk (λf, apn n f) (eq_of_phomotopy !apn_pconst) - - definition papn_fun [constructor] {n : ℕ} {A : Type*} (B : Type*) (p : Ω[n] A) : - ppmap A B →* Ω[n] B := - papply _ p ∘* papn_pt n A B - - definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) : - loopn_succ_in B n ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n := - !apn_succ_phomotopy_in - - definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) : - Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):= - begin - apply pinv_right_phomotopy_of_phomotopy, - refine _ ⬝* !passoc⁻¹*, - apply phomotopy_pinv_left_of_phomotopy, - apply apn_succ_phomotopy_in - end + -- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a) + -- : pupi P ≃* pupi Q := + -- pequiv_of_equiv (pi_equiv_pi_right g) + -- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end end pointed open pointed namespace fiber - definition pfiber.sigma_char [constructor] {A B : Type*} (f : A →* B) - : pfiber f ≃* pointed.MK (Σa, f a = pt) ⟨pt, respect_pt f⟩ := - pequiv_of_equiv (fiber.sigma_char f pt) idp - - definition ppoint_sigma_char [constructor] {A B : Type*} (f : A →* B) - : ppoint f ~* pmap.mk pr1 idp ∘* pfiber.sigma_char f := - !phomotopy.refl - - definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) := - pequiv_of_equiv - (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl - : (fiber.sigma_char (ap1 f) (Point (Ω B))) - ... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f) - : (sigma_equiv_sigma_right (λp, - calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl - : equiv_eq_closed_left _ (con.assoc _ _ _) - ... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f) - : eq_equiv_inv_con_eq_idp - ... ≃ (respect_pt f) = ap f p ⬝ (respect_pt f) - : eq_equiv_eq_symm)) - ... ≃ fiber.mk (Point A) (respect_pt f) = fiber.mk pt (respect_pt f) - : fiber_eq_equiv - ... ≃ Ω (pfiber f) - : erfl) - (begin cases f with f p, cases A with A a, cases B with B b, esimp at p, esimp at f, - induction p, reflexivity end) - - definition pfiber_equiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g) - : pfiber f ≃* pfiber g := - begin - fapply pequiv_of_equiv, - { refine (fiber.sigma_char f pt ⬝e _ ⬝e (fiber.sigma_char g pt)⁻¹ᵉ), - apply sigma_equiv_sigma_right, intros a, - apply equiv_eq_closed_left, apply (to_homotopy h) }, - { refine (fiber_eq rfl _), - change (h pt)⁻¹ ⬝ respect_pt f = idp ⬝ respect_pt g, - rewrite idp_con, apply inv_con_eq_of_eq_con, symmetry, exact (to_homotopy_pt h) } - end - - definition transport_fiber_equiv [constructor] {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2) - : fiber f b1 ≃ fiber f b2 := - calc fiber f b1 ≃ Σa, f a = b1 : fiber.sigma_char - ... ≃ Σa, f a = b2 : sigma_equiv_sigma_right (λa, equiv_eq_closed_right (f a) p) - ... ≃ fiber f b2 : fiber.sigma_char - - definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B') - : pfiber (g ∘* f) ≃* pfiber f := - begin - fapply pequiv_of_equiv, esimp, - refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B), - esimp, apply (ap (fiber.mk (Point A))), refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, - rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con - end - - definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) - : pfiber (f ∘* g) ≃* pfiber f := - begin - fapply pequiv_of_equiv, esimp, - refine fiber.equiv_precompose f g (Point B), - esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp, - { apply respect_pt g }, - { apply pathover_eq_Fl' } - end - - definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} (h : A ≃* C) - (k : B ≃* D) (s : k ∘* f ~* g ∘* h) : pfiber f ≃* pfiber g := - calc pfiber f ≃* pfiber (k ∘* f) : pequiv_postcompose - ... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s - ... ≃* pfiber g : pequiv_precompose definition ap1_ppoint_phomotopy {A B : Type*} (f : A →* B) : Ω→ (ppoint f) ∘* pfiber_loop_space f ~* ppoint (Ω→ f) := @@ -453,125 +95,6 @@ namespace fiber end fiber -namespace eq --algebra.homotopy_group - - definition phomotopy_group_functor_pid (n : ℕ) (A : Type*) : π→[n] (pid A) ~* pid (π[n] A) := - ptrunc_functor_phomotopy 0 !apn_pid ⬝* !ptrunc_functor_pid - -end eq - -namespace susp - - definition iterate_psusp_functor (n : ℕ) {A B : Type*} (f : A →* B) : - iterate_psusp n A →* iterate_psusp n B := - begin - induction n with n g, - { exact f }, - { exact psusp_functor g } - end - -end susp - -namespace is_conn -- homotopy.connectedness - - structure conntype (n : ℕ₋₂) : Type := - (carrier : Type) - (struct : is_conn n carrier) - - notation `Type[`:95 n:0 `]`:0 := conntype n - - attribute conntype.carrier [coercion] - attribute conntype.struct [instance] [priority 1300] - - section - universe variable u - structure pconntype (n : ℕ₋₂) extends conntype.{u} n, pType.{u} - - notation `Type*[`:95 n:0 `]`:0 := pconntype n - - /- - There are multiple coercions from pconntype to Type. Type class inference doesn't recognize - that all of them are definitionally equal (for performance reasons). One instance is - automatically generated, and we manually add the missing instances. - -/ - - definition is_conn_pconntype [instance] {n : ℕ₋₂} (X : Type*[n]) : is_conn n X := - conntype.struct X - - /- Now all the instances work -/ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n X := _ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype.to_pType X) := _ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype.to_conntype X) := _ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype._trans_of_to_pType X) := _ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype._trans_of_to_conntype X) := _ - - structure truncconntype (n k : ℕ₋₂) extends trunctype.{u} n, - conntype.{u} k renaming struct→conn_struct - - notation n `-Type[`:95 k:0 `]`:0 := truncconntype n k - - definition is_conn_truncconntype [instance] {n k : ℕ₋₂} (X : n-Type[k]) : - is_conn k (truncconntype._trans_of_to_trunctype X) := - conntype.struct X - - definition is_trunc_truncconntype [instance] {n k : ℕ₋₂} (X : n-Type[k]) : is_trunc n X := - trunctype.struct X - - structure ptruncconntype (n k : ℕ₋₂) extends ptrunctype.{u} n, - pconntype.{u} k renaming struct→conn_struct - - notation n `-Type*[`:95 k:0 `]`:0 := ptruncconntype n k - - attribute ptruncconntype._trans_of_to_pconntype ptruncconntype._trans_of_to_ptrunctype - ptruncconntype._trans_of_to_pconntype_1 ptruncconntype._trans_of_to_ptrunctype_1 - ptruncconntype._trans_of_to_pconntype_2 ptruncconntype._trans_of_to_ptrunctype_2 - ptruncconntype.to_pconntype ptruncconntype.to_ptrunctype - truncconntype._trans_of_to_conntype truncconntype._trans_of_to_trunctype - truncconntype.to_conntype truncconntype.to_trunctype [unfold 3] - attribute pconntype._trans_of_to_conntype pconntype._trans_of_to_pType - pconntype.to_pType pconntype.to_conntype [unfold 2] - - definition is_conn_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) : - is_conn k (ptruncconntype._trans_of_to_ptrunctype X) := - conntype.struct X - - definition is_trunc_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) : - is_trunc n (ptruncconntype._trans_of_to_pconntype X) := - trunctype.struct X - - definition ptruncconntype_eq {n k : ℕ₋₂} {X Y : n-Type*[k]} (p : X ≃* Y) : X = Y := - begin - induction X with X Xt Xp Xc, induction Y with Y Yt Yp Yc, - note q := pType_eq_elim (eq_of_pequiv p), - cases q with r s, esimp at *, induction r, - exact ap0111 (ptruncconntype.mk X) !is_prop.elim (eq_of_pathover_idp s) !is_prop.elim - end - - end - - -end is_conn - -namespace succ_str - variables {N : succ_str} - - protected definition add [reducible] (n : N) (k : ℕ) : N := - iterate S k n - - infix ` +' `:65 := succ_str.add - - definition add_succ (n : N) (k : ℕ) : n +' (k + 1) = (S n) +' k := - by induction k with k p; reflexivity; exact ap S p - - -end succ_str - -namespace join - - definition pjoin [constructor] (A B : Type*) : Type* := pointed.MK (join A B) (inl pt) - -end join - namespace circle @@ -582,11 +105,11 @@ namespace circle to the square which defined H on the path constructor -/ - definition natural_square_tr_elim_loop {A : Type} {f g : S¹ → A} (p : f base = g base) + definition natural_square_elim_loop {A : Type} {f g : S¹ → A} (p : f base = g base) (q : square p p (ap f loop) (ap g loop)) - : natural_square_tr (circle.rec p (eq_pathover q)) loop = q := + : natural_square (circle.rec p (eq_pathover q)) loop = q := begin - refine !natural_square_tr_eq ⬝ _, + -- refine !natural_square_eq ⬝ _, refine ap square_of_pathover !rec_loop ⬝ _, exact to_right_inv !eq_pathover_equiv_square q end @@ -594,162 +117,8 @@ namespace circle end circle --- this should replace various definitions in homotopy.susp, lines 241 - 338 -namespace new_susp - - variables {X Y Z : Type*} - - definition loop_psusp_unit [constructor] (X : Type*) : X →* Ω(psusp X) := - begin - fconstructor, - { intro x, exact merid x ⬝ (merid pt)⁻¹ }, - { apply con.right_inv }, - end - - definition loop_psusp_unit_natural (f : X →* Y) - : loop_psusp_unit Y ∘* f ~* ap1 (psusp_functor f) ∘* loop_psusp_unit X := - begin - induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, - fconstructor, - { intro x', esimp [psusp_functor], symmetry, - exact - !idp_con ⬝ - (!ap_con ⬝ - whisker_left _ !ap_inv) ⬝ - (!elim_merid ◾ (inverse2 !elim_merid)) }, - { rewrite [▸*,idp_con (con.right_inv _)], - apply inv_con_eq_of_eq_con, - refine _ ⬝ !con.assoc', - rewrite inverse2_right_inv, - refine _ ⬝ !con.assoc', - rewrite [ap_con_right_inv], - xrewrite [idp_con_idp, -ap_compose (concat idp)] }, - end - - definition loop_psusp_counit [constructor] (X : Type*) : psusp (Ω X) →* X := - begin - fconstructor, - { intro x, induction x, exact pt, exact pt, exact a }, - { reflexivity }, - end - - definition loop_psusp_counit_natural (f : X →* Y) - : f ∘* loop_psusp_counit X ~* loop_psusp_counit Y ∘* (psusp_functor (ap1 f)) := - begin - induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, - fconstructor, - { intro x', induction x' with p, - { reflexivity }, - { reflexivity }, - { esimp, apply eq_pathover, apply hdeg_square, - xrewrite [ap_compose' f, ap_compose' (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*], - xrewrite [+elim_merid,▸*,idp_con] }}, - { reflexivity } - end - - definition loop_psusp_counit_unit (X : Type*) - : ap1 (loop_psusp_counit X) ∘* loop_psusp_unit (Ω X) ~* pid (Ω X) := - begin - induction X with X x, fconstructor, - { intro p, esimp, - refine !idp_con ⬝ - (!ap_con ⬝ - whisker_left _ !ap_inv) ⬝ - (!elim_merid ◾ inverse2 !elim_merid) }, - { rewrite [▸*,inverse2_right_inv (elim_merid id idp)], - refine !con.assoc ⬝ _, - xrewrite [ap_con_right_inv (susp.elim x x (λa, a)) (merid idp),idp_con_idp,-ap_compose] } - end - - definition loop_psusp_unit_counit (X : Type*) - : loop_psusp_counit (psusp X) ∘* psusp_functor (loop_psusp_unit X) ~* pid (psusp X) := - begin - induction X with X x, fconstructor, - { intro x', induction x', - { reflexivity }, - { exact merid pt }, - { apply eq_pathover, - xrewrite [▸*, ap_id, ap_compose' (susp.elim north north (λa, a)), +elim_merid,▸*], - apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹ }}, - { reflexivity } - end - - -- TODO: rename to psusp_adjoint_loop (also in above lemmas) - definition psusp_adjoint_loop_unpointed [constructor] (X Y : Type*) : psusp X →* Y ≃ X →* Ω Y := - begin - fapply equiv.MK, - { intro f, exact ap1 f ∘* loop_psusp_unit X }, - { intro g, exact loop_psusp_counit Y ∘* psusp_functor g }, - { intro g, apply eq_of_phomotopy, esimp, - refine !pwhisker_right !ap1_pcompose ⬝* _, - refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_natural⁻¹* ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_unit ⬝* _, - apply pid_pcompose }, - { intro f, apply eq_of_phomotopy, esimp, - refine !pwhisker_left !psusp_functor_compose ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _, - refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_counit ⬝* _, - apply pcompose_pid }, - end - - definition psusp_adjoint_loop_pconst (X Y : Type*) : - psusp_adjoint_loop_unpointed X Y (pconst (psusp X) Y) ~* pconst X (Ω Y) := - begin - refine pwhisker_right _ !ap1_pconst ⬝* _, - apply pconst_pcompose - end - - definition psusp_adjoint_loop [constructor] (X Y : Type*) : ppmap (psusp X) Y ≃* ppmap X (Ω Y) := - begin - apply pequiv_of_equiv (psusp_adjoint_loop_unpointed X Y), - apply eq_of_phomotopy, - apply psusp_adjoint_loop_pconst - end - -end new_susp open new_susp - --- this should replace corresponding definitions in homotopy.sphere -namespace new_sphere - - open sphere sphere.ops - - -- the definition was wrong for n = 0 - definition new.surf {n : ℕ} : Ω[n] (S* n) := - begin - induction n with n s, - { exact south }, - { exact (loopn_succ_in (S* (succ n)) n)⁻¹ᵉ* (apn n (equator n) s), } - end - - - definition psphere_pmap_pequiv' (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A := - begin - revert A, induction n with n IH: intro A, - { refine _ ⬝e* !pmap_pbool_pequiv, exact pequiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ* }, - { refine psusp_adjoint_loop (S* n) A ⬝e* IH (Ω A) ⬝e* !loopn_succ_in⁻¹ᵉ* } - end - - definition psphere_pmap_pequiv (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A := - begin - fapply pequiv_change_fun, - { exact psphere_pmap_pequiv' A n }, - { exact papn_fun A new.surf }, - { revert A, induction n with n IH: intro A, - { reflexivity }, - { intro f, refine ap !loopn_succ_in⁻¹ᵉ* (IH (Ω A) _ ⬝ !apn_pcompose _) ⬝ _, - exact !loopn_succ_in_inv_natural⁻¹* _ }} - end - -end new_sphere - namespace sphere - open sphere.ops new_sphere - -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) : -- f ~* pconst (S* n) (S* m) := -- begin @@ -761,39 +130,3 @@ namespace sphere -- end end sphere - -namespace cofiber - - -- replace with the definition of pcofiber (and remove primes in homotopy.smash) - definition pcofiber' [constructor] {A B : Type*} (f : A →* B) : Type* := - pointed.MK (cofiber f) !cofiber.base - attribute pcofiber [constructor] - -- move ppushout attribute out namespace - - protected definition elim {A : Type} {B : Type} {f : A → B} {P : Type} - (Pinl : P) (Pinr : B → P) (Pglue : Π (x : A), Pinl = Pinr (f x)) (y : cofiber f) : P := - begin - induction y using pushout.elim with x x x, induction x, exact Pinl, exact Pinr x, exact Pglue x, - end - -end cofiber -attribute cofiber.rec cofiber.elim [recursor 8] [unfold 8] - -namespace wedge - open pushout unit - definition wedge (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B) - local attribute wedge [reducible] - definition pwedge' (A B : Type*) : Type* := pointed.mk' (wedge A B) - - protected definition rec {A B : Type*} {P : wedge A B → Type} (Pinl : Π(x : A), P (inl x)) - (Pinr : Π(x : B), P (inr x)) (Pglue : pathover P (Pinl pt) (glue ⋆) (Pinr pt)) - (y : wedge A B) : P y := - by induction y; apply Pinl; apply Pinr; induction x; exact Pglue - - protected definition elim {A B : Type*} {P : Type} (Pinl : A → P) - (Pinr : B → P) (Pglue : Pinl pt = Pinr pt) (y : wedge A B) : P := - by induction y with a b x; exact Pinl a; exact Pinr b; induction x; exact Pglue - -end wedge - -attribute wedge.rec wedge.elim [recursor 7] [unfold 7] diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 7b895d7..e0e3585 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -13,7 +13,7 @@ open eq pointed equiv sigma of the type of pointed maps, giving the connectivity of the domain and the truncation level of the codomain. This is is_trunc_pmap at the end. - + First we define the type of dependent pointed maps as a tool, because these appear in the more general statement is_trunc_ppi (the generality needed for induction). @@ -24,13 +24,6 @@ open eq pointed equiv sigma namespace pointed - -- needs another name! (one more p?) - structure ppi (A : Type*) (P : A → Type*) := - (to_fun : Π a : A, P a) - (resp_pt : to_fun (Point A) = Point (P (Point A))) - - attribute ppi.to_fun [coercion] - abbreviation ppi_resp_pt [unfold 3] := @ppi.resp_pt definition pointed_ppi [instance] [constructor] {A : Type*} @@ -79,7 +72,7 @@ namespace pointed esimp at *, fapply apd011 ppi.mk, { apply eq_of_homotopy h }, - { esimp, apply concato_eq, apply pathover_eq_Fl, apply inv_con_eq_of_eq_con, + { esimp, apply concato_eq, apply eq_pathover_Fl, apply inv_con_eq_of_eq_con, rewrite [ap_eq_apd10, apd10_eq_of_homotopy], exact r } end @@ -105,11 +98,11 @@ namespace pointed ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), ppi_resp_pt f = ap (λh, h pt) p ⬝ ppi_resp_pt g : sigma_equiv_sigma_right - (λp, pathover_eq_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g)) + (λp, eq_pathover_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g)) ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), ppi_resp_pt f = apd10 p pt ⬝ ppi_resp_pt g : sigma_equiv_sigma_right - (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _)) + (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _))) ... ≃ Σ(p : f ~ g), ppi_resp_pt f = p pt ⬝ ppi_resp_pt g : sigma_equiv_sigma_left' eq_equiv_homotopy ... ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f