# Subsets of rings

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elisabeth Stenholm and Maša Žaucer.

Created on 2022-04-05.
Last modified on 2024-04-20.

module ring-theory.subsets-rings where

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

open import group-theory.subgroups-abelian-groups

open import ring-theory.rings


## Idea

A subset of a ring is a subtype of the underlying type of a ring

## Definition

### Subsets of rings

subset-Ring :
(l : Level) {l1 : Level} (R : Ring l1) → UU (lsuc l ⊔ l1)
subset-Ring l R = subtype l (type-Ring R)

is-set-subset-Ring :
(l : Level) {l1 : Level} (R : Ring l1) → is-set (subset-Ring l R)
is-set-subset-Ring l R =
is-set-function-type is-set-type-Prop

module _
{l1 l2 : Level} (R : Ring l1) (S : subset-Ring l2 R)
where

is-in-subset-Ring : type-Ring R → UU l2
is-in-subset-Ring = is-in-subtype S

is-prop-is-in-subset-Ring : (x : type-Ring R) → is-prop (is-in-subset-Ring x)
is-prop-is-in-subset-Ring = is-prop-is-in-subtype S

type-subset-Ring : UU (l1 ⊔ l2)
type-subset-Ring = type-subtype S

inclusion-subset-Ring : type-subset-Ring → type-Ring R
inclusion-subset-Ring = inclusion-subtype S

ap-inclusion-subset-Ring :
(x y : type-subset-Ring) →
x ＝ y → (inclusion-subset-Ring x ＝ inclusion-subset-Ring y)
ap-inclusion-subset-Ring = ap-inclusion-subtype S

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

is-closed-under-eq-subset-Ring :
{x y : type-Ring R} → is-in-subset-Ring x → (x ＝ y) → is-in-subset-Ring y
is-closed-under-eq-subset-Ring =
is-closed-under-eq-subtype S

is-closed-under-eq-subset-Ring' :
{x y : type-Ring R} → is-in-subset-Ring y → (x ＝ y) → is-in-subset-Ring x
is-closed-under-eq-subset-Ring' =
is-closed-under-eq-subtype' S


### The condition that a subset contains zero

module _
{l1 l2 : Level} (R : Ring l1) (S : subset-Ring l2 R)
where

contains-zero-subset-Ring : UU l2
contains-zero-subset-Ring = is-in-subset-Ring R S (zero-Ring R)


### The condition that a subset contains one

  contains-one-subset-Ring : UU l2
contains-one-subset-Ring = is-in-subset-Ring R S (one-Ring R)


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

  is-closed-under-addition-subset-Ring : UU (l1 ⊔ l2)
is-closed-under-addition-subset-Ring =
{x y : type-Ring R} →
is-in-subset-Ring R S x → is-in-subset-Ring R S y →
is-in-subset-Ring R S (add-Ring R x y)


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

  is-closed-under-negatives-subset-Ring : UU (l1 ⊔ l2)
is-closed-under-negatives-subset-Ring =
{x : type-Ring R} →
is-in-subset-Ring R S x → is-in-subset-Ring R S (neg-Ring R x)


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

  is-closed-under-multiplication-subset-Ring : UU (l1 ⊔ l2)
is-closed-under-multiplication-subset-Ring =
(x y : type-Ring R) → is-in-subset-Ring R S x → is-in-subset-Ring R S y →
is-in-subset-Ring R S (mul-Ring R x y)


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

  is-closed-under-left-multiplication-subset-Ring-Prop : Prop (l1 ⊔ l2)
is-closed-under-left-multiplication-subset-Ring-Prop =
Π-Prop
( type-Ring R)
( λ x →
Π-Prop
( type-Ring R)
( λ y →
function-Prop
( is-in-subset-Ring R S y)
( S (mul-Ring R x y))))

is-closed-under-left-multiplication-subset-Ring : UU (l1 ⊔ l2)
is-closed-under-left-multiplication-subset-Ring =
type-Prop is-closed-under-left-multiplication-subset-Ring-Prop

is-prop-is-closed-under-left-multiplication-subset-Ring :
is-prop is-closed-under-left-multiplication-subset-Ring
is-prop-is-closed-under-left-multiplication-subset-Ring =
is-prop-type-Prop is-closed-under-left-multiplication-subset-Ring-Prop


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

  is-closed-under-right-multiplication-subset-Ring-Prop : Prop (l1 ⊔ l2)
is-closed-under-right-multiplication-subset-Ring-Prop =
Π-Prop
( type-Ring R)
( λ x →
Π-Prop
( type-Ring R)
( λ y →
function-Prop
( is-in-subset-Ring R S x)
( S (mul-Ring R x y))))

is-closed-under-right-multiplication-subset-Ring : UU (l1 ⊔ l2)
is-closed-under-right-multiplication-subset-Ring =
type-Prop is-closed-under-right-multiplication-subset-Ring-Prop

is-prop-is-closed-under-right-multiplication-subset-Ring :
is-prop is-closed-under-right-multiplication-subset-Ring
is-prop-is-closed-under-right-multiplication-subset-Ring =
is-prop-type-Prop is-closed-under-right-multiplication-subset-Ring-Prop


### The condition that a subset is an additive subgroup

module _
{l1 : Level} (R : Ring l1)
where

is-additive-subgroup-subset-Ring :
{l2 : Level} → subset-Ring l2 R → UU (l1 ⊔ l2)
is-additive-subgroup-subset-Ring = is-subgroup-Ab (ab-Ring R)

is-prop-is-additive-subgroup-subset-Ring :
{l2 : Level} (A : subset-Ring l2 R) →
is-prop (is-additive-subgroup-subset-Ring A)
is-prop-is-additive-subgroup-subset-Ring =
is-prop-is-subgroup-Ab (ab-Ring R)