Isomorphisms of semigroups
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-03-17.
Last modified on 2023-09-19.
module group-theory.isomorphisms-semigroups where
Imports
open import category-theory.isomorphisms-in-large-precategories open import foundation.action-on-identifications-functions 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.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation-core.function-extensionality open import group-theory.equivalences-semigroups open import group-theory.homomorphisms-semigroups open import group-theory.precategory-of-semigroups open import group-theory.semigroups
Idea
Isomorphisms of semigroups are homomorphisms that have a two-sided inverse.
Definition
The predicate of being an isomorphism of semigroups
module _ {l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2) (f : type-hom-Semigroup G H) where is-iso-hom-Semigroup : UU (l1 ⊔ l2) is-iso-hom-Semigroup = is-iso-hom-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} f hom-inv-is-iso-hom-Semigroup : is-iso-hom-Semigroup → type-hom-Semigroup H G hom-inv-is-iso-hom-Semigroup = hom-inv-is-iso-hom-Large-Precategory ( Semigroup-Large-Precategory) { X = G} { Y = H} ( f) map-inv-is-iso-hom-Semigroup : is-iso-hom-Semigroup → type-Semigroup H → type-Semigroup G map-inv-is-iso-hom-Semigroup U = map-hom-Semigroup H G (hom-inv-is-iso-hom-Semigroup U) is-section-hom-inv-is-iso-hom-Semigroup : (U : is-iso-hom-Semigroup) → comp-hom-Semigroup H G H f (hom-inv-is-iso-hom-Semigroup U) = id-hom-Semigroup H is-section-hom-inv-is-iso-hom-Semigroup = is-section-hom-inv-is-iso-hom-Large-Precategory ( Semigroup-Large-Precategory) { X = G} { Y = H} ( f) is-section-map-inv-is-iso-hom-Semigroup : (U : is-iso-hom-Semigroup) → ( map-hom-Semigroup G H f ∘ map-inv-is-iso-hom-Semigroup U) ~ id is-section-map-inv-is-iso-hom-Semigroup U = htpy-eq-hom-Semigroup H H ( comp-hom-Semigroup H G H f (hom-inv-is-iso-hom-Semigroup U)) ( id-hom-Semigroup H) ( is-section-hom-inv-is-iso-hom-Semigroup U) is-retraction-hom-inv-is-iso-hom-Semigroup : (U : is-iso-hom-Semigroup) → comp-hom-Semigroup G H G (hom-inv-is-iso-hom-Semigroup U) f = id-hom-Semigroup G is-retraction-hom-inv-is-iso-hom-Semigroup = is-retraction-hom-inv-is-iso-hom-Large-Precategory ( Semigroup-Large-Precategory) { X = G} { Y = H} ( f) is-retraction-map-inv-is-iso-hom-Semigroup : (U : is-iso-hom-Semigroup) → ( map-inv-is-iso-hom-Semigroup U ∘ map-hom-Semigroup G H f) ~ id is-retraction-map-inv-is-iso-hom-Semigroup U = htpy-eq-hom-Semigroup G G ( comp-hom-Semigroup G H G (hom-inv-is-iso-hom-Semigroup U) f) ( id-hom-Semigroup G) ( is-retraction-hom-inv-is-iso-hom-Semigroup U)
Isomorphisms of semigroups
module _ {l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2) where type-iso-Semigroup : UU (l1 ⊔ l2) type-iso-Semigroup = iso-Large-Precategory Semigroup-Large-Precategory G H hom-iso-Semigroup : type-iso-Semigroup → type-hom-Semigroup G H hom-iso-Semigroup = hom-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} map-iso-Semigroup : type-iso-Semigroup → type-Semigroup G → type-Semigroup H map-iso-Semigroup f = map-hom-Semigroup G H (hom-iso-Semigroup f) preserves-mul-iso-Semigroup : (f : type-iso-Semigroup) (x y : type-Semigroup G) → map-iso-Semigroup f (mul-Semigroup G x y) = mul-Semigroup H (map-iso-Semigroup f x) (map-iso-Semigroup f y) preserves-mul-iso-Semigroup f = preserves-mul-hom-Semigroup G H (hom-iso-Semigroup f) is-iso-iso-Semigroup : (f : type-iso-Semigroup) → is-iso-hom-Semigroup G H (hom-iso-Semigroup f) is-iso-iso-Semigroup = is-iso-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} hom-inv-iso-Semigroup : type-iso-Semigroup → type-hom-Semigroup H G hom-inv-iso-Semigroup = hom-inv-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} map-inv-iso-Semigroup : type-iso-Semigroup → type-Semigroup H → type-Semigroup G map-inv-iso-Semigroup f = map-hom-Semigroup H G (hom-inv-iso-Semigroup f) preserves-mul-inv-iso-Semigroup : (f : type-iso-Semigroup) (x y : type-Semigroup H) → map-inv-iso-Semigroup f (mul-Semigroup H x y) = mul-Semigroup G (map-inv-iso-Semigroup f x) (map-inv-iso-Semigroup f y) preserves-mul-inv-iso-Semigroup f = preserves-mul-hom-Semigroup H G (hom-inv-iso-Semigroup f) is-section-hom-inv-iso-Semigroup : (f : type-iso-Semigroup) → comp-hom-Semigroup H G H (hom-iso-Semigroup f) (hom-inv-iso-Semigroup f) = id-hom-Semigroup H is-section-hom-inv-iso-Semigroup = is-section-hom-inv-iso-Large-Precategory ( Semigroup-Large-Precategory) { X = G} { Y = H} is-section-map-inv-iso-Semigroup : (f : type-iso-Semigroup) → (map-iso-Semigroup f ∘ map-inv-iso-Semigroup f) ~ id is-section-map-inv-iso-Semigroup f = htpy-eq-hom-Semigroup H H ( comp-hom-Semigroup H G H ( hom-iso-Semigroup f) ( hom-inv-iso-Semigroup f)) ( id-hom-Semigroup H) ( is-section-hom-inv-iso-Semigroup f) is-retraction-hom-inv-iso-Semigroup : (f : type-iso-Semigroup) → comp-hom-Semigroup G H G (hom-inv-iso-Semigroup f) (hom-iso-Semigroup f) = id-hom-Semigroup G is-retraction-hom-inv-iso-Semigroup = is-retraction-hom-inv-iso-Large-Precategory ( Semigroup-Large-Precategory) { X = G} { Y = H} is-retraction-map-inv-iso-Semigroup : (f : type-iso-Semigroup) → ( map-inv-iso-Semigroup f ∘ map-iso-Semigroup f) ~ id is-retraction-map-inv-iso-Semigroup f = htpy-eq-hom-Semigroup G G ( comp-hom-Semigroup G H G ( hom-inv-iso-Semigroup f) ( hom-iso-Semigroup f)) ( id-hom-Semigroup G) ( is-retraction-hom-inv-iso-Semigroup f)
Properties
Being an isomorphism is a property
module _ {l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2) where abstract is-prop-is-iso-hom-Semigroup : (f : type-hom-Semigroup G H) → is-prop (is-iso-hom-Semigroup G H f) is-prop-is-iso-hom-Semigroup = is-prop-is-iso-hom-Large-Precategory ( Semigroup-Large-Precategory) { X = G} { Y = H} is-iso-prop-hom-Semigroup : type-hom-Semigroup G H → Prop (l1 ⊔ l2) is-iso-prop-hom-Semigroup = is-iso-prop-hom-Large-Precategory ( Semigroup-Large-Precategory) { X = G} { Y = H}
The inverse of an equivalence of semigroups preserves the binary operation
module _ {l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2) where abstract preserves-mul-map-inv-is-equiv-Semigroup : ( f : type-hom-Semigroup G H) ( U : is-equiv (map-hom-Semigroup G H f)) → preserves-mul-Semigroup H G (map-inv-is-equiv U) preserves-mul-map-inv-is-equiv-Semigroup (f , μ-f) U x y = map-inv-is-equiv ( is-emb-is-equiv U ( map-inv-is-equiv U (mul-Semigroup H x y)) ( mul-Semigroup G ( map-inv-is-equiv U x) ( map-inv-is-equiv U y))) ( ( ( is-section-map-inv-is-equiv U (mul-Semigroup H x y)) ∙ ( ( ap ( λ t → mul-Semigroup H t y) ( inv (is-section-map-inv-is-equiv U x))) ∙ ( ap ( mul-Semigroup H (f (map-inv-is-equiv U x))) ( inv (is-section-map-inv-is-equiv U y))))) ∙ ( inv ( μ-f ( map-inv-is-equiv U x) ( map-inv-is-equiv U y))))
A homomorphism of semigroups is an equivalence of semigroups if and only if it is an isomorphism
module _ {l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2) where abstract is-iso-is-equiv-hom-Semigroup : (f : type-hom-Semigroup G H) → is-equiv-hom-Semigroup G H f → is-iso-hom-Semigroup G H f pr1 (pr1 (is-iso-is-equiv-hom-Semigroup (f , μ-f) U)) = map-inv-is-equiv U pr2 (pr1 (is-iso-is-equiv-hom-Semigroup (f , μ-f) U)) = preserves-mul-map-inv-is-equiv-Semigroup G H (f , μ-f) U pr1 (pr2 (is-iso-is-equiv-hom-Semigroup (f , μ-f) U)) = eq-htpy-hom-Semigroup H H (is-section-map-inv-is-equiv U) pr2 (pr2 (is-iso-is-equiv-hom-Semigroup (f , μ-f) U)) = eq-htpy-hom-Semigroup G G (is-retraction-map-inv-is-equiv U) abstract is-equiv-is-iso-hom-Semigroup : (f : type-hom-Semigroup G H) → is-iso-hom-Semigroup G H f → is-equiv-hom-Semigroup G H f is-equiv-is-iso-hom-Semigroup (f , μ-f) ((g , μ-g) , S , R) = is-equiv-is-invertible g ( htpy-eq (ap pr1 S)) ( htpy-eq (ap pr1 R)) equiv-iso-equiv-Semigroup : equiv-Semigroup G H ≃ type-iso-Semigroup G H equiv-iso-equiv-Semigroup = ( equiv-type-subtype ( λ f → is-property-is-equiv (map-hom-Semigroup G H f)) ( is-prop-is-iso-hom-Semigroup G H) ( is-iso-is-equiv-hom-Semigroup) ( is-equiv-is-iso-hom-Semigroup)) ∘e ( equiv-right-swap-Σ)
Two semigroups are equal if and only if they are isomorphic
module _ {l : Level} (G : Semigroup l) where is-contr-total-iso-Semigroup : is-contr (Σ (Semigroup l) (type-iso-Semigroup G)) is-contr-total-iso-Semigroup = is-contr-equiv' ( Σ (Semigroup l) (equiv-Semigroup G)) ( equiv-tot (equiv-iso-equiv-Semigroup G)) ( is-contr-total-equiv-Semigroup G) id-iso-Semigroup : type-iso-Semigroup G G id-iso-Semigroup = id-iso-Large-Precategory Semigroup-Large-Precategory {X = G} iso-eq-Semigroup : (H : Semigroup l) → Id G H → type-iso-Semigroup G H iso-eq-Semigroup = iso-eq-Large-Precategory Semigroup-Large-Precategory G
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-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-09-10. Egbert Rijke and Fredrik Bakke. Cyclic groups (#723).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659).