The precategory of commutative semirings

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-06.
Last modified on 2024-03-11.

module commutative-algebra.precategory-of-commutative-semirings where
Imports 
open import category-theory.full-large-subprecategories
open import category-theory.large-precategories
open import category-theory.precategories

open import commutative-algebra.commutative-semirings

open import foundation.universe-levels

open import ring-theory.precategory-of-semirings

Idea

The precategory of commutative semirings consists of commutative semirings and homomorphisms of semirings.

Definitions

The precategory of commutative semirings as a full subprecategory of semirings

Commutative-Semiring-Full-Large-Precategory :
  Full-Large-Subprecategory (λ l → l) Semiring-Large-Precategory
Commutative-Semiring-Full-Large-Precategory = is-commutative-prop-Semiring

The large precategory of commutative semirings

Commutative-Semiring-Large-Precategory : Large-Precategory lsuc (_⊔_)
Commutative-Semiring-Large-Precategory =
  large-precategory-Full-Large-Subprecategory
    ( Semiring-Large-Precategory)
    ( Commutative-Semiring-Full-Large-Precategory)

The precategory of commutative semirings of universe level l

Commutative-Semiring-Precategory : (l : Level) → Precategory (lsuc l) l
Commutative-Semiring-Precategory =
  precategory-Large-Precategory Commutative-Semiring-Large-Precategory

Recent changes