Homotopy Type Theory Sandbox (Rev #70, changes)

Showing changes from revision #69 to #70: Added | ~~Removed~~ | ~~Chan~~ged

Commutative algebra

~~As of 6 June 2022, the HoTT web is regarded as deprecated. All further HoTT-related editing should happen on the main nLab web.~~

Cancellative elements

Given a commutative ring $R$ , a term $e:R$ is left cancellative if for all $a:R$ and $b:R$ , $e \cdot a = e \cdot b$ implies $a = b$ .

~~Euclidean semirings~~

\mathrm{isLeftCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(e \cdot a = e \cdot b) \to (a = b)

~~Given~~ A a term ~~additively~~ ~~cancellative~~ ~~commutative~~ ~~semiring~~ $e : R$ R e:R , a is ~~term~~ ~~$e:R$~~ right cancellative is if for all~~left cancellative~~ $a:R$ if and ~~for~~ ~~all~~ $a b : R$ ~~a:R~~ b:R , ~~and~~ $a \cdot e = b : \cdot R e$ ~~b:R~~ a \cdot e = b \cdot e , implies $e \cdot a = e \cdot b$ e ~~\cdot~~ a = e ~~\cdot~~ b ~~implies~~ ~~$a = b$~~ .

isLeftCancellative isRightCancellative (e) ≔ \prod_{a : R} \prod_{b : R} (e \cdot a = e \cdot e = b \cdot e) \to (a = b)

~~\mathrm{isLeftCancellative}(e)~~ \mathrm{isRightCancellative}(e) \coloneqq \prod_{a:R} \prod_{b ~~:R}(e~~ :R}(a \cdot a = e = b \cdot b) e) \to (a = b)

A An term $e:R$ is ~~right~~ cancellative if ~~for~~ it ~~all~~ is both left cancellative and right cancellative. ~~$a:R$~~ ~~and~~ ~~$b:R$~~ , ~~$a \cdot e = b \cdot e$~~ ~~implies~~ ~~$a = b$~~ .

isRightCancellative isCancellative (e) ≔ \prod_{a : R} isLeftCancellative \prod_{b : R} (a \cdot e = b \cdot e) \to \times isRightCancellative (a e = b)

~~\mathrm{isRightCancellative}(e)~~ \mathrm{isCancellative}(e) \coloneqq ~~\prod_{a:R}~~ \mathrm{isLeftCancellative}(e) ~~\prod_{b~~ \times ~~:R}(a~~ \mathrm{isRightCancellative}(e) ~~\cdot~~ e = b ~~\cdot~~ e) ~~\to~~ (a = b)

An The ~~term~~ ~~$e:R$~~ monoid of cancellative elements in $R$ is the subset of all cancellative elements in~~cancellative~~ $R$ ~~if it is both left cancellative and right cancellative.~~

isCancellative Can (e R) ≔ isLeftCancellative \sum_{e : R} (isCancellative e) \times isRightCancellative (e)

~~\mathrm{isCancellative}(e)~~ \mathrm{Can}(R) \coloneqq ~~\mathrm{isLeftCancellative}(e)~~ \sum_{e:R} ~~\times~~ \mathrm{isCancellative}(e) ~~\mathrm{isRightCancellative}(e)~~

~~The multiplicative submonoid of cancellative elements in $R$ is the subset of all cancellative elements in $R$~~

Invertible elements

~~$\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)$~~

Given a commutative ring $R$ , a term $e:R$ is left invertible if the fiber of right multiplication by $e$ at $1$ is inhabited.

A Euclidean semiring is a additively cancellative commutative semiring $R$ for which there exists a function $d \colon \mathrm{Can}(R) \to \mathbb{N}$ from the multiplicative submonoid of cancellative elements in $R$ to the natural numbers, often called a degree function, a function $(-)\div(-):R \times \mathrm{Can}(R) \to R$ called the division function, and a function $(-)\;\%\;(-):R \times \mathrm{Can}(R) \to R$ called the remainder function, such that for all $a \in R$ and $b \in \mathrm{Can}(R)$ , $a = (a \div b) \cdot b + (a\;\%\; b)$ and either $a\;\%\; b = 0$ or $d(a\;\%\; b) \lt d(b)$ .

\mathrm{isLeftInvertible}(e) \coloneqq \sum_{a:R} a \cdot e = 1

~~Non-cancellative and non-invertible elements~~

A term $e:R$ is right invertible if the fiber of left multiplication by $e$ at $1$ is inhabited.

Given a commutative ring $R$ , an element $x \in R$ is non-cancellative if: if there is an element $y \in \mathrm{Can}(R)$ with injection $i:\mathrm{Can}(R) \to R$ such that $i(y) = x$ , then $0 = 1$ . An element $x \in R$ is non-invertible if: if there is an element $y \in R^\times$ with injection $j:R^\times \to R$ such that $j(y) = x$ , then $0 = 1$ .

\mathrm{isRightInvertible}(e) \coloneqq \sum_{a:R} e \cdot a = 1

~~$A_n$ abelian groups~~

An term $e:R$ is invertible or a unit if it is both left invertible and right invertible.

~~$A_1$ -abelian groups are pointed objects in abelian groups~~

\mathrm{isInvertible}(e) \coloneqq \mathrm{isLeftInvertible}(e) \times \mathrm{isRightInvertible}(e)

~~$A_2$~~ The ~~-abelian groups are unital magma objects in abelian groups~~group of units in $R$ is the subset of all units in $R$

~~$A_3$ -abelian groups are monoid objects in abelian groups~~

R^\times \coloneqq \sum_{e:R} \mathrm{isInvertible}(e)

Non-cancellative and non-invertible elements

Given a commutative ring $R$ , the monoid of cancellative elements in $R$ is denoted as $\mathrm{Can}(R)$ with injection $i:\mathrm{Can}(R) \to R$ and the group of units is denoted as $R^\times$ with injection $j:R^\times \to R$ . An element $x \in R$ is non-cancellative if for all elements $y \in \mathrm{Can}(R)$ , if $i(y) = x$ , then $0 = 1$ . An element $x \in R$ is non-invertible if for all elements $y \in R^\times$ , if $j(y) = x$ , then $0 = 1$ .

A commutative ring is an integral domain if every non-cancellative element is equal to zero. A commutative ring is a field if every non-invertible element is equal to zero.

References

Frank Quinn, Proof Projects for Teachers (pdf)
Henri Lombardi, Claude Quitté, Commutative algebra: Constructive methods (Finite projective modules) (arXiv:1605.04832)

category: not redirected to nlab yet

Revision on June 19, 2022 at 21:18:24 by Anonymous?. See the history of this page for a list of all contributions to it.

Homotopy Type Theory Sandbox (Rev #70, changes)

Commutative algebra

Cancellative elements

Euclidean semirings

Invertible elements

Non-cancellative and non-invertible elements

A nA_n abelian groups

Non-cancellative and non-invertible elements

References

$A_n$ abelian groups