Cycle prime decomposition is closed under cartesian product (#624)

In this pull request, I wanted to prove that the cartesian product of
the cycles prime decomposition of `n` and `m` is equal to the cycle
prime decomposition of `mul-\bN n m`. Initially, I thought it would be
easy by using the fundamental theorem of arithmetic but I encountered
some unexpected problems that I had to solve ^^.
The main idea was to 

1. Show that if we take the sorted concatenation of the lists
corresponding to the prime decomposition of `n` and `m` we obtain a
prime decomposition of `mul-\bN n m`. This was harder than I thought. I
had to show that `mul-list-\bN` is invariant by permuting the list. I
made the general case, and to do it I had to show that every
transposition (on Fin n) is a composition of adjacent transpositions.
2. Then I used the fundamental theorem of arithmetic to demonstrate that
the sorted concatenation of the lists corresponding to the prime
decomposition of `n` and `m` is equal to the prime decomposition of
`mul-\bN n m`.
3. Finally, I expected to only need to permute the cycles in the
cartesian product of the cycles prime decomposition associated to `n`
and `m` with the permutation given by the sort by insertion. I thought
that applying step 2. would be sufficient to conclude. But I had to show
this property : `map-list f (permute-list p t)` is equal to
`permute-list (map-list p f) t` and which was quite hard to prove.

---------

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md

@@ -7,6 +7,7 @@ module elementary-number-theory.fundamental-theorem-of-arithmetic where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.based-strong-induction-natural-numbers
 open import elementary-number-theory.bezouts-lemma-integers
 open import elementary-number-theory.decidable-total-order-natural-numbers
@@ -23,6 +24,8 @@ open import elementary-number-theory.relatively-prime-natural-numbers
 open import elementary-number-theory.strict-inequality-natural-numbers
 open import elementary-number-theory.well-ordering-principle-natural-numbers
 
+open import finite-group-theory.permutations-standard-finite-types
+
 open import foundation.cartesian-product-types
 open import foundation.contractible-types
 open import foundation.coproduct-types
@@ -36,9 +39,12 @@ open import foundation.type-arithmetic-empty-type
 open import foundation.unit-type
 open import foundation.universe-levels
 
+open import lists.concatenation-lists
 open import lists.functoriality-lists
 open import lists.lists
+open import lists.permutation-lists
 open import lists.predicates-on-lists
+open import lists.sort-by-insertion-lists
 open import lists.sorted-lists
 ```
 
@@ -934,3 +940,138 @@ pr2 (fundamental-theorem-arithmetic-list-ℕ x H) d =
        ( is-prime-decomposition-list-fundamental-theorem-arithmetic-ℕ x H)
        ( pr2 d))
 ```
+
+### The sorted list associated with the concatenation of the prime decomposition of `n` and the prime decomposition of `m` is the prime decomposition of `n *ℕ m`
+
+```agda
+is-prime-list-concat-list-ℕ :
+  (p q : list ℕ) → is-prime-list-ℕ p → is-prime-list-ℕ q →
+  is-prime-list-ℕ (concat-list p q)
+is-prime-list-concat-list-ℕ nil q Pp Pq = Pq
+is-prime-list-concat-list-ℕ (cons x p) q Pp Pq =
+  pr1 Pp , is-prime-list-concat-list-ℕ p q (pr2 Pp) Pq
+
+all-elements-is-prime-list-ℕ :
+  (p : list ℕ) → UU lzero
+all-elements-is-prime-list-ℕ p = (x : ℕ) → x ∈-list p → is-prime-ℕ x
+
+all-elements-is-prime-list-tail-ℕ :
+  (p : list ℕ) (x : ℕ) (P : all-elements-is-prime-list-ℕ (cons x p)) →
+  all-elements-is-prime-list-ℕ p
+all-elements-is-prime-list-tail-ℕ p x P y I = P y (is-in-tail y x p I)
+
+all-elements-is-prime-list-is-prime-list-ℕ :
+  (p : list ℕ) → is-prime-list-ℕ p → all-elements-is-prime-list-ℕ p
+all-elements-is-prime-list-is-prime-list-ℕ (cons x p) P .x (is-head .x .p) =
+  pr1 P
+all-elements-is-prime-list-is-prime-list-ℕ
+  ( cons x p)
+  ( P)
+  ( y)
+  ( is-in-tail .y .x .p I) =
+  all-elements-is-prime-list-is-prime-list-ℕ p (pr2 P) y I
+
+is-prime-list-all-elements-is-prime-list-ℕ :
+  (p : list ℕ) → all-elements-is-prime-list-ℕ p → is-prime-list-ℕ p
+is-prime-list-all-elements-is-prime-list-ℕ nil P = raise-star
+is-prime-list-all-elements-is-prime-list-ℕ (cons x p) P =
+  P x (is-head x p) ,
+  is-prime-list-all-elements-is-prime-list-ℕ
+    ( p)
+    ( all-elements-is-prime-list-tail-ℕ p x P)
+
+is-prime-list-permute-list-ℕ :
+  (p : list ℕ) (t : Permutation (length-list p)) → is-prime-list-ℕ p →
+  is-prime-list-ℕ (permute-list p t)
+is-prime-list-permute-list-ℕ p t P =
+  is-prime-list-all-elements-is-prime-list-ℕ
+    ( permute-list p t)
+    ( λ x I → all-elements-is-prime-list-is-prime-list-ℕ
+      ( p)
+      ( P)
+      ( x)
+      ( is-in-list-is-in-permute-list
+        ( p)
+        ( t)
+        ( x)
+        ( I)))
+
+is-decomposition-list-concat-list-ℕ :
+  (n m : ℕ) (p q : list ℕ) →
+  is-decomposition-list-ℕ n p → is-decomposition-list-ℕ m q →
+  is-decomposition-list-ℕ (n *ℕ m) (concat-list p q)
+is-decomposition-list-concat-list-ℕ n m p q Dp Dq =
+  ( eq-mul-list-concat-list-ℕ p q ∙
+    ( ap (mul-ℕ (mul-list-ℕ p)) Dq ∙
+      ap (λ n → n *ℕ m) Dp))
+
+is-decomposition-list-permute-list-ℕ :
+  (n : ℕ) (p : list ℕ) (t : Permutation (length-list p)) →
+  is-decomposition-list-ℕ n p →
+  is-decomposition-list-ℕ n (permute-list p t)
+is-decomposition-list-permute-list-ℕ n p t D =
+  inv (invariant-permutation-mul-list-ℕ p t) ∙ D
+
+is-prime-decomposition-list-sort-concatenation-ℕ :
+  (x y : ℕ) (H : leq-ℕ 1 x) (I : leq-ℕ 1 y) (p q : list ℕ) →
+  is-prime-decomposition-list-ℕ x p →
+  is-prime-decomposition-list-ℕ y q →
+  is-prime-decomposition-list-ℕ
+    (x *ℕ y)
+    ( insertion-sort-list
+      ( ℕ-Decidable-Total-Order)
+      ( concat-list p q))
+pr1 (is-prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq) =
+  is-sorting-insertion-sort-list ℕ-Decidable-Total-Order (concat-list p q)
+pr1
+  ( pr2
+    ( is-prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq)) =
+  tr
+    ( λ p → is-prime-list-ℕ p)
+    ( inv
+      ( eq-permute-list-permutation-insertion-sort-list
+        ( ℕ-Decidable-Total-Order)
+        ( concat-list p q)))
+    ( is-prime-list-permute-list-ℕ
+      ( concat-list p q)
+      ( permutation-insertion-sort-list
+        ( ℕ-Decidable-Total-Order)
+        ( concat-list p q))
+      ( is-prime-list-concat-list-ℕ
+        ( p)
+        ( q)
+        ( is-prime-list-is-prime-decomposition-list-ℕ x p Dp)
+        ( is-prime-list-is-prime-decomposition-list-ℕ y q Dq)))
+pr2
+  ( pr2
+    ( is-prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq)) =
+  tr
+    ( λ p → is-decomposition-list-ℕ (x *ℕ y) p)
+    ( inv
+      ( eq-permute-list-permutation-insertion-sort-list
+        ( ℕ-Decidable-Total-Order)
+        ( concat-list p q)))
+    ( is-decomposition-list-permute-list-ℕ
+      ( x *ℕ y)
+      ( concat-list p q)
+      ( permutation-insertion-sort-list
+        ( ℕ-Decidable-Total-Order)
+        ( concat-list p q))
+      ( is-decomposition-list-concat-list-ℕ
+        ( x)
+        ( y)
+        ( p)
+        ( q)
+        ( is-decomposition-list-is-prime-decomposition-list-ℕ x p Dp)
+        ( is-decomposition-list-is-prime-decomposition-list-ℕ y q Dq)))
+
+prime-decomposition-list-sort-concatenation-ℕ :
+  (x y : ℕ) (H : leq-ℕ 1 x) (I : leq-ℕ 1 y) (p q : list ℕ) →
+  is-prime-decomposition-list-ℕ x p →
+  is-prime-decomposition-list-ℕ y q →
+  prime-decomposition-list-ℕ (x *ℕ y) (preserves-leq-mul-ℕ 1 x 1 y H I)
+pr1 (prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq) =
+  insertion-sort-list ℕ-Decidable-Total-Order (concat-list p q)
+pr2 (prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq) =
+  is-prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq
+```

src/elementary-number-theory/inequality-natural-numbers.lagda.md

@@ -381,6 +381,20 @@ preserves-order-mul-ℕ' k m n H =
     ( commutative-mul-ℕ n k)
 ```
 
+### Multiplication preserves inequality
+
+```agda
+preserves-leq-mul-ℕ :
+  (m m' n n' : ℕ) → m ≤-ℕ m' → n ≤-ℕ n' → (m *ℕ n) ≤-ℕ (m' *ℕ n')
+preserves-leq-mul-ℕ m m' n n' H K =
+  transitive-leq-ℕ
+    ( m *ℕ n)
+    ( m' *ℕ n)
+    ( m' *ℕ n')
+    ( preserves-order-mul-ℕ' m' n n' K)
+    ( preserves-order-mul-ℕ n m m' H)
+```
+
 ### Multiplication by a nonzero element reflects the ordering on ℕ
 
 ```agda

src/elementary-number-theory/multiplication-lists-of-natural-numbers.lagda.md

@@ -7,10 +7,17 @@ module elementary-number-theory.multiplication-lists-of-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
 
+open import finite-group-theory.permutations-standard-finite-types
+
+open import foundation.identity-types
+
+open import lists.concatenation-lists
 open import lists.lists
+open import lists.permutation-lists
 ```
 
 </details>
@@ -27,3 +34,33 @@ mul-list-ℕ :
   list ℕ → ℕ
 mul-list-ℕ = fold-list 1 mul-ℕ
 ```
+
+## Properties
+
+### `mul-list-ℕ` is invariant by permutation
+
+```agda
+invariant-permutation-mul-list-ℕ :
+  (l : list ℕ) (t : Permutation (length-list l)) →
+  mul-list-ℕ l ＝ mul-list-ℕ (permute-list l t)
+invariant-permutation-mul-list-ℕ =
+  invariant-permutation-fold-list
+    ( 1)
+    ( mul-ℕ)
+    ( λ a1 a2 b →
+      ( inv (associative-mul-ℕ a1 a2 b) ∙
+        ( ap (λ n → n *ℕ b) (commutative-mul-ℕ a1 a2) ∙
+          ( associative-mul-ℕ a2 a1 b))))
+```
+
+### `mul-list-ℕ` of a concatenation of lists
+
+```agda
+eq-mul-list-concat-list-ℕ :
+  (p q : list ℕ) →
+  (mul-list-ℕ (concat-list p q)) ＝ (mul-list-ℕ p) *ℕ (mul-list-ℕ q)
+eq-mul-list-concat-list-ℕ nil q = inv (left-unit-law-add-ℕ (mul-list-ℕ q))
+eq-mul-list-concat-list-ℕ (cons x p) q =
+  ap (mul-ℕ x) (eq-mul-list-concat-list-ℕ p q) ∙
+  inv (associative-mul-ℕ x (mul-list-ℕ p) (mul-list-ℕ q))
+```

src/finite-group-theory/permutations-standard-finite-types.lagda.md

@@ -16,6 +16,7 @@ open import elementary-number-theory.natural-numbers
 open import finite-group-theory.transpositions
 
 open import foundation.automorphisms
+open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
@@ -25,8 +26,10 @@ open import foundation.equivalence-extensionality
 open import foundation.equivalences
 open import foundation.equivalences-maybe
 open import foundation.functions
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.injective-maps
+open import foundation.negation
 open import foundation.propositions
 open import foundation.sets
 open import foundation.unit-type
@@ -438,3 +441,68 @@ abstract
     retr-permutation-list-transpositions-Fin'
       n f (map-equiv f (inr star)) refl y (map-equiv f y) refl
 ```
+
+```agda
+permutation-list-standard-transpositions-Fin :
+  (n : ℕ) →
+  list (Σ (Fin n × Fin n) (λ (i , j) → ¬ (i ＝ j))) →
+  Permutation n
+permutation-list-standard-transpositions-Fin n =
+  fold-list
+    ( id-equiv)
+    ( λ (_ , neq) p →
+      standard-transposition (has-decidable-equality-Fin n) neq ∘e p)
+
+list-standard-transpositions-permutation-Fin :
+  (n : ℕ) (f : Permutation n) →
+  list (Σ (Fin n × Fin n) (λ (i , j) → ¬ (i ＝ j)))
+list-standard-transpositions-permutation-Fin n f =
+  map-list
+    ( λ P →
+      ( element-two-elements-transposition-Fin P ,
+        other-element-two-elements-transposition-Fin P) ,
+      neq-elements-two-elements-transposition-Fin P)
+    ( list-transpositions-permutation-Fin n f)
+
+private
+  htpy-permutation-list :
+    (n : ℕ)
+    (l : list
+      (2-Element-Decidable-Subtype lzero (Fin (succ-ℕ n)))) →
+    htpy-equiv
+      ( permutation-list-standard-transpositions-Fin
+        ( succ-ℕ n)
+        ( map-list
+          ( λ P →
+            ( element-two-elements-transposition-Fin P ,
+              other-element-two-elements-transposition-Fin P) ,
+            neq-elements-two-elements-transposition-Fin P)
+          ( l)))
+      ( permutation-list-transpositions l)
+  htpy-permutation-list n nil = refl-htpy
+  htpy-permutation-list n (cons P l) =
+    ( htpy-two-elements-transpositon-Fin P ·r
+      map-equiv
+        ( permutation-list-standard-transpositions-Fin
+          ( succ-ℕ n)
+          ( map-list
+            ( λ P →
+              ( element-two-elements-transposition-Fin P ,
+                other-element-two-elements-transposition-Fin P) ,
+              neq-elements-two-elements-transposition-Fin P)
+           ( l)))) ∙h
+    ( map-transposition P ·l
+      htpy-permutation-list n l)
+
+retr-permutation-list-standard-transpositions-Fin :
+  (n : ℕ) (f : Permutation n) →
+  htpy-equiv
+    ( permutation-list-standard-transpositions-Fin
+      ( n)
+      ( list-standard-transpositions-permutation-Fin n f))
+    ( f)
+retr-permutation-list-standard-transpositions-Fin 0 f ()
+retr-permutation-list-standard-transpositions-Fin (succ-ℕ n) f =
+  htpy-permutation-list n (list-transpositions-permutation-Fin (succ-ℕ n) f) ∙h
+  retr-permutation-list-transpositions-Fin (succ-ℕ n) f
+```