checkpoint for direct sum of graded modules

2017-03-31 18:21:02 -04:00 · 2017-03-31 18:21:02 -04:00 · 5bb2c7859d
commit 5bb2c7859d
parent 200885ad21
7 changed files with 223 additions and 18 deletions
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@ -20,14 +20,14 @@ namespace group
  section

    parameters {I : Set} (Y : I → AbGroup)
-    variables {A' : AbGroup}
+    variables {A' : AbGroup} {Y' : I → AbGroup}

    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 : AbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
+    definition dirsum : AddAbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)

    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier :=

@ -35,6 +35,38 @@ 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

+    parameter {Y}
+    definition dirsum.rec {P : dirsum → Type} [H : Πg, is_prop (P g)]
+      (h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 1) (h₃ : Πg h, P g → P h → P (g * h)) :
+      Πg, P g :=
+    begin
+      refine @set_quotient.rec_prop _ _ _ H _,
+      refine @set_quotient.rec_prop _ _ _ (λx, !H) _,
+      esimp, intro l, induction l with s l ih,
+        exact h₂,
+      induction s with v v,
+        induction v with i y,
+        exact h₃ _ _ (h₁ i y) ih,
+      induction v with i y,
+      refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
+      refine transport P _ (h₁ i y⁻¹),
+      refine _ ⬝ !one_mul,
+      refine _ ⬝ ap (λx, mul x _) (to_respect_one (dirsum_incl i)),
+      apply gqg_eq_of_rel',
+      apply tr, esimp,
+      refine transport dirsum_rel _ (dirsum_rel.rmk i y⁻¹ y),
+      rewrite [mul.left_inv, mul.assoc],
+    end
+
+    definition dirsum_homotopy {φ ψ : dirsum →g A'}
+      (h : Πi (y : Y i), φ (dirsum_incl i y) = ψ (dirsum_incl i y)) : φ ~ ψ :=
+    begin
+      refine dirsum.rec _ _ _,
+          exact h,
+        refine !respect_one ⬝ !respect_one⁻¹,
+      intro g₁ g₂ h₁ h₂, rewrite [+ to_respect_mul, h₁, h₂]
+    end
+
    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
@ -60,7 +92,44 @@ namespace group
      intro x, induction x with i y, exact H i y
    end

-
  end

+  variables {I J : Set} {Y Y' Y'' : I → AddAbGroup}
+
+  definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' :=
+  dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
+
+  theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) :
+    dirsum_functor f' ∘g dirsum_functor f ~ dirsum_functor (λi, f' i ∘g f i) :=
+  begin
+    apply dirsum_homotopy,
+    intro i y, reflexivity,
+  end
+
+  variable (Y)
+  definition dirsum_functor_gid : dirsum_functor (λi, gid (Y i)) ~ gid (dirsum Y) :=
+  begin
+    apply dirsum_homotopy,
+    intro i y, reflexivity,
+  end
+  variable {Y}
+
+  definition dirsum_functor_add (f f' : Πi, Y i →g Y' i) :
+    homomorphism_add (dirsum_functor f) (dirsum_functor f') ~
+    dirsum_functor (λi, homomorphism_add (f i) (f' i)) :=
+  begin
+    apply dirsum_homotopy,
+    intro i y, exact sorry
+  end
+
+  definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :
+    dirsum_functor f ~ dirsum_functor f' :=
+  begin
+    apply dirsum_homotopy,
+    intro i y, exact sorry
+  end
+
+  definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y :=
+  dirsum_elim (λj, dirsum_incl Y (f j))
+
 end group
--- a/algebra/free_commutative_group.hlean
+++ b/algebra/free_commutative_group.hlean
@ -8,13 +8,14 @@ Constructions with groups

 import algebra.group_theory hit.set_quotient types.list types.sum .free_group

-open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list trunc function equiv
+open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list trunc function equiv trunc_index
+     group

 namespace group

  variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}

-  variables (X : Set) {l l' : list (X ⊎ X)}
+  variables (X : Set) {Y : Set} {l l' : list (X ⊎ X)}

  /- Free Abelian Group of a set -/
  namespace free_ab_group
@ -197,4 +198,36 @@ namespace group
      reflexivity }
  end

+  definition free_ab_group_functor (f : X → Y) : free_ab_group X →g free_ab_group Y :=
+  free_ab_group_elim (free_ab_group_inclusion ∘ f)
+
+-- set_option pp.all true
+--   definition free_ab_group.rec {P : free_ab_group X → Type} [H : Πg, is_prop (P g)]
+--     (h₁ : Πx, P (free_ab_group_inclusion x))
+--     (h₂ : P 0)
+--     (h₃ : Πg h, P g → P h → P (g * h))
+--     (h₄ : Πg, P g → P g⁻¹) :
+--     Πg, P g :=
+--   begin
+--     refine @set_quotient.rec_prop _ _ _ H _,
+--     refine @set_quotient.rec_prop _ _ _ (λx, !H) _,
+--     esimp, intro l, induction l with s l ih,
+--       exact h₂,
+--     induction s with v v,
+--       induction v with i y,
+--       exact h₃ _ _ (h₁ i y) ih,
+--     induction v with i y,
+--     refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
+--     refine transport P _ (h₁ i y⁻¹),
+--     refine _ ⬝ !mul_one,
+--     refine _ ⬝ ap (mul _) (to_respect_one (dirsum_incl i)),
+--     apply gqg_eq_of_rel',
+--     apply tr, esimp,
+--     refine transport dirsum_rel _ (dirsum_rel.rmk i y⁻¹ y),
+--     rewrite [mul.left_inv, mul.assoc],
+--     apply ap (mul _),
+--     refine _ ⬝ (mul_inv (class_of [inr ⟨i, y⟩]) (ι ⟨i, 1⟩))⁻¹ᵖ,
+--     refine ap011 mul _ _,
+--   end
+
 end group
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@ -2,14 +2,14 @@

 -- Author: Floris van Doorn

-import .left_module
+import .left_module .direct_sum

-open algebra eq left_module pointed function equiv is_equiv is_trunc prod
+open algebra eq left_module pointed function equiv is_equiv is_trunc prod group

 namespace left_module

-definition graded (str : Type) (I : Type) : Type := I → str
-definition graded_module (R : Ring) : Type → Type := graded (LeftModule R)
+definition graded [reducible] (str : Type) (I : Type) : Type := I → str
+definition graded_module [reducible] (R : Ring) : Type → Type := graded (LeftModule R)

 variables {R : Ring} {I : Type} {M M₁ M₂ M₃ : graded_module R I}

@ -149,6 +149,41 @@ definition graded_hom_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M
  : M₁ →gm M₂ :=
 graded_iso_of_eq p

+/- direct sum of graded R-modules -/
+
+variables {J : Set} (N : graded_module R J)
+definition dirsum' : AddAbGroup :=
+group.dirsum (λj, AddAbGroup_of_LeftModule (N j))
+variable {N}
+definition dirsum_smul [constructor] (r : R) : dirsum' N →g dirsum' N :=
+dirsum_functor (λi, smul_homomorphism (N i) r)
+
+definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) :
+  dirsum_smul (r + s) n = dirsum_smul r n + dirsum_smul s n :=
+begin
+  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_add⁻¹,
+  intro i ni, exact to_smul_right_distrib r s ni
+end
+
+definition dirsum_mul_smul (r s : R) (n : dirsum' N) :
+  dirsum_smul (r * s) n = dirsum_smul r (dirsum_smul s n) :=
+begin
+  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_compose⁻¹,
+  intro i ni, exact to_mul_smul r s ni
+end
+
+definition dirsum_one_smul (n : dirsum' N) : dirsum_smul 1 n = n :=
+begin
+  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_gid,
+  intro i ni, exact to_one_smul ni
+end
+
+definition dirsum : LeftModule R :=
+LeftModule_of_AddAbGroup (dirsum' N) (λr n, dirsum_smul r n) (λr, homomorphism.addstruct (dirsum_smul r))
+  dirsum_smul_right_distrib
+  dirsum_mul_smul
+  dirsum_one_smul
+
 /- exact couples -/

 definition is_exact_gmod (f : M₁ →gm M₂) (f' : M₂ →gm M₃) : Type :=
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@ -8,7 +8,7 @@ Modules prod vector spaces over a ring.
 (We use "left_module," which is more precise, because "module" is a keyword.)
 -/
 import algebra.field ..move_to_lib
-open is_trunc pointed function sigma eq algebra prod is_equiv equiv
+open is_trunc pointed function sigma eq algebra prod is_equiv equiv group

 structure has_scalar [class] (F V : Type) :=
 (smul : F → V → V)
@ -80,6 +80,7 @@ section left_module

  proposition sub_smul_right_distrib (a b : R) (v : M) : (a - b) • v = a • v - b • v :=
  by rewrite [sub_eq_add_neg, smul_right_distrib, neg_smul]
+
 end left_module

 /- vector spaces -/
@ -145,18 +146,56 @@ end module_hom
 structure LeftModule (R : Ring) :=
 (carrier : Type) (struct : left_module R carrier)

-local attribute LeftModule.carrier [coercion]
+attribute LeftModule.carrier [coercion]
 attribute LeftModule.struct [instance]

 definition pointed_LeftModule_carrier [instance] {R : Ring} (M : LeftModule R) :
  pointed (LeftModule.carrier M) :=
 pointed.mk zero

-definition pSet_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : Set* :=
+definition pSet_of_LeftModule {R : Ring} (M : LeftModule R) : Set* :=
 pSet.mk' (LeftModule.carrier M)

+definition AddAbGroup_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : AddAbGroup :=
+AddAbGroup.mk M _
+
+definition left_module_AddAbGroup_of_LeftModule [instance] {R : Ring} (M : LeftModule R) :
+  left_module R (AddAbGroup_of_LeftModule M) :=
+LeftModule.struct M
+
+definition left_module_of_ab_group (G : Type) [gG : add_ab_group G] (R : Type) [ring R]
+  (smul : R → G → G)
+  (h1 : Π (r : R) (x y : G), smul r (x + y) = (smul r x + smul r y))
+  (h2 : Π (r s : R) (x : G), smul (r + s) x = (smul r x + smul s x))
+  (h3 : Π r s x, smul (r * s) x = smul r (smul s x))
+  (h4 : Π x, smul 1 x = x) : left_module R G  :=
+begin
+  cases gG with Gs Gm Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5,
+  exact left_module.mk smul Gs Gm Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5 h1 h2 h3 h4
+end
+
+definition LeftModule_of_AddAbGroup {R : Ring} (G : AddAbGroup) (smul : R → G → G)
+  (h1 h2 h3 h4) : LeftModule R :=
+LeftModule.mk G (left_module_of_ab_group G R smul h1 h2 h3 h4)
+
+
 section
-  variable {R : Ring}
+  variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R}
+
+  definition smul_homomorphism [constructor] (M : LeftModule R) (r : R) :
+    AddAbGroup_of_LeftModule M →g AddAbGroup_of_LeftModule M :=
+  add_homomorphism.mk (λg, r • g) (smul_left_distrib r)
+
+  proposition to_smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
+  !smul_left_distrib
+
+  proposition to_smul_right_distrib (a b : R) (u : M) : (a + b) • u = a • u + b • u :=
+  !smul_right_distrib
+
+  proposition to_mul_smul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) :=
+  !mul_smul
+
+  proposition to_one_smul (u : M) : (1 : R) • u = u := !one_smul

  structure homomorphism (M₁ M₂ : LeftModule R) : Type :=
    (fn : LeftModule.carrier M₁ → LeftModule.carrier M₂)
@ -171,7 +210,8 @@ section
  homomorphism.p φ

  section
-    variables {M₁ M₂ : LeftModule R} (φ : M₁ →lm M₂)
+
+    variable (φ : M₁ →lm M₂)

    definition to_respect_add (x y : M₁) : φ (x + y) = φ x + φ y :=
    respect_add φ x y
@ -220,7 +260,6 @@ section
 end

  section
-  variables {M M₁ M₂ M₃ : LeftModule R}

  definition LeftModule.struct2 [instance] (M : LeftModule R) : left_module R M :=
  LeftModule.struct M
@ -256,8 +295,11 @@ end
  definition equiv_of_isomorphism [constructor] (φ : M₁ ≃lm M₂) : M₁ ≃ M₂ :=
  equiv.mk φ !isomorphism.is_equiv_to_hom

+  section
+  local attribute pSet_of_LeftModule [coercion]
  definition pequiv_of_isomorphism [constructor] (φ : M₁ ≃lm M₂) : M₁ ≃* M₂ :=
  pequiv_of_equiv (equiv_of_isomorphism φ) (to_respect_zero φ)
+  end

  definition isomorphism_of_equiv [constructor] (φ : M₁ ≃ M₂)
    (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
@ -320,8 +362,11 @@ end
    : M₁ →lm M₂ :=
  isomorphism_of_eq p

+  section
+  local attribute pSet_of_LeftModule [coercion]
  definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
  @is_exact M₁ M₂ M₃ (homomorphism_fn f) (homomorphism_fn f')
+  end

  end

--- a/algebra/module_chain_complex.hlean
+++ b/algebra/module_chain_complex.hlean
@ -10,7 +10,7 @@ open left_module

 structure module_chain_complex (R : Ring) (N : succ_str) : Type :=
 (mod : N → LeftModule R)
-(hom : Π (n : N), left_module.homomorphism (mod (S n)) (mod n))
+(hom : Π (n : N), mod (S n) →lm mod n)
 (is_chain_complex :
  Π (n : N) (x : mod (S (S n))), hom n (hom (S n) x) = 0)

--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@ -13,6 +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}
+            {N' : normal_subgroup_rel G'}
  variables {A B : AbGroup}

  /- Quotient Group -/
@ -195,7 +196,7 @@ namespace group
    apply rel_of_eq _ H
  end

-  definition rel_of_ab_qg_map_eq_one {K : subgroup_rel A} (a :A) (H : ab_qg_map K a = 1) : K a := 
+  definition rel_of_ab_qg_map_eq_one {K : subgroup_rel A} (a :A) (H : ab_qg_map K a = 1) : K a :=
  begin
    have e : (a * 1⁻¹ = a),
    from calc
@ -268,6 +269,14 @@ namespace group
    exact H
  end

+  definition quotient_group_functor [constructor] (φ : G →g G') (h : Πg, N g → N' (φ g)) :
+    quotient_group N →g quotient_group N' :=
+  begin
+    apply quotient_group_elim (qg_map N' ∘g φ),
+    intro g Ng, esimp,
+    refine qg_map_eq_one (φ g) (h g Ng)
+  end
+
 ------------------------------------------------
  -- FIRST ISOMORPHISM THEOREM
 ------------------------------------------------
@ -402,7 +411,7 @@ definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
    exact is_embedding_kernel_quotient_extension f
  end

-definition ab_group_first_iso_thm {A B : AbGroup} (f : A →g B) 
+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,
@ -464,6 +473,10 @@ definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g
    definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h :=
    eq_of_rel (tr (rincl H))

+    -- this one might work if the previous one doesn't (maybe make this the default one?)
+    definition gqg_eq_of_rel' {g h : A₁} (H : S (g * h⁻¹)) : class_of g = class_of h :> quotient_ab_group_gen :=
+    gqg_eq_of_rel H
+
    definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
      : quotient_ab_group_gen →g A₂ :=
    begin
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@ -490,6 +490,16 @@ namespace group
    φ ⬝g ψ ~ ψ ∘ φ :=
  by reflexivity

+  definition add_homomorphism.mk [constructor] {G H : AddGroup} (φ : G → H) (h : is_add_hom φ) : G →g H :=
+  homomorphism.mk φ h
+
+  definition homomorphism_add [constructor] {G H : AddAbGroup} (φ ψ : G →g H) : G →g H :=
+  add_homomorphism.mk (λg, φ g + ψ g)
+    abstract begin
+      intro g g', refine ap011 add !to_respect_add !to_respect_add ⬝ _,
+      refine !add.assoc ⬝ ap (add _) (!add.assoc⁻¹ ⬝ ap (λx, x * _) !add.comm ⬝ !add.assoc) ⬝ !add.assoc⁻¹
+    end end
+
  definition pmap_of_homomorphism_gid (G : Group) : pmap_of_homomorphism (gid G) ~* pid G :=
  begin
    fapply phomotopy_of_homotopy, reflexivity