Invertible elements in rings
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Gregor Perčič and malarbol.
Created on 2022-03-21.
Last modified on 2024-04-25.
module ring-theory.invertible-elements-rings where
Imports
open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.invertible-elements-monoids open import ring-theory.rings
Idea
Invertible elements in a ring are elements that have a two-sided multiplicative inverse. Such elements are also called the (multiplicative) units of the ring.
The set of units of any ring forms a
group, called the
group of units. The group of units of a
ring is constructed in
ring-theory.groups-of-units-rings.
Definitions
Left invertible elements of rings
module _ {l : Level} (R : Ring l) where is-left-inverse-element-Ring : (x y : type-Ring R) → UU l is-left-inverse-element-Ring = is-left-inverse-element-Monoid (multiplicative-monoid-Ring R) is-left-invertible-element-Ring : type-Ring R → UU l is-left-invertible-element-Ring = is-left-invertible-element-Monoid (multiplicative-monoid-Ring R) module _ {l : Level} (R : Ring l) {x : type-Ring R} where retraction-is-left-invertible-element-Ring : is-left-invertible-element-Ring R x → type-Ring R retraction-is-left-invertible-element-Ring = retraction-is-left-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-left-inverse-retraction-is-left-invertible-element-Ring : (H : is-left-invertible-element-Ring R x) → is-left-inverse-element-Ring R x ( retraction-is-left-invertible-element-Ring H) is-left-inverse-retraction-is-left-invertible-element-Ring = is-left-inverse-retraction-is-left-invertible-element-Monoid ( multiplicative-monoid-Ring R)
Right invertible elements of rings
module _ {l : Level} (R : Ring l) where is-right-inverse-element-Ring : (x y : type-Ring R) → UU l is-right-inverse-element-Ring = is-right-inverse-element-Monoid (multiplicative-monoid-Ring R) is-right-invertible-element-Ring : type-Ring R → UU l is-right-invertible-element-Ring = is-right-invertible-element-Monoid (multiplicative-monoid-Ring R) module _ {l : Level} (R : Ring l) {x : type-Ring R} where section-is-right-invertible-element-Ring : is-right-invertible-element-Ring R x → type-Ring R section-is-right-invertible-element-Ring = section-is-right-invertible-element-Monoid (multiplicative-monoid-Ring R) is-right-inverse-section-is-right-invertible-element-Ring : (H : is-right-invertible-element-Ring R x) → is-right-inverse-element-Ring R x ( section-is-right-invertible-element-Ring H) is-right-inverse-section-is-right-invertible-element-Ring = is-right-inverse-section-is-right-invertible-element-Monoid ( multiplicative-monoid-Ring R)
Invertible elements of rings
module _ {l : Level} (R : Ring l) (x : type-Ring R) where is-inverse-element-Ring : type-Ring R → UU l is-inverse-element-Ring = is-inverse-element-Monoid (multiplicative-monoid-Ring R) x is-invertible-element-Ring : UU l is-invertible-element-Ring = is-invertible-element-Monoid (multiplicative-monoid-Ring R) x module _ {l : Level} (R : Ring l) {x : type-Ring R} where inv-is-invertible-element-Ring : is-invertible-element-Ring R x → type-Ring R inv-is-invertible-element-Ring = inv-is-invertible-element-Monoid (multiplicative-monoid-Ring R) is-right-inverse-inv-is-invertible-element-Ring : (H : is-invertible-element-Ring R x) → is-right-inverse-element-Ring R x (inv-is-invertible-element-Ring H) is-right-inverse-inv-is-invertible-element-Ring = is-right-inverse-inv-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-left-inverse-inv-is-invertible-element-Ring : (H : is-invertible-element-Ring R x) → is-left-inverse-element-Ring R x (inv-is-invertible-element-Ring H) is-left-inverse-inv-is-invertible-element-Ring = is-left-inverse-inv-is-invertible-element-Monoid ( multiplicative-monoid-Ring R)
Properties
Being an invertible element is a property
module _ {l : Level} (R : Ring l) where is-prop-is-invertible-element-Ring : (x : type-Ring R) → is-prop (is-invertible-element-Ring R x) is-prop-is-invertible-element-Ring = is-prop-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-invertible-element-prop-Ring : type-Ring R → Prop l is-invertible-element-prop-Ring = is-invertible-element-prop-Monoid ( multiplicative-monoid-Ring R)
Inverses are left/right inverses
module _ {l : Level} (R : Ring l) where is-left-invertible-is-invertible-element-Ring : (x : type-Ring R) → is-invertible-element-Ring R x → is-left-invertible-element-Ring R x is-left-invertible-is-invertible-element-Ring = is-left-invertible-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-right-invertible-is-invertible-element-Ring : (x : type-Ring R) → is-invertible-element-Ring R x → is-right-invertible-element-Ring R x is-right-invertible-is-invertible-element-Ring = is-right-invertible-is-invertible-element-Monoid ( multiplicative-monoid-Ring R)
The inverse invertible element
module _ {l : Level} (R : Ring l) where is-right-invertible-left-inverse-Ring : (x : type-Ring R) (H : is-left-invertible-element-Ring R x) → is-right-invertible-element-Ring R ( retraction-is-left-invertible-element-Ring R H) is-right-invertible-left-inverse-Ring = is-right-invertible-left-inverse-Monoid ( multiplicative-monoid-Ring R) is-left-invertible-right-inverse-Ring : (x : type-Ring R) (H : is-right-invertible-element-Ring R x) → is-left-invertible-element-Ring R ( section-is-right-invertible-element-Ring R H) is-left-invertible-right-inverse-Ring = is-left-invertible-right-inverse-Monoid ( multiplicative-monoid-Ring R) is-invertible-element-inverse-Ring : (x : type-Ring R) (H : is-invertible-element-Ring R x) → is-invertible-element-Ring R ( inv-is-invertible-element-Ring R H) is-invertible-element-inverse-Ring = is-invertible-element-inverse-Monoid ( multiplicative-monoid-Ring R)
Any invertible element of a monoid has a contractible type of right inverses
module _ {l : Level} (R : Ring l) where is-contr-is-right-invertible-element-Ring : (x : type-Ring R) → is-invertible-element-Ring R x → is-contr (is-right-invertible-element-Ring R x) is-contr-is-right-invertible-element-Ring = is-contr-is-right-invertible-element-Monoid ( multiplicative-monoid-Ring R)
Any invertible element of a monoid has a contractible type of left inverses
module _ {l : Level} (R : Ring l) where is-contr-is-left-invertible-Ring : (x : type-Ring R) → is-invertible-element-Ring R x → is-contr (is-left-invertible-element-Ring R x) is-contr-is-left-invertible-Ring = is-contr-is-left-invertible-Monoid ( multiplicative-monoid-Ring R)
The unit of a monoid is invertible
module _ {l : Level} (R : Ring l) where is-left-invertible-element-one-Ring : is-left-invertible-element-Ring R (one-Ring R) is-left-invertible-element-one-Ring = is-left-invertible-element-unit-Monoid ( multiplicative-monoid-Ring R) is-right-invertible-element-one-Ring : is-right-invertible-element-Ring R (one-Ring R) is-right-invertible-element-one-Ring = is-right-invertible-element-unit-Monoid ( multiplicative-monoid-Ring R) is-invertible-element-one-Ring : is-invertible-element-Ring R (one-Ring R) is-invertible-element-one-Ring = is-invertible-element-unit-Monoid ( multiplicative-monoid-Ring R)
Invertible elements are closed under multiplication
module _ {l : Level} (R : Ring l) where is-left-invertible-element-mul-Ring : (x y : type-Ring R) → is-left-invertible-element-Ring R x → is-left-invertible-element-Ring R y → is-left-invertible-element-Ring R (mul-Ring R x y) is-left-invertible-element-mul-Ring = is-left-invertible-element-mul-Monoid ( multiplicative-monoid-Ring R) is-right-invertible-element-mul-Ring : (x y : type-Ring R) → is-right-invertible-element-Ring R x → is-right-invertible-element-Ring R y → is-right-invertible-element-Ring R (mul-Ring R x y) is-right-invertible-element-mul-Ring = is-right-invertible-element-mul-Monoid ( multiplicative-monoid-Ring R) is-invertible-element-mul-Ring : (x y : type-Ring R) → is-invertible-element-Ring R x → is-invertible-element-Ring R y → is-invertible-element-Ring R (mul-Ring R x y) is-invertible-element-mul-Ring = is-invertible-element-mul-Monoid ( multiplicative-monoid-Ring R)
Invertible elements are closed under negatives
module _ {l : Level} (R : Ring l) where is-invertible-element-neg-Ring : (x : type-Ring R) → is-invertible-element-Ring R x → is-invertible-element-Ring R (neg-Ring R x) is-invertible-element-neg-Ring x = map-Σ _ ( neg-Ring R) ( λ y → map-product ( mul-neg-Ring R x y ∙_) ( mul-neg-Ring R y x ∙_)) is-invertible-element-neg-Ring' : (x : type-Ring R) → is-invertible-element-Ring R (neg-Ring R x) → is-invertible-element-Ring R x is-invertible-element-neg-Ring' x H = tr ( is-invertible-element-Ring R) ( neg-neg-Ring R x) ( is-invertible-element-neg-Ring (neg-Ring R x) H)
The inverse of an invertible element is invertible
module _ {l : Level} (R : Ring l) where is-invertible-element-inv-is-invertible-element-Ring : {x : type-Ring R} (H : is-invertible-element-Ring R x) → is-invertible-element-Ring R (inv-is-invertible-element-Ring R H) is-invertible-element-inv-is-invertible-element-Ring = is-invertible-element-inv-is-invertible-element-Monoid ( multiplicative-monoid-Ring R)
An element is invertible if and only if multiplying by it is an equivalence
An element x is invertible if and only if z ↦ xz is an equivalence
module _ {l : Level} (R : Ring l) {x : type-Ring R} where inv-is-invertible-element-is-equiv-mul-Ring : is-equiv (mul-Ring R x) → type-Ring R inv-is-invertible-element-is-equiv-mul-Ring = inv-is-invertible-element-is-equiv-mul-Monoid ( multiplicative-monoid-Ring R) is-right-inverse-inv-is-invertible-element-is-equiv-mul-Ring : (H : is-equiv (mul-Ring R x)) → mul-Ring R x (inv-is-invertible-element-is-equiv-mul-Ring H) ＝ one-Ring R is-right-inverse-inv-is-invertible-element-is-equiv-mul-Ring = is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid ( multiplicative-monoid-Ring R) is-left-inverse-inv-is-invertible-element-is-equiv-mul-Ring : (H : is-equiv (mul-Ring R x)) → mul-Ring R (inv-is-invertible-element-is-equiv-mul-Ring H) x ＝ one-Ring R is-left-inverse-inv-is-invertible-element-is-equiv-mul-Ring = is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid ( multiplicative-monoid-Ring R) is-invertible-element-is-equiv-mul-Ring : is-equiv (mul-Ring R x) → is-invertible-element-Ring R x is-invertible-element-is-equiv-mul-Ring = is-invertible-element-is-equiv-mul-Monoid ( multiplicative-monoid-Ring R) left-div-is-invertible-element-Ring : is-invertible-element-Ring R x → type-Ring R → type-Ring R left-div-is-invertible-element-Ring = left-div-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-section-left-div-is-invertible-element-Ring : (H : is-invertible-element-Ring R x) → mul-Ring R x ∘ left-div-is-invertible-element-Ring H ~ id is-section-left-div-is-invertible-element-Ring = is-section-left-div-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-retraction-left-div-is-invertible-element-Ring : (H : is-invertible-element-Ring R x) → left-div-is-invertible-element-Ring H ∘ mul-Ring R x ~ id is-retraction-left-div-is-invertible-element-Ring = is-retraction-left-div-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-equiv-mul-is-invertible-element-Ring : is-invertible-element-Ring R x → is-equiv (mul-Ring R x) is-equiv-mul-is-invertible-element-Ring = is-equiv-mul-is-invertible-element-Monoid ( multiplicative-monoid-Ring R)
An element x is invertible if and only if z ↦ zx is an equivalence
module _ {l : Level} (R : Ring l) {x : type-Ring R} where inv-is-invertible-element-is-equiv-mul-Ring' : is-equiv (mul-Ring' R x) → type-Ring R inv-is-invertible-element-is-equiv-mul-Ring' = inv-is-invertible-element-is-equiv-mul-Monoid' ( multiplicative-monoid-Ring R) is-left-inverse-inv-is-invertible-element-is-equiv-mul-Ring' : (H : is-equiv (mul-Ring' R x)) → mul-Ring R (inv-is-invertible-element-is-equiv-mul-Ring' H) x ＝ one-Ring R is-left-inverse-inv-is-invertible-element-is-equiv-mul-Ring' = is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' ( multiplicative-monoid-Ring R) is-right-inverse-inv-is-invertible-element-is-equiv-mul-Ring' : (H : is-equiv (mul-Ring' R x)) → mul-Ring R x (inv-is-invertible-element-is-equiv-mul-Ring' H) ＝ one-Ring R is-right-inverse-inv-is-invertible-element-is-equiv-mul-Ring' = is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' ( multiplicative-monoid-Ring R) is-invertible-element-is-equiv-mul-Ring' : is-equiv (mul-Ring' R x) → is-invertible-element-Ring R x is-invertible-element-is-equiv-mul-Ring' = is-invertible-element-is-equiv-mul-Monoid' ( multiplicative-monoid-Ring R) right-div-is-invertible-element-Ring : is-invertible-element-Ring R x → type-Ring R → type-Ring R right-div-is-invertible-element-Ring = right-div-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-section-right-div-is-invertible-element-Ring : (H : is-invertible-element-Ring R x) → mul-Ring' R x ∘ right-div-is-invertible-element-Ring H ~ id is-section-right-div-is-invertible-element-Ring = is-section-right-div-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-retraction-right-div-is-invertible-element-Ring : (H : is-invertible-element-Ring R x) → right-div-is-invertible-element-Ring H ∘ mul-Ring' R x ~ id is-retraction-right-div-is-invertible-element-Ring = is-retraction-right-div-is-invertible-element-Monoid ( multiplicative-monoid-Ring R) is-equiv-mul-is-invertible-element-Ring' : is-invertible-element-Ring R x → is-equiv (mul-Ring' R x) is-equiv-mul-is-invertible-element-Ring' = is-equiv-mul-is-invertible-element-Monoid' ( multiplicative-monoid-Ring R)
See also
- The group of multiplicative units of a ring is defined in
ring-theory.groups-of-units-rings.
Recent changes
- 2024-04-25. malarbol and Fredrik Bakke. The discrete field of rational numbers (#1111).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).