Univalent Groups
Table of Contents
1 Groups
module Lib.Groups where
This file defines the type of groups in univalent mathematics. It also shows that isomorphic groups can be identified.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.SubTypes import Lib.Univalence import Lib.Prop.Htpy import Lib.Prop.Levels import Lib.Prop.Proposition import Lib.Prop.Set
1.2 Semi-group (definitions, accessors)
1.2.1 Definition, universe
An operation μ is associative whenever there is a witness μ (μ x y) z = μ x (μ y z).
is-assoc (X : U) (f : X → X → X) : U = (x y z : X) → Path X (f (f x y) z) (f x (f y z))
A semi-group is a set together with an associative operation.
has-assoc-op (X : U) : U = Σ (X → X → X) (is-assoc X) is-semi-group (X : UU-Set) : U = has-assoc-op (Set/type X) Semigroup : U = Σ UU-Set is-semi-group
1.2.2 Accessors
Semigroup/Set (G : Semigroup) : UU-Set = G.1 Semigroup/is-semi-group (G : Semigroup) : is-semi-group (Semigroup/Set G) = G.2 Semigroup/type (G : Semigroup) : U = Set/type (Semigroup/Set G) Semigroup/is-set (G : Semigroup) : is-set (Semigroup/type G) = (Semigroup/Set G).2 Semigroup/op (G : Semigroup) : (Semigroup/type G) → (Semigroup/type G) → (Semigroup/type G) = (Semigroup/is-semi-group G).1 Semigroup/is-assoc (G : Semigroup) : is-assoc (Semigroup/type G) (Semigroup/op G) = (Semigroup/is-semi-group G).2 Semigroup/map (G : Semigroup) (H : Semigroup) : U = Semigroup/type G → Semigroup/type H
1.3 Monoid (definitions, accessors)
1.3.1 Definition
A semi-group is unital if there is a unit e : G that satisfies the left and right unit laws.
left-unit-law (G : Semigroup) (e : Semigroup/type G) : U = (y : Semigroup/type G) → Path (Semigroup/type G) (Semigroup/op G e y) y right-unit-law (G : Semigroup) (e : Semigroup/type G) : U = (x : Semigroup/type G) → Path (Semigroup/type G) (Semigroup/op G x e) x is-unital (G : Semigroup) : U = Σ (Semigroup/type G) (λe. (left-unit-law G e) * (right-unit-law G e))
Unital semi-groups are called monoids. As such, we can define the universe of monoids.
Monoid : U = Σ Semigroup is-unital
1.3.2 Accessors
Monoid/Semigroup (M : Monoid) : Semigroup = M.1 Monoid/is-unital (M : Monoid) : is-unital (Monoid/Semigroup M) = M.2 Monoid/Set (M : Monoid) : UU-Set = Semigroup/Set (Monoid/Semigroup M) Monoid/is-semi-group (M : Monoid) : is-semi-group (Monoid/Set M) = Semigroup/is-semi-group (Monoid/Semigroup M) Monoid/type (M : Monoid) : U = Set/type (Monoid/Set M) Monoid/is-set (M : Monoid) : is-set (Monoid/type M) = Set/is-set (Monoid/Set M) Monoid/op (M : Monoid) : (Monoid/type M) → (Monoid/type M) → (Monoid/type M) = (Semigroup/op (Monoid/Semigroup M)) Monoid/is-assoc (M : Monoid) : is-assoc (Monoid/type M) (Monoid/op M) = (Semigroup/is-assoc (Monoid/Semigroup M)) Monoid/unit (M : Monoid) : (Monoid/type M) = (Monoid/is-unital M).1 Monoid/left-unit-law (M : Monoid) : left-unit-law (Monoid/Semigroup M) (Monoid/unit M) = (Monoid/is-unital M).2.1 Monoid/right-unit-law (M : Monoid) : right-unit-law (Monoid/Semigroup M) (Monoid/unit M) = (Monoid/is-unital M).2.2
1.3.3 Is property
The unit of a semi-group is unique when it exists. We show this by showing that being unital is a property of semi-groups rather than a structure on it, that is, we show that is-unital is a proposition.
is-unital/is-prop/sg (X : U) (is-set-X : is-set X) (f : X → X → X) (assoc-f : (x y z : X) → Path X (f (f x y) z) (f x (f y z))) (e : X) (left-unit : left-unit-law ((X, is-set-X), (f, assoc-f)) e) (right-unit : right-unit-law ((X, is-set-X), (f, assoc-f)) e) (e' : X) (left-unit' : left-unit-law ((X, is-set-X), (f, assoc-f)) e') (right-unit' : right-unit-law ((X, is-set-X), (f, assoc-f)) e') : Path (is-unital ((X, is-set-X), (f, assoc-f))) (e, (left-unit, right-unit)) (e', (left-unit', right-unit')) = let G : Semigroup = ((X, is-set-X), (f, assoc-f)) in SgPath-prop X (λz. (left-unit-law G z) * (right-unit-law G z)) (λz. is-prop/prod (left-unit-law G z) (right-unit-law G z) (is-prop/pi X (λy. Path X (f z y) y) (λy. is-set-X (f z y) y)) (is-prop/pi X (λx. Path X (f x z) x) (λx. is-set-X (f x z) x))) (e, (left-unit, right-unit)) (e', (left-unit', right-unit')) (comp X e (f e e') (inv X (f e e') e (right-unit' e)) e' (left-unit e')) is-unital/is-prop (G : Semigroup) : is-prop (is-unital G) = λx y. is-unital/is-prop/sg (Semigroup/type G) (Set/is-set (Semigroup/Set G)) (Semigroup/op G) (Semigroup/is-assoc G) x.1 x.2.1 x.2.2 y.1 y.2.1 y.2.2
1.4 Invertible monoids
A monoid is invertible if ∀ x : M, there exists x-1 such that x ⋅ x-1 = e and x-1 ⋅ x = e.
is-invertible-Monoid (M : Monoid) (x : Monoid/type M) : U = Σ (Monoid/type M) (λy. (Path (Monoid/type M) (Monoid/op M y x) (Monoid/unit M)) * (Path (Monoid/type M) (Monoid/op M x y) (Monoid/unit M)))
Once again, being invertible is a property of monoids.
is-invertible-Monoid/is-prop/sg (M : Monoid) (x : Monoid/type M) (y : Monoid/type M) (p : Path (Monoid/type M) (Monoid/op M y x) (Monoid/unit M)) (q : Path (Monoid/type M) (Monoid/op M x y) (Monoid/unit M)) (y' : Monoid/type M) (p' : Path (Monoid/type M) (Monoid/op M y' x) (Monoid/unit M)) (q' : Path (Monoid/type M) (Monoid/op M x y') (Monoid/unit M)) : Path (is-invertible-Monoid M x) (y, (p, q)) (y', (p', q')) = let X : U = Monoid/type M f : X → X → X = Monoid/op M e : X = Monoid/unit M in SgPath-prop X (λz. (Path X (f z x) e) * (Path X (f x z) e)) (λz. is-prop/prod (Path X (f z x) e) (Path X (f x z) e) (Monoid/is-set M (f z x) e) (Monoid/is-set M (f x z) e)) (y, (p, q)) (y', (p', q')) (comp-n X five-Nat y (f e y) (inv X (f e y) y (Monoid/left-unit-law M y)) (f (f y' x) y) (ap X X (λz. f z y) e (f y' x) (inv X (f y' x) e p')) (f y' (f x y)) (Monoid/is-assoc M y' x y) (f y' e) (ap X X (f y') (f x y) e q) y' (Monoid/right-unit-law M y')) is-invertible-Monoid/is-prop (M : Monoid) (x : Monoid/type M) : is-prop (is-invertible-Monoid M x) = λy z. is-invertible-Monoid/is-prop/sg M x y.1 y.2.1 y.2.2 z.1 z.2.1 z.2.2
1.5 Groups
1.5.1 Definition
A group is a monoid such that all its elements are invertible.
left-inv (M : Monoid) (x y : Monoid/type M) : U = Path (Monoid/type M) (Monoid/op M y x) (Monoid/unit M) right-inv (M : Monoid) (x y : Monoid/type M) : U = Path (Monoid/type M) (Monoid/op M x y) (Monoid/unit M) is-group' (G : Semigroup) (e : is-unital G) : U = Σ (Semigroup/map G G) (λi. ((x : Semigroup/type G) → left-inv (G, e) x (i x)) * ((x : Semigroup/type G) → right-inv (G, e) x (i x))) is-group (G : Semigroup) : U = Σ (is-unital G) (is-group' G) Group : U = Σ Semigroup is-group
1.5.2 Accessors
Group/Semigroup (G : Group) : Semigroup = G.1 Group/is-group (G : Group) : is-group (Group/Semigroup G) = G.2 Group/Set (G : Group) : UU-Set = Semigroup/Set (Group/Semigroup G) Group/type (G : Group) : U = Semigroup/type (Group/Semigroup G) Group/is-set (G : Group) : is-set (Group/type G) = (Group/Set G).2 Group/is-unital (G : Group) : is-unital (Group/Semigroup G) = (Group/is-group G).1 Group/Monoid (G : Group) : Monoid = (Group/Semigroup G, Group/is-unital G) Group/is-semi-group (G : Group) : is-semi-group (Group/Set G) = Monoid/is-semi-group (Group/Monoid G) Group/op (G : Group) : (Group/type G) → (Group/type G) → (Group/type G) = Semigroup/op (Group/Semigroup G) Group/is-assoc (G : Group) : is-assoc (Group/type G) (Group/op G) = Semigroup/is-assoc (Group/Semigroup G) Group/map (G H : Group) : U = Group/type G → Group/type H Group/unit (G : Group) : Group/type G = Monoid/unit (Group/Monoid G) Group/left-unit-law (G : Group) : left-unit-law (Group/Semigroup G) (Group/unit G) = Monoid/left-unit-law (Group/Monoid G) Group/right-unit-law (G : Group) : right-unit-law (Group/Semigroup G) (Group/unit G) = Monoid/right-unit-law (Group/Monoid G) Group/inv (G : Group) : Group/map G G = (Group/is-group G).2.1 Group/left-inv (G : Group) : (x : Group/type G) → left-inv (Group/Monoid G) x (Group/inv G x) = (Group/is-group G).2.2.1 Group/right-inv (G : Group) : (x : Group/type G) → right-inv (Group/Monoid G) x (Group/inv G x) = (Group/is-group G).2.2.2
1.5.3 Property
is-group is a proposition.
is-group'/is-prop/sg (G : Semigroup) (e : Semigroup/type G) (left-unit : left-unit-law G e) (right-unit : right-unit-law G e) (i : Semigroup/map G G) (left-inv-i : (x : Semigroup/type G) → left-inv (G, (e, (left-unit, right-unit))) x (i x)) (right-inv-i : (x : Semigroup/type G) → right-inv (G, (e, (left-unit, right-unit))) x (i x)) (i' : Semigroup/map G G) (left-inv-i' : (x : Semigroup/type G) → left-inv (G, (e, (left-unit, right-unit))) x (i' x)) (right-inv-i' : (x : Semigroup/type G) → right-inv (G, (e, (left-unit, right-unit))) x (i' x)) : Path (is-group' G (e, (left-unit, right-unit))) (i, (left-inv-i, right-inv-i)) (i', (left-inv-i', right-inv-i')) = let X : U = Semigroup/type G f : X → X → X = Semigroup/op G in SgPath-prop (X → X) (λg. ((x : X) → Path X (f (g x) x) e) * ((x : X) → Path X (f x (g x)) e)) (λg. is-prop/prod ((x : X) → Path X (f (g x) x) e) ((x : X) → Path X (f x (g x)) e) (is-prop/pi X (λx. Path X (f (g x) x) e) (λx. Semigroup/is-set G (f (g x) x) e)) (is-prop/pi X (λx. Path X (f x (g x)) e) (λx. Semigroup/is-set G (f x (g x)) e))) (i, (left-inv-i, right-inv-i)) (i', (left-inv-i', right-inv-i')) (eq-htpy' X X i i' (λx. (comp-n X five-Nat (i x) (f e (i x)) (inv X (f e (i x)) (i x) (left-unit (i x))) (f (f (i' x) x) (i x)) (ap X X (λz. f z (i x)) e (f (i' x) x) (inv X (f (i' x) x) e (left-inv-i' x))) (f (i' x) (f x (i x))) (Semigroup/is-assoc G (i' x) x (i x)) (f (i' x) e) (ap X X (f (i' x)) (f x (i x)) e (right-inv-i x)) (i' x) (right-unit (i' x))))) is-group'/is-prop (G : Semigroup) (e : is-unital G) : is-prop (is-group' G e) = λx y. is-group'/is-prop/sg G e.1 e.2.1 e.2.2 x.1 x.2.1 x.2.2 y.1 y.2.1 y.2.2 is-group/is-prop (G : Semigroup) : is-prop (is-group G) = is-prop/sg (is-unital G) (is-group' G) (is-unital/is-prop G) (is-group'/is-prop G)
1.6 Semigroups homomorphisms
1.6.1 Definition
If f is a function between two (semi-)groups G and H with associative operations μG and μH, f is a (semi-)group homomorphism if f(μG x y) = μH (f x) (f y) for any x, y of G.
preserves-mul (A B : U) (f : A → B) (g : A → A → A) (h : B → B → B) : U = (x y : A) → Path B (f (g x y)) (h (f x) (f y))
Of course, a function preserving multiplication between semi-groups is a property rather than a structure, thus we can show that preserves-mul is a proposition.
Semigroup/preserves-mul (G H : Semigroup) (f : Semigroup/map G H) : U = preserves-mul (Semigroup/type G) (Semigroup/type H) f (Semigroup/op G) (Semigroup/op H) preserves-mul/is-prop (G H : Semigroup) (f : Semigroup/map G H) : is-prop (Semigroup/preserves-mul G H f) = is-prop/pi ( Semigroup/type G) ( λx. (y : Semigroup/type G) → Path (Semigroup/type H) (f (Semigroup/op G x y)) (Semigroup/op H (f x) (f y))) ( λx. is-prop/pi ( Semigroup/type G) ( λy. Path (Semigroup/type H) (f (Semigroup/op G x y)) (Semigroup/op H (f x) (f y))) ( λy. Semigroup/is-set H (f (Semigroup/op G x y)) (Semigroup/op H (f x) (f y))))
We can hence define the type of homomorphisms for (semi-)groups.
Semigroup/hom (G H : Semigroup) : U = Σ (Semigroup/map G H) (Semigroup/preserves-mul G H)
1.6.2 Accessors
Semigroup/hom/map (G H : Semigroup) (f : Semigroup/hom G H) : Semigroup/map G H = f.1 Semigroup/hom/preserves-mul (G H : Semigroup) (f : Semigroup/hom G H) : Semigroup/preserves-mul G H (Semigroup/hom/map G H f) = f.2
1.6.3 Identity homomorphism
Semigroup/hom/id (G : Semigroup) : Semigroup/hom G G = (id (Semigroup/type G), λx y. refl (Semigroup/type G) (Semigroup/op G x y))
1.6.4 Characterization of identity
As it is a property for a function to preserve multiplication, the equality of semi-group homomorphisms is equivalent to the type of homotopies between the underlying functions. First, we show that an identity between homomorphisms implies homotopy between the underlying maps.
Semigroup/htpy (G H : Semigroup) (f g : Semigroup/hom G H) : U = Htpy' (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H f) (Semigroup/hom/map G H g) Semigroup/hom/htpy/refl (G H : Semigroup) (f : Semigroup/hom G H) : Semigroup/htpy G H f f = Htpy'/refl (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H f) Semigroup/hom/htpy (G H : Semigroup) (f g : Semigroup/hom G H) (p : Path (Semigroup/hom G H) f g) : Semigroup/htpy G H f g = J (Semigroup/hom G H) f (λh _. Htpy' (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H f) (Semigroup/hom/map G H h)) (Semigroup/hom/htpy/refl G H f) g p
Then, we show that the above map is an equivalence. To do so, we use the fundamental theorem and hence we need to show that the total space Σ (Semigroup/hom G H) (Semigroup/hom/htpy G H) is contractible.
Semigroup/hom/htpy/is-contr (G H : Semigroup) (f : Semigroup/hom G H) : is-contr (Σ (Semigroup/hom G H) (Semigroup/htpy G H f)) = substructure/is-contr-total-Eq ( Semigroup/map G H) ( λg. Htpy' (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H f) g) ( λg. Semigroup/preserves-mul G H g) ( Htpy/is-contr-total-htpy (Semigroup/type G) (λ_. Semigroup/type H) (Semigroup/hom/map G H f)) ( preserves-mul/is-prop G H) ( Semigroup/hom/map G H f) ( Htpy'/refl (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H f)) ( Semigroup/hom/preserves-mul G H f)
We can conclude that Semigroup/hom/htpy is a family of equivalences.
Semigroup/hom/htpy/is-equiv (G H : Semigroup) (f : Semigroup/hom G H) : (g : Semigroup/hom G H) → is-equiv (Path (Semigroup/hom G H) f g) (Semigroup/htpy G H f g) (Semigroup/hom/htpy G H f g) = fundamental-theorem-id (Semigroup/hom G H) (Semigroup/htpy G H f) f (Semigroup/hom/htpy G H f) (Semigroup/hom/htpy/is-contr G H f) Semigroup/hom/htpy/Equiv (G H : Semigroup) (f g : Semigroup/hom G H) : Equiv (Path (Semigroup/hom G H) f g) (Semigroup/htpy G H f g) = (Semigroup/hom/htpy G H f g, Semigroup/hom/htpy/is-equiv G H f g)
Thus, we have a map from homotopies to paths.
Semigroup/hom/Eq (G H : Semigroup) (f g : Semigroup/hom G H) : (Htpy' (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H f) (Semigroup/hom/map G H g)) → Path (Semigroup/hom G H) f g = is-equiv/inv-map (Path (Semigroup/hom G H) f g) (Semigroup/htpy G H f g) (Semigroup/hom/htpy G H f g) (Semigroup/hom/htpy/is-equiv G H f g)
As such, the homomorphisms between semi-groups is a set: their identity types are equivalent to homotopies, i.e., to functions over propositions (as the identity types of H are propositions).
Semigroup/hom/is-set (G H : Semigroup) : is-set (Semigroup/hom G H) = λf g. is-prop/closed-equiv (Path (Semigroup/hom G H) f g) (Semigroup/htpy G H f g) (Semigroup/hom/htpy/Equiv G H f g) (is-prop/pi (Semigroup/type G) (λx. Path (Semigroup/type H) (Semigroup/hom/map G H f x) (Semigroup/hom/map G H g x)) (λx. Semigroup/is-set H (Semigroup/hom/map G H f x) (Semigroup/hom/map G H g x)))
1.6.5 Closure under composition
Semigroup/hom/comp/map (G H K : Semigroup) (g : Semigroup/hom H K) (f : Semigroup/hom G H) : (Semigroup/map G K) = λz. Semigroup/hom/map H K g (Semigroup/hom/map G H f z) Semigroup/hom/comp/preserves-mul (G H K : Semigroup) (f : Semigroup/hom G H) (g : Semigroup/hom H K) : Semigroup/preserves-mul G K (Semigroup/hom/comp/map G H K g f) = let m : Semigroup/map G H = Semigroup/hom/map G H f m' : Semigroup/map H K = Semigroup/hom/map H K g mg : Semigroup/type G → Semigroup/type G → Semigroup/type G = Semigroup/op G mh : Semigroup/type H → Semigroup/type H → Semigroup/type H = Semigroup/op H mk : Semigroup/type K → Semigroup/type K → Semigroup/type K = Semigroup/op K in λx y. comp (Semigroup/type K) (Semigroup/hom/comp/map G H K g f (mg x y)) (m' (mh (m x) (m y))) (ap (Semigroup/type H) (Semigroup/type K) m' (m (mg x y)) (mh (m x) (m y)) (Semigroup/hom/preserves-mul G H f x y)) (mk (m' (m x)) (m' (m y))) (Semigroup/hom/preserves-mul H K g (m x) (m y)) Semigroup/hom/comp (G H K : Semigroup) (g : Semigroup/hom H K) (f : Semigroup/hom G H) : Semigroup/hom G K = (Semigroup/hom/comp/map G H K g f, Semigroup/hom/comp/preserves-mul G H K f g)
1.6.6 Laws of a category
It is easy to show that homomorphisms follow the laws of a category using the identifications of homomorphic types. First, we show that id is left unit ;
Semigroup/hom/left-unit-law (G H : Semigroup) (f : Semigroup/hom G H) : Path (Semigroup/hom G H) (Semigroup/hom/comp G H H (Semigroup/hom/id H) f) f = Semigroup/hom/Eq G H (Semigroup/hom/comp G H H (Semigroup/hom/id H) f) f (λx. refl (Semigroup/type H) (Semigroup/hom/map G H f x))
And right unit.
Semigroup/hom/right-unit-law (G H : Semigroup) (f : Semigroup/hom G H) : Path (Semigroup/hom G H) (Semigroup/hom/comp G G H f (Semigroup/hom/id G)) f = Semigroup/hom/Eq G H (Semigroup/hom/comp G G H f (Semigroup/hom/id G)) f (λx. refl (Semigroup/type H) (Semigroup/hom/map G H f x))
Finally, composition is associative.
Semigroup/hom/comp/assoc (G H K L : Semigroup) (f : Semigroup/hom G H) (g : Semigroup/hom H K) (h : Semigroup/hom K L) : Path (Semigroup/hom G L) (Semigroup/hom/comp G K L h (Semigroup/hom/comp G H K g f)) (Semigroup/hom/comp G H L (Semigroup/hom/comp H K L h g) f) = Semigroup/hom/Eq G L ( Semigroup/hom/comp G K L h (Semigroup/hom/comp G H K g f)) ( Semigroup/hom/comp G H L (Semigroup/hom/comp H K L h g) f) ( λx. refl ( Semigroup/type L) ( Semigroup/hom/map K L h (Semigroup/hom/map H K g (Semigroup/hom/map G H f x))))
1.6.7 Isomorphisms
An isomorphism is a bijective homomorphism.
Semigroup/hom/left-inv (G H : Semigroup) (h : Semigroup/hom G H) (h' : Semigroup/hom H G) : U = Path (Semigroup/hom G G) (Semigroup/hom/comp G H G h' h) (Semigroup/hom/id G) Semigroup/hom/right-inv (G H : Semigroup) (h : Semigroup/hom G H) (h' : Semigroup/hom H G) : U = Path (Semigroup/hom H H) (Semigroup/hom/comp H G H h h') (Semigroup/hom/id H) Semigroup/is-iso (G H : Semigroup) (h : Semigroup/hom G H) : U = Σ (Semigroup/hom H G) (λh'. (Semigroup/hom/left-inv G H h h') * (Semigroup/hom/right-inv G H h h')) Semigroup/is-iso/hom (G H : Semigroup) (h : Semigroup/hom G H) (i : Semigroup/is-iso G H h) : Semigroup/hom H G = i.1 Semigroup/is-iso/map (G H : Semigroup) (h : Semigroup/hom G H) (i : Semigroup/is-iso G H h) : Semigroup/map H G = Semigroup/hom/map H G (Semigroup/is-iso/hom G H h i) Semigroup/is-iso/left-htpy (G H : Semigroup) (h : Semigroup/hom G H) (i : Semigroup/is-iso G H h) : Semigroup/hom/left-inv G H h (Semigroup/is-iso/hom G H h i) = i.2.1 Semigroup/is-iso/right-htpy (G H : Semigroup) (h : Semigroup/hom G H) (i : Semigroup/is-iso G H h) : Semigroup/hom/right-inv G H h (Semigroup/is-iso/hom G H h i) = i.2.2 Semigroup/Iso (G H : Semigroup) : U = Σ (Semigroup/hom G H) (Semigroup/is-iso G H) Semigroup/Iso/hom (G H : Semigroup) (i : Semigroup/Iso G H) : Semigroup/hom G H = i.1 Semigroup/Iso/inv-map (G H : Semigroup) (i : Semigroup/Iso G H) : Semigroup/hom H G = Semigroup/is-iso/hom G H (Semigroup/Iso/hom G H i) i.2 Semigroup/Iso/left-htpy (G H : Semigroup) (i : Semigroup/Iso G H) : Semigroup/hom/left-inv G H (Semigroup/Iso/hom G H i) (Semigroup/Iso/inv-map G H i) = Semigroup/is-iso/left-htpy G H (Semigroup/Iso/hom G H i) i.2 Semigroup/Iso/right-htpy (G H : Semigroup) (i : Semigroup/Iso G H) : Semigroup/hom/right-inv G H (Semigroup/Iso/hom G H i) (Semigroup/Iso/inv-map G H i) = Semigroup/is-iso/right-htpy G H (Semigroup/Iso/hom G H i) i.2
Of course, being an isomorphism is still a property.
Semigroup/is-iso/is-prop (G H : Semigroup) (h : Semigroup/hom G H) : is-prop (Semigroup/is-iso G H h) = λk k'. let f : Semigroup/hom H G = Semigroup/is-iso/hom G H h k f' : Semigroup/hom H G = Semigroup/is-iso/hom G H h k' in SgPath-prop ( Semigroup/hom H G) ( λi. (Semigroup/hom/left-inv G H h i) * (Semigroup/hom/right-inv G H h i)) ( λi. is-prop/prod ( Semigroup/hom/left-inv G H h i) ( Semigroup/hom/right-inv G H h i) ( Semigroup/hom/is-set G G (Semigroup/hom/comp G H G i h) (Semigroup/hom/id G)) ( Semigroup/hom/is-set H H (Semigroup/hom/comp H G H h i) (Semigroup/hom/id H))) k k' ( comp-n ( Semigroup/hom H G) five-Nat f ( Semigroup/hom/comp H H G f (Semigroup/hom/id H)) ( inv ( Semigroup/hom H G) ( Semigroup/hom/comp H H G f (Semigroup/hom/id H)) f ( Semigroup/hom/right-unit-law H G f)) ( Semigroup/hom/comp H H G f ( Semigroup/hom/comp H G H h f')) ( ap ( Semigroup/hom H H) ( Semigroup/hom H G) ( λg. (Semigroup/hom/comp H H G f g)) ( Semigroup/hom/id H) ( Semigroup/hom/comp H G H h f') ( inv ( Semigroup/hom H H) ( Semigroup/hom/comp H G H h f') ( Semigroup/hom/id H) ( Semigroup/is-iso/right-htpy G H h k'))) ( Semigroup/hom/comp H G G ( Semigroup/hom/comp G H G f h) f') ( Semigroup/hom/comp/assoc H G H G f' h f) ( Semigroup/hom/comp H G G ( Semigroup/hom/id G) f') ( ap ( Semigroup/hom G G) ( Semigroup/hom H G) ( λg. (Semigroup/hom/comp H G G g f')) ( Semigroup/hom/comp G H G f h) ( Semigroup/hom/id G) ( Semigroup/is-iso/left-htpy G H h k)) f' ( Semigroup/hom/left-unit-law H G f'))
1.6.8 Iso G G
id is an isomorphism.
Semigroup/Iso/id (G : Semigroup) : Semigroup/Iso G G = ( Semigroup/hom/id G, ( Semigroup/hom/id G, ( Semigroup/hom/Eq G G (Semigroup/hom/comp G G G (Semigroup/hom/id G) (Semigroup/hom/id G)) (Semigroup/hom/id G) (λx. refl (Semigroup/type G) x), Semigroup/hom/Eq G G (Semigroup/hom/comp G G G (Semigroup/hom/id G) (Semigroup/hom/id G)) (Semigroup/hom/id G) (λx. refl (Semigroup/type G) x))))
1.7 Isomorphic semi-groups are equal
We show that isomorphic groups can be identified. First, we show that a semi-group homomorphism h is an isomorphism iff its underlying map is an equivalence. If a homomorphism is an isomorphism, then the underlying inverse map provides an inverse.
Semigroup/hom/is-iso/is-equiv (G H : Semigroup) (h : Semigroup/hom G H) (i : Semigroup/is-iso G H h) : is-equiv (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H h) = has-inverse/is-equiv ( Semigroup/type G) ( Semigroup/type H) ( Semigroup/hom/map G H h) ( Semigroup/is-iso/map G H h i, ( Semigroup/hom/htpy H H (Semigroup/hom/comp H G H h (Semigroup/is-iso/hom G H h i)) (Semigroup/hom/id H) (Semigroup/is-iso/right-htpy G H h i), Semigroup/hom/htpy G G (Semigroup/hom/comp G H G (Semigroup/is-iso/hom G H h i) h) (Semigroup/hom/id G) (Semigroup/is-iso/left-htpy G H h i)))
For the converse, assume that the underlying map is an equivalence. Then its inverse is also a semi-group homomorphism, since we have the following chain of equations: f-1(μH x y) = f-1(μH (f (f-1 x)) (f (f-1 y))) = f-1(f (μG (f-1 x) (f-1 y))) = μG (f-1 x) (f-1 y)
Semigroup/hom/is-equiv/is-iso/hom (G H : Semigroup) (h : Semigroup/hom G H) (e : is-equiv (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H h)) : Semigroup/hom H G = let f : Semigroup/map G H = Semigroup/hom/map G H h h' : Semigroup/map H G = is-equiv/inv-map (Semigroup/type G) (Semigroup/type H) f e muG : Semigroup/type G → (Semigroup/map G G) = Semigroup/op G muH : Semigroup/type H → (Semigroup/map H H) = Semigroup/op H in ( h', λx y. comp-n ( Semigroup/type G) four-Nat ( h' (muH x y)) ( h' (muH (f (h' x)) y)) ( ap ( Semigroup/type H) ( Semigroup/type G) ( λz. h' (muH z y)) x ( f (h' x)) ( inv ( Semigroup/type H) ( f (h' x)) x ( is-equiv/inv-right-htpy (Semigroup/type G) (Semigroup/type H) f e x))) ( h' (muH (f (h' x)) (f (h' y)))) ( ap ( Semigroup/type H) ( Semigroup/type G) ( λz. h' (muH (f (h' x)) z)) y ( f (h' y)) ( inv ( Semigroup/type H) ( f (h' y)) y ( is-equiv/inv-right-htpy (Semigroup/type G) (Semigroup/type H) f e y))) ( h' (f (muG (h' x) (h' y)))) ( ap ( Semigroup/type H) ( Semigroup/type G) h' ( muH (f (h' x)) (f (h' y))) (f (muG (h' x) (h' y))) ( inv ( Semigroup/type H) ( f (muG (h' x) (h' y))) ( muH (f (h' x)) (f (h' y))) ( Semigroup/hom/preserves-mul G H h (h' x) (h' y)))) ( muG (h' x) (h' y)) ( is-equiv/inv-left-htpy (Semigroup/type G) (Semigroup/type H) f e (muG (h' x) (h' y)))) Semigroup/hom/is-equiv/is-iso (G H : Semigroup) (h : Semigroup/hom G H) (e : is-equiv (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H h)) : Semigroup/is-iso G H h = let h' : Semigroup/hom H G = Semigroup/hom/is-equiv/is-iso/hom G H h e in ( h', ( Semigroup/hom/Eq G G ( Semigroup/hom/comp G H G h' h) ( Semigroup/hom/id G) ( is-equiv/inv-left-htpy ( Semigroup/type G) ( Semigroup/type H) ( Semigroup/hom/map G H h) e), Semigroup/hom/Eq H H ( Semigroup/hom/comp H G H h h') ( Semigroup/hom/id H) ( is-equiv/inv-right-htpy ( Semigroup/type G) ( Semigroup/type H) ( Semigroup/hom/map G H h) e)))
That is, there is an equivalence between Iso G H and Σ (e : G ≅ H) e(μG x y) = μH (e x) (e y).
Semigroup/Iso/Equiv/type (G H : Semigroup) : U = (Σ ( Equiv (Semigroup/type G) (Semigroup/type H)) ( λe. preserves-mul ( Semigroup/type G) ( Semigroup/type H) ( Equiv/map (Semigroup/type G) (Semigroup/type H) e) ( Semigroup/op G) ( Semigroup/op H))) Semigroup/Iso/Equiv (G H : Semigroup) : Equiv (Semigroup/Iso G H) (Semigroup/Iso/Equiv/type G H) = Equiv/trans ( Semigroup/Iso G H) ( Σ (Semigroup/hom G H) (λh. is-equiv (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H h))) ( Semigroup/Iso/Equiv/type G H) ( subtype/Equiv-tot ( Semigroup/hom G H) ( Semigroup/is-iso G H) ( λh. is-equiv (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H h)) ( Semigroup/is-iso/is-prop G H) ( λh. is-equiv/is-prop (Semigroup/type G) (Semigroup/type H) (Semigroup/hom/map G H h)) ( Semigroup/hom/is-iso/is-equiv G H) ( Semigroup/hom/is-equiv/is-iso G H)) ( Equiv/assoc-Sg ( Semigroup/map G H) ( Semigroup/preserves-mul G H) ( is-equiv (Semigroup/type G) (Semigroup/type H)))
We define the family of maps iso-eq : G = H → Iso G H by path induction.
Semigroup/iso-eq (G H : Semigroup) (p : Path Semigroup G H) : Semigroup/Iso G H = J Semigroup G ( λK _. Semigroup/Iso G K) ( Semigroup/Iso/id G) H p
Then, we show that this family of maps is a family of equivalences. First, we show that the sigma-type Σ (has-assoc-op G) preserves-mul is contractible.
preserves-mul-id/type (G : Semigroup) : U = Σ (has-assoc-op (Semigroup/type G)) (λmu. Semigroup/preserves-mul G (Semigroup/Set G, mu) (id (Semigroup/type G))) preserves-mul-id/center (G : Semigroup) : preserves-mul-id/type G = ( Semigroup/is-semi-group G, λx y. refl (Semigroup/type G) (Semigroup/op G x y)) preserves-mul-id/contraction (G : Semigroup) (t : preserves-mul-id/type G) : Path (preserves-mul-id/type G) (preserves-mul-id/center G) t = SgPath-prop ( has-assoc-op (Semigroup/type G)) ( λmu. Semigroup/preserves-mul G (Semigroup/Set G, mu) (id (Semigroup/type G))) ( λmu. preserves-mul/is-prop G (Semigroup/Set G, mu) (id (Semigroup/type G))) ( preserves-mul-id/center G) t ( SgPath-prop ( Semigroup/type G → Semigroup/type G → Semigroup/type G) ( is-assoc (Semigroup/type G)) ( λmu. is-prop/pi ( Semigroup/type G) ( λx. (y z : Semigroup/type G) → Path (Semigroup/type G) (mu (mu x y) z) (mu x (mu y z))) ( λx. is-prop/pi ( Semigroup/type G) ( λy. (z : Semigroup/type G) → Path (Semigroup/type G) (mu (mu x y) z) (mu x (mu y z))) ( λy. is-prop/pi ( Semigroup/type G) ( λz. Path (Semigroup/type G) (mu (mu x y) z) (mu x (mu y z))) ( λz. Semigroup/is-set G (mu (mu x y) z) (mu x (mu y z)))))) ( preserves-mul-id/center G).1 t.1 ( eq-htpy' ( Semigroup/type G) ( Semigroup/map G G) ( preserves-mul-id/center G).1.1 t.1.1 ( λx. eq-htpy' ( Semigroup/type G) ( Semigroup/type G) (( preserves-mul-id/center G).1.1 x) ( t.1.1 x) ( λy. t.2 x y)))) preserves-mul-id/is-contr (G : Semigroup) : is-contr (preserves-mul-id/type G) = ( preserves-mul-id/center G, preserves-mul-id/contraction G)
Then, we can show the desired property.
Semigroup/iso-eq/is-contr-Equiv-type (G : Semigroup) : is-contr (Σ Semigroup (Semigroup/Iso/Equiv/type G)) = str-principle-id UU-Set is-semi-group ( λH. Equiv (Semigroup/type G) (Set/type H)) ( λH is-semi-group-H e. preserves-mul ( Semigroup/type G) ( Set/type H) ( Equiv/map (Semigroup/type G) (Set/type H) e) ( Semigroup/op G) ( is-semi-group-H.1)) ( substructure/is-contr-total-Eq U ( Equiv (Semigroup/type G)) ( is-set) ( ua/is-contr-total-equiv (Semigroup/type G)) ( is-set/is-prop) ( Semigroup/type G) ( Equiv/refl (Semigroup/type G)) ( Semigroup/is-set G)) ( Semigroup/Set G) ( Equiv/refl (Semigroup/type G)) ( preserves-mul-id/is-contr G) Semigroup/iso-eq/contr-Iso (G : Semigroup) : is-contr (Σ Semigroup (Semigroup/Iso G)) = ( is-contr/is-contr-equiv ( Σ Semigroup (Semigroup/Iso G)) ( Σ Semigroup (Semigroup/Iso/Equiv/type G)) ( Equiv/Sg-fam Semigroup ( Semigroup/Iso G) ( Semigroup/Iso/Equiv/type G) ( λH. Semigroup/Iso/Equiv G H)) ( Semigroup/iso-eq/is-contr-Equiv-type G)) lock Semigroup/hom/htpy/is-equiv Semigroup/iso-eq/is-equiv (G : Semigroup) : (H : Semigroup) → is-equiv (Path Semigroup G H) (Semigroup/Iso G H) (Semigroup/iso-eq G H) = fundamental-theorem-id Semigroup ( Semigroup/Iso G) G ( Semigroup/iso-eq G) ( Semigroup/iso-eq/contr-Iso G)
Thus, isomorphic semi-groups are identifiable.
Semigroup/eq-iso (G H : Semigroup) : Semigroup/Iso G H → Path Semigroup G H = is-equiv/inv-map ( Path Semigroup G H) ( Semigroup/Iso G H) ( Semigroup/iso-eq G H) ( Semigroup/iso-eq/is-equiv G H)
1.8 Group homomorphisms
1.8.1 Definition
We define group homomorphisms similarly to semi-group homomorphisms.
Group/preserves-mul (G H : Group) (f : Group/map G H) : U = Semigroup/preserves-mul ( Group/Semigroup G) ( Group/Semigroup H) f Group/hom (G H : Group) : U = Semigroup/hom ( Group/Semigroup G) ( Group/Semigroup H)
They come with the same accessors.
Group/hom/map (G H : Group) (f : Group/hom G H) : Group/map G H = Semigroup/hom/map ( Group/Semigroup G) ( Group/Semigroup H) f Group/hom/preserves-mul (G H : Group) (f : Group/hom G H) : Group/preserves-mul G H (Group/hom/map G H f) = Semigroup/hom/preserves-mul ( Group/Semigroup G) ( Group/Semigroup H) f
Of course, all the properties of semi-group homomorphisms carry on to group homomorphisms. We can define them all if needed, but we don't need everything for now.
1.8.2 Identity and Composition
Identity group homomorphism:
Group/hom/id (G : Group) : Group/hom G G = Semigroup/hom/id ( Group/Semigroup G)
Composition of group homomorphisms:
Group/hom/comp (G H K : Group) (g : Group/hom H K) (f : Group/hom G H) : Group/hom G K = Semigroup/hom/comp ( Group/Semigroup G) ( Group/Semigroup H) ( Group/Semigroup K) g f
1.8.3 Isomorphisms
We define group isomorphisms similarly to semi-group isomorphisms.
Group/is-iso (G H : Group) (h : Group/hom G H) : U = Semigroup/is-iso ( Group/Semigroup G) ( Group/Semigroup H) h Group/Iso (G H : Group) : U = Semigroup/Iso ( Group/Semigroup G) ( Group/Semigroup H)
1.8.4 Iso G G
Group/Iso/id (G : Group) : Group/Iso G G = Semigroup/Iso/id (Group/Semigroup G)
1.9 Isomorphic groups are equal
We define iso-eq for groups.
Group/iso-eq (G H : Group) (p : Path Group G H) : Group/Iso G H = Semigroup/iso-eq ( Group/Semigroup G) ( Group/Semigroup H) ( ap Group Semigroup (λt. t.1) G H p)
It is easy to show that iso-eq is a family of equivalences: it suffices to remark that being a group is a property of semi-groups. Thus, ap pr1 is an equivalence.
Group/ap-pr1/is-equiv (G H : Group) : is-equiv ( Path Group G H) ( Path Semigroup (Group/Semigroup G) (Group/Semigroup H)) ( ap Group Semigroup (λt. t.1) G H) = pr1/is-inj Semigroup is-group (is-group/is-prop) G H
We have also shown that Semigroup/iso-eq. Hence, Group/iso-eq is again an equivalence by the 3-out-of-2 property of equivalences.
Group/iso-eq/is-equiv (G H : Group) : is-equiv (Path Group G H) (Group/Iso G H) (Group/iso-eq G H) = is-equiv/comp-is-equiv ( Path Group G H) ( Path Semigroup ( Group/Semigroup G) ( Group/Semigroup H)) ( Group/Iso G H) ( ap Group Semigroup (λt. t.1) G H) ( Semigroup/iso-eq ( Group/Semigroup G) ( Group/Semigroup H)) ( Group/ap-pr1/is-equiv G H) ( Semigroup/iso-eq/is-equiv ( Group/Semigroup G) ( Group/Semigroup H)) Group/eq-iso (G H : Group) : (Group/Iso G H) → Path Group G H = is-equiv/inv-map ( Path Group G H) ( Group/Iso G H) ( Group/iso-eq G H) ( Group/iso-eq/is-equiv G H)
1.10 Unlock
unlock Semigroup/hom/htpy/is-equiv