Permutation 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/equivalences.lagda.md

@@ -691,6 +691,33 @@ module _
           ( is-equiv-q))
 ```
 
+### For an equivalence `e`, `map-equiv e x = y` if and only if `map-inv-equiv e y = x`
+
+```agda
+module _
+  {l1 l2 : Level}
+  {A : UU l1}
+  {B : UU l2}
+  (e : A ≃ B)
+  where abstract
+
+  eq-map-inv-equiv-eq-map-equiv :
+    (x : A) (y : B) → map-equiv e x ＝ y → map-inv-equiv e y ＝ x
+  eq-map-inv-equiv-eq-map-equiv x _ refl =
+    is-retraction-map-inv-equiv e x
+
+  eq-map-equiv-eq-map-inv-equiv :
+    (x : A) (y : B) → map-inv-equiv e y ＝ x → map-equiv e x ＝ y
+  eq-map-equiv-eq-map-inv-equiv _ y refl =
+    is-section-map-inv-equiv e y
+
+  eq-map-inv-equiv-iff-eq-map-equiv :
+    (x : A) (y : B) → (map-equiv e x ＝ y) ↔ (map-inv-equiv e y ＝ x)
+  eq-map-inv-equiv-iff-eq-map-equiv x y =
+    ( eq-map-inv-equiv-eq-map-equiv x y ,
+      eq-map-equiv-eq-map-inv-equiv x y)
+```
+
 ## See also
 
 - For the notion of coherently invertible maps, also known as half-adjoint

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/homomorphisms-abelian-groups.lagda.md

@@ -28,8 +28,10 @@ open import group-theory.homomorphisms-semigroups
 
 ## Idea
 
-Homomorphisms between abelian groups are just homomorphisms between their
-underlying groups.
+{{#concept "Homomorphisms" Disambiguation="between abelian groups" Agda=hom-Ab}}
+between [abelian groups](group-theory.abelian-groups.md) are just
+[homomorphisms](group-theory.homomorphisms-groups.md) between their underlying
+[groups](group-theory.groups.md).
 
 ## Definition
 

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)