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
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)
See also
Table of files related to cyclic types, groups, and rings
Recent changes
- 2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
- 2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).