finish categorical structure of graded modules

algebra/graded.hlean

@@ -13,51 +13,161 @@ definition graded_module (R : Ring) : Type → Type := graded (LeftModule R)
 
 variables {R : Ring} {I : Type} {M M₁ M₂ M₃ : graded_module R I}
 
-structure graded_module_hom (M₁ M₂ : graded_module R I) : Type :=
+/-
+  morphisms between graded modules.
+  The definition is unconventional in two ways:
+  (1) The degree is determined by an endofunction instead of a element of I (and in this case we
+    don't need to assume that I is a group). The "standard" degree i corresponds to the endofunction
+    which is addition with i on the right. However, this is more flexible. For example, the
+    composition of two graded module homomorphisms φ₂ and φ₁ with degrees i₂ and i₁ has type
+    M₁ i → M₂ ((i + i₁) + i₂).
+    However, a homomorphism with degree i₁ + i₂ must have type
+    M₁ i → M₂ (i + (i₁ + i₂)),
+    which means that we need to insert a transport. With endofunctions this is not a problem:
+    λi, (i + i₁) + i₂
+    is a perfectly fine degree of a map
+  (2) Since we cannot eliminate all possible transports, we don't define a homomorphism as function
+    M₁ i →lm M₂ (i + deg f)  or  M₁ i →lm M₂ (deg f i)
+    but as a function taking a path as argument. Specifically, for every path
+    deg f i = j
+    we get a function M₁ i → M₂ j.
+-/
+structure graded_hom (M₁ M₂ : graded_module R I) : Type :=
 mk' ::  (d : I → I)
-        (fn : Π⦃i j : I⦄ (p : d i = j), M₁ i →lm M₂ j)
+        (fn' : Π⦃i j : I⦄ (p : d i = j), M₁ i →lm M₂ j)
 
-abbreviation degree := @graded_module_hom.d
+notation M₁ ` →gm ` M₂ := graded_hom M₁ M₂
-attribute graded_module_hom.fn [coercion]
 
-definition graded_module_hom.mk {M₁ M₂ : graded_module R I} (d : I → I)
+abbreviation deg [unfold 5] := @graded_hom.d
-  (fn : Πi, M₁ i →lm M₂ (d i)) : graded_module_hom M₁ M₂ :=
+notation `↘` := graded_hom.fn' -- there is probably a better character for this?
-graded_module_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
 
-notation M₁ ` →gm ` M₂ := graded_module_hom M₁ M₂
+definition graded_hom_fn [unfold 5] [coercion] (f : M₁ →gm M₂) (i : I) : M₁ i →lm M₂ (deg f i) :=
+↘f idp
 
--- definition graded_module_hom (d : I → I) (M₁ M₂ : graded_module R I) : Type :=
+definition graded_hom.mk [constructor] {M₁ M₂ : graded_module R I} (d : I → I)
--- Π⦃i j : I⦄ (p : d i = j), M₁ i →lm M₂ j
+  (fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ :=
-exit
+graded_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
--- notation M₁ ` →[` d `] ` M₂ := graded_module_hom d M₁ M₂
-variables {d d' d₁ d₂ d₃ : I → I} {f' : M₂ →[d'] M₃} {f : M₁ →[d] M₂} {f₁ : M₁ →[d₁] M₂}
-          {f₂ : M₁ →[d₂] M₂} {f₃ : M₁ →[d₃] M₂}
 
-definition graded_module_hom_ap (f : M₁ →[d] M₂) {i : I} (x : M₁ i) : M₂ (d i) :=
+variables {f' : M₂ →gm M₃} {f : M₁ →gm M₂}
-f idp x
 
-abbreviation gap := @graded_module_hom_ap
+definition graded_hom_compose [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂) : M₁ →gm M₃ :=
+graded_hom.mk (deg f' ∘ deg f) (λi, f' (deg f i) ∘lm f i)
 
-definition is_exact_gmod (f : M₁ →[d] M₂) (f' : M₂ →[d'] M₃) : Type :=
+variable (M)
-Π{i j k} (p : d i = j) (q : d' j = k), is_exact_mod (f p) (f' q)
+definition graded_hom_id [constructor] [refl] : M →gm M :=
+graded_hom.mk id (λi, lmid)
+variable {M}
+
+abbreviation gmid [constructor] := graded_hom_id M
+infixr ` ∘gm `:75 := graded_hom_compose
+
+structure graded_iso (M₁ M₂ : graded_module R I) : Type :=
+  (to_hom : M₁ →gm M₂)
+  (is_equiv_deg : is_equiv (deg to_hom))
+  (is_equiv_to_hom : Π⦃i j⦄ (p : deg to_hom i = j), is_equiv (↘to_hom p))
+
+infix ` ≃gm `:25 := graded_iso
+attribute graded_iso.to_hom [coercion]
+attribute graded_iso.is_equiv_deg [instance] [priority 1010]
+attribute graded_iso._trans_of_to_hom [unfold 5]
+
+definition is_equiv_graded_iso [instance] [priority 1010] (φ : M₁ ≃gm M₂) (i : I) :
+  is_equiv (φ i) :=
+graded_iso.is_equiv_to_hom φ idp
+
+definition isomorphism_of_graded_iso' [constructor] (φ : M₁ ≃gm M₂) {i j : I} (p : deg φ i = j) :
+  M₁ i ≃lm M₂ j :=
+isomorphism.mk (↘φ p) !graded_iso.is_equiv_to_hom
+
+definition isomorphism_of_graded_iso [constructor] (φ : M₁ ≃gm M₂) (i : I) :
+  M₁ i ≃lm M₂ (deg φ i) :=
+isomorphism.mk (φ i) _
+
+definition graded_iso_of_isomorphism [constructor] (d : I ≃ I) (φ : Πi, M₁ i ≃lm M₂ (d i)) :
+  M₁ ≃gm M₂ :=
+begin
+  apply graded_iso.mk (graded_hom.mk d φ), apply to_is_equiv, intro i j p, induction p,
+  exact to_is_equiv (equiv_of_isomorphism (φ i)),
+end
+
+definition graded_iso_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂)
+  : M₁ ≃gm M₂ :=
+graded_iso_of_isomorphism erfl (λi, isomorphism_of_eq (p i))
+
+-- definition graded_iso.MK [constructor] (d : I ≃ I) (fn : Πi, M₁ i →lm M₂ (d i))
+--   : M₁ ≃gm M₂ :=
+-- graded_iso.mk _ _ _ --d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
+
+definition isodeg [unfold 5] (φ : M₁ ≃gm M₂) : I ≃ I :=
+equiv.mk (deg φ) _
+
+definition graded_iso_to_lminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
+graded_hom.mk (deg φ)⁻¹
+  abstract begin
+    intro i, apply to_lminv,
+    apply isomorphism_of_graded_iso' φ,
+    apply to_right_inv (isodeg φ) i
+  end end
+
+definition to_gminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
+graded_hom.mk (deg φ)⁻¹
+  abstract begin
+    intro i, apply isomorphism.to_hom, symmetry,
+    apply isomorphism_of_graded_iso' φ,
+    apply to_right_inv (isodeg φ) i
+  end end
+
+variable (M)
+definition graded_iso.refl [refl] [constructor] : M ≃gm M :=
+graded_iso_of_isomorphism equiv.rfl (λi, isomorphism.rfl)
+variable {M}
+
+definition graded_iso.rfl [refl] [constructor] : M ≃gm M := graded_iso.refl M
+
+definition graded_iso.symm [symm] [constructor] (φ : M₁ ≃gm M₂) : M₂ ≃gm M₁ :=
+graded_iso.mk (to_gminv φ) !is_equiv_inv
+  (λi j p, @is_equiv_compose _ _ _ _ _ !isomorphism.is_equiv_to_hom !is_equiv_cast)
+
+definition graded_iso.trans [trans] [constructor] (φ : M₁ ≃gm M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
+graded_iso_of_isomorphism (isodeg φ ⬝e isodeg ψ)
+  (λi, isomorphism_of_graded_iso φ i ⬝lm isomorphism_of_graded_iso ψ (deg φ i))
+
+definition graded_iso.eq_trans [trans] [constructor]
+   {M₁ M₂ : graded_module R I} {M₃ : graded_module R I} (φ : M₁ ~ M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
+proof graded_iso.trans (graded_iso_of_eq φ) ψ qed
+
+definition graded_iso.trans_eq [trans] [constructor]
+  {M₁ : graded_module R I} {M₂ M₃ : graded_module R I} (φ : M₁ ≃gm M₂) (ψ : M₂ ~ M₃) : M₁ ≃gm M₃ :=
+graded_iso.trans φ (graded_iso_of_eq ψ)
+
+postfix `⁻¹ᵍᵐ`:(max + 1) := graded_iso.symm
+infixl ` ⬝gm `:75 := graded_iso.trans
+infixl ` ⬝gmp `:75 := graded_iso.trans_eq
+infixl ` ⬝pgm `:75 := graded_iso.eq_trans
+
+definition graded_hom_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂)
+  : M₁ →gm M₂ :=
+graded_iso_of_eq p
+
+/- exact couples -/
+
+definition is_exact_gmod (f : M₁ →gm M₂) (f' : M₂ →gm M₃) : Type :=
+Π{i j k} (p : deg f i = j) (q : deg f' j = k), is_exact_mod (↘f p) (↘f' q)
 
 structure exact_couple (M₁ M₂ : graded_module R I) : Type :=
-  (di dj dk : I → I)
+  (i : M₁ →gm M₁) (j : M₁ →gm M₂) (k : M₂ →gm M₁)
-  ( i : M₁ →[di] M₁) (j : M₁ →[dj] M₂) (k : M₂ →[dk] M₁)
+  (exact_ij : is_exact_gmod i j)
-  ( exact_ij : is_exact_gmod i j)
+  (exact_jk : is_exact_gmod j k)
-  ( exact_jk : is_exact_gmod j k)
+  (exact_ki : is_exact_gmod k i)
-  ( exact_ki : is_exact_gmod k i)
 
-  variables {di dj dk : I → I}
+  variables {i : M₁ →gm M₁} {j : M₁ →gm M₂} {k : M₂ →gm M₁}
-            {i : M₁ →[di] M₁} {j : M₁ →[dj] M₂} {k : M₂ →[dk] M₁}
+            (exact_ij : is_exact_gmod i j)
-            ( exact_ij : is_exact_gmod i j)
+            (exact_jk : is_exact_gmod j k)
-            ( exact_jk : is_exact_gmod j k)
+            (exact_ki : is_exact_gmod k i)
-            ( exact_ki : is_exact_gmod k i)
 
   namespace derived_couple
 
-  definition d : graded_module_hom _ M₂ M₂ :=
+  definition d : M₂ →gm M₂ := j ∘gm k
-  _
 
   end derived_couple
 

algebra/module.hlean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Nathaniel Thomas, Jeremy Avigad
+Authors: Nathaniel Thomas, Jeremy Avigad, Floris van Doorn
 
 Modules prod vector spaces over a ring.
 
@@ -221,13 +221,19 @@ end
 
   section
   variables {M M₁ M₂ M₃ : LeftModule R}
+
+  definition LeftModule.struct2 [instance] (M : LeftModule R) : left_module R M :=
+  LeftModule.struct M
+
+  definition homomorphism.mk' [constructor] (φ : M₁ → M₂)
+    (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
+    (q : Π(r : R) x, φ (r • x) = r • φ x) : M₁ →lm M₂ :=
+  homomorphism.mk φ (p, q)
+
   definition to_respect_zero (φ : M₁ →lm M₂) : φ 0 = 0 :=
   respect_zero φ
 
-  definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
+  definition homomorphism_compose [constructor] (f' : M₂ →lm M₃) (f : M₁ →lm M₂) : M₁ →lm M₃ :=
-  @is_exact M₁ M₂ M₃ (homomorphism_fn f) (homomorphism_fn f')
-
-  definition homomorphism_compose (f' : M₂ →lm M₃) (f : M₁ →lm M₂) : M₁ →lm M₃ :=
   homomorphism.mk (f' ∘ f) !is_module_hom_comp
 
   variable (M)
@@ -253,13 +259,6 @@ end
   definition pequiv_of_isomorphism [constructor] (φ : M₁ ≃lm M₂) : M₁ ≃* M₂ :=
   pequiv_of_equiv (equiv_of_isomorphism φ) (to_respect_zero φ)
 
-  definition LeftModule.struct2 [instance] (M : LeftModule R) : left_module R M :=
-  LeftModule.struct M
-
-  definition homomorphism.mk' (φ : M₁ → M₂) (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
-    (q : Π(r : R) x, φ (r • x) = r • φ x) : M₁ →lm M₂ :=
-  homomorphism.mk φ (p, q)
-
   definition isomorphism_of_equiv [constructor] (φ : M₁ ≃ M₂)
     (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
     (q : Πr x, φ (r • x) = r • φ x) : M₁ ≃lm M₂ :=
@@ -281,7 +280,7 @@ end
   --   { apply is_prop.elim}
   -- end
 
-  definition to_ginv [constructor] (φ : M₁ ≃lm M₂) : M₂ →lm M₁ :=
+  definition to_lminv [constructor] (φ : M₁ ≃lm M₂) : M₂ →lm M₁ :=
   homomorphism.mk φ⁻¹
     abstract begin
     split,
@@ -296,8 +295,10 @@ end
   isomorphism.mk lmid !is_equiv_id
   variable {M}
 
+  definition isomorphism.rfl [refl] [constructor] : M ≃lm M := isomorphism.refl M
+
   definition isomorphism.symm [symm] [constructor] (φ : M₁ ≃lm M₂) : M₂ ≃lm M₁ :=
-  isomorphism.mk (to_ginv φ) !is_equiv_inv
+  isomorphism.mk (to_lminv φ) !is_equiv_inv
 
   definition isomorphism.trans [trans] [constructor] (φ : M₁ ≃lm M₂) (ψ : M₂ ≃lm M₃) : M₁ ≃lm M₃ :=
   isomorphism.mk (ψ ∘lm φ) !is_equiv_compose
@@ -319,6 +320,9 @@ end
     : M₁ →lm M₂ :=
   isomorphism_of_eq p
 
+  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