From 20a044b2e413090c4ff4e8274bf5281afbe36af2 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 30 Mar 2017 18:27:09 -0400 Subject: [PATCH] finish categorical structure of graded modules --- algebra/graded.hlean | 172 +++++++++++++++++++++++++++++++++++-------- algebra/module.hlean | 32 ++++---- 2 files changed, 159 insertions(+), 45 deletions(-) diff --git a/algebra/graded.hlean b/algebra/graded.hlean index 4eee23b..30c486a 100644 --- a/algebra/graded.hlean +++ b/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 -attribute graded_module_hom.fn [coercion] +notation M₁ ` →gm ` M₂ := graded_hom M₁ M₂ -definition graded_module_hom.mk {M₁ M₂ : graded_module R I} (d : I → I) - (fn : Πi, M₁ i →lm M₂ (d i)) : graded_module_hom M₁ M₂ := -graded_module_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i) +abbreviation deg [unfold 5] := @graded_hom.d +notation `↘` := graded_hom.fn' -- there is probably a better character for this? -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 := --- Π⦃i j : I⦄ (p : d i = j), M₁ i →lm M₂ j -exit --- 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_hom.mk [constructor] {M₁ M₂ : graded_module R I} (d : I → I) + (fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ := +graded_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i) -definition graded_module_hom_ap (f : M₁ →[d] M₂) {i : I} (x : M₁ i) : M₂ (d i) := -f idp x +variables {f' : M₂ →gm M₃} {f : M₁ →gm M₂} -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 := -Π{i j k} (p : d i = j) (q : d' j = k), is_exact_mod (f p) (f' q) +variable (M) +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₁ →[di] M₁) (j : M₁ →[dj] M₂) (k : M₂ →[dk] M₁) - ( exact_ij : is_exact_gmod i j) - ( exact_jk : is_exact_gmod j k) - ( exact_ki : is_exact_gmod k i) + (i : M₁ →gm M₁) (j : M₁ →gm M₂) (k : M₂ →gm M₁) + (exact_ij : is_exact_gmod i j) + (exact_jk : is_exact_gmod j k) + (exact_ki : is_exact_gmod k i) - variables {di dj dk : I → I} - {i : M₁ →[di] M₁} {j : M₁ →[dj] M₂} {k : M₂ →[dk] M₁} - ( exact_ij : is_exact_gmod i j) - ( exact_jk : is_exact_gmod j k) - ( exact_ki : is_exact_gmod k i) + variables {i : M₁ →gm M₁} {j : M₁ →gm M₂} {k : M₂ →gm M₁} + (exact_ij : is_exact_gmod i j) + (exact_jk : is_exact_gmod j k) + (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 diff --git a/algebra/module.hlean b/algebra/module.hlean index c51e13f..87d198d 100644 --- a/algebra/module.hlean +++ b/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 := - @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₃ := + definition homomorphism_compose [constructor] (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