# Subsets of commutative semirings

Content created by Egbert Rijke and Maša Žaucer.

Created on 2023-03-18.

module commutative-algebra.subsets-commutative-semirings where

Imports
open import commutative-algebra.commutative-semirings

open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import ring-theory.subsets-semirings


## Idea

A subset of a commutative semiring is a subtype of its underlying type.

## Definition

### Subsets of commutative semirings

subset-Commutative-Semiring :
(l : Level) {l1 : Level} (A : Commutative-Semiring l1) → UU (lsuc l ⊔ l1)
subset-Commutative-Semiring l A =
subset-Semiring l (semiring-Commutative-Semiring A)

is-set-subset-Commutative-Semiring :
(l : Level) {l1 : Level} (A : Commutative-Semiring l1) →
is-set (subset-Commutative-Semiring l A)
is-set-subset-Commutative-Semiring l A =
is-set-subset-Semiring l (semiring-Commutative-Semiring A)

module _
{l1 l2 : Level} (A : Commutative-Semiring l1)
(S : subset-Commutative-Semiring l2 A)
where

type-subset-Commutative-Semiring : UU (l1 ⊔ l2)
type-subset-Commutative-Semiring =
type-subset-Semiring (semiring-Commutative-Semiring A) S

inclusion-subset-Commutative-Semiring :
type-subset-Commutative-Semiring → type-Commutative-Semiring A
inclusion-subset-Commutative-Semiring =
inclusion-subset-Semiring (semiring-Commutative-Semiring A) S

ap-inclusion-subset-Commutative-Semiring :
(x y : type-subset-Commutative-Semiring) →
x ＝ y →
( inclusion-subset-Commutative-Semiring x ＝
inclusion-subset-Commutative-Semiring y)
ap-inclusion-subset-Commutative-Semiring =
ap-inclusion-subset-Semiring (semiring-Commutative-Semiring A) S

is-in-subset-Commutative-Semiring : type-Commutative-Semiring A → UU l2
is-in-subset-Commutative-Semiring = is-in-subtype S

is-prop-is-in-subset-Commutative-Semiring :
(x : type-Commutative-Semiring A) →
is-prop (is-in-subset-Commutative-Semiring x)
is-prop-is-in-subset-Commutative-Semiring =
is-prop-is-in-subtype S

is-closed-under-eq-subset-Commutative-Semiring :
{x y : type-Commutative-Semiring A} →
is-in-subset-Commutative-Semiring x → x ＝ y →
is-in-subset-Commutative-Semiring y
is-closed-under-eq-subset-Commutative-Semiring =
is-closed-under-eq-subtype S

is-in-subset-inclusion-subset-Commutative-Semiring :
(x : type-subset-Commutative-Semiring) →
is-in-subset-Commutative-Semiring (inclusion-subset-Commutative-Semiring x)
is-in-subset-inclusion-subset-Commutative-Semiring =
is-in-subtype-inclusion-subtype S


### The condition that a subset contains zero

module _
{l1 l2 : Level} (A : Commutative-Semiring l1)
(S : subset-Commutative-Semiring l2 A)
where

contains-zero-subset-Commutative-Semiring : UU l2
contains-zero-subset-Commutative-Semiring =
contains-zero-subset-Semiring (semiring-Commutative-Semiring A) S


### The condition that a subset contains one

  contains-one-subset-Commutative-Semiring : UU l2
contains-one-subset-Commutative-Semiring =
contains-one-subset-Semiring (semiring-Commutative-Semiring A) S


### The condition that a subset is closed under addition

  is-closed-under-addition-subset-Commutative-Semiring : UU (l1 ⊔ l2)


### The condition that a subset is closed under multiplication

  is-closed-under-multiplication-subset-Commutative-Semiring : UU (l1 ⊔ l2)
is-closed-under-multiplication-subset-Commutative-Semiring =
is-closed-under-multiplication-subset-Semiring
( semiring-Commutative-Semiring A)
( S)


### The condition that a subset is closed under multiplication from the left by an arbitrary element

  is-closed-under-left-multiplication-subset-Commutative-Semiring : UU (l1 ⊔ l2)
is-closed-under-left-multiplication-subset-Commutative-Semiring =
is-closed-under-left-multiplication-subset-Semiring
( semiring-Commutative-Semiring A)
( S)


### The condition that a subset is closed-under-multiplication from the right by an arbitrary element

  is-closed-under-right-multiplication-subset-Commutative-Semiring :
UU (l1 ⊔ l2)
is-closed-under-right-multiplication-subset-Commutative-Semiring =
is-closed-under-right-multiplication-subset-Semiring
( semiring-Commutative-Semiring A)
( S)