The poset of cyclic rings

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-09-21.
Last modified on 2024-03-11.

module ring-theory.poset-of-cyclic-rings where
open import foundation.universe-levels

open import order-theory.large-posets

open import ring-theory.category-of-cyclic-rings


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.


The large poset of cyclic rings

Cyclic-Ring-Large-Poset : Large-Poset lsuc (_⊔_)
Cyclic-Ring-Large-Poset =
    ( Cyclic-Ring-Large-Category)
    ( is-large-poset-Cyclic-Ring-Large-Category)

See also

Recent changes