Multiplication by diagonal matrices

src/foundation.lagda.md

@@ -452,6 +452,7 @@ open import foundation.similarity-preserving-maps-large-similarity-relations pub
 open import foundation.similarity-subtypes public
 open import foundation.singleton-induction public
 open import foundation.singleton-subtypes public
+open import foundation.singleton-subtypes-discrete-types public
 open import foundation.slice public
 open import foundation.small-maps public
 open import foundation.small-types public

src/foundation/singleton-subtypes-discrete-types.lagda.md

@@ -0,0 +1,89 @@
+# Singleton subtypes of discrete types
+
+```agda
+module foundation.singleton-subtypes-discrete-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
+open import foundation.decidable-subtypes
+open import foundation.dependent-pair-types
+open import foundation.discrete-types
+open import foundation.functoriality-coproduct-types
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.singleton-subtypes
+open import foundation.universe-levels
+
+open import foundation-core.subtypes
+open import foundation-core.transport-along-identifications
+```
+
+</details>
+
+## Idea
+
+[Singleton subtypes](foundation.singleton-subtypes.md) on
+[discrete types](foundation.discrete-types.md) are
+[decidable subtypes](foundation.decidable-subtypes.md).
+
+## Properties
+
+### Any singleton subtype of a discrete type is decidable
+
+```agda
+module _
+  {l1 l2 : Level}
+  (XD@(X , decide-eq-X) : Discrete-Type l1)
+  (S : subtype l2 X)
+  (((x , x∈S) , is-center-x) : is-singleton-subtype S)
+  where
+
+  is-decidable-is-singleton-subtype-Discrete-Type : is-decidable-subtype S
+  is-decidable-is-singleton-subtype-Discrete-Type y =
+    map-coproduct
+      ( λ x=y → tr (is-in-subtype S) x=y x∈S)
+      ( λ x≠y y∈S → x≠y (ap (inclusion-subtype S) (is-center-x (y , y∈S))))
+      ( decide-eq-X x y)
+```
+
+### The standard decidable singleton subtype associated with an element of a discrete type
+
+```agda
+module _
+  {l : Level}
+  (XD@(X , decide-eq-X) : Discrete-Type l)
+  where
+
+  decidable-standard-singleton-subtype-Discrete-Type :
+    X → decidable-subtype l X
+  decidable-standard-singleton-subtype-Discrete-Type y x =
+    ( x ＝ y ,
+      is-set-type-Discrete-Type XD x y ,
+      decide-eq-X x y)
+```
+
+### The standard decidable singleton subtype is contractible
+
+```agda
+module _
+  {l : Level}
+  (XD@(X , decide-eq-X) : Discrete-Type l)
+  (x : X)
+  where
+
+  is-contr-type-decidable-standard-singleton-subtype-Discrete-Type :
+    is-contr
+      ( type-decidable-subtype
+        ( decidable-standard-singleton-subtype-Discrete-Type XD x))
+  is-contr-type-decidable-standard-singleton-subtype-Discrete-Type =
+    ( (x , refl) ,
+      λ (y , x=y) →
+        eq-type-subtype
+          ( subtype-decidable-subtype
+            ( decidable-standard-singleton-subtype-Discrete-Type XD x))
+          ( inv x=y))
+```

src/group-theory/invertible-elements-monoids.lagda.md

@@ -168,6 +168,9 @@ module _
     is-invertible-element-Monoid M x
   pr2 (is-invertible-element-prop-Monoid x) =
     is-prop-is-invertible-element-Monoid x
+
+  invertible-element-Monoid : UU l
+  invertible-element-Monoid = type-subtype is-invertible-element-prop-Monoid
 ```
 
 ### Inverses are left/right inverses
@@ -292,6 +295,11 @@ module _
     left-unit-law-mul-Monoid M (unit-Monoid M)
   pr2 (pr2 is-invertible-element-unit-Monoid) =
     left-unit-law-mul-Monoid M (unit-Monoid M)
+
+  invertible-element-unit-Monoid :
+    invertible-element-Monoid M
+  invertible-element-unit-Monoid =
+    ( unit-Monoid M , is-invertible-element-unit-Monoid)
 ```
 
 ### Invertible elements are closed under multiplication
@@ -350,6 +358,14 @@ module _
       ( is-left-invertible-element-mul-Monoid x y
         ( is-left-invertible-is-invertible-element-Monoid M x H)
         ( is-left-invertible-is-invertible-element-Monoid M y K))
+
+  mul-invertible-element-Monoid :
+    invertible-element-Monoid M →
+    invertible-element-Monoid M →
+    invertible-element-Monoid M
+  mul-invertible-element-Monoid (x , is-inv-x) (y , is-inv-y) =
+    ( mul-Monoid M x y ,
+      is-invertible-element-mul-Monoid x y is-inv-x is-inv-y)
 ```
 
 ### The inverse of an invertible element is invertible
@@ -367,6 +383,12 @@ module _
     is-left-inverse-inv-is-invertible-element-Monoid M H
   pr2 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) =
     is-right-inverse-inv-is-invertible-element-Monoid M H
+
+  invertible-element-inv-invertible-element-Monoid :
+    invertible-element-Monoid M → invertible-element-Monoid M
+  invertible-element-inv-invertible-element-Monoid (x , is-invertible-x) =
+    ( inv-is-invertible-element-Monoid M is-invertible-x ,
+      is-invertible-element-inv-is-invertible-element-Monoid is-invertible-x)
 ```
 
 ### An element is invertible if and only if multiplying by it is an equivalence
@@ -400,25 +422,27 @@ module _
   inv-is-invertible-element-is-equiv-mul-Monoid H =
     map-inv-is-equiv H (unit-Monoid M)
 
-  is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
-    (H : is-equiv (mul-Monoid M x)) →
-    mul-Monoid M x (inv-is-invertible-element-is-equiv-mul-Monoid H) ＝
-    unit-Monoid M
-  is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
-    is-section-map-inv-is-equiv H (unit-Monoid M)
-
-  is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
-    (H : is-equiv (mul-Monoid M x)) →
-    mul-Monoid M (inv-is-invertible-element-is-equiv-mul-Monoid H) x ＝
-    unit-Monoid M
-  is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
-    is-injective-is-equiv H
-      ( ( inv (associative-mul-Monoid M _ _ _)) ∙
-        ( ap
-          ( mul-Monoid' M x)
-          ( is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H)) ∙
-        ( left-unit-law-mul-Monoid M x) ∙
-        ( inv (right-unit-law-mul-Monoid M x)))
+  abstract
+    is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
+      (H : is-equiv (mul-Monoid M x)) →
+      mul-Monoid M x (inv-is-invertible-element-is-equiv-mul-Monoid H) ＝
+      unit-Monoid M
+    is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
+      is-section-map-inv-is-equiv H (unit-Monoid M)
+
+    is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
+      (H : is-equiv (mul-Monoid M x)) →
+      mul-Monoid M (inv-is-invertible-element-is-equiv-mul-Monoid H) x ＝
+      unit-Monoid M
+    is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
+      is-injective-is-equiv H
+        ( ( inv (associative-mul-Monoid M _ _ _)) ∙
+          ( ap
+            ( mul-Monoid' M x)
+            ( is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid
+              ( H))) ∙
+          ( left-unit-law-mul-Monoid M x) ∙
+          ( inv (right-unit-law-mul-Monoid M x)))
 
   is-invertible-element-is-equiv-mul-Monoid :
     is-equiv (mul-Monoid M x) → is-invertible-element-Monoid M x
@@ -434,25 +458,26 @@ module _
   left-div-is-invertible-element-Monoid H =
     mul-Monoid M (inv-is-invertible-element-Monoid M H)
 
-  is-section-left-div-is-invertible-element-Monoid :
-    (H : is-invertible-element-Monoid M x) →
-    mul-Monoid M x ∘ left-div-is-invertible-element-Monoid H ~ id
-  is-section-left-div-is-invertible-element-Monoid H y =
-    ( inv (associative-mul-Monoid M _ _ _)) ∙
-    ( ap
-      ( mul-Monoid' M y)
-      ( is-right-inverse-inv-is-invertible-element-Monoid M H)) ∙
-    ( left-unit-law-mul-Monoid M y)
-
-  is-retraction-left-div-is-invertible-element-Monoid :
-    (H : is-invertible-element-Monoid M x) →
-    left-div-is-invertible-element-Monoid H ∘ mul-Monoid M x ~ id
-  is-retraction-left-div-is-invertible-element-Monoid H y =
-    ( inv (associative-mul-Monoid M _ _ _)) ∙
-    ( ap
-      ( mul-Monoid' M y)
-      ( is-left-inverse-inv-is-invertible-element-Monoid M H)) ∙
-    ( left-unit-law-mul-Monoid M y)
+  abstract
+    is-section-left-div-is-invertible-element-Monoid :
+      (H : is-invertible-element-Monoid M x) →
+      mul-Monoid M x ∘ left-div-is-invertible-element-Monoid H ~ id
+    is-section-left-div-is-invertible-element-Monoid H y =
+      ( inv (associative-mul-Monoid M _ _ _)) ∙
+      ( ap
+        ( mul-Monoid' M y)
+        ( is-right-inverse-inv-is-invertible-element-Monoid M H)) ∙
+      ( left-unit-law-mul-Monoid M y)
+
+    is-retraction-left-div-is-invertible-element-Monoid :
+      (H : is-invertible-element-Monoid M x) →
+      left-div-is-invertible-element-Monoid H ∘ mul-Monoid M x ~ id
+    is-retraction-left-div-is-invertible-element-Monoid H y =
+      ( inv (associative-mul-Monoid M _ _ _)) ∙
+      ( ap
+        ( mul-Monoid' M y)
+        ( is-left-inverse-inv-is-invertible-element-Monoid M H)) ∙
+      ( left-unit-law-mul-Monoid M y)
 
   is-equiv-mul-is-invertible-element-Monoid :
     is-invertible-element-Monoid M x → is-equiv (mul-Monoid M x)

src/group-theory/products-of-finite-families-of-elements-commutative-monoids.lagda.md

@@ -37,6 +37,7 @@ open import foundation.universal-property-propositional-truncation-into-sets
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
+open import group-theory.homomorphisms-commutative-monoids
 open import group-theory.products-of-finite-families-of-elements-commutative-semigroups
 open import group-theory.products-of-finite-sequences-of-elements-commutative-monoids
 
@@ -781,3 +782,52 @@ module _
           ( product-unit-finite-Commutative-Monoid M _))) ∙
       ( right-unit-law-mul-Commutative-Monoid M _)
 ```
+
+### Commutative monoid homomorphisms distribute over finite sums
+
+```agda
+abstract
+  distributive-hom-product-finite-Commutative-Monoid :
+    {l1 l2 l3 : Level} (M : Commutative-Monoid l1) (N : Commutative-Monoid l2)
+    (φ : hom-Commutative-Monoid M N) (A : Finite-Type l3)
+    (u : type-Finite-Type A → type-Commutative-Monoid M) →
+    map-hom-Commutative-Monoid M N φ
+      ( product-finite-Commutative-Monoid M A u) ＝
+    product-finite-Commutative-Monoid N A (map-hom-Commutative-Monoid M N φ ∘ u)
+  distributive-hom-product-finite-Commutative-Monoid M N φ FA@(A , is-fin-A) u =
+    rec-trunc-Prop
+      ( Id-Prop
+        ( set-Commutative-Monoid N)
+        ( map-hom-Commutative-Monoid M N φ
+          ( product-finite-Commutative-Monoid M FA u))
+        ( product-finite-Commutative-Monoid N FA
+          ( map-hom-Commutative-Monoid M N φ ∘ u)))
+      ( λ cA →
+        equational-reasoning
+          map-hom-Commutative-Monoid M N φ
+            ( product-finite-Commutative-Monoid M FA u)
+          ＝
+            map-hom-Commutative-Monoid M N φ
+              ( product-count-Commutative-Monoid M A cA u)
+            by
+              ap
+                ( map-hom-Commutative-Monoid M N φ)
+                ( eq-product-finite-product-count-Commutative-Monoid M FA cA u)
+          ＝
+            product-count-Commutative-Monoid N A cA
+              ( map-hom-Commutative-Monoid M N φ ∘ u)
+            by
+              distributive-hom-product-fin-sequence-type-Commutative-Monoid
+                ( M)
+                ( N)
+                ( φ)
+                ( _)
+                ( _)
+          ＝
+            product-finite-Commutative-Monoid N FA
+              ( map-hom-Commutative-Monoid M N φ ∘ u)
+            by
+              inv
+                ( eq-product-finite-product-count-Commutative-Monoid N FA cA _))
+      ( is-fin-A)
+```

src/group-theory/products-of-finite-sequences-of-elements-commutative-monoids.lagda.md

@@ -315,6 +315,24 @@ hom-product-fin-sequence-type-Commutative-Monoid M n =
     product-unit-fin-sequence-type-Commutative-Monoid M n)
 ```
 
+### Commutative monoid homomorphisms distribute over the product operation
+
+```agda
+abstract
+  distributive-hom-product-fin-sequence-type-Commutative-Monoid :
+    {l1 l2 : Level} (M : Commutative-Monoid l1) (N : Commutative-Monoid l2)
+    (φ : hom-Commutative-Monoid M N)
+    (n : ℕ) (u : fin-sequence-type-Commutative-Monoid M n) →
+    map-hom-Commutative-Monoid M N φ
+      ( product-fin-sequence-type-Commutative-Monoid M n u) ＝
+    product-fin-sequence-type-Commutative-Monoid N n
+      ( map-hom-Commutative-Monoid M N φ ∘ u)
+  distributive-hom-product-fin-sequence-type-Commutative-Monoid M N =
+    distributive-hom-product-fin-sequence-type-Monoid
+      ( monoid-Commutative-Monoid M)
+      ( monoid-Commutative-Monoid N)
+```
+
 ## See also
 
 - [Products of finite families of elements in commutative monoids](group-theory.products-of-finite-families-of-elements-commutative-monoids.md)

src/group-theory/products-of-finite-sequences-of-elements-groups.lagda.md

@@ -20,6 +20,7 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import group-theory.groups
+open import group-theory.homomorphisms-groups
 open import group-theory.powers-of-elements-groups
 open import group-theory.products-of-finite-sequences-of-elements-monoids
 
@@ -187,3 +188,19 @@ abstract
   product-constant-fin-sequence-type-Group G =
     product-constant-fin-sequence-type-Monoid (monoid-Group G)
 ```
+
+### Group homomorphisms distribute over products
+
+```agda
+abstract
+  distributive-hom-product-fin-sequence-type-Group :
+    {l1 l2 : Level} (G : Group l1) (H : Group l2) (φ : hom-Group G H) →
+    (n : ℕ) (u : fin-sequence-type-Group G n) →
+    map-hom-Group G H φ (product-fin-sequence-type-Group G n u) ＝
+    product-fin-sequence-type-Group H n (map-hom-Group G H φ ∘ u)
+  distributive-hom-product-fin-sequence-type-Group G H φ =
+    distributive-hom-product-fin-sequence-type-Monoid
+      ( monoid-Group G)
+      ( monoid-Group H)
+      ( hom-monoid-hom-Group G H φ)
+```

src/group-theory/products-of-finite-sequences-of-elements-monoids.lagda.md

@@ -19,6 +19,7 @@ open import foundation.unit-type
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
+open import group-theory.homomorphisms-monoids
 open import group-theory.monoids
 open import group-theory.powers-of-elements-monoids
 
@@ -222,3 +223,21 @@ abstract
       ( product-constant-fin-sequence-type-Monoid M n x)
       ( refl)
 ```
+
+### Monoid homomorphisms distribute over products
+
+```agda
+abstract
+  distributive-hom-product-fin-sequence-type-Monoid :
+    {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (φ : hom-Monoid M N) →
+    (n : ℕ) (u : fin-sequence-type-Monoid M n) →
+    map-hom-Monoid M N φ (product-fin-sequence-type-Monoid M n u) ＝
+    product-fin-sequence-type-Monoid N n (map-hom-Monoid M N φ ∘ u)
+  distributive-hom-product-fin-sequence-type-Monoid M N φ 0 u =
+    preserves-unit-hom-Monoid M N φ
+  distributive-hom-product-fin-sequence-type-Monoid M N φ (succ-ℕ n) u =
+    ( preserves-mul-hom-Monoid M N φ) ∙
+    ( ap-mul-Monoid N
+      ( distributive-hom-product-fin-sequence-type-Monoid M N φ n (u ∘ inl))
+      ( refl))
+```