Skip to content

Commit

Permalink
Small fixes concrete groups (#897)
Browse files Browse the repository at this point in the history
  • Loading branch information
@fredrik-bakke
fredrik-bakke committed Nov 4, 2023
1 parent 6fe1741 commit 52fdf4c
Show file tree
Hide file tree
Showing 18 changed files with 372 additions and 262 deletions.
23 changes: 11 additions & 12 deletions src/category-theory/groupoids.lagda.md
View file
Expand Up @@ -76,8 +76,8 @@ module _
id-hom-Groupoid = id-hom-Category category-Groupoid

comp-hom-Groupoid :
{x y z : obj-Groupoid} → hom-Groupoid y z →
hom-Groupoid x y → hom-Groupoid x z
{x y z : obj-Groupoid} →
hom-Groupoid y z → hom-Groupoid x y → hom-Groupoid x z
comp-hom-Groupoid = comp-hom-Category category-Groupoid

associative-comp-hom-Groupoid :
Expand Down Expand Up @@ -136,30 +136,29 @@ module _
fundamental-theorem-id
( is-contr-equiv'
( Σ ( Σ (type-1-Type X) (λ y → x ＝ y))
( λ yp →
Σ ( Σ (pr1 yp ＝ x) (λ q → (q ∙ pr2 yp) ＝ refl))
( λ ql → (pr2 yp ∙ pr1 ql) ＝ refl)))
( λ (y , p) →
Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl))
( λ (q , l) → p ∙ q ＝ refl)))
( ( equiv-tot
( λ y →
equiv-tot
( λ p →
associative-Σ
( y ＝ x)
( λ q → (q ∙ p) ＝ refl)
( λ qr → (p ∙ pr1 qr) ＝ refl)))) ∘e
( λ q → q ∙ p ＝ refl)
( λ (q , r) → p ∙ q ＝ refl)))) ∘e
( associative-Σ
( type-1-Type X)
( λ y → x ＝ y)
( λ yp →
Σ ( Σ (pr1 yp ＝ x) (λ q → (q ∙ pr2 yp) ＝ refl))
( λ ql → (pr2 yp ∙ pr1 ql) ＝ refl))))
( λ (y , p) →
Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl))
( λ (q , l) → p ∙ q ＝ refl))))
( is-contr-iterated-Σ 2
( is-torsorial-path x ,
( x , refl) ,
( is-contr-equiv
( Σ (x ＝ x) (λ q → q ＝ refl))
( equiv-tot
( λ q → equiv-concat (inv right-unit) refl))
( equiv-tot (λ q → equiv-concat (inv right-unit) refl))
( is-torsorial-path' refl)) ,
( refl , refl) ,
( is-proof-irrelevant-is-prop
Expand Down
12 changes: 6 additions & 6 deletions src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md
View file
Expand Up @@ -146,28 +146,28 @@ module _
( comp-hom-Group
( symmetric-Group (raise-Fin-Set l (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
( comp-hom-Group
( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
( hom-group-hom-Concrete-Group
( UU-Fin-Group l (n +ℕ 2))
( UU-Fin-Group (lsuc l) 2)
( cartier-delooping-sign (n +ℕ 2)))
( hom-inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
( iso-loop-group-fin-UU-Fin-Group l (n +ℕ 2))))
( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l (n +ℕ 2))))
( comp-hom-Group
( symmetric-Group (raise-Fin-Set l (n +ℕ 2)))
( symmetric-Group (Fin-Set (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
( comp-hom-Group
( symmetric-Group (Fin-Set (n +ℕ 2)))
( symmetric-Group (Fin-Set 2))
( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
( symmetric-abstract-UU-fin-group-quotient-hom
( orientation-Complete-Undirected-Graph)
( even-difference-orientation-Complete-Undirected-Graph)
Expand Down
96 changes: 48 additions & 48 deletions src/finite-group-theory/delooping-sign-homomorphism.lagda.md
View file
Expand Up @@ -1085,16 +1085,16 @@ module _
( comp-hom-Group
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( hom-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( iso-loop-group-fin-UU-Fin-Group l4 2))
( iso-loop-group-equiv-Set
Expand All @@ -1104,17 +1104,17 @@ module _
( quotient-delooping-sign-loop n))
( comp-hom-Group
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l4 2))
( hom-group-hom-Concrete-Group
( UU-Fin-Group l1 (n +ℕ 2))
( UU-Fin-Group l4 2)
( quotient-delooping-sign (n +ℕ 2)))
( hom-iso-Group
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2)))))
eq-quotient-delooping-loop-UU-Fin-Group n =
Expand Down Expand Up @@ -1298,47 +1298,47 @@ module _
( eq-is-prop
( is-prop-preserves-mul-Semigroup
( semigroup-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))))
( semigroup-Group (abstract-group-Concrete-Group (UU-Fin-Group l4 2)))
( semigroup-Group (group-Concrete-Group (UU-Fin-Group l4 2)))
( pr1
( comp-hom-Group
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l4 2))
( hom-group-hom-Concrete-Group
( UU-Fin-Group l1 (n +ℕ 2))
( UU-Fin-Group l4 2)
( quotient-delooping-sign (n +ℕ 2)))
( hom-iso-Group
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2))))))))

symmetric-abstract-UU-fin-group-quotient-hom :
(n : ℕ) →
hom-Group
( symmetric-Group (Fin-Set 2))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
symmetric-abstract-UU-fin-group-quotient-hom n =
comp-hom-Group
( symmetric-Group (Fin-Set 2))
( symmetric-Group (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-hom-Group
( symmetric-Group (quotient-set-Fin (n +ℕ 2)))
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( hom-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( iso-loop-group-fin-UU-Fin-Group l4 2))
( iso-loop-group-equiv-Set
Expand All @@ -1357,28 +1357,28 @@ module _
( comp-hom-Group
( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-hom-Group
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l4 2))
( hom-group-hom-Concrete-Group
( UU-Fin-Group l1 (n +ℕ 2))
( UU-Fin-Group l4 2)
( quotient-delooping-sign (n +ℕ 2)))
( hom-inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2))))
( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))))
( comp-hom-Group
( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))
( symmetric-Group (Fin-Set (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-hom-Group
( symmetric-Group (Fin-Set (n +ℕ 2)))
( symmetric-Group (Fin-Set 2))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( symmetric-abstract-UU-fin-group-quotient-hom n)
( sign-homomorphism
( n +ℕ 2)
Expand All @@ -1393,24 +1393,24 @@ module _
comp-hom-Group
( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( f)
( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))))
( inv (eq-quotient-delooping-loop-UU-Fin-Group n))) ∙
( associative-comp-hom-Group
( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( hom-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( iso-loop-group-fin-UU-Fin-Group l4 2))
( iso-loop-group-equiv-Set
Expand All @@ -1423,16 +1423,16 @@ module _
( comp-hom-Group
( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( hom-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( iso-loop-group-fin-UU-Fin-Group l4 2))
( iso-loop-group-equiv-Set
Expand All @@ -1446,33 +1446,33 @@ module _
( is-prop-preserves-mul-Semigroup
( semigroup-Group (symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))))
( semigroup-Group
( abstract-group-Concrete-Group (UU-Fin-Group l4 2)))
( group-Concrete-Group (UU-Fin-Group l4 2)))
( pr1
( comp-hom-Group
( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))
( symmetric-Group (Fin-Set (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-hom-Group
( symmetric-Group (Fin-Set (n +ℕ 2)))
( symmetric-Group (Fin-Set 2))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-hom-Group
( symmetric-Group (Fin-Set 2))
( symmetric-Group (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-hom-Group
( symmetric-Group (quotient-set-Fin (n +ℕ 2)))
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( hom-iso-Group
( loop-group-Set (quotient-set-Fin (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( comp-iso-Group
( loop-group-Set ( quotient-set-Fin (n +ℕ 2)))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l4 2))
( group-Concrete-Group (UU-Fin-Group l4 2))
( inv-iso-Group
( abstract-group-Concrete-Group
( group-Concrete-Group
( UU-Fin-Group l4 2))
( loop-group-Set (raise-Set l4 (Fin-Set 2)))
( iso-loop-group-fin-UU-Fin-Group l4 2))
Expand Down Expand Up @@ -1580,28 +1580,28 @@ module _
( comp-hom-Group
( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2))
( group-Concrete-Group (UU-Fin-Group (lsuc l2) 2))
( comp-hom-Group
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group (lsuc l2) 2))
( hom-group-hom-Concrete-Group
( UU-Fin-Group l1 (n +ℕ 2))
( UU-Fin-Group (lsuc l2) 2)
( delooping-sign (n +ℕ 2)))
( hom-inv-iso-Group
( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2)))
( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))
( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2))))
( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))))
( comp-hom-Group
( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))
( symmetric-Group (Fin-Set (n +ℕ 2)))
( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2))
( group-Concrete-Group (UU-Fin-Group (lsuc l2) 2))
( comp-hom-Group
( symmetric-Group (Fin-Set (n +ℕ 2)))
( symmetric-Group (Fin-Set 2))
( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2))
( group-Concrete-Group (UU-Fin-Group (lsuc l2) 2))
( symmetric-abstract-UU-fin-group-quotient-hom
( λ n X → type-UU-Fin 2 (Q n X))
( λ n X → Id-Equivalence-Relation (set-UU-Fin 2 (Q n X)))
Expand Down

0 comments on commit 52fdf4c

Please sign in to comment.