Homotopy Type Theory Sandbox > history (Rev #73, changes)

Showing changes from revision #72 to #73: 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-regular Non-invertible and non-invertible elements and fields

An element x:Rx:R is non-regular non-invertible ifxx being regular invertible implies that0=10 = 1

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

An Zero is always a non-invertible element ofx:R x:R R . is By non-invertible definition of non-invertible, ifx0 x 0 being is invertible invertible, implies then that the ring0R=1 0 R = 1 is trivial.

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

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

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

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

A commutative ring is integral if every non-regular 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)

Real numbers

Pointed abelian groups

A pointed abelian group is a set AA with an element 1:A1:A called one and a binary operation ()():A×AA(-)-(-):A \times A \to A called subtraction such that

  • for all elements a:Aa:A, aa=11a - a = 1 - 1

  • for all elements a:Aa:A, (11)((11)a)=a(1 - 1) - ((1 - 1) - a) = a

  • for all elements a:Aa:A and b:Ab:A, a((11)b)=b((11)a)a - ((1 - 1) - b) = b - ((1 - 1) - a)

  • for all elements a:Aa:A, b:Ab:A, and c:Ac:A, a(bc)=(a((11)c))ba - (b - c) = (a - ((1 - 1) - c)) - b

Pointed halving groups

A pointed halving group is a pointed abelian group G with a function ()/2:GG(-)/2:G \to G called halving or dividing by two such that for all elements g:Gg:G, g/2=gg/2g/2 = g - g/2.

Totally ordered pointed halving groups

A pointed halving group RR is a totally ordered pointed halving group if it comes with a function max:R×RR\max:R \times R \to R such that

  • for all elements a:Ra:R, max(a,a)=a\max(a, a) = a

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=max(b,a)\max(a, b) = \max(b, a)

  • for all elements a:Ra:R, b:Rb:R, and c:Rc:R, max(a,max(b,c))=max(max(a,b),c)\max(a, \max(b, c)) = \max(\max(a, b), c)

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=a\max(a, b) = a or max(a,b)=b\max(a, b) = b

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=b\max(a, b) = b implies that for all elements c:Rc:R, max(ac,bc)=bc\max(a - c, b - c) = b - c

Strictly ordered pointed halving groups

A totally ordered pointed halving group RR is a strictly ordered pointed abelian group if it comes with a type family <\lt such that

  • for all elements a:Ra:R and b:Rb:R, a<ba \lt b is a proposition
  • for all elements a:Ra:R, a<aa \lt a is false
  • for all elements a:Ra:R, b:Rb:R, and c:Rc:R, if a<ca \lt c, then a<ba \lt b or b<cb \lt c
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b is false and b<ab \lt a is false, then a=ba = b
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b, then b<ab \lt a is false.
  • 11<11 - 1 \lt 1
  • for all elements a:Ra:R and b:Rb:R, if 11<a1 - 1 \lt a and 11<b1 - 1 \lt b, then (11)<a((11)b)(1 - 1) \lt a - ((1 - 1) - b)

The homotopy initial strictly ordered pointed halving group is the dyadic rational numbers 𝔻\mathbb{D}.

Archimedean ordered pointed halving groups

A strictly ordered pointed halving group AA is an Archimedean ordered pointed halving group if for all elements a:Aa:A and b:Ab:A, if a<ba \lt b, then there merely exists a dyadic rational number d:𝔻d:\mathbb{D} such that a<h(d)a \lt h(d) and h(d)<bh(d) \lt b.

Sequentially Cauchy complete Archimedean ordered pointed halving groups

Let AA be an Archimedean ordered pointed halving group and let

A + a:A11<aA_{+} \coloneqq \sum_{a:A} 1 - 1 \lt a

be the positive elements in AA.

A sequence in AA is a function x:Ax:\mathbb{N} \to A.

A sequence x:Ax:\mathbb{N} \to A is a Cauchy sequence if for all positive elements ϵ:A +\epsilon:A_{+}, there merely exists a natural number N:N:\mathbb{N} such that for all natural numbers i:i:\mathbb{N} and j:j:\mathbb{N} such that NiN \leq i and NjN \leq j, max(x ix j,x jx i)<ϵ\max(x_i - x_j, x_j - x_i) \lt \epsilon.

An element l:Al:A is said to be a limit of the sequence x:Ax:\mathbb{N} \to A if for all positive elements ϵ:A +\epsilon:A_{+}, there merely exists a natural number N:N:\mathbb{N} such that for all natural numbers i:i:\mathbb{N} such that NiN \leq i, max(x il,lx i)<ϵ\max(x_i - l, l - x_i) \lt \epsilon

AA is sequentially Cauchy complete if every Cauchy sequence in AA merely has a limit.

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