From f96c92b72d3f1b5dbea4fa960c4486710acd378f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 30 Mar 2017 15:02:24 -0400 Subject: [PATCH] start on graded R-modules --- algebra/graded.hlean | 70 ++++++++++++++++++++++++++--- algebra/module.hlean | 104 ++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 167 insertions(+), 7 deletions(-) diff --git a/algebra/graded.hlean b/algebra/graded.hlean index 36f84cf..4eee23b 100644 --- a/algebra/graded.hlean +++ b/algebra/graded.hlean @@ -1,7 +1,65 @@ -/- -Copyright (c) 2016 Egbert Rijke. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Egbert Rijke +/- Graded modules -/ -Graded modules and rings. --/ +-- Author: Floris van Doorn + +import ..algebra.module + +open algebra eq left_module pointed function equiv is_equiv is_trunc prod + +namespace left_module + +definition graded (str : Type) (I : Type) : Type := I → str +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 := +mk' :: (d : I → I) + (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] + +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) + +notation M₁ ` →gm ` M₂ := graded_module_hom M₁ M₂ + +-- 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_module_hom_ap (f : M₁ →[d] M₂) {i : I} (x : M₁ i) : M₂ (d i) := +f idp x + +abbreviation gap := @graded_module_hom_ap + +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) + +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) + + 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) + + namespace derived_couple + + definition d : graded_module_hom _ M₂ M₂ := + _ + + end derived_couple + + +end left_module diff --git a/algebra/module.hlean b/algebra/module.hlean index 76e2b43..c51e13f 100644 --- a/algebra/module.hlean +++ b/algebra/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 +open is_trunc pointed function sigma eq algebra prod is_equiv equiv structure has_scalar [class] (F V : Type) := (smul : F → V → V) @@ -219,6 +219,108 @@ section end end + section + variables {M M₁ M₂ M₃ : LeftModule R} + 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₃ := + homomorphism.mk (f' ∘ f) !is_module_hom_comp + + variable (M) + definition homomorphism_id [constructor] [refl] : M →lm M := + homomorphism.mk (@id M) !is_module_hom_id + variable {M} + + abbreviation lmid [constructor] := homomorphism_id M + infixr ` ∘lm `:75 := homomorphism_compose + + structure isomorphism (M₁ M₂ : LeftModule R) := + (to_hom : M₁ →lm M₂) + (is_equiv_to_hom : is_equiv to_hom) + + infix ` ≃lm `:25 := isomorphism + attribute isomorphism.to_hom [coercion] + attribute isomorphism.is_equiv_to_hom [instance] + attribute isomorphism._trans_of_to_hom [unfold 4] + + definition equiv_of_isomorphism [constructor] (φ : M₁ ≃lm M₂) : M₁ ≃ M₂ := + equiv.mk φ !isomorphism.is_equiv_to_hom + + 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₂ := + isomorphism.mk (homomorphism.mk φ (p, q)) !to_is_equiv + + definition isomorphism_of_eq [constructor] {M₁ M₂ : LeftModule R} (p : M₁ = M₂ :> LeftModule R) + : M₁ ≃lm M₂ := + isomorphism_of_equiv (equiv_of_eq (ap LeftModule.carrier p)) + begin intros, induction p, reflexivity end + begin intros, induction p, reflexivity end + + -- definition pequiv_of_isomorphism_of_eq {M₁ M₂ : LeftModule R} (p : M₁ = M₂ :> LeftModule R) : + -- pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_LeftModule p) := + -- begin + -- induction p, + -- apply pequiv_eq, + -- fapply pmap_eq, + -- { intro g, reflexivity}, + -- { apply is_prop.elim} + -- end + + definition to_ginv [constructor] (φ : M₁ ≃lm M₂) : M₂ →lm M₁ := + homomorphism.mk φ⁻¹ + abstract begin + split, + intro g₁ g₂, apply eq_of_fn_eq_fn' φ, + rewrite [respect_add φ, +right_inv φ], + intro r x, apply eq_of_fn_eq_fn' φ, + rewrite [to_respect_smul φ, +right_inv φ], + end end + + variable (M) + definition isomorphism.refl [refl] [constructor] : M ≃lm M := + isomorphism.mk lmid !is_equiv_id + variable {M} + + definition isomorphism.symm [symm] [constructor] (φ : M₁ ≃lm M₂) : M₂ ≃lm M₁ := + isomorphism.mk (to_ginv φ) !is_equiv_inv + + definition isomorphism.trans [trans] [constructor] (φ : M₁ ≃lm M₂) (ψ : M₂ ≃lm M₃) : M₁ ≃lm M₃ := + isomorphism.mk (ψ ∘lm φ) !is_equiv_compose + + definition isomorphism.eq_trans [trans] [constructor] + {M₁ M₂ : LeftModule R} {M₃ : LeftModule R} (φ : M₁ = M₂) (ψ : M₂ ≃lm M₃) : M₁ ≃lm M₃ := + proof isomorphism.trans (isomorphism_of_eq φ) ψ qed + + definition isomorphism.trans_eq [trans] [constructor] + {M₁ : LeftModule R} {M₂ M₃ : LeftModule R} (φ : M₁ ≃lm M₂) (ψ : M₂ = M₃) : M₁ ≃lm M₃ := + isomorphism.trans φ (isomorphism_of_eq ψ) + + postfix `⁻¹ˡᵐ`:(max + 1) := isomorphism.symm + infixl ` ⬝lm `:75 := isomorphism.trans + infixl ` ⬝lmp `:75 := isomorphism.trans_eq + infixl ` ⬝plm `:75 := isomorphism.eq_trans + + definition homomorphism_of_eq [constructor] {M₁ M₂ : LeftModule R} (p : M₁ = M₂ :> LeftModule R) + : M₁ →lm M₂ := + isomorphism_of_eq p + + end + end end left_module