Quotients of modules and vector spaces #1808

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

lowasser wants to merge 33 commits into UniMath:master from lowasser:quotient-module

src/group-theory/quotients-abelian-groups.lagda.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -37,11 +37,14 @@ open import group-theory.subgroups-abelian-groups @@
     ## Idea
-    Given a subgroup `B` of an abelian group `A`, the quotient group is an abelian
-    group `A/B` equipped with a group homomorphism `q : A → A/B` such that
-    `H ⊆ ker q`, and such that `q` satisfies the universal abelian group with the
-    property that any group homomorphism `f : A → C` such that `B ⊆ ker f` extends
-    uniquely along `q` to a group homomorphism `A/B → C`.
+    Given a [subgroup](group-theory.subgroups-abelian-groups.md) `B` of an
+    [abelian group](group-theory.abelian-groups.md) `A`, the
+    {{#concept "quotient group" Disambiguation="of an abelian group and a subgroup" Agda=quotient-Ab}}
+    is an abelian group `A/B` equipped with a
+    [group homomorphism](group-theory.homomorphisms-abelian-groups.md) `q : A → A/B`
+    such that `H ⊆ ker q`, and such that `q` satisfies the universal property of the
+    quotient group that any group homomorphism `f : A → C` such that `B ⊆ ker f`
+    extends uniquely along `q` to a group homomorphism `A/B → C`.
     ## Definitions
@@ Expand Down @@

src/linear-algebra.lagda.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -54,6 +54,8 @@ open import linear-algebra.normed-real-vector-spaces public @@
     open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces public
     open import linear-algebra.orthogonality-real-inner-product-spaces public
     open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
+    open import linear-algebra.quotients-left-modules-rings public
+    open import linear-algebra.quotients-vector-spaces public
     open import linear-algebra.rational-modules public
     open import linear-algebra.real-inner-product-spaces public
     open import linear-algebra.real-inner-product-spaces-are-normed public
@@ Expand Down @@

src/linear-algebra/left-modules-rings.lagda.md

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -9,6 +9,7 @@ module linear-algebra.left-modules-rings where
  
    ```agda

    open import elementary-number-theory.ring-of-integers

    open import foundation.action-on-identifications-binary-functions

    open import foundation.action-on-identifications-functions

    open import foundation.dependent-pair-types

    open import foundation.equality-dependent-pair-types

    @@ -87,9 +88,22 @@ module _
  
      is-set-type-left-module-Ring = pr2 set-left-module-Ring

      add-left-module-Ring :

        (x y : type-left-module-Ring) → type-left-module-Ring

        type-left-module-Ring → type-left-module-Ring → type-left-module-Ring

      add-left-module-Ring = add-Ab ab-left-module-Ring

      ap-add-left-module-Ring :

        {x x' : type-left-module-Ring} →

        x ＝ x' →

        {y y' : type-left-module-Ring} →

        y ＝ y' →

        add-left-module-Ring x y ＝ add-left-module-Ring x' y'

      ap-add-left-module-Ring =

        ap-binary add-left-module-Ring

      diff-left-module-Ring :

        type-left-module-Ring → type-left-module-Ring → type-left-module-Ring

      diff-left-module-Ring = right-subtraction-Ab ab-left-module-Ring

      zero-left-module-Ring : type-left-module-Ring

      zero-left-module-Ring = zero-Ab ab-left-module-Ring

    @@ -558,6 +572,40 @@ module _
  
        left-module-hom-left-module-Ring R S h (left-module-ring-Ring S)

    ```

    ### Negation is distributive over subtraction

    ```agda

    module _

      {l1 l2 : Level} (R : Ring l1) (M : left-module-Ring l2 R)

      where

      abstract

        distributive-neg-diff-left-module-Ring :

          (a b : type-left-module-Ring R M) →

          neg-left-module-Ring R M (diff-left-module-Ring R M a b) ＝

          diff-left-module-Ring R M b a

        distributive-neg-diff-left-module-Ring =

          neg-right-subtraction-Ab (ab-left-module-Ring R M)

    ```

    ### `(a - b) + (b - c) = a - c`

    ```agda

    module _

      {l1 l2 : Level} (R : Ring l1) (M : left-module-Ring l2 R)

      where

      abstract

        add-diff-left-module-Ring :

          (a b c : type-left-module-Ring R M) →

          add-left-module-Ring R M

            ( diff-left-module-Ring R M a b)

            ( diff-left-module-Ring R M b c) ＝

          diff-left-module-Ring R M a c

        add-diff-left-module-Ring =

          add-right-subtraction-Ab (ab-left-module-Ring R M)

    ```

    ## See also

    - [Left modules over commutative rings](linear-algebra.left-modules-commutative-rings.md)

src/linear-algebra/left-submodules-rings.lagda.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -28,6 +28,7 @@ open import group-theory.homomorphisms-abelian-groups @@
     open import group-theory.homomorphisms-semigroups
     open import group-theory.monoids
     open import group-theory.semigroups
+    open import group-theory.subgroups-abelian-groups
     open import linear-algebra.left-modules-rings
     open import linear-algebra.subsets-left-modules-rings
@@ Expand Down Expand Up / @@ -94,6 +95,10 @@ module _ @@
       subset-left-submodule-Ring =
         inclusion-subtype (is-left-submodule-prop-Ring R M) N
+      is-in-left-submodule-Ring : type-left-module-Ring R M → UU l3
+      is-in-left-submodule-Ring =
+        is-in-subtype subset-left-submodule-Ring
       type-left-submodule-Ring : UU (l2 ⊔ l3)
       type-left-submodule-Ring = type-subtype subset-left-submodule-Ring
@@ Expand Down Expand Up / @@ -353,6 +358,13 @@ module _ @@
       pr1 ab-left-submodule-Ring = group-left-submodule-Ring
       pr2 ab-left-submodule-Ring = commutative-add-left-submodule-Ring
+      subgroup-ab-left-submodule-Ring : Subgroup-Ab l3 (ab-left-module-Ring R M)
+      subgroup-ab-left-submodule-Ring =
+        ( subset-left-submodule-Ring R M N ,
+          contains-zero-left-submodule-Ring R M N ,
+          is-closed-under-addition-left-submodule-Ring R M N _ _ ,
+          is-closed-under-negation-left-submodule-Ring R M N _)
       endomorphism-ring-left-submodule-Ring : Ring (l2 ⊔ l3)
       endomorphism-ring-left-submodule-Ring =
         endomorphism-ring-Ab ab-left-submodule-Ring
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Quotients of modules and vector spaces #1808

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Quotients of modules and vector spaces #1808

Are you sure you want to change the base?

Uh oh!

Quotients of modules and vector spaces #1808

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!