Homotopy Type Theory Sandbox > history (changes)

Showing changes from revision #73 to #74: Added | Removed | Changed


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.


Contents

Commutative algebra

Trivial ring

A commutative ring RR is trivial if 0=10 = 1.

Discrete rings

A commutative ring RR is discrete if for all elements x:Rx:R and y:Ry:R, either x=yx = y, or x=yx = y implies 0=10 = 1.

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

Regular elements

Given a commutative ring RR, a term e:Re:R is left regular if for all a:Ra:R and b:Rb:R, ea=ebe \cdot a = e \cdot b implies a=ba = b.

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

A term e:Re:R is right regular if for all a:Ra:R and b:Rb:R, ae=bea \cdot e = b \cdot e implies a=ba = b.

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

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

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

The multiplicative monoid of regular elements in RR is the submonoid of all regular elements in RR

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

Non-regular elements and integral rings

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

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

Zero is always a non-regular element of RR. By definition of non-regular, if 00 is regular, then the ring RR is trivial.

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

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

Invertible elements

Given a commutative ring RR, a term e:Re:R is left invertible if the fiber of right multiplication by ee at 11 is inhabited.

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

A term e:Re:R is right invertible if the fiber of left multiplication by ee at 11 is inhabited.

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

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

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

The multiplicative group of invertible elements in RR is the subgroup of all invertible elements in RR

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

Non-invertible elements and fields

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

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

Zero is always a non-invertible element of RR. By definition of non-invertible, if 00 is invertible, then the ring RR is trivial.

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

isContr( x:RisNonInvertible(x))\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)

Last revised on June 19, 2022 at 23:05:26. See the history of this page for a list of all contributions to it.