Homotopy Type Theory UMyn8W7b (Rev #70, changes)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #69 to #70: Added | Removed | Changed

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 RR, a term e:Re:R is left cancellative if for all a:Ra:R and b:Rb:R, e⋅a=e⋅be \cdot a = e \cdot b implies a=ba = b.

Euclidean semirings

isLeftCancellative(e)≔∏ a:R∏ b:R(e⋅a=e⋅b)→(a=b)\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 semiringe:R R e:R , a is terme:Re:Rright cancellative is if for allleft cancellativea:Ra:R if and for all a b:R a:R b:R , anda⋅e=b : ⋅ R e b:R a \cdot e = b \cdot e , impliese⋅a=e⋅b e \cdot a = e \cdot b implies a=ba = b.

isLeftCancellative isRightCancellative(e)≔∏ a:R∏ b:R(e⋅a=e⋅e=b⋅e)→(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 terme:Re:R is right cancellative if for it all is both left cancellative and right cancellative.a:Ra:R and b:Rb:R, a⋅e=b⋅ea \cdot e = b \cdot e implies a=ba = b.

isRightCancellative isCancellative(e)≔∏ a:RisLeftCancellative∏ b:R(a⋅e=b⋅e) → ×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 terme:Re:Rmonoid of cancellative elements in RR is the subset of all cancellative elements incancellativeRR if it is both left cancellative and right cancellative.

isCancellative Can( e R)≔isLeftCancellative∑ e:R(isCancellativee)×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 RR is the subset of all cancellative elements in RR

Invertible elements

Can(R)≔∑ e:RisCancellative(e)\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)

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.

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

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

Non-cancellative and non-invertible elements

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

Given a commutative ring RR, an element x∈Rx \in R is non-cancellative if: if there is an element y∈Can(R)y \in \mathrm{Can}(R) with injection i:Can(R)→Ri:\mathrm{Can}(R) \to R such that i(y)=xi(y) = x, then 0=10 = 1. An element x∈Rx \in R is non-invertible if: if there is an element y∈R ×y \in R^\times with injection j:R ×→Rj:R^\times \to R such that j(y)=xj(y) = x, then 0=10 = 1.

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

A nA_n abelian groups

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

A 1A_1-abelian groups are pointed objects in abelian groups

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

A 2A_2The -abelian groups are unital magma objects in abelian groupsgroup of units in RR is the subset of all units in RR

A 3A_3-abelian groups are monoid objects in abelian groups

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

Non-cancellative and non-invertible elements

Given a commutative ring RR, the monoid of cancellative elements in RR is denoted as Can(R)\mathrm{Can}(R) with injection i:Can(R)→Ri:\mathrm{Can}(R) \to R and the group of units is denoted as R ×R^\times with injection j:R ×→Rj:R^\times \to R. An element x∈Rx \in R is non-cancellative if for all elements y∈Can(R)y \in \mathrm{Can}(R), if i(y)=xi(y) = x, then 0=10 = 1. An element x∈Rx \in R is non-invertible if for all elements y∈R ×y \in R^\times, if j(y)=xj(y) = x, then 0=10 = 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.

DiscussNext revision (394 more)Previous revision (69 more)Current version of pageHide changesHistory (463 revisions)Rollback Source