Isomorphisms of concrete groups

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-09-20.
Last modified on 2023-09-13.

module group-theory.isomorphisms-concrete-groups where
Imports 
open import category-theory.isomorphisms-in-large-precategories

open import foundation.universe-levels

open import group-theory.concrete-groups
open import group-theory.precategory-of-concrete-groups

Idea

Isomorphisms of concrete groups are isomorphisms in the large precategory of concrete groups.

Definition

iso-Concrete-Group :
  {l1 l2 : Level} → Concrete-Group l1 → Concrete-Group l2 → UU (l1 ⊔ l2)
iso-Concrete-Group = iso-Large-Precategory Concrete-Group-Large-Precategory

Properties

Equivalences of concrete groups are isomorphisms of concrete groups

This remains to be shown. #736

Recent changes