From daedc1dc4892cc4fd26c67443afa9ec623594f16 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 27 Apr 2017 19:04:30 -0400 Subject: [PATCH] continue convergence theorem --- algebra/graded.hlean | 57 ++++++++++++++---- algebra/quotient_group.hlean | 6 +- algebra/subgroup.hlean | 10 +--- algebra/submodule.hlean | 112 +++++++++++++++++++++++++++++++++-- move_to_lib.hlean | 34 ++++++++++- 5 files changed, 190 insertions(+), 29 deletions(-) diff --git a/algebra/graded.hlean b/algebra/graded.hlean index 1602b53..df16627 100644 --- a/algebra/graded.hlean +++ b/algebra/graded.hlean @@ -424,7 +424,7 @@ definition graded_quotient_map [constructor] (S : Πi, submodule_rel (M i)) : graded_hom.mk erfl (λi, quotient_map (S i)) definition graded_homology (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_module R I := -λi, homology (g i) (f ↘ (to_right_inv (deg f) i)) +λi, homology (g i) (f ← i) definition graded_homology_intro [constructor] (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_kernel g →gm graded_homology g f := @@ -484,10 +484,10 @@ namespace left_module definition E' : graded_module R I := graded_homology d d definition is_contr_E' {x : I} (H : is_contr (E x)) : is_contr (E' x) := - sorry + !is_contr_homology definition is_contr_D' {x : I} (H : is_contr (D x)) : is_contr (D' x) := - sorry + !is_contr_image_module definition i' : D' →gm D' := graded_image_lift i ∘gm graded_submodule_incl _ @@ -595,10 +595,10 @@ namespace left_module ij := i'j' X, jk := j'k' X, ki := k'i' X⦄ parameters {R : Ring} {I : Set} (X : exact_couple R I) (B : I → ℕ) - (Dub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X)) s x) = y → is_contr (D X y)) - (Dlb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s x) = y → is_contr (D X y)) - (Eub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X)) s x) = y → is_contr (E X y)) - (Elb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s x) = y → is_contr (E X y)) + (Dub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → (deg (k X))⁻¹ (iterate (deg (i X)) s ((deg (j X))⁻¹ x)) = y → is_contr (D X y)) + (Eub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → (deg (k X))⁻¹ (iterate (deg (i X)) s ((deg (j X))⁻¹ x)) = y → is_contr (E X y)) + (Dlb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s (deg (k X) x)) = y → is_contr (D X y)) + (Elb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s (deg (k X) x)) = y → is_contr (E X y)) -- also need a single deg j and/or deg k here -- we start counting pages at 0, not at 2. @@ -642,13 +642,48 @@ namespace left_module deg (d (page r)) ~ deg (j X) ∘ iterate (deg (i X))⁻¹ r ∘ deg (k X) := compose2 (deg_j r) (deg_k r) - definition Eub' (x : I) (r : ℕ) (h : B (deg (k X) x) ≤ r) : + definition deg_d_inv (r : ℕ) : + (deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ := + sorry --inv_homotopy_inv (deg_d r) ⬝hty _ --compose2 (deg_j r) (deg_k r) + + include Elb Eub + definition Eub' (x : I) (r : ℕ) (h : B x ≤ r) : is_contr (E (page r) (deg (d (page r)) x)) := is_contr_E _ _ (Elb h (deg_d r x)⁻¹) - definition Estable {x : I} {r : ℕ} (H : B (deg (k X) x) ≤ r) : - E (page (r + 1)) x ≃ E (page r) x := - sorry + definition Elb' (x : I) (r : ℕ) (h : B x ≤ r) : + is_contr (E (page r) ((deg (d (page r)))⁻¹ x)) := + is_contr_E _ _ (Eub h (deg_d_inv r x)⁻¹) + + -- definition Dub' (x : I) (r : ℕ) (h : B x ≤ r) : + -- is_contr (D (page r) (deg (d (page r)) x)) := + -- is_contr_D _ _ (Dlb h (deg_d r x)⁻¹) + + -- definition Dlb' (x : I) (r : ℕ) (h : B x ≤ r) : + -- is_contr (D (page r) ((deg (d (page r)))⁻¹ x)) := + -- is_contr_D _ _ (Dub h (deg_d_inv r x)⁻¹) + + definition Estable {x : I} {r : ℕ} (H : B x ≤ r) : + E (page (r + 1)) x ≃lm E (page r) x := + begin + change homology (d (page r) x) (d (page r) ← x) ≃lm E (page r) x, + apply homology_isomorphism, + exact Elb' _ _ H, exact Eub' _ _ H + end + + definition is_equiv_i {x y : I} {r : ℕ} (H : B y ≤ r) (p : deg (i (page r)) x = y) : + is_equiv (i (page r) ↘ p) := + begin + induction p, + exact sorry + end + + definition Dstable {x : I} {r : ℕ} (H : B x ≤ r) : + D (page (r + 1)) x ≃lm D (page r) x := + begin + change image_module (i (page r) ← x) ≃lm D (page r) x, + exact image_module_isomorphism (isomorphism.mk (i (page r) ← x) (is_equiv_i H _)) + end definition inf_page : graded_module R I := λx, E (page (B (deg (k X) x))) x diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index b7be5ec..474fd64 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -144,11 +144,7 @@ namespace group homomorphism.mk class_of (λ g h, idp) definition ab_qg_map {G : AbGroup} (N : subgroup_rel G) : G →g quotient_ab_group N := - begin - fapply homomorphism.mk, - exact class_of, - exact λ g h, idp - end + qg_map _ definition is_surjective_ab_qg_map {A : AbGroup} (N : subgroup_rel A) : is_surjective (ab_qg_map N) := begin diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index 27eaf46..35870cf 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -243,11 +243,7 @@ namespace group end definition is_embedding_incl_of_subgroup {G : Group} (H : subgroup_rel G) : is_embedding (incl_of_subgroup H) := - begin - fapply function.is_embedding_of_is_injective, - intro h h', - fapply subtype_eq - end + function.is_embedding_pr1 _ definition ab_kernel_incl {G H : AbGroup} (f : G →g H) : ab_kernel f →g G := begin @@ -447,8 +443,8 @@ definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : subgroup_rel definition ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) : ab_subgroup R →g ab_subgroup S := - ab_subgroup_functor (gid A) H - + ab_subgroup_functor (gid A) H + definition is_embedding_ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) : is_embedding (ab_subgroup_of_subgroup_incl H) := begin fapply is_embedding_subgroup_of_subgroup_incl, diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean index e8118ac..4ad5375 100644 --- a/algebra/submodule.hlean +++ b/algebra/submodule.hlean @@ -1,12 +1,39 @@ import .left_module .quotient_group -open algebra eq group sigma is_trunc function trunc +open algebra eq group sigma is_trunc function trunc equiv is_equiv -- move to subgroup attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2] attribute normal_subgroup_rel.to_subgroup_rel [constructor] + definition is_equiv_incl_of_subgroup {G : Group} (H : subgroup_rel G) (h : Πg, H g) : + is_equiv (incl_of_subgroup H) := + have is_surjective (incl_of_subgroup H), + begin intro g, exact image.mk ⟨g, h g⟩ idp end, + have is_embedding (incl_of_subgroup H), from is_embedding_incl_of_subgroup H, + function.is_equiv_of_is_surjective_of_is_embedding (incl_of_subgroup H) + +definition subgroup_isomorphism [constructor] {G : Group} (H : subgroup_rel G) (h : Πg, H g) : + subgroup H ≃g G := +isomorphism.mk _ (is_equiv_incl_of_subgroup H h) + +definition is_equiv_qg_map {G : Group} (H : normal_subgroup_rel G) (H₂ : Π⦃g⦄, H g → g = 1) : + is_equiv (qg_map H) := +set_quotient.is_equiv_class_of _ (λg h r, eq_of_mul_inv_eq_one (H₂ r)) + +definition quotient_group_isomorphism [constructor] {G : Group} (H : normal_subgroup_rel G) + (h : Πg, H g → g = 1) : quotient_group H ≃g G := +(isomorphism.mk _ (is_equiv_qg_map H h))⁻¹ᵍ + +definition is_equiv_ab_qg_map {G : AbGroup} (H : subgroup_rel G) (h : Π⦃g⦄, H g → g = 1) : + is_equiv (ab_qg_map H) := +proof is_equiv_qg_map _ h qed + +definition ab_quotient_group_isomorphism [constructor] {G : AbGroup} (H : subgroup_rel G) + (h : Πg, H g → g = 1) : quotient_ab_group H ≃g G := +(isomorphism.mk _ (is_equiv_ab_qg_map H h))⁻¹ᵍ + namespace left_module /- submodules -/ variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M} @@ -105,7 +132,7 @@ definition incl_smul (S : submodule_rel M) (r : R) (m : M) (h : S m) : r • ⟨m, h⟩ = ⟨_, contains_smul S r h⟩ :> submodule S := by reflexivity -definition submodule_rel_of_submodule [constructor] (S₂ S₁ : submodule_rel M) : +definition submodule_rel_submodule [constructor] (S₂ S₁ : submodule_rel M) : submodule_rel (submodule S₂) := submodule_rel.mk (λm, S₁ (submodule_incl S₂ m)) (contains_zero S₁) @@ -114,6 +141,23 @@ submodule_rel.mk (λm, S₁ (submodule_incl S₂ m)) intro m r p, induction m with m hm, exact contains_smul S₁ r p end +definition submodule_rel_submodule_trivial [constructor] {S₂ S₁ : submodule_rel M} + (h : Π⦃m⦄, S₁ m → m = 0) ⦃m : submodule S₂⦄ (Sm : submodule_rel_submodule S₂ S₁ m) : m = 0 := +begin + fapply subtype_eq, + apply h Sm +end + +definition is_prop_submodule (S : submodule_rel M) [H : is_prop M] : is_prop (submodule S) := +begin apply @is_trunc_sigma, exact H end +local attribute is_prop_submodule [instance] +definition is_contr_submodule [instance] (S : submodule_rel M) [is_contr M] : is_contr (submodule S) := +is_contr_of_inhabited_prop 0 + +definition submodule_isomorphism [constructor] (S : submodule_rel M) (h : Πg, S g) : + submodule S ≃lm M := +isomorphism.mk (submodule_incl S) (is_equiv_incl_of_subgroup (subgroup_rel_of_submodule_rel S) h) + /- quotient modules -/ definition quotient_module' (S : submodule_rel M) : AddAbGroup := @@ -123,7 +167,7 @@ definition quotient_module_smul [constructor] (S : submodule_rel M) (r : R) : quotient_module' S →a quotient_module' S := quotient_ab_group_functor (smul_homomorphism M r) (λg, contains_smul S r) -set_option formatter.hide_full_terms false + definition quotient_module_smul_right_distrib (r s : R) (n : quotient_module' S) : quotient_module_smul S (r + s) n = quotient_module_smul S r n + quotient_module_smul S s n := @@ -172,6 +216,18 @@ lm_homomorphism_of_group_homomorphism exact to_respect_smul φ r m end +definition is_prop_quotient_module (S : submodule_rel M) [H : is_prop M] : is_prop (quotient_module S) := +begin apply @set_quotient.is_trunc_set_quotient, exact H end +local attribute is_prop_quotient_module [instance] + +definition is_contr_quotient_module [instance] (S : submodule_rel M) [is_contr M] : + is_contr (quotient_module S) := +is_contr_of_inhabited_prop 0 + +definition quotient_module_isomorphism [constructor] (S : submodule_rel M) (h : Π⦃m⦄, S m → m = 0) : + quotient_module S ≃lm M := +(isomorphism.mk (quotient_map S) (is_equiv_ab_qg_map (subgroup_rel_of_submodule_rel S) h))⁻¹ˡᵐ + /- specific submodules -/ definition has_scalar_image (φ : M₁ →lm M₂) ⦃m : M₂⦄ (r : R) (h : image φ m) : image φ (r • m) := @@ -186,6 +242,14 @@ submodule_rel_of_subgroup_rel (image_subgroup (group_homomorphism_of_lm_homomorphism φ)) (has_scalar_image φ) +definition image_rel_trivial (φ : M₁ →lm M₂) [H : is_contr M₁] ⦃m : M₂⦄ (h : image_rel φ m) : m = 0 := +begin + refine image.rec _ h, + intro x p, + refine p⁻¹ ⬝ ap φ _ ⬝ to_respect_zero φ, + apply @is_prop.elim, apply is_trunc_succ, exact H +end + definition image_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (image_rel φ) -- unfortunately this is note definitionally equal: @@ -213,21 +277,50 @@ begin reflexivity end +definition is_contr_image_module [instance] (φ : M₁ →lm M₂) [is_contr M₂] : + is_contr (image_module φ) := +!is_contr_submodule + +definition is_contr_image_module_of_is_contr_dom (φ : M₁ →lm M₂) [is_contr M₁] : + is_contr (image_module φ) := +is_contr.mk 0 + begin + have Π(x : image_module φ), is_prop (0 = x), from _, + apply @total_image.rec, + exact this, + intro m, + induction (is_prop.elim 0 m), apply subtype_eq, + exact (to_respect_zero φ)⁻¹ + end + +definition image_module_isomorphism [constructor] (φ : M₁ ≃lm M₂) : image_module φ ≃lm M₂ := +submodule_isomorphism _ (λm, image.mk (φ⁻¹ˡᵐ m) proof to_right_inv (equiv_of_isomorphism φ) m qed) + definition has_scalar_kernel (φ : M₁ →lm M₂) ⦃m : M₁⦄ (r : R) (p : φ m = 0) : φ (r • m) = 0 := begin refine to_respect_smul φ r m ⬝ ap (λx, r • x) p ⬝ smul_zero r, end -definition kernel_rel [constructor](φ : M₁ →lm M₂) : submodule_rel M₁ := +definition kernel_rel [constructor] (φ : M₁ →lm M₂) : submodule_rel M₁ := submodule_rel_of_subgroup_rel (kernel_subgroup (group_homomorphism_of_lm_homomorphism φ)) (has_scalar_kernel φ) +definition kernel_rel_full (φ : M₁ →lm M₂) [is_contr M₂] (m : M₁) : kernel_rel φ m := +!is_prop.elim + definition kernel_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (kernel_rel φ) +definition is_contr_kernel_module [instance] (φ : M₁ →lm M₂) [is_contr M₁] : + is_contr (kernel_module φ) := +!is_contr_submodule + +definition kernel_module_isomorphism [constructor] (φ : M₁ →lm M₂) [is_contr M₂] : kernel_module φ ≃lm M₁ := +submodule_isomorphism _ (kernel_rel_full φ) + definition homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : LeftModule R := -@quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_of_submodule _ (image_rel φ)) +@quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_submodule _ (image_rel φ)) definition homology.mk (m : M₂) (h : ψ m = 0) : homology ψ φ := quotient_map _ ⟨m, h⟩ @@ -255,6 +348,15 @@ quotient_elim (θ ∘lm submodule_incl _) exact ap θ p⁻¹ ⬝ H m' end +definition is_contr_homology [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) [is_contr M₂] : + is_contr (homology ψ φ) := +begin apply @is_contr_quotient_module end + +definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) [is_contr M₁] [is_contr M₃] : + homology ψ φ ≃lm M₂ := +quotient_module_isomorphism _ (submodule_rel_submodule_trivial (image_rel_trivial φ)) ⬝lm +!kernel_module_isomorphism + -- remove: -- definition homology.rec (P : homology ψ φ → Type) diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 3b6d9df..6a6d8c8 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -1,6 +1,6 @@ -- definitions, theorems and attributes which should be moved to files in the HoTT library -import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc +import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group is_trunc function sphere unit sum prod bool @@ -1164,3 +1164,35 @@ structure Ring := attribute Ring.carrier [coercion] attribute Ring.struct [instance] + +namespace set_quotient + definition is_prop_set_quotient {A : Type} (R : A → A → Prop) [is_prop A] : is_prop (set_quotient R) := + begin + apply is_prop.mk, intro x y, + induction x using set_quotient.rec_prop, induction y using set_quotient.rec_prop, + exact ap class_of !is_prop.elim + end + + local attribute is_prop_set_quotient [instance] + definition is_trunc_set_quotient [instance] (n : ℕ₋₂) {A : Type} (R : A → A → Prop) [is_trunc n A] : + is_trunc n (set_quotient R) := + begin + cases n with n, { apply is_contr_of_inhabited_prop, exact class_of !center }, + cases n with n, { apply _ }, + apply is_trunc_succ_succ_of_is_set + end + + definition is_equiv_class_of [constructor] {A : Type} [is_set A] (R : A → A → Prop) + (p : Π⦃a b⦄, R a b → a = b) : is_equiv (@class_of A R) := + begin + fapply adjointify, + { intro x, induction x, exact a, exact p H }, + { intro x, induction x using set_quotient.rec_prop, reflexivity }, + { intro a, reflexivity } + end + + definition equiv_set_quotient [constructor] {A : Type} [is_set A] (R : A → A → Prop) + (p : Π⦃a b⦄, R a b → a = b) : A ≃ set_quotient R := + equiv.mk _ (is_equiv_class_of R p) + +end set_quotient