From eb8601dc93741814d0b0c29679bd070c1976faef Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 5 Oct 2018 18:03:12 -0400 Subject: [PATCH] prove some properties about is_built_from One property in this commit which we will use is the resulting short exact sequence if you have only two nontrivial subgroups. --- algebra/left_module.hlean | 110 +++++++++++++++++++++++++++++--------- 1 file changed, 84 insertions(+), 26 deletions(-) diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean index 83ee6ea..acc277a 100644 --- a/algebra/left_module.hlean +++ b/algebra/left_module.hlean @@ -280,7 +280,8 @@ section induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p, exact ap (homomorphism.mk φ₁) !is_prop.elim end -end + + end section @@ -403,6 +404,11 @@ end (h : Π(r : R) g, φ (r • g) = r • φ g) : M₁ ≃lm M₂ := isomorphism.mk (lm_homomorphism_of_group_homomorphism φ h) (group.isomorphism.is_equiv_to_hom φ) + definition trivial_homomorphism [constructor] (M₁ M₂ : LeftModule R) : M₁ →lm M₂ := + lm_homomorphism_of_group_homomorphism (group.trivial_add_homomorphism M₁ M₂) + (λs m, (smul_zero s)⁻¹) + + section local attribute pSet_of_LeftModule [coercion] definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type := @@ -493,31 +499,6 @@ end is_built_from.mk (λn, part H (n+1)) (λn, ses H (n+1)) isomorphism.rfl (pred (n₀ H)) (λs Hle, HD' H _ (le_succ_of_pred_le Hle)) - definition isomorphism_of_is_contr_part (H : is_built_from D E) (n : ℕ) (HE : is_contr (E n)) : - part H n ≃lm part H (n+1) := - isomorphism_of_is_contr_left (ses H n) HE - - definition is_contr_submodules (H : is_built_from D E) (HD : is_contr D) (n : ℕ) : - is_contr (part H n) := - begin - induction n with n IH, - { exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e0 H)) _ }, - { exact is_contr_right_of_short_exact_mod (ses H n) IH } - end - - definition is_contr_quotients (H : is_built_from D E) (HD : is_contr D) (n : ℕ) : - is_contr (E n) := - begin - apply is_contr_left_of_short_exact_mod (ses H n), - exact is_contr_submodules H HD n - end - - definition is_contr_total (H : is_built_from D E) (HE : Πn, is_contr (E n)) : is_contr D := - have is_contr (part H 0), from - nat.rec_down (λn, is_contr (part H n)) _ (HD' H _ !le.refl) - (λn H2, is_contr_middle_of_short_exact_mod (ses H n) (HE n) H2), - is_contr_equiv_closed (equiv_of_isomorphism (e0 H)) _ - definition is_built_from_isomorphism (e : D ≃lm D') (f : Πn, E n ≃lm E' n) (H : is_built_from D E) : is_built_from D' E' := ⦃is_built_from, H, e0 := e0 H ⬝lm e, @@ -527,9 +508,86 @@ end is_built_from D' E := ⦃is_built_from, H, e0 := e0 H ⬝lm e⦄ + definition isomorphism_of_is_contr_submodule (H : is_built_from D E) (n : ℕ) + (HE : is_contr (E n)) : part H n ≃lm part H (n+1) := + isomorphism_of_is_contr_left (ses H n) HE + + definition isomorphism_of_is_contr_submodules_range (H : is_built_from D E) {n k : ℕ} + (Hnk : n ≤ k) (HE : Πl, n ≤ l → l < k → is_contr (E l)) : part H n ≃lm part H k := + begin + induction Hnk with k Hnk IH, + { reflexivity }, + { refine IH (λl Hnl Hlk, HE l Hnl (lt.step Hlk)) ⬝lm + isomorphism_of_is_contr_submodule H k (HE k Hnk !self_lt_succ), } + end + + definition is_contr_quotients_of_is_contr_total (H : is_built_from D E) (HD : is_contr D) (n : ℕ) : + is_contr (part H n) := + begin + induction n with n IH, + { exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e0 H)) _ }, + { exact is_contr_right_of_short_exact_mod (ses H n) IH } + end + + definition is_contr_quotients_of_is_contr_submodules (H : is_built_from D E) {n : ℕ} + (HE : Πk, n ≤ k → is_contr (E k)) : is_contr (part H n) := + begin + refine is_contr_equiv_closed_rev _ (HD' H (max n (n₀ H)) !le_max_right), + apply equiv_of_isomorphism, + apply isomorphism_of_is_contr_submodules_range H !le_max_left, + intros l Hnl Hl', exact HE l Hnl + end + /- alternate direct proof -/ + -- nat.rec_down (λk, is_contr (part H (n + k))) _ (HD' H _ !nat.le_add_left) + -- (λk H2, is_contr_middle_of_short_exact_mod (ses H (n + k)) (HE (n + k) !nat.le_add_right) + -- proof H2 qed) + + definition isomorphism_of_is_contr_submodules (H : is_built_from D E) {n : ℕ} + (HE : Πk, n < k → is_contr (E k)) : E n ≃lm part H n := + isomorphism_of_is_contr_right (ses H n) (is_contr_quotients_of_is_contr_submodules H HE) + + -- definition is_contr_quotients_of_is_contr_submodules1 (H : is_built_from D E) (n : ℕ) + -- (HE : Πk, n ≤ k → is_contr (E k)) : is_contr (part H n) := + -- nat.rec_down (λk, is_contr (part H (n + k))) _ (HD' H _ !nat.le_add_left) + -- (λk H2, is_contr_middle_of_short_exact_mod (ses H (n + k)) (HE (n + k) !nat.le_add_right) + -- proof H2 qed) + definition isomorphism_zero_of_is_built_from (H : is_built_from D E) (p : n₀ H = 1) : E 0 ≃lm D := isomorphism_of_is_contr_right (ses H 0) (HD' H 1 (le_of_eq p)) ⬝lm e0 H + definition isomorphism_total_of_is_contr_submodules (H : is_built_from D E) {n : ℕ} + (HE : Πk, k < n → is_contr (E k)) : D ≃lm part H n := + (e0 H)⁻¹ˡᵐ ⬝lm isomorphism_of_is_contr_submodules_range H !zero_le (λk H0k Hkn, HE k Hkn) + + definition isomorphism_of_is_contr_submodules_but_one (H : is_built_from D E) {n : ℕ} + (HE : Πk, k ≠ n → is_contr (E k)) : D ≃lm E n := + (e0 H)⁻¹ˡᵐ ⬝lm + isomorphism_of_is_contr_submodules_range H !zero_le (λk H0k Hkn, HE k (ne_of_lt Hkn)) ⬝lm + (isomorphism_of_is_contr_submodules H (λk Hk, HE k (ne.symm (ne_of_lt Hk))))⁻¹ˡᵐ + + definition short_exact_mod_of_is_contr_submodules (H : is_built_from D E) {n m : ℕ} (Hnm : n < m) + (HE : Πk, k ≠ n → k ≠ m → is_contr (E k)) : short_exact_mod (E n) D (E m) := + begin + refine short_exact_mod_isomorphism isomorphism.rfl _ _ (ses H n), + { exact isomorphism_total_of_is_contr_submodules H (λk Hk, HE k (ne_of_lt Hk) + (ne_of_lt (lt.trans Hk Hnm))) }, + { exact isomorphism_of_is_contr_submodules H + (λk Hk, HE k (ne.symm (ne_of_lt (lt.trans Hnm Hk))) (ne.symm (ne_of_lt Hk))) ⬝lm + (isomorphism_of_is_contr_submodules_range H Hnm + (λk Hnk Hkm, HE k (ne.symm (ne_of_lt Hnk)) (ne_of_lt Hkm)))⁻¹ˡᵐ } + end + + definition is_contr_submodules (H : is_built_from D E) (HD : is_contr D) (n : ℕ) : + is_contr (E n) := + begin + apply is_contr_left_of_short_exact_mod (ses H n), + exact is_contr_quotients_of_is_contr_total H HD n + end + + definition is_contr_total (H : is_built_from D E) (HE : Πn, is_contr (E n)) : is_contr D := + have is_contr (part H 0), from is_contr_quotients_of_is_contr_submodules H (λn H, HE n), + is_contr_equiv_closed (equiv_of_isomorphism (e0 H)) _ + section int open int definition left_module_int_of_ab_group [constructor] (A : Type) [add_ab_group A] : left_module rℤ A :=