Normed algebras on the real numbers

src/commutative-algebra/algebras-commutative-rings.lagda.md

@@ -71,6 +71,12 @@ module _
     type-algebra-Commutative-Ring
   add-algebra-Commutative-Ring = add-Ab ab-add-algebra-Commutative-Ring
 
+  diff-algebra-Commutative-Ring :
+    type-algebra-Commutative-Ring → type-algebra-Commutative-Ring →
+    type-algebra-Commutative-Ring
+  diff-algebra-Commutative-Ring =
+    right-subtraction-Ab ab-add-algebra-Commutative-Ring
+
   zero-algebra-Commutative-Ring : type-algebra-Commutative-Ring
   zero-algebra-Commutative-Ring = zero-Ab ab-add-algebra-Commutative-Ring
 
@@ -273,6 +279,58 @@ module _
         ( y)
 ```
 
+### Distributivity of multiplication over differences
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Commutative-Ring l1)
+  (A : algebra-Commutative-Ring l2 R)
+  where abstract
+
+  left-distributive-mul-diff-algebra-Commutative-Ring :
+    (x y z : type-algebra-Commutative-Ring R A) →
+    mul-algebra-Commutative-Ring R A
+      ( x)
+      ( diff-algebra-Commutative-Ring R A y z) ＝
+    diff-algebra-Commutative-Ring R A
+      ( mul-algebra-Commutative-Ring R A x y)
+      ( mul-algebra-Commutative-Ring R A x z)
+  left-distributive-mul-diff-algebra-Commutative-Ring x y z =
+    preserves-diff-linear-map-left-module-Commutative-Ring
+      ( R)
+      ( left-module-algebra-Commutative-Ring R A)
+      ( left-module-algebra-Commutative-Ring R A)
+      ( linear-map-ev-left-bilinear-map-left-module-Commutative-Ring
+        ( R)
+        ( left-module-algebra-Commutative-Ring R A)
+        ( left-module-algebra-Commutative-Ring R A)
+        ( left-module-algebra-Commutative-Ring R A)
+        ( bilinear-mul-algebra-Commutative-Ring R A)
+        ( x))
+
+  right-distributive-mul-diff-algebra-Commutative-Ring :
+    (x y z : type-algebra-Commutative-Ring R A) →
+    mul-algebra-Commutative-Ring R A
+      ( diff-algebra-Commutative-Ring R A x y)
+      ( z) ＝
+    diff-algebra-Commutative-Ring R A
+      ( mul-algebra-Commutative-Ring R A x z)
+      ( mul-algebra-Commutative-Ring R A y z)
+  right-distributive-mul-diff-algebra-Commutative-Ring x y z =
+    preserves-diff-linear-map-left-module-Commutative-Ring
+      ( R)
+      ( left-module-algebra-Commutative-Ring R A)
+      ( left-module-algebra-Commutative-Ring R A)
+      ( linear-map-ev-right-bilinear-map-left-module-Commutative-Ring
+        ( R)
+        ( left-module-algebra-Commutative-Ring R A)
+        ( left-module-algebra-Commutative-Ring R A)
+        ( left-module-algebra-Commutative-Ring R A)
+        ( bilinear-mul-algebra-Commutative-Ring R A)
+        ( z))
+```
+
 ### Zero laws of multiplication
 
 ```agda

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

@@ -195,3 +195,21 @@ right-unit-law-comp-hom-Ab :
 right-unit-law-comp-hom-Ab A B =
   right-unit-law-comp-hom-Semigroup (semigroup-Ab A) (semigroup-Ab B)
 ```
+
+### Abelian group homomorphisms preserve subtraction
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Ab l1)
+  (H : Ab l2)
+  (φ : hom-Ab G H)
+  where abstract
+
+  preserves-right-subtraction-hom-Ab :
+    {x y : type-Ab G} →
+    map-hom-Ab G H φ (right-subtraction-Ab G x y) ＝
+    right-subtraction-Ab H (map-hom-Ab G H φ x) (map-hom-Ab G H φ y)
+  preserves-right-subtraction-hom-Ab =
+    preserves-right-div-hom-Group (group-Ab G) (group-Ab H) φ
+```

src/linear-algebra.lagda.md

@@ -60,11 +60,14 @@ open import linear-algebra.linear-maps-left-modules-commutative-rings public
 open import linear-algebra.linear-maps-left-modules-rings public
 open import linear-algebra.linear-maps-vector-spaces public
 open import linear-algebra.linear-spans-left-modules-rings public
+open import linear-algebra.lipschitz-continuity-scalar-multiplication-normed-real-vector-spaces public
+open import linear-algebra.lipschitz-maps-normed-real-vector-spaces public
 open import linear-algebra.matrices public
 open import linear-algebra.matrices-on-rings public
 open import linear-algebra.multiplication-matrices public
 open import linear-algebra.negation-linear-maps-left-modules-rings public
 open import linear-algebra.normed-complex-vector-spaces public
+open import linear-algebra.normed-real-algebras public
 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
@@ -73,6 +76,7 @@ open import linear-algebra.precategory-of-left-modules-rings public
 open import linear-algebra.precategory-of-vector-spaces public
 open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
 open import linear-algebra.rational-modules public
+open import linear-algebra.real-algebras public
 open import linear-algebra.real-inner-product-spaces public
 open import linear-algebra.real-inner-product-spaces-are-normed public
 open import linear-algebra.real-vector-spaces public

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

@@ -66,6 +66,12 @@ module _
   add-left-module-Commutative-Ring =
     add-left-module-Ring (ring-Commutative-Ring R) M
 
+  diff-left-module-Commutative-Ring :
+    (x y : type-left-module-Commutative-Ring) →
+    type-left-module-Commutative-Ring
+  diff-left-module-Commutative-Ring =
+    diff-left-module-Ring (ring-Commutative-Ring R) M
+
   mul-left-module-Commutative-Ring :
     type-Commutative-Ring R → type-left-module-Commutative-Ring →
     type-left-module-Commutative-Ring

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

@@ -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
@@ -90,6 +91,16 @@ module _
     (x y : 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 :
+    (x y : 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 +569,53 @@ module _
     left-module-hom-left-module-Ring R S h (left-module-ring-Ring S)
 ```
 
+### Left distributivity of scalar multiplication over differences
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where abstract
+
+  left-distributive-mul-diff-left-module-Ring :
+    (r : type-Ring R) (x y : type-left-module-Ring R M) →
+    mul-left-module-Ring R M r (diff-left-module-Ring R M x y) ＝
+    diff-left-module-Ring R M
+      ( mul-left-module-Ring R M r x)
+      ( mul-left-module-Ring R M r y)
+  left-distributive-mul-diff-left-module-Ring r x y =
+    ( left-distributive-mul-add-left-module-Ring R M
+      ( r)
+      ( x)
+      ( neg-left-module-Ring R M y)) ∙
+    ( ap-add-left-module-Ring R M
+      ( refl)
+      ( right-negative-law-mul-left-module-Ring R M r y))
+```
+
+### Right distributivity of scalar multiplication over differences
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where abstract
+
+  right-distributive-mul-diff-left-module-Ring :
+    (r s : type-Ring R) (x : type-left-module-Ring R M) →
+    mul-left-module-Ring R M (diff-Ring R r s) x ＝
+    diff-left-module-Ring R M
+      ( mul-left-module-Ring R M r x)
+      ( mul-left-module-Ring R M s x)
+  right-distributive-mul-diff-left-module-Ring r s x =
+    ( right-distributive-mul-add-left-module-Ring R M r (neg-Ring R s) x) ∙
+    ( ap-add-left-module-Ring R M
+      ( refl)
+      ( left-negative-law-mul-left-module-Ring R M s x))
+```
+
 ## See also
 
 - [Left modules over commutative rings](linear-algebra.left-modules-commutative-rings.md)

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

@@ -350,6 +350,28 @@ module _
         ( N)
 ```
 
+### Linear maps preserve differences
+
+```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 abstract
+
+  preserves-diff-linear-map-left-module-Commutative-Ring :
+    {x y : type-left-module-Commutative-Ring R M} →
+    map-linear-map-left-module-Commutative-Ring R M N f
+      ( diff-left-module-Commutative-Ring R M x y) ＝
+    diff-left-module-Commutative-Ring R N
+      ( map-linear-map-left-module-Commutative-Ring R M N f x)
+      ( map-linear-map-left-module-Commutative-Ring R M N f y)
+  preserves-diff-linear-map-left-module-Commutative-Ring =
+    preserves-diff-linear-map-left-module-Ring (ring-Commutative-Ring R) M N f
+```
+
 ## See also
 
 - [Linear maps between left modules over rings](linear-algebra.linear-maps-left-modules-rings.md)

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

@@ -403,6 +403,30 @@ module _
       eq-htpy-linear-map-left-module-Ring R M N _ _ refl-htpy
 ```
 
+### Linear maps preserve differences
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (N : left-module-Ring l3 R)
+  (f : linear-map-left-module-Ring R M N)
+  where abstract
+
+  preserves-diff-linear-map-left-module-Ring :
+    {x y : type-left-module-Ring R M} →
+    map-linear-map-left-module-Ring R M N f (diff-left-module-Ring R M x y) ＝
+    diff-left-module-Ring R N
+      ( map-linear-map-left-module-Ring R M N f x)
+      ( map-linear-map-left-module-Ring R M N f y)
+  preserves-diff-linear-map-left-module-Ring =
+    preserves-right-subtraction-hom-Ab
+      ( ab-left-module-Ring R M)
+      ( ab-left-module-Ring R N)
+      ( hom-ab-linear-map-left-module-Ring R M N f)
+```
+
 ## See also
 
 - [Linear maps between left modules over commutative rings](linear-algebra.linear-maps-left-modules-commutative-rings.md)

src/linear-algebra/lipschitz-continuity-scalar-multiplication-normed-real-vector-spaces.lagda.md

@@ -0,0 +1,99 @@
+# Lipschitz continuity of scalar multiplication in normed real vector spaces
+
+```agda
+module linear-algebra.lipschitz-continuity-scalar-multiplication-normed-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.lipschitz-maps-normed-real-vector-spaces
+open import linear-algebra.normed-real-vector-spaces
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
+open import real-numbers.distance-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.multiplication-real-numbers
+```
+
+</details>
+
+## Idea
+
+Scalar multiplication in
+[normed real vector spaces](linear-algebra.normed-real-vector-spaces.md) is
+[Lipschitz continuous](linear-algebra.lipschitz-maps-normed-real-vector-spaces.md)
+in each argument.
+
+## Properties
+
+### Given a constant `c`, `v ↦ cv` is Lipschitz continuous
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Normed-ℝ-Vector-Space l1 l2)
+  (c : ℝ l1)
+  where abstract
+
+  is-lipschitz-left-mul-Normed-ℝ-Vector-Space :
+    is-lipschitz-map-Normed-ℝ-Vector-Space V V (mul-Normed-ℝ-Vector-Space V c)
+  is-lipschitz-left-mul-Normed-ℝ-Vector-Space =
+    is-lipschitz-real-constant-map-Normed-ℝ-Vector-Space
+      ( V)
+      ( V)
+      ( mul-Normed-ℝ-Vector-Space V c)
+      ( nonnegative-abs-ℝ c)
+      ( λ x y → leq-eq-ℝ (multiplicative-dist-Normed-ℝ-Vector-Space V c x y))
+```
+
+### Given a constant vector `v`, `c ↦ cv` is Lipschitz continuous
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Normed-ℝ-Vector-Space l1 l2)
+  (v : type-Normed-ℝ-Vector-Space V)
+  where abstract
+
+  is-lipschitz-right-mul-Normed-ℝ-Vector-Space :
+    is-lipschitz-map-Normed-ℝ-Vector-Space
+      ( normed-real-vector-space-ℝ l1)
+      ( V)
+      ( λ c → mul-Normed-ℝ-Vector-Space V c v)
+  is-lipschitz-right-mul-Normed-ℝ-Vector-Space =
+    let
+      dist-V = dist-Normed-ℝ-Vector-Space V
+      norm-V = map-norm-Normed-ℝ-Vector-Space V
+      _*V_ = mul-Normed-ℝ-Vector-Space V
+      _-V_ = diff-Normed-ℝ-Vector-Space V
+    in
+      is-lipschitz-real-constant-map-Normed-ℝ-Vector-Space
+        ( normed-real-vector-space-ℝ l1)
+        ( V)
+        ( λ c → mul-Normed-ℝ-Vector-Space V c v)
+        ( nonnegative-norm-Normed-ℝ-Vector-Space V v)
+        ( λ c1 c2 →
+          leq-eq-ℝ
+            ( equational-reasoning
+              dist-V (c1 *V v) (c2 *V v)
+              ＝ norm-V ((c1 -ℝ c2) *V v)
+                by
+                  ap
+                    ( norm-V)
+                    ( inv
+                      ( right-distributive-mul-diff-Normed-ℝ-Vector-Space V
+                        ( c1)
+                        ( c2)
+                        ( v)))
+              ＝ dist-ℝ c1 c2 *ℝ norm-V v
+                by is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space V _ _
+              ＝ norm-V v *ℝ dist-ℝ c1 c2
+                by commutative-mul-ℝ _ _))
+```