Skip to content

Commit 05cf7be

Browse files
lowasserEgbertRijke
lowasser
and
EgbertRijke
authored
The type of permutations on n elements is finite with cardinality n! (#1936)
This implies that it can be summed over, which will allow us to define determinants. --------- Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
1 parent 349f1a2 commit 05cf7be

27 files changed

Lines changed: 2863 additions & 866 deletions

‎references.bib‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -469,6 +469,15 @@ @online{Esc17YetAnother
469469
howpublished = {{{Google}} groups forum discussion},
470470
}
471471

472+
@online{Esc19CoderivedSet,
473+
title = {Factorial Law},
474+
author = {Escardó, Martín Hötzel},
475+
year = 2019,
476+
month = nov,
477+
url = {https://martinescardo.github.io/TypeTopology/Factorial.Law.html},
478+
howpublished = {{{TypeTopology}} website},
479+
}
480+
472481
@online{Esc19DefinitionsEquivalence,
473482
title = {Definitions of Equivalence Satisfying Judgmental/Strict Groupoid Laws?},
474483
author = {Escardó, Martín Hötzel},

‎src/finite-group-theory.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ open import finite-group-theory.alternating-concrete-groups public
1010
open import finite-group-theory.alternating-groups public
1111
open import finite-group-theory.cartier-delooping-sign-homomorphism public
1212
open import finite-group-theory.concrete-quaternion-group public
13+
open import finite-group-theory.counting-automorphisms-finite-types public
14+
open import finite-group-theory.counting-permutations-standard-finite-types public
1315
open import finite-group-theory.delooping-sign-homomorphism public
1416
open import finite-group-theory.finite-abelian-groups public
1517
open import finite-group-theory.finite-commutative-monoids public

‎src/finite-group-theory/concrete-quaternion-group.lagda.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ open import elementary-number-theory.natural-numbers
1111
1212
open import foundation.dependent-pair-types
1313
open import foundation.equivalences
14+
open import foundation.equivalences-types-with-isolated-elements
1415
open import foundation.identity-types
1516
open import foundation.isolated-elements
1617
open import foundation.transport-along-identifications
@@ -49,7 +50,6 @@ equiv-face-cube k X Y e d a =
4950
( axis-cube (succ-ℕ k) Y)
5051
( inv
5152
( natural-inclusion-equiv-complement-isolated-element
52-
( dim-equiv-cube (succ-ℕ k) X Y e)
5353
( pair d
5454
( λ z →
5555
has-decidable-equality-has-cardinality-ℕ
@@ -65,7 +65,7 @@ equiv-face-cube k X Y e d a =
6565
( has-cardinality-dim-cube (succ-ℕ k) Y)
6666
( map-dim-equiv-cube (succ-ℕ k) X Y e d)
6767
( z)))
68-
( refl)
68+
( dim-equiv-cube (succ-ℕ k) X Y e , refl)
6969
( d')))) ∘e
7070
( axis-equiv-cube (succ-ℕ k) X Y e
7171
( inclusion-complement-element-Type-With-Cardinality-ℕ k

‎src/finite-group-theory/counting-automorphisms-finite-types.lagda.md‎

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
# Counting automorphisms of finite types
2+
3+
```agda
4+
module finite-group-theory.counting-automorphisms-finite-types where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.equality-natural-numbers
11+
open import elementary-number-theory.factorials
12+
open import elementary-number-theory.natural-numbers
13+
14+
open import finite-group-theory.counting-permutations-standard-finite-types
15+
16+
open import foundation.action-on-identifications-functions
17+
open import foundation.automorphisms
18+
open import foundation.dependent-pair-types
19+
open import foundation.equivalences
20+
open import foundation.functoriality-propositional-truncation
21+
open import foundation.identity-types
22+
open import foundation.propositional-truncations
23+
open import foundation.sets
24+
open import foundation.transport-along-identifications
25+
open import foundation.universe-levels
26+
27+
open import univalent-combinatorics.counting
28+
open import univalent-combinatorics.finite-types
29+
open import univalent-combinatorics.standard-finite-types
30+
```
31+
32+
</details>
33+
34+
## Idea
35+
36+
Given a [finite type](univalent-combinatorics.finite-types.md) `X` with
37+
cardinality `n`, the type of [automorphisms](foundation.automorphisms.md) of `X`
38+
has cardinality equal to the [factorial](elementary-number-theory.factorials.md)
39+
of `n`.
40+
41+
## Properties
42+
43+
### Counting permutations of `X` from a counting of `X`
44+
45+
```agda
46+
module _
47+
{l1 : Level} {X : UU l1} ((n , e) : count X)
48+
where
49+
50+
count-aut :
51+
count (Aut X)
52+
count-aut =
53+
( factorial-ℕ n ,
54+
conjugation-aut e ∘e equiv-count (count-Permutation n))
55+
56+
number-of-elements-count-aut :
57+
number-of-elements-count count-aut ＝ factorial-ℕ n
58+
number-of-elements-count-aut = refl
59+
```
60+
61+
### The automorphisms of a type `X` with cardinality `n` have cardinality `n!`
62+
63+
```agda
64+
module _
65+
{l1 : Level} (n : ℕ)
66+
where
67+
68+
abstract
69+
has-cardinality-factorial-aut-has-cardinality-ℕ :
70+
{X : UU l1} →
71+
has-cardinality-ℕ n X → has-cardinality-ℕ (factorial-ℕ n) (Aut X)
72+
has-cardinality-factorial-aut-has-cardinality-ℕ =
73+
map-trunc-Prop
74+
( λ e → equiv-count (count-aut (n , e)))
75+
76+
aut-Type-With-Cardinality-ℕ :
77+
Type-With-Cardinality-ℕ l1 n → Type-With-Cardinality-ℕ l1 (factorial-ℕ n)
78+
aut-Type-With-Cardinality-ℕ (X , e) =
79+
( Aut X , has-cardinality-factorial-aut-has-cardinality-ℕ e)
80+
```
81+
82+
### The automorphisms of a finite type
83+
84+
```agda
85+
module _
86+
{l1 : Level}
87+
where
88+
89+
abstract
90+
is-finite-aut-is-finite :
91+
{X : UU l1} → is-finite X → is-finite (Aut X)
92+
is-finite-aut-is-finite = map-trunc-Prop count-aut
93+
94+
aut-Finite-Type : Finite-Type l1 → Finite-Type l1
95+
aut-Finite-Type (X , H) =
96+
( Aut X , is-finite-aut-is-finite H)
97+
98+
abstract
99+
number-of-elements-aut-Finite-Type :
100+
(X : Finite-Type l1) →
101+
number-of-elements-Finite-Type (aut-Finite-Type X) ＝
102+
factorial-ℕ (number-of-elements-Finite-Type X)
103+
number-of-elements-aut-Finite-Type (X , H) =
104+
apply-universal-property-trunc-Prop H
105+
( Id-Prop ℕ-Set _ _)
106+
( λ (n , e) →
107+
inv
108+
( compute-number-of-elements-is-finite
109+
( count-aut (n , e))
110+
( is-finite-aut-is-finite H)) ∙
111+
ap factorial-ℕ (compute-number-of-elements-is-finite (n , e) H))
112+
```

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

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
# Counting permutations of standard finite types
2+
3+
```agda
4+
{-# OPTIONS --lossy-unification #-}
5+
6+
module finite-group-theory.counting-permutations-standard-finite-types where
7+
```
8+
9+
<details><summary>Imports</summary>
10+
11+
```agda
12+
open import elementary-number-theory.factorials
13+
open import elementary-number-theory.natural-numbers
14+
15+
open import finite-group-theory.permutations-standard-finite-types
16+
17+
open import foundation.automorphisms
18+
open import foundation.automorphisms-discrete-types
19+
open import foundation.cartesian-product-types
20+
open import foundation.contractible-types
21+
open import foundation.coproduct-types
22+
open import foundation.dependent-pair-types
23+
open import foundation.empty-types
24+
open import foundation.equivalences
25+
open import foundation.equivalences-contractible-types
26+
open import foundation.function-types
27+
open import foundation.functoriality-cartesian-product-types
28+
open import foundation.identity-types
29+
open import foundation.unit-type
30+
open import foundation.universe-levels
31+
32+
open import univalent-combinatorics.cartesian-product-types
33+
open import univalent-combinatorics.counting
34+
open import univalent-combinatorics.equality-standard-finite-types
35+
open import univalent-combinatorics.finite-types
36+
open import univalent-combinatorics.standard-finite-types
37+
```
38+
39+
</details>
40+
41+
## Idea
42+
43+
The [permutations](finite-group-theory.permutations-standard-finite-types.md) of
44+
the [standard finite type](univalent-combinatorics.standard-finite-types.md)
45+
with `n` elements are a [finite type](univalent-combinatorics.finite-types.md)
46+
with `n` [factorial](elementary-number-theory.factorials.md) elements.
47+
48+
## Proof
49+
50+
### `Permutation (n + 1) ≃ Permutation n × Fin (n + 1)`
51+
52+
```agda
53+
module _
54+
(n : ℕ)
55+
where
56+
57+
compute-Permutation-succ-ℕ :
58+
Permutation (succ-ℕ n) ≃ Permutation n × Fin (succ-ℕ n)
59+
compute-Permutation-succ-ℕ =
60+
equiv-product
61+
( conjugation-aut (compute-complement-neg-one-Fin n))
62+
( id-equiv) ∘e
63+
compute-aut-Discrete-Type (Fin-Discrete-Type (succ-ℕ n)) (inr star)
64+
```
65+
66+
### Counting the elements of `Permutation n`
67+
68+
```agda
69+
is-contr-Permutation-0 : is-contr (Permutation 0)
70+
is-contr-Permutation-0 = is-contr-equiv-is-empty id id
71+
72+
equiv-count-Permutation :
73+
(n : ℕ) → Fin (factorial-ℕ n) ≃ Permutation n
74+
equiv-count-Permutation zero-ℕ =
75+
equiv-is-contr is-contr-Fin-1 is-contr-Permutation-0
76+
equiv-count-Permutation (succ-ℕ n) =
77+
inv-equiv (compute-Permutation-succ-ℕ n) ∘e
78+
equiv-product (equiv-count-Permutation n) id-equiv ∘e
79+
inv-equiv (product-Fin (factorial-ℕ n) (succ-ℕ n))
80+
81+
count-Permutation : (n : ℕ) → count (Permutation n)
82+
pr1 (count-Permutation n) = factorial-ℕ n
83+
pr2 (count-Permutation n) = equiv-count-Permutation n
84+
```
85+
86+
### `Permutation n` is finite
87+
88+
```agda
89+
finite-type-Permutation : (n : ℕ) → Finite-Type lzero
90+
finite-type-Permutation n =
91+
( Permutation n , is-finite-count (count-Permutation n))
92+
```
93+
94+
### The number of elements of `Permutation n` is n
95+
96+
```agda
97+
abstract
98+
number-of-elements-count-Permutation :
99+
(n : ℕ) →
100+
number-of-elements-count (count-Permutation n) ＝ factorial-ℕ n
101+
number-of-elements-count-Permutation n = refl
102+
103+
number-of-elements-Permutation :
104+
(n : ℕ) →
105+
number-of-elements-Finite-Type (finite-type-Permutation n) ＝ factorial-ℕ n
106+
number-of-elements-Permutation n =
107+
inv (compute-number-of-elements-is-finite (count-Permutation n) _)
108+
```

0 commit comments

Comments
 (0)