From 038f28524d5102d8c82670e087b6b6d175ce1e03 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= Date: Tue, 11 Jun 2024 18:02:59 -0400 Subject: [PATCH] Added functor instance for lm_carrier. Started on canonical Z-mod. str. for Ab.Grps. --- theories/Algebra/Rings/Z.v | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v index ee0a10a886e..05d881ba30e 100644 --- a/theories/Algebra/Rings/Z.v +++ b/theories/Algebra/Rings/Z.v @@ -1,6 +1,7 @@ Require Import Classes.interfaces.canonical_names. Require Import Algebra.AbGroups. Require Import Algebra.Rings.CRing. +Require Import Algebra.Rings.Module. Require Import Spaces.BinInt Spaces.Pos. Require Import WildCat.Core. @@ -254,3 +255,38 @@ Proof. apply ap. exact IHp. Defined. + +Section Lm_carrierIsEquiv. + + (** lm_carrier is a 1-functor (LeftModule R) -> AbGroup. *) + Global Instance lm_carrieris0fun {R} : Is0Functor (lm_carrier R). + Proof. + snrapply Build_Is0Functor. + intros a b f. + destruct f. + exact lm_homo_map. + Defined. + + Global Instance lm_carrieris1fun {R} : Is1Functor (lm_carrier R). + Proof. + snrapply Build_Is1Functor. + - intros a b f g e. assumption. + - reflexivity. + - reflexivity. + Defined. + (* I think the above should be moved to Module.v, as it is not specifically a property of the integers. *) + + (** Every abelian group admits a canonical left Z-module structure. *) + Definition can_Z : AbGroup -> (LeftModule cring_Z). + Proof. + intros A. snrapply Build_LeftModule. + - assumption. + - snrapply (Build_IsLeftModule _). + + intros n a. exact (ab_mul n a). + + unfold LeftHeteroDistribute. intros n. exact preserves_sg_op. + + unfold RightHeteroDistribute. intros m n a. destruct m, n; simpl. + -- + (* This might be the wrong way to do this. On this path I need to prove that grp_pow respects addition of natural numbers. *) + Admitted. + +End Lm_carrierIsEquiv. \ No newline at end of file