# Theory Module

Up to index of Isabelle/HOL/HOL-Algebra

theory Module
imports CRing
begin

    (*  Title:      HOL/Algebra/Module.thy
        ID:         $Id: Module.thy,v 1.10 2005/06/17 14:13:05 haftmann Exp $
        Author:     Clemens Ballarin, started 15 April 2003
        Copyright:  Clemens Ballarin
    *)

    header {* Modules over an Abelian Group *}

    theory Module imports CRing begin

    record ('a, 'b) module = "'b ring" +
      smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)

    locale module = cring R + abelian_group M +
      assumes smult_closed [simp, intro]:
          "[| a ∈ carrier R; x ∈ carrier M |] ==> a \<odot>M x ∈ carrier M"
        and smult_l_distr:
          "[| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
          (a ⊕ b) \<odot>M x = a \<odot>M x ⊕M b \<odot>M x"
        and smult_r_distr:
          "[| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
          a \<odot>M (x ⊕M y) = a \<odot>M x ⊕M a \<odot>M y"
        and smult_assoc1:
          "[| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
          (a ⊗ b) \<odot>M x = a \<odot>M (b \<odot>M x)"
        and smult_one [simp]:
          "x ∈ carrier M ==> \<one> \<odot>M x = x"

    locale algebra = module R M + cring M +
      assumes smult_assoc2:
          "[| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
          (a \<odot>M x) ⊗M y = a \<odot>M (x ⊗M y)"

    lemma moduleI:
      includes struct R + struct M
      assumes cring: "cring R"
        and abelian_group: "abelian_group M"
        and smult_closed:
          "!!a x. [| a ∈ carrier R; x ∈ carrier M |] ==> a \<odot>M x ∈ carrier M"
        and smult_l_distr:
          "!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
          (a ⊕ b) \<odot>M x = (a \<odot>M x) ⊕M (b \<odot>M x)"
        and smult_r_distr:
          "!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
          a \<odot>M (x ⊕M y) = (a \<odot>M x) ⊕M (a \<odot>M y)"
        and smult_assoc1:
          "!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
          (a ⊗ b) \<odot>M x = a \<odot>M (b \<odot>M x)"
        and smult_one:
          "!!x. x ∈ carrier M ==> \<one> \<odot>M x = x"
      shows "module R M"
      by (auto intro: module.intro cring.axioms abelian_group.axioms
        module_axioms.intro prems)

    lemma algebraI:
      includes struct R + struct M
      assumes R_cring: "cring R"
        and M_cring: "cring M"
        and smult_closed:
          "!!a x. [| a ∈ carrier R; x ∈ carrier M |] ==> a \<odot>M x ∈ carrier M"
        and smult_l_distr:
          "!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
          (a ⊕ b) \<odot>M x = (a \<odot>M x) ⊕M (b \<odot>M x)"
        and smult_r_distr:
          "!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
          a \<odot>M (x ⊕M y) = (a \<odot>M x) ⊕M (a \<odot>M y)"
        and smult_assoc1:
          "!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
          (a ⊗ b) \<odot>M x = a \<odot>M (b \<odot>M x)"
        and smult_one:
          "!!x. x ∈ carrier M ==> (one R) \<odot>M x = x"
        and smult_assoc2:
          "!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
          (a \<odot>M x) ⊗M y = a \<odot>M (x ⊗M y)"
      shows "algebra R M"
      by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms
        module_axioms.intro prems)

    lemma (in algebra) R_cring:
      "cring R"
      by (rule cring.intro)

    lemma (in algebra) M_cring:
      "cring M"
      by (rule cring.intro)

    lemma (in algebra) module:
      "module R M"
      by (auto intro: moduleI R_cring is_abelian_group
        smult_l_distr smult_r_distr smult_assoc1)

    subsection {* Basic Properties of Algebras *}

    lemma (in algebra) smult_l_null [simp]:
      "x ∈ carrier M ==> \<zero> \<odot>M x = \<zero>M"
    proof -
      assume M: "x ∈ carrier M"
      note facts = M smult_closed
      from facts have "\<zero> \<odot>M x = (\<zero> \<odot>M x ⊕M \<zero> \<odot>M x) ⊕M \<ominus>M (\<zero> \<odot>M x)" by algebra
      also from M have "... = (\<zero> ⊕ \<zero>) \<odot>M x ⊕M \<ominus>M (\<zero> \<odot>M x)"
        by (simp add: smult_l_distr del: R.l_zero R.r_zero)
      also from facts have "... = \<zero>M" by algebra
      finally show ?thesis .
    qed

    lemma (in algebra) smult_r_null [simp]:
      "a ∈ carrier R ==> a \<odot>M \<zero>M = \<zero>M";
    proof -
      assume R: "a ∈ carrier R"
      note facts = R smult_closed
      from facts have "a \<odot>M \<zero>M = (a \<odot>M \<zero>M ⊕M a \<odot>M \<zero>M) ⊕M \<ominus>M (a \<odot>M \<zero>M)"
        by algebra
      also from R have "... = a \<odot>M (\<zero>M ⊕M \<zero>M) ⊕M \<ominus>M (a \<odot>M \<zero>M)"
        by (simp add: smult_r_distr del: M.l_zero M.r_zero)
      also from facts have "... = \<zero>M" by algebra
      finally show ?thesis .
    qed

    lemma (in algebra) smult_l_minus:
      "[| a ∈ carrier R; x ∈ carrier M |] ==> (\<ominus>a) \<odot>M x = \<ominus>M (a \<odot>M x)"
    proof -
      assume RM: "a ∈ carrier R" "x ∈ carrier M"
      note facts = RM smult_closed
      from facts have "(\<ominus>a) \<odot>M x = (\<ominus>a \<odot>M x ⊕M a \<odot>M x) ⊕M \<ominus>M(a \<odot>M x)"
        by algebra
      also from RM have "... = (\<ominus>a ⊕ a) \<odot>M x ⊕M \<ominus>M(a \<odot>M x)"
        by (simp add: smult_l_distr)
      also from facts smult_l_null have "... = \<ominus>M(a \<odot>M x)" by algebra
      finally show ?thesis .
    qed

    lemma (in algebra) smult_r_minus:
      "[| a ∈ carrier R; x ∈ carrier M |] ==> a \<odot>M (\<ominus>Mx) = \<ominus>M (a \<odot>M x)"
    proof -
      assume RM: "a ∈ carrier R" "x ∈ carrier M"
      note facts = RM smult_closed
      from facts have "a \<odot>M (\<ominus>Mx) = (a \<odot>M \<ominus>Mx ⊕M a \<odot>M x) ⊕M \<ominus>M(a \<odot>M x)"
        by algebra
      also from RM have "... = a \<odot>M (\<ominus>Mx ⊕M x) ⊕M \<ominus>M(a \<odot>M x)"
        by (simp add: smult_r_distr)
      also from facts smult_r_null have "... = \<ominus>M(a \<odot>M x)" by algebra
      finally show ?thesis .
    qed

    end

lemma moduleI:

      [| cring R; abelian_group M;
         !!a x. [| a ∈ carrier R; x ∈ carrier M |] ==> a \<odot>M x ∈ carrier M;
         !!a b x.
            [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |]
            ==> (a ⊕R b) \<odot>M x = a \<odot>M x ⊕M b \<odot>M x;
         !!a x y.
            [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |]
            ==> a \<odot>M (x ⊕M y) = a \<odot>M x ⊕M a \<odot>M y;
         !!a b x.
            [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |]
            ==> a ⊗R b \<odot>M x = a \<odot>M (b \<odot>M x);
         !!x. x ∈ carrier M ==> \<one>R \<odot>M x = x |]
      ==> module R M

lemma algebraI:

      [| cring R; cring M;
         !!a x. [| a ∈ carrier R; x ∈ carrier M |] ==> a \<odot>M x ∈ carrier M;
         !!a b x.
            [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |]
            ==> (a ⊕R b) \<odot>M x = a \<odot>M x ⊕M b \<odot>M x;
         !!a x y.
            [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |]
            ==> a \<odot>M (x ⊕M y) = a \<odot>M x ⊕M a \<odot>M y;
         !!a b x.
            [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |]
            ==> a ⊗R b \<odot>M x = a \<odot>M (b \<odot>M x);
         !!x. x ∈ carrier M ==> \<one>R \<odot>M x = x;
         !!a x y.
            [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |]
            ==> a \<odot>M x ⊗M y = a \<odot>M (x ⊗M y) |]
      ==> algebra R M

lemma R_cring:

      algebra R M ==> cring R

lemma M_cring:

      algebra R M ==> cring M

lemma module:

      algebra R M ==> module R M

### Basic Properties of Algebras

lemma smult_l_null:

      [| algebra R M; x ∈ carrier M |] ==> \<zero>R \<odot>M x = \<zero>M

lemma smult_r_null:

      [| algebra R M; a ∈ carrier R |] ==> a \<odot>M \<zero>M = \<zero>M

lemma smult_l_minus:

      [| algebra R M; a ∈ carrier R; x ∈ carrier M |]
      ==> \<ominus>R a \<odot>M x = \<ominus>M (a \<odot>M x)

lemma smult_r_minus:

      [| algebra R M; a ∈ carrier R; x ∈ carrier M |]
      ==> a \<odot>M \<ominus>M x = \<ominus>M (a \<odot>M x)