Isomorphisms of groups
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Eléonore Mangel.
Created on 2022-03-17.
Last modified on 2023-09-19.
module group-theory.isomorphisms-groups where
Imports
open import category-theory.isomorphisms-in-large-precategories open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels open import group-theory.category-of-semigroups open import group-theory.equivalences-semigroups open import group-theory.groups open import group-theory.homomorphisms-groups open import group-theory.isomorphisms-semigroups open import group-theory.precategory-of-groups
Definitions
The predicate of being an isomorphism of groups
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : type-hom-Group G H) where is-iso-hom-Group : UU (l1 ⊔ l2) is-iso-hom-Group = is-iso-hom-Semigroup (semigroup-Group G) (semigroup-Group H) f is-prop-is-iso-hom-Group : is-prop is-iso-hom-Group is-prop-is-iso-hom-Group = is-prop-is-iso-hom-Semigroup (semigroup-Group G) (semigroup-Group H) f is-iso-prop-hom-Group : Prop (l1 ⊔ l2) is-iso-prop-hom-Group = is-iso-prop-hom-Semigroup (semigroup-Group G) (semigroup-Group H) f hom-inv-is-iso-hom-Group : is-iso-hom-Group → type-hom-Group H G hom-inv-is-iso-hom-Group = hom-inv-is-iso-hom-Semigroup (semigroup-Group G) (semigroup-Group H) f map-inv-is-iso-hom-Group : is-iso-hom-Group → type-Group H → type-Group G map-inv-is-iso-hom-Group = map-inv-is-iso-hom-Semigroup (semigroup-Group G) (semigroup-Group H) f is-section-hom-inv-is-iso-hom-Group : (U : is-iso-hom-Group) → comp-hom-Group H G H f (hom-inv-is-iso-hom-Group U) = id-hom-Group H is-section-hom-inv-is-iso-hom-Group = is-section-hom-inv-is-iso-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) ( f) is-section-map-inv-is-iso-hom-Group : (U : is-iso-hom-Group) → ( map-hom-Group G H f ∘ map-inv-is-iso-hom-Group U) ~ id is-section-map-inv-is-iso-hom-Group = is-section-map-inv-is-iso-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) ( f) is-retraction-hom-inv-is-iso-hom-Group : (U : is-iso-hom-Group) → comp-hom-Group G H G (hom-inv-is-iso-hom-Group U) f = id-hom-Group G is-retraction-hom-inv-is-iso-hom-Group = is-retraction-hom-inv-is-iso-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) ( f) is-retraction-map-inv-is-iso-hom-Group : (U : is-iso-hom-Group) → ( map-inv-is-iso-hom-Group U ∘ map-hom-Group G H f) ~ id is-retraction-map-inv-is-iso-hom-Group = is-retraction-map-inv-is-iso-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) ( f)
The predicate of being an equivalence of groups
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) where is-equiv-hom-Group : type-hom-Group G H → UU (l1 ⊔ l2) is-equiv-hom-Group = is-equiv-hom-Semigroup (semigroup-Group G) (semigroup-Group H) equiv-Group : UU (l1 ⊔ l2) equiv-Group = equiv-Semigroup (semigroup-Group G) (semigroup-Group H)
Group isomorphisms
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) where type-iso-Group : UU (l1 ⊔ l2) type-iso-Group = type-iso-Semigroup (semigroup-Group G) (semigroup-Group H) hom-iso-Group : type-iso-Group → type-hom-Group G H hom-iso-Group = hom-iso-Semigroup (semigroup-Group G) (semigroup-Group H) map-iso-Group : type-iso-Group → type-Group G → type-Group H map-iso-Group = map-iso-Semigroup (semigroup-Group G) (semigroup-Group H) preserves-mul-iso-Group : (f : type-iso-Group) (x y : type-Group G) → map-iso-Group f (mul-Group G x y) = mul-Group H (map-iso-Group f x) (map-iso-Group f y) preserves-mul-iso-Group = preserves-mul-iso-Semigroup (semigroup-Group G) (semigroup-Group H) is-iso-iso-Group : (f : type-iso-Group) → is-iso-hom-Group G H (hom-iso-Group f) is-iso-iso-Group = is-iso-iso-Semigroup (semigroup-Group G) (semigroup-Group H) hom-inv-iso-Group : type-iso-Group → type-hom-Group H G hom-inv-iso-Group = hom-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H) map-inv-iso-Group : type-iso-Group → type-Group H → type-Group G map-inv-iso-Group = map-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H) preserves-mul-inv-iso-Group : (f : type-iso-Group) (x y : type-Group H) → map-inv-iso-Group f (mul-Group H x y) = mul-Group G (map-inv-iso-Group f x) (map-inv-iso-Group f y) preserves-mul-inv-iso-Group = preserves-mul-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H) is-section-hom-inv-iso-Group : (f : type-iso-Group) → comp-hom-Group H G H (hom-iso-Group f) (hom-inv-iso-Group f) = id-hom-Group H is-section-hom-inv-iso-Group = is-section-hom-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H) is-section-map-inv-iso-Group : (f : type-iso-Group) → ( map-iso-Group f ∘ map-inv-iso-Group f) ~ id is-section-map-inv-iso-Group = is-section-map-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H) is-retraction-hom-inv-iso-Group : (f : type-iso-Group) → comp-hom-Group G H G (hom-inv-iso-Group f) (hom-iso-Group f) = id-hom-Group G is-retraction-hom-inv-iso-Group = is-retraction-hom-inv-iso-Semigroup ( semigroup-Group G) ( semigroup-Group H) is-retraction-map-inv-iso-Group : (f : type-iso-Group) → ( map-inv-iso-Group f ∘ map-iso-Group f) ~ id is-retraction-map-inv-iso-Group = is-retraction-map-inv-iso-Semigroup ( semigroup-Group G) ( semigroup-Group H) is-iso-is-equiv-hom-Group : (f : type-hom-Group G H) → is-equiv-hom-Group G H f → is-iso-hom-Group G H f is-iso-is-equiv-hom-Group = is-iso-is-equiv-hom-Semigroup (semigroup-Group G) (semigroup-Group H) is-equiv-is-iso-hom-Group : (f : type-hom-Group G H) → is-iso-hom-Group G H f → is-equiv-hom-Group G H f is-equiv-is-iso-hom-Group = is-equiv-is-iso-hom-Semigroup (semigroup-Group G) (semigroup-Group H) equiv-iso-equiv-Group : equiv-Group G H ≃ type-iso-Group equiv-iso-equiv-Group = equiv-iso-equiv-Semigroup (semigroup-Group G) (semigroup-Group H) iso-equiv-Group : equiv-Group G H → type-iso-Group iso-equiv-Group = map-equiv equiv-iso-equiv-Group
The identity isomorphism
module _ {l : Level} (G : Group l) where id-iso-Group : type-iso-Group G G id-iso-Group = id-iso-Large-Precategory Group-Large-Precategory {X = G}
Properties
The total space of group isomorphisms from a given group G
is contractible
module _ {l : Level} (G : Group l) where iso-eq-Group : (H : Group l) → Id G H → type-iso-Group G H iso-eq-Group = iso-eq-Large-Precategory Group-Large-Precategory G abstract extensionality-Group' : (H : Group l) → Id G H ≃ type-iso-Group G H extensionality-Group' H = ( extensionality-Semigroup ( semigroup-Group G) ( semigroup-Group H)) ∘e ( equiv-ap-inclusion-subtype is-group-Prop {s = G} {t = H}) abstract is-contr-total-iso-Group : is-contr (Σ (Group l) (type-iso-Group G)) is-contr-total-iso-Group = is-contr-equiv' ( Σ (Group l) (Id G)) ( equiv-tot extensionality-Group') ( is-contr-total-path G)
Group isomorphisms are stable by composition
module _ {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (K : Group l3) where comp-iso-Group : type-iso-Group H K → type-iso-Group G H → type-iso-Group G K comp-iso-Group = comp-iso-Large-Precategory Group-Large-Precategory {X = G} {Y = H} {Z = K}
Group isomorphisms are stable by inversion
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) where inv-iso-Group : type-iso-Group G H → type-iso-Group H G inv-iso-Group = inv-iso-Large-Precategory Group-Large-Precategory {X = G} {Y = H}
Recent changes
- 2023-09-19. Egbert Rijke. Isomorphisms in large categories and large precategories (#791).
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-09-10. Egbert Rijke and Fredrik Bakke. Cyclic groups (#723).
- 2023-05-06. Egbert Rijke. Big cleanup continued (#597).
- 2023-03-15. Fredrik Bakke. Remove blank lines at the start and end of code blocks (#508).