This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
The poset of cyclic rings
module ring-theory.poset-of-cyclic-rings where
Imports
open import foundation.universe-levels open import order-theory.large-posets open import ring-theory.category-of-cyclic-rings
Idea
The large poset of cyclic rings is just the large category of cyclic rings, which happens to be a large poset.
The large poset of cyclic rings is dual to the large poset of subgroups of the group of integers.
Definition
The large poset of cyclic rings
Cyclic-Ring-Large-Poset : Large-Poset lsuc (_⊔_) Cyclic-Ring-Large-Poset = large-poset-Large-Category ( Cyclic-Ring-Large-Category) ( is-large-poset-Cyclic-Ring-Large-Category)