Homotopy Type Theory UMyn8W7b (Rev #73)

As of 6 June 2022, the HoTT web is regarded as deprecated. The vast majority of the articles have since been ported to the main nLab web. All further HoTT-related editing should happen on the main nLab web.

Commutative algebra

Commutative algebra

Trivial ring

A commutative ring $R$ is trivial if $0 = 1$ .

Discrete rings

A commutative ring $R$ is discrete if for all elements $x:R$ and $y:R$ , either $x = y$ , or $x = y$ implies $0 = 1$ .

\prod_{x:R} \prod_{y:R} (x = y) + (x = y) \to (0 = 1)

Regular elements

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

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

A term $e:R$ is right regular if for all $a:R$ and $b:R$ , $a \cdot e = b \cdot e$ implies $a = b$ .

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

An term $e:R$ is regular if it is both left regular and right regular.

\mathrm{isRegular}(e) \coloneqq \mathrm{isLeftRegular}(e) \times \mathrm{isRightRegular}(e)

The multiplicative monoid of regular elements in $R$ is the submonoid of all regular elements in $R$

\mathrm{Reg}(R) \coloneqq \sum_{e:R} \mathrm{isRegular}(e)

Non-regular elements and integral rings

An element $x:R$ is non-regular if $x$ being regular implies that $0 = 1$

\mathrm{isNonRegular}(x) \coloneqq \mathrm{isRegular}(x) \to (0 = 1)

Zero is always a non-regular element of $R$ . By definition of non-regular, if $0$ is regular, then the ring $R$ is trivial.

A commutative ring is integral if the type of all non-regular elements in $R$ is contractible:

\mathrm{isContr}\left(\sum_{x:R} \mathrm{isNonRegular}(x)\right)

Invertible elements

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

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

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

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

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

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

The multiplicative group of invertible elements in $R$ is the subgroup of all invertible elements in $R$

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

Non-invertible elements and fields

An element $x:R$ is non-invertible if $x$ being invertible implies that $0 = 1$

\mathrm{isNonInvertible}(x) \coloneqq \mathrm{isInvertible}(x) \to (0 = 1)

Zero is always a non-invertible element of $R$ . By definition of non-invertible, if $0$ is invertible, then the ring $R$ is trivial.

A commutative ring is a field if the type of all non-invertible elements in $R$ is contractible:

\mathrm{isContr}\left(\sum_{x:R} \mathrm{isNonInvertible}(x)\right)

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 20, 2022 at 02:30:53 by Anonymous?. See the history of this page for a list of all contributions to it.