The classification of cyclic rings (UniMath#757)

Co-authored-by: izak <gregapercic000@gmail.com>

src/category-theory.lagda.md

@@ -56,6 +56,8 @@ open import category-theory.functors-large-precategories public
 open import category-theory.functors-precategories public
 open import category-theory.groupoids public
 open import category-theory.homotopies-natural-transformations-large-precategories public
+open import category-theory.initial-objects-large-categories public
+open import category-theory.initial-objects-large-precategories public
 open import category-theory.initial-objects-precategories public
 open import category-theory.isomorphisms-in-categories public
 open import category-theory.isomorphisms-in-large-categories public

src/category-theory/initial-objects-large-categories.lagda.md

@@ -0,0 +1,39 @@
+# Initial objects of large categories
+
+```agda
+module category-theory.initial-objects-large-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.initial-objects-large-precategories
+open import category-theory.large-categories
+
+open import foundation.contractible-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An **initial object** in a [large category](category-theory.large-categories.md)
+`C` is an object `X` such that `hom X Y` is
+[contractible](foundation.contractible-types.md) for any object `Y`.
+
+## Definitions
+
+### Initial objects in large categories
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β)
+  {l : Level} (X : obj-Large-Category C l)
+  where
+
+  is-initial-obj-Large-Category : UUω
+  is-initial-obj-Large-Category =
+    is-initial-obj-Large-Precategory (large-precategory-Large-Category C) X
+```

src/category-theory/initial-objects-large-precategories.lagda.md

@@ -0,0 +1,39 @@
+# Initial objects of large precategories
+
+```agda
+module category-theory.initial-objects-large-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-precategories
+
+open import foundation.contractible-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An **initial object** in a [large category](category-theory.large-categories.md)
+`C` is an object `X` such that `hom X Y` is
+[contractible](foundation.contractible-types.md) for any object `Y`.
+
+## Definitions
+
+### Initial objects in large categories
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β)
+  {l : Level} (X : obj-Large-Precategory C l)
+  where
+
+  is-initial-obj-Large-Precategory : UUω
+  is-initial-obj-Large-Precategory =
+    {l2 : Level} (Y : obj-Large-Precategory C l2) →
+    is-contr (type-hom-Large-Precategory C X Y)
+```

src/category-theory/initial-objects-precategories.lagda.md

@@ -12,6 +12,7 @@ open import category-theory.precategories
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.function-types
+open import foundation.propositions
 open import foundation.universe-levels
 
 open import foundation-core.identity-types
@@ -30,10 +31,22 @@ it exists, is an object with the universal property that there is a
 ### The universal property of an initial object in a precategory
 
 ```agda
-is-initial-obj-Precategory :
-  {l1 l2 : Level} (C : Precategory l1 l2) → obj-Precategory C → UU (l1 ⊔ l2)
-is-initial-obj-Precategory C x =
-  (y : obj-Precategory C) → is-contr (type-hom-Precategory C x y)
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2) (x : obj-Precategory C)
+  where
+
+  is-initial-prop-obj-Precategory : Prop (l1 ⊔ l2)
+  is-initial-prop-obj-Precategory =
+    Π-Prop
+      ( obj-Precategory C)
+      ( λ y → is-contr-Prop (type-hom-Precategory C x y))
+
+  is-initial-obj-Precategory : UU (l1 ⊔ l2)
+  is-initial-obj-Precategory = type-Prop is-initial-prop-obj-Precategory
+
+  is-prop-is-initial-obj-Precategory : is-prop is-initial-obj-Precategory
+  is-prop-is-initial-obj-Precategory =
+    is-prop-type-Prop is-initial-prop-obj-Precategory
 
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
@@ -51,7 +64,6 @@ module _
     (f : type-hom-Precategory C x y) →
     hom-is-initial-obj-Precategory y ＝ f
   is-unique-hom-is-initial-obj-Precategory = contraction ∘ t
-
 ```
 
 ### Initial objects in precategories
@@ -62,7 +74,6 @@ initial-obj-Precategory :
 initial-obj-Precategory C =
   Σ (obj-Precategory C) (is-initial-obj-Precategory C)
 
-
 module _
   {l1 l2 : Level}
   (C : Precategory l1 l2)
@@ -72,7 +83,8 @@ module _
   obj-initial-obj-Precategory : obj-Precategory C
   obj-initial-obj-Precategory = pr1 t
 
-  is-initial-obj-initial-obj-Precategory : is-initial-obj-Precategory C obj-initial-obj-Precategory
+  is-initial-obj-initial-obj-Precategory :
+    is-initial-obj-Precategory C obj-initial-obj-Precategory
   is-initial-obj-initial-obj-Precategory = pr2 t
 
   hom-initial-obj-Precategory :

src/category-theory/isomorphisms-in-large-categories.lagda.md

@@ -156,21 +156,26 @@ This is because, by the J-rule, it is enough to construct an isomorphism given
 isomorphism.
 
 ```agda
-iso-eq-Large-Category :
-  {α : Level → Level} {β : Level → Level → Level} →
+module _
+  {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Category α β) {l1 : Level}
-  (X : obj-Large-Category C l1) (Y : obj-Large-Category C l1) →
-  X ＝ Y → iso-Large-Category C X Y
-iso-eq-Large-Category C =
-  iso-eq-Large-Precategory (large-precategory-Large-Category C)
+  (X Y : obj-Large-Category C l1)
+  where
 
-compute-iso-eq-Large-Category :
-  {α : Level → Level} {β : Level → Level → Level} →
-  (C : Large-Category α β) {l1 : Level}
-  (X : obj-Large-Category C l1) (Y : obj-Large-Category C l1) →
-  iso-eq-Category (category-Large-Category C l1) X Y ~
-  iso-eq-Large-Category C X Y
-compute-iso-eq-Large-Category C X .X refl = refl
+  iso-eq-Large-Category :
+    X ＝ Y → iso-Large-Category C X Y
+  iso-eq-Large-Category =
+    iso-eq-Large-Precategory (large-precategory-Large-Category C) X Y
+
+  compute-iso-eq-Large-Category :
+    iso-eq-Category (category-Large-Category C l1) X Y ~
+    iso-eq-Large-Category
+  compute-iso-eq-Large-Category refl = refl
+
+  eq-iso-Large-Category :
+    iso-Large-Category C X Y → X ＝ Y
+  eq-iso-Large-Category =
+    map-inv-is-equiv (is-large-category-Large-Category C X Y)
 ```
 
 ## Properties

src/category-theory/isomorphisms-in-large-precategories.lagda.md

@@ -183,8 +183,7 @@ module _
   all-elements-equal-is-iso-hom-Large-Precategory :
     (f : type-hom-Large-Precategory C X Y)
     (H K : is-iso-hom-Large-Precategory C f) → H ＝ K
-  all-elements-equal-is-iso-hom-Large-Precategory f
-    (pair g (pair p q)) (pair g' (pair p' q')) =
+  all-elements-equal-is-iso-hom-Large-Precategory f (g , p , q) (g' , p' , q') =
     eq-type-subtype
       ( λ g →
         prod-Prop

src/category-theory/terminal-objects-precategories.lagda.md

@@ -11,8 +11,8 @@ open import category-theory.precategories
 
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
-open import foundation.universe-levels
 open import foundation.function-types
+open import foundation.universe-levels
 
 open import foundation-core.identity-types
 ```
@@ -52,7 +52,6 @@ module _
     (f : type-hom-Precategory C y x) →
     hom-is-terminal-obj-Precategory y ＝ f
   is-unique-hom-is-terminal-obj-Precategory = contraction ∘ t
-
 ```
 
 ### Terminal objects in precategories
@@ -63,7 +62,6 @@ terminal-obj-Precategory :
 terminal-obj-Precategory C =
   Σ (obj-Precategory C) (is-terminal-obj-Precategory C)
 
-
 module _
   {l1 l2 : Level}
   (C : Precategory l1 l2)
@@ -73,7 +71,8 @@ module _
   obj-terminal-obj-Precategory : obj-Precategory C
   obj-terminal-obj-Precategory = pr1 t
 
-  is-terminal-obj-terminal-obj-Precategory : is-terminal-obj-Precategory C obj-terminal-obj-Precategory
+  is-terminal-obj-terminal-obj-Precategory :
+    is-terminal-obj-Precategory C obj-terminal-obj-Precategory
   is-terminal-obj-terminal-obj-Precategory = pr2 t
 
   hom-terminal-obj-Precategory :

src/commutative-algebra.lagda.md

@@ -20,6 +20,7 @@ open import commutative-algebra.full-ideals-commutative-rings public
 open import commutative-algebra.function-commutative-rings public
 open import commutative-algebra.function-commutative-semirings public
 open import commutative-algebra.gaussian-integers public
+open import commutative-algebra.groups-of-units-commutative-rings public
 open import commutative-algebra.homomorphisms-commutative-rings public
 open import commutative-algebra.homomorphisms-commutative-semirings public
 open import commutative-algebra.ideals-commutative-rings public