Eigenvalues, eigenvectors, and eigenspaces of linear endomaps #1765

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 47 commits into UniMath:master from lowasser:eigenvectors

src/linear-algebra.lagda.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -5,6 +5,7 @@ @@
     ```agda
     module linear-algebra where
+    open import linear-algebra.addition-linear-maps-left-modules-commutative-rings public
     open import linear-algebra.addition-linear-maps-left-modules-rings public
     open import linear-algebra.bilinear-forms-real-vector-spaces public
     open import linear-algebra.cauchy-schwarz-inequality-complex-inner-product-spaces public
@@ Expand All / @@ -17,6 +18,8 @@ open import linear-algebra.constant-tuples public @@
     open import linear-algebra.dependent-products-left-modules-commutative-rings public
     open import linear-algebra.dependent-products-left-modules-rings public
     open import linear-algebra.diagonal-matrices-on-rings public
+    open import linear-algebra.difference-linear-maps-left-modules-commutative-rings public
+    open import linear-algebra.difference-linear-maps-left-modules-rings public
     open import linear-algebra.dot-product-standard-euclidean-vector-spaces public
     open import linear-algebra.finite-sequences-in-abelian-groups public
     open import linear-algebra.finite-sequences-in-commutative-monoids public
@@ Expand All / @@ -30,6 +33,7 @@ open import linear-algebra.finite-sequences-in-rings public @@
     open import linear-algebra.finite-sequences-in-semigroups public
     open import linear-algebra.finite-sequences-in-semirings public
     open import linear-algebra.functoriality-matrices public
+    open import linear-algebra.kernels-linear-maps-left-modules-commutative-rings public
     open import linear-algebra.kernels-linear-maps-left-modules-rings public
     open import linear-algebra.kernels-linear-maps-vector-spaces public
     open import linear-algebra.large-left-modules-large-rings public
@@ Expand Down @@

src/linear-algebra/addition-linear-maps-left-modules-commutative-rings.lagda.md

-Original file line number
+Diff line change
@@ -0,0 +1,77 @@
+    # Addition of linear maps between left modules over commutative rings
+    ```agda
+    module linear-algebra.addition-linear-maps-left-modules-commutative-rings where
+    ```
+    <details><summary>Imports</summary>
+    ```agda
+    open import commutative-algebra.commutative-rings
+    open import foundation.action-on-identifications-binary-functions
+    open import foundation.dependent-pair-types
+    open import foundation.identity-types
+    open import foundation.universe-levels
+    open import group-theory.abelian-groups
+    open import group-theory.function-abelian-groups
+    open import group-theory.subgroups-abelian-groups
+    open import linear-algebra.addition-linear-maps-left-modules-rings
+    open import linear-algebra.left-modules-commutative-rings
+    open import linear-algebra.linear-maps-left-modules-commutative-rings
+    ```
+    </details>
+    ## Idea
+    Given two
+    [linear maps](linear-algebra.linear-maps-left-modules-commutative-rings.md) `f`
+    and `g` from a [left module](linear-algebra.left-modules-commutative-rings.md)
+    `M` over a [commutative ring](commutative-algebra.commutative-rings.md) `R` to a
+    left module `N` over `R`, then the map `x ↦ f x + g x` is a linear map.
+    ## Definition
+    ```agda
+    module _
+      {l1 l2 l3 : Level}
+      (R : Commutative-Ring l1)
+      (M : left-module-Commutative-Ring l2 R)
+      (N : left-module-Commutative-Ring l3 R)
+      (f g : linear-map-left-module-Commutative-Ring R M N)
+      where
+      add-linear-map-left-module-Commutative-Ring :
+        linear-map-left-module-Commutative-Ring R M N
+      add-linear-map-left-module-Commutative-Ring =
+        add-linear-map-left-module-Ring (ring-Commutative-Ring R) M N f g
+    ```
+    ## Properties
+    ### Linear maps form an Abelian group under addition and negation
+    ```agda
+    module _
+      {l1 l2 l3 : Level}
+      (R : Commutative-Ring l1)
+      (M : left-module-Commutative-Ring l2 R)
+      (N : left-module-Commutative-Ring l3 R)
+      where
+      subgroup-add-linear-map-left-module-Commutative-Ring :
+        Subgroup-Ab
+          ( l1 ⊔ l2 ⊔ l3)
+          ( function-Ab
+            ( ab-left-module-Commutative-Ring R N)
+            ( type-left-module-Commutative-Ring R M))
+      subgroup-add-linear-map-left-module-Commutative-Ring =
+        subgroup-add-linear-map-left-module-Ring (ring-Commutative-Ring R) M N
+      ab-add-linear-map-left-module-Commutative-Ring : Ab (l1 ⊔ l2 ⊔ l3)
+      ab-add-linear-map-left-module-Commutative-Ring =
+        ab-add-linear-map-left-module-Ring (ring-Commutative-Ring R) M N
+    ```

src/linear-algebra/difference-linear-maps-left-modules-commutative-rings.lagda.md

-Original file line number
+Diff line change
@@ -0,0 +1,48 @@
+    # The difference of linear maps between left modules over commutative rings
+    ```agda
+    module linear-algebra.difference-linear-maps-left-modules-commutative-rings where
+    ```
+    <details><summary>Imports</summary>
+    ```agda
+    open import commutative-algebra.commutative-rings
+    open import foundation.universe-levels
+    open import group-theory.abelian-groups
+    open import linear-algebra.addition-linear-maps-left-modules-commutative-rings
+    open import linear-algebra.left-modules-commutative-rings
+    open import linear-algebra.linear-maps-left-modules-commutative-rings
+    ```
+    </details>
+    ## Idea
+    The
+    {{#concept "difference" Disambiguation="of linear maps between left modules over rings" Agda=diff-linear-map-left-module-Commutative-Ring}}
+    of two [linear maps](linear-algebra.linear-maps-left-modules-rings.md) `f` and
+    `g` between two [left modules](linear-algebra.left-modules-rings.md) over a
+    [commutative ring](commutative-algebra.commutative-rings.md) is the linear map
+    `x ↦ f x - g x`.
+    ## Definition
+    ```agda
+    module _
+      {l1 l2 l3 : Level}
+      (R : Commutative-Ring l1)
+      (M : left-module-Commutative-Ring l2 R)
+      (N : left-module-Commutative-Ring l3 R)
+      where
+      diff-linear-map-left-module-Commutative-Ring :
+        linear-map-left-module-Commutative-Ring R M N →
+        linear-map-left-module-Commutative-Ring R M N →
+        linear-map-left-module-Commutative-Ring R M N
+      diff-linear-map-left-module-Commutative-Ring =
+        right-subtraction-Ab (ab-add-linear-map-left-module-Commutative-Ring R M N)
+    ```

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

-Original file line number
+Diff line change
@@ -0,0 +1,47 @@
+    # The difference of linear maps between left modules over rings
+    ```agda
+    module linear-algebra.difference-linear-maps-left-modules-rings where
+    ```
+    <details><summary>Imports</summary>
+    ```agda
+    open import foundation.universe-levels
+    open import group-theory.abelian-groups
+    open import linear-algebra.addition-linear-maps-left-modules-rings
+    open import linear-algebra.left-modules-rings
+    open import linear-algebra.linear-maps-left-modules-rings
+    open import ring-theory.rings
+    ```
+    </details>
+    ## Idea
+    The
+    {{#concept "difference" Disambiguation="of linear maps between left modules over rings" Agda=diff-linear-map-left-module-Ring}}
+    of two [linear maps](linear-algebra.linear-maps-left-modules-rings.md) `f` and
+    `g` between two [left modules](linear-algebra.left-modules-rings.md) over a
+    [ring](ring-theory.rings.md) is the linear map `x ↦ f x - g x`.
+    ## Definition
+    ```agda
+    module _
+      {l1 l2 l3 : Level}
+      (R : Ring l1)
+      (M : left-module-Ring l2 R)
+      (N : left-module-Ring l3 R)
+      where
+      diff-linear-map-left-module-Ring :
+        linear-map-left-module-Ring R M N →
+        linear-map-left-module-Ring R M N →
+        linear-map-left-module-Ring R M N
+      diff-linear-map-left-module-Ring =
+        right-subtraction-Ab (ab-add-linear-map-left-module-Ring R M N)
+    ```

src/linear-algebra/kernels-linear-maps-left-modules-commutative-rings.lagda.md

-Original file line number
+Diff line change
@@ -0,0 +1,69 @@
+    # Kernels of linear maps between left modules over commutative rings
+    ```agda
+    module linear-algebra.kernels-linear-maps-left-modules-commutative-rings where
+    ```
+    <details><summary>Imports</summary>
+    ```agda
+    open import commutative-algebra.commutative-rings
+    open import foundation.action-on-identifications-functions
+    open import foundation.dependent-pair-types
+    open import foundation.identity-types
+    open import foundation.subtypes
+    open import foundation.universe-levels
+    open import linear-algebra.kernels-linear-maps-left-modules-rings
+    open import linear-algebra.left-modules-commutative-rings
+    open import linear-algebra.left-submodules-commutative-rings
+    open import linear-algebra.linear-maps-left-modules-commutative-rings
+    open import linear-algebra.subsets-left-modules-commutative-rings
+    ```
+    </details>
+    ## Idea
+    The
+    {{#concept "kernel" WDID=Q2914509 WD="kernel" Disambiguation="of a linear map between left modules over commutative rings" Agda=kernel-linear-map-left-module-Commutative-Ring}}
+    of a [linear map](linear-algebra.linear-maps-left-modules-commutative-rings.md)
+    from a [left module](linear-algebra.left-modules-commutative-rings.md) over a
+    [commutative ring](commutative-algebra.commutative-rings.md) to another left
+    module over the same ring is the preimage of zero under the linear map.
+    ## Definition
+    ```agda
+    module _
+      {l1 l2 l3 : Level}
+      (R : Commutative-Ring l1)
+      (M : left-module-Commutative-Ring l2 R)
+      (N : left-module-Commutative-Ring l3 R)
+      (f : linear-map-left-module-Commutative-Ring R M N)
+      where
+      subset-kernel-linear-map-left-module-Commutative-Ring :
+        subset-left-module-Commutative-Ring l3 R M
+      subset-kernel-linear-map-left-module-Commutative-Ring =
+        subset-kernel-linear-map-left-module-Ring (ring-Commutative-Ring R) M N f
+      kernel-linear-map-left-module-Commutative-Ring :
+        left-submodule-Commutative-Ring l3 R M
+      kernel-linear-map-left-module-Commutative-Ring =
+        kernel-linear-map-left-module-Ring
+          ( ring-Commutative-Ring R)
+          ( M)
+          ( N)
+          ( f)
+      left-module-kernel-linear-map-left-module-Commutative-Ring :
+        left-module-Commutative-Ring (l2 ⊔ l3) R
+      left-module-kernel-linear-map-left-module-Commutative-Ring =
+        left-module-kernel-linear-map-left-module-Ring
+          ( ring-Commutative-Ring R)
+          ( M)
+          ( N)
+          ( f)
+    ```

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

-Original file line number
+Diff line change
@@ Expand Up / @@ -10,6 +10,7 @@ module linear-algebra.left-submodules-commutative-rings where @@
     open import commutative-algebra.commutative-rings
     open import foundation.propositions
+    open import foundation.subtypes
     open import foundation.universe-levels
     open import linear-algebra.left-modules-commutative-rings
@@ Expand Down Expand Up / @@ -63,4 +64,20 @@ module _ @@
         left-module-Commutative-Ring (l2 ⊔ l3) R
       left-module-left-submodule-Commutative-Ring =
         left-module-left-submodule-Ring (ring-Commutative-Ring R) M S
+      subset-left-submodule-Commutative-Ring :
+        subset-left-module-Commutative-Ring l3 R M
+      subset-left-submodule-Commutative-Ring =
+        subset-left-submodule-Ring (ring-Commutative-Ring R) M S
+      is-in-left-submodule-Commutative-Ring :
+        type-left-module-Commutative-Ring R M → UU l3
+      is-in-left-submodule-Commutative-Ring =
+        is-in-subtype subset-left-submodule-Commutative-Ring
+      contains-zero-left-submodule-Commutative-Ring :
+        is-in-left-submodule-Commutative-Ring
+          ( zero-left-module-Commutative-Ring R M)
+      contains-zero-left-submodule-Commutative-Ring =
+        contains-zero-left-submodule-Ring (ring-Commutative-Ring R) M S
     ```

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

-Original file line number
+Diff line change
@@ Expand Up / @@ -79,6 +79,24 @@ module _ @@
         is-linear-endo-left-module-Commutative-Ring R M
           ( map-linear-endo-left-module-Commutative-Ring)
       is-linear-endo-map-linear-endo-left-module-Commutative-Ring = pr2 f
+      is-additive-map-linear-endo-left-module-Commutative-Ring :
+        is-additive-map-left-module-Commutative-Ring
+          ( R)
+          ( M)
+          ( M)
+          ( map-linear-endo-left-module-Commutative-Ring)
+      is-additive-map-linear-endo-left-module-Commutative-Ring =
+        is-additive-map-linear-map-left-module-Commutative-Ring R M M f
+      is-homogeneous-map-linear-endo-left-module-Commutative-Ring :
+        is-homogeneous-map-left-module-Commutative-Ring
+          ( R)
+          ( M)
+          ( M)
+          ( map-linear-endo-left-module-Commutative-Ring)
+      is-homogeneous-map-linear-endo-left-module-Commutative-Ring =
+        is-homogeneous-map-linear-map-left-module-Commutative-Ring R M M f
     ```
     ## Properties
@@ Expand Down @@

...gebra/scalar-multiplication-linear-maps-left-modules-commutative-rings.lagda.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -30,7 +30,7 @@ linear map. @@
     ## Definition
-    ### The linear transformation of scalar multiplication
+    ### The linear endomap of scalar multiplication
     ```agda
     module _
@@ Expand Down @@

src/linear-algebra/scalar-multiplication-linear-maps-vector-spaces.lagda.md

-Original file line number
+Diff line change
@@ Expand Up @@
     ## Definition
-    ### The linear transformation of scalar multiplication
+    ### The linear endomap of scalar multiplication
     ```agda
     module _
@@ Expand Down @@

src/spectral-theory.lagda.md

-Original file line number
+Diff line change
@@ -0,0 +1,19 @@
+    # Spectral theory
+    ## Idea
+    {{#concept "Spectral theory" WDID=Q2409122 WD="spectral theory"}} studies
+    [eigenvectors and eigenvalues](spectral-theory.eigenvalues-eigenvectors-linear-endomaps-vector-spaces.md)
+    of linear operators and their generalizations to broader notions of operators on
+    different kinds of spaces.
+    ## Modules in the spectral theory namespace
+    ```agda
+    module spectral-theory where
+    open import spectral-theory.eigenmodules-linear-endomaps-left-modules-commutative-rings public
+    open import spectral-theory.eigenspaces-linear-endomaps-vector-spaces public
+    open import spectral-theory.eigenvalues-eigenelements-linear-endomaps-left-modules-commutative-rings public
+    open import spectral-theory.eigenvalues-eigenvectors-linear-endomaps-vector-spaces public
+    ```

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Eigenvalues, eigenvectors, and eigenspaces of linear endomaps #1765

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Eigenvalues, eigenvectors, and eigenspaces of linear endomaps #1765

Are you sure you want to change the base?

Uh oh!

Eigenvalues, eigenvectors, and eigenspaces of linear endomaps #1765

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!