This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Invertible elements in monoids
module group-theory.invertible-elements-monoids where
Imports
open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.injective-maps open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.universe-levels open import group-theory.monoids
Idea
An element x : M in a monoid M is said to be
left invertible if there is an element y : M such that yx ＝ e, and it
is said to be right invertible if there is an element y : M such that
xy ＝ e. The element x is said to be invertible if it has a two-sided
inverse, i.e., if if there is an element y : M such that xy = e and
yx = e. Left inverses of elements are also called retractions and right
inverses are also called sections.
Definitions
Right invertible elements
module _ {l : Level} (M : Monoid l) (x : type-Monoid M) where is-right-inverse-element-Monoid : type-Monoid M → UU l is-right-inverse-element-Monoid y = mul-Monoid M x y ＝ unit-Monoid M is-right-invertible-element-Monoid : UU l is-right-invertible-element-Monoid = Σ (type-Monoid M) is-right-inverse-element-Monoid module _ {l : Level} (M : Monoid l) {x : type-Monoid M} where section-is-right-invertible-element-Monoid : is-right-invertible-element-Monoid M x → type-Monoid M section-is-right-invertible-element-Monoid = pr1 is-right-inverse-section-is-right-invertible-element-Monoid : (H : is-right-invertible-element-Monoid M x) → is-right-inverse-element-Monoid M x ( section-is-right-invertible-element-Monoid H) is-right-inverse-section-is-right-invertible-element-Monoid = pr2
Left invertible elements
module _ {l : Level} (M : Monoid l) (x : type-Monoid M) where is-left-inverse-element-Monoid : type-Monoid M → UU l is-left-inverse-element-Monoid y = mul-Monoid M y x ＝ unit-Monoid M is-left-invertible-element-Monoid : UU l is-left-invertible-element-Monoid = Σ (type-Monoid M) is-left-inverse-element-Monoid module _ {l : Level} (M : Monoid l) {x : type-Monoid M} where retraction-is-left-invertible-element-Monoid : is-left-invertible-element-Monoid M x → type-Monoid M retraction-is-left-invertible-element-Monoid = pr1 is-left-inverse-retraction-is-left-invertible-element-Monoid : (H : is-left-invertible-element-Monoid M x) → is-left-inverse-element-Monoid M x ( retraction-is-left-invertible-element-Monoid H) is-left-inverse-retraction-is-left-invertible-element-Monoid = pr2
Invertible elements
module _ {l : Level} (M : Monoid l) (x : type-Monoid M) where is-inverse-element-Monoid : type-Monoid M → UU l is-inverse-element-Monoid y = is-right-inverse-element-Monoid M x y × is-left-inverse-element-Monoid M x y is-invertible-element-Monoid : UU l is-invertible-element-Monoid = Σ (type-Monoid M) is-inverse-element-Monoid module _ {l : Level} (M : Monoid l) {x : type-Monoid M} where inv-is-invertible-element-Monoid : is-invertible-element-Monoid M x → type-Monoid M inv-is-invertible-element-Monoid = pr1 is-right-inverse-inv-is-invertible-element-Monoid : (H : is-invertible-element-Monoid M x) → is-right-inverse-element-Monoid M x (inv-is-invertible-element-Monoid H) is-right-inverse-inv-is-invertible-element-Monoid H = pr1 (pr2 H) is-left-inverse-inv-is-invertible-element-Monoid : (H : is-invertible-element-Monoid M x) → is-left-inverse-element-Monoid M x (inv-is-invertible-element-Monoid H) is-left-inverse-inv-is-invertible-element-Monoid H = pr2 (pr2 H)
Properties
Being an invertible element is a property
module _ {l : Level} (M : Monoid l) where all-elements-equal-is-invertible-element-Monoid : (x : type-Monoid M) → all-elements-equal (is-invertible-element-Monoid M x) all-elements-equal-is-invertible-element-Monoid x (y , p , q) (y' , p' , q') = eq-type-subtype ( λ z → product-Prop ( Id-Prop (set-Monoid M) (mul-Monoid M x z) (unit-Monoid M)) ( Id-Prop (set-Monoid M) (mul-Monoid M z x) (unit-Monoid M))) ( ( inv (left-unit-law-mul-Monoid M y)) ∙ ( inv (ap (λ z → mul-Monoid M z y) q')) ∙ ( associative-mul-Monoid M y' x y) ∙ ( ap (mul-Monoid M y') p) ∙ ( right-unit-law-mul-Monoid M y')) is-prop-is-invertible-element-Monoid : (x : type-Monoid M) → is-prop (is-invertible-element-Monoid M x) is-prop-is-invertible-element-Monoid x = is-prop-all-elements-equal ( all-elements-equal-is-invertible-element-Monoid x) is-invertible-element-prop-Monoid : type-Monoid M → Prop l pr1 (is-invertible-element-prop-Monoid x) = is-invertible-element-Monoid M x pr2 (is-invertible-element-prop-Monoid x) = is-prop-is-invertible-element-Monoid x
Inverses are left/right inverses
module _ {l : Level} (M : Monoid l) where is-left-invertible-is-invertible-element-Monoid : (x : type-Monoid M) → is-invertible-element-Monoid M x → is-left-invertible-element-Monoid M x pr1 (is-left-invertible-is-invertible-element-Monoid x is-invertible-x) = pr1 is-invertible-x pr2 (is-left-invertible-is-invertible-element-Monoid x is-invertible-x) = pr2 (pr2 is-invertible-x) is-right-invertible-is-invertible-element-Monoid : (x : type-Monoid M) → is-invertible-element-Monoid M x → is-right-invertible-element-Monoid M x pr1 (is-right-invertible-is-invertible-element-Monoid x is-invertible-x) = pr1 is-invertible-x pr2 (is-right-invertible-is-invertible-element-Monoid x is-invertible-x) = pr1 (pr2 is-invertible-x)
The inverse invertible element
module _ {l : Level} (M : Monoid l) where is-right-invertible-left-inverse-Monoid : (x : type-Monoid M) (lx : is-left-invertible-element-Monoid M x) → is-right-invertible-element-Monoid M (pr1 lx) pr1 (is-right-invertible-left-inverse-Monoid x lx) = x pr2 (is-right-invertible-left-inverse-Monoid x lx) = pr2 lx is-left-invertible-right-inverse-Monoid : (x : type-Monoid M) (rx : is-right-invertible-element-Monoid M x) → is-left-invertible-element-Monoid M (pr1 rx) pr1 (is-left-invertible-right-inverse-Monoid x rx) = x pr2 (is-left-invertible-right-inverse-Monoid x rx) = pr2 rx is-invertible-element-inverse-Monoid : (x : type-Monoid M) (x' : is-invertible-element-Monoid M x) → is-invertible-element-Monoid M (pr1 x') pr1 (is-invertible-element-inverse-Monoid x x') = x pr1 (pr2 (is-invertible-element-inverse-Monoid x x')) = pr2 (pr2 x') pr2 (pr2 (is-invertible-element-inverse-Monoid x x')) = pr1 (pr2 x')
Any invertible element of a monoid has a contractible type of right inverses
module _ {l : Level} (M : Monoid l) where is-contr-is-right-invertible-element-Monoid : (x : type-Monoid M) → is-invertible-element-Monoid M x → is-contr (is-right-invertible-element-Monoid M x) pr1 (pr1 (is-contr-is-right-invertible-element-Monoid x (y , p , q))) = y pr2 (pr1 (is-contr-is-right-invertible-element-Monoid x (y , p , q))) = p pr2 (is-contr-is-right-invertible-element-Monoid x (y , p , q)) (y' , q') = eq-type-subtype ( λ u → Id-Prop (set-Monoid M) (mul-Monoid M x u) (unit-Monoid M)) ( ( inv (right-unit-law-mul-Monoid M y)) ∙ ( ap (mul-Monoid M y) (inv q')) ∙ ( inv (associative-mul-Monoid M y x y')) ∙ ( ap (mul-Monoid' M y') q) ∙ ( left-unit-law-mul-Monoid M y'))
Any invertible element of a monoid has a contractible type of left inverses
module _ {l : Level} (M : Monoid l) where is-contr-is-left-invertible-Monoid : (x : type-Monoid M) → is-invertible-element-Monoid M x → is-contr (is-left-invertible-element-Monoid M x) pr1 (pr1 (is-contr-is-left-invertible-Monoid x (y , p , q))) = y pr2 (pr1 (is-contr-is-left-invertible-Monoid x (y , p , q))) = q pr2 (is-contr-is-left-invertible-Monoid x (y , p , q)) (y' , p') = eq-type-subtype ( λ u → Id-Prop (set-Monoid M) (mul-Monoid M u x) (unit-Monoid M)) ( ( inv (left-unit-law-mul-Monoid M y)) ∙ ( ap (mul-Monoid' M y) (inv p')) ∙ ( associative-mul-Monoid M y' x y) ∙ ( ap (mul-Monoid M y') p) ∙ ( right-unit-law-mul-Monoid M y'))
The unit of a monoid is invertible
module _ {l : Level} (M : Monoid l) where is-left-invertible-element-unit-Monoid : is-left-invertible-element-Monoid M (unit-Monoid M) pr1 is-left-invertible-element-unit-Monoid = unit-Monoid M pr2 is-left-invertible-element-unit-Monoid = left-unit-law-mul-Monoid M (unit-Monoid M) is-right-invertible-element-unit-Monoid : is-right-invertible-element-Monoid M (unit-Monoid M) pr1 is-right-invertible-element-unit-Monoid = unit-Monoid M pr2 is-right-invertible-element-unit-Monoid = left-unit-law-mul-Monoid M (unit-Monoid M) is-invertible-element-unit-Monoid : is-invertible-element-Monoid M (unit-Monoid M) pr1 is-invertible-element-unit-Monoid = unit-Monoid M pr1 (pr2 is-invertible-element-unit-Monoid) = left-unit-law-mul-Monoid M (unit-Monoid M) pr2 (pr2 is-invertible-element-unit-Monoid) = left-unit-law-mul-Monoid M (unit-Monoid M)
Invertible elements are closed under multiplication
module _ {l : Level} (M : Monoid l) where is-left-invertible-element-mul-Monoid : (x y : type-Monoid M) → is-left-invertible-element-Monoid M x → is-left-invertible-element-Monoid M y → is-left-invertible-element-Monoid M (mul-Monoid M x y) pr1 (is-left-invertible-element-mul-Monoid x y (lx , H) (ly , I)) = mul-Monoid M ly lx pr2 (is-left-invertible-element-mul-Monoid x y (lx , H) (ly , I)) = ( associative-mul-Monoid M ly lx (mul-Monoid M x y)) ∙ ( ap ( mul-Monoid M ly) ( ( inv (associative-mul-Monoid M lx x y)) ∙ ( ap (λ z → mul-Monoid M z y) H) ∙ ( left-unit-law-mul-Monoid M y))) ∙ ( I) is-right-invertible-element-mul-Monoid : (x y : type-Monoid M) → is-right-invertible-element-Monoid M x → is-right-invertible-element-Monoid M y → is-right-invertible-element-Monoid M (mul-Monoid M x y) pr1 (is-right-invertible-element-mul-Monoid x y (rx , H) (ry , I)) = mul-Monoid M ry rx pr2 (is-right-invertible-element-mul-Monoid x y (rx , H) (ry , I)) = ( associative-mul-Monoid M x y (mul-Monoid M ry rx)) ∙ ( ap ( mul-Monoid M x) ( ( inv (associative-mul-Monoid M y ry rx)) ∙ ( ap (λ z → mul-Monoid M z rx) I) ∙ ( left-unit-law-mul-Monoid M rx))) ∙ ( H) is-invertible-element-mul-Monoid : (x y : type-Monoid M) → is-invertible-element-Monoid M x → is-invertible-element-Monoid M y → is-invertible-element-Monoid M (mul-Monoid M x y) pr1 (is-invertible-element-mul-Monoid x y (x' , Lx , Rx) (y' , Ly , Ry)) = mul-Monoid M y' x' pr1 (pr2 (is-invertible-element-mul-Monoid x y H K)) = pr2 ( is-right-invertible-element-mul-Monoid x y ( is-right-invertible-is-invertible-element-Monoid M x H) ( is-right-invertible-is-invertible-element-Monoid M y K)) pr2 (pr2 (is-invertible-element-mul-Monoid x y H K)) = pr2 ( is-left-invertible-element-mul-Monoid x y ( is-left-invertible-is-invertible-element-Monoid M x H) ( is-left-invertible-is-invertible-element-Monoid M y K))
The inverse of an invertible element is invertible
module _ {l : Level} (M : Monoid l) where is-invertible-element-inv-is-invertible-element-Monoid : {x : type-Monoid M} (H : is-invertible-element-Monoid M x) → is-invertible-element-Monoid M (inv-is-invertible-element-Monoid M H) pr1 (is-invertible-element-inv-is-invertible-element-Monoid {x} H) = x pr1 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) = is-left-inverse-inv-is-invertible-element-Monoid M H pr2 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) = is-right-inverse-inv-is-invertible-element-Monoid M H
An element is invertible if and only if multiplying by it is an equivalence
Proof: Suppose that the map z ↦ xz is an equivalence. Then there is a
unique element y such that xy ＝ 1. Thus we have a right inverse of x. To
see that y is also a left inverse of x, note that the map z ↦ xz is
injective by the assumption that it is an equivalence. Therefore it suffices to
show that x(yx) ＝ x1. This follows from the following calculation:
x(yx) ＝ (xy)x ＝ 1x ＝ x ＝ x1.
This completes the proof that if z ↦ xz is an equivalence, then x is
invertible. The converse is straightfoward.
In the following code we give the above proof, as well as the analogous proof
that x is invertible if z ↦ zx is an equivalence, and the converse of both
statements.
An element x is invertible if and only if z ↦ xz is an equivalence
module _ {l : Level} (M : Monoid l) {x : type-Monoid M} where inv-is-invertible-element-is-equiv-mul-Monoid : is-equiv (mul-Monoid M x) → type-Monoid M inv-is-invertible-element-is-equiv-mul-Monoid H = map-inv-is-equiv H (unit-Monoid M) is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid : (H : is-equiv (mul-Monoid M x)) → mul-Monoid M x (inv-is-invertible-element-is-equiv-mul-Monoid H) ＝ unit-Monoid M is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H = is-section-map-inv-is-equiv H (unit-Monoid M) is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid : (H : is-equiv (mul-Monoid M x)) → mul-Monoid M (inv-is-invertible-element-is-equiv-mul-Monoid H) x ＝ unit-Monoid M is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H = is-injective-is-equiv H ( ( inv (associative-mul-Monoid M _ _ _)) ∙ ( ap ( mul-Monoid' M x) ( is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H)) ∙ ( left-unit-law-mul-Monoid M x) ∙ ( inv (right-unit-law-mul-Monoid M x))) is-invertible-element-is-equiv-mul-Monoid : is-equiv (mul-Monoid M x) → is-invertible-element-Monoid M x pr1 (is-invertible-element-is-equiv-mul-Monoid H) = inv-is-invertible-element-is-equiv-mul-Monoid H pr1 (pr2 (is-invertible-element-is-equiv-mul-Monoid H)) = is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H pr2 (pr2 (is-invertible-element-is-equiv-mul-Monoid H)) = is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H left-div-is-invertible-element-Monoid : is-invertible-element-Monoid M x → type-Monoid M → type-Monoid M left-div-is-invertible-element-Monoid H = mul-Monoid M (inv-is-invertible-element-Monoid M H) is-section-left-div-is-invertible-element-Monoid : (H : is-invertible-element-Monoid M x) → mul-Monoid M x ∘ left-div-is-invertible-element-Monoid H ~ id is-section-left-div-is-invertible-element-Monoid H y = ( inv (associative-mul-Monoid M _ _ _)) ∙ ( ap ( mul-Monoid' M y) ( is-right-inverse-inv-is-invertible-element-Monoid M H)) ∙ ( left-unit-law-mul-Monoid M y) is-retraction-left-div-is-invertible-element-Monoid : (H : is-invertible-element-Monoid M x) → left-div-is-invertible-element-Monoid H ∘ mul-Monoid M x ~ id is-retraction-left-div-is-invertible-element-Monoid H y = ( inv (associative-mul-Monoid M _ _ _)) ∙ ( ap ( mul-Monoid' M y) ( is-left-inverse-inv-is-invertible-element-Monoid M H)) ∙ ( left-unit-law-mul-Monoid M y) is-equiv-mul-is-invertible-element-Monoid : is-invertible-element-Monoid M x → is-equiv (mul-Monoid M x) is-equiv-mul-is-invertible-element-Monoid H = is-equiv-is-invertible ( left-div-is-invertible-element-Monoid H) ( is-section-left-div-is-invertible-element-Monoid H) ( is-retraction-left-div-is-invertible-element-Monoid H)
An element x is invertible if and only if z ↦ zx is an equivalence
module _ {l : Level} (M : Monoid l) {x : type-Monoid M} where inv-is-invertible-element-is-equiv-mul-Monoid' : is-equiv (mul-Monoid' M x) → type-Monoid M inv-is-invertible-element-is-equiv-mul-Monoid' H = map-inv-is-equiv H (unit-Monoid M) is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' : (H : is-equiv (mul-Monoid' M x)) → mul-Monoid M (inv-is-invertible-element-is-equiv-mul-Monoid' H) x ＝ unit-Monoid M is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H = is-section-map-inv-is-equiv H (unit-Monoid M) is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' : (H : is-equiv (mul-Monoid' M x)) → mul-Monoid M x (inv-is-invertible-element-is-equiv-mul-Monoid' H) ＝ unit-Monoid M is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H = is-injective-is-equiv H ( ( associative-mul-Monoid M _ _ _) ∙ ( ap ( mul-Monoid M x) ( is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H)) ∙ ( right-unit-law-mul-Monoid M x) ∙ ( inv (left-unit-law-mul-Monoid M x))) is-invertible-element-is-equiv-mul-Monoid' : is-equiv (mul-Monoid' M x) → is-invertible-element-Monoid M x pr1 (is-invertible-element-is-equiv-mul-Monoid' H) = inv-is-invertible-element-is-equiv-mul-Monoid' H pr1 (pr2 (is-invertible-element-is-equiv-mul-Monoid' H)) = is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H pr2 (pr2 (is-invertible-element-is-equiv-mul-Monoid' H)) = is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H right-div-is-invertible-element-Monoid : is-invertible-element-Monoid M x → type-Monoid M → type-Monoid M right-div-is-invertible-element-Monoid H = mul-Monoid' M (inv-is-invertible-element-Monoid M H) is-section-right-div-is-invertible-element-Monoid : (H : is-invertible-element-Monoid M x) → mul-Monoid' M x ∘ right-div-is-invertible-element-Monoid H ~ id is-section-right-div-is-invertible-element-Monoid H y = ( associative-mul-Monoid M _ _ _) ∙ ( ap ( mul-Monoid M y) ( is-left-inverse-inv-is-invertible-element-Monoid M H)) ∙ ( right-unit-law-mul-Monoid M y) is-retraction-right-div-is-invertible-element-Monoid : (H : is-invertible-element-Monoid M x) → right-div-is-invertible-element-Monoid H ∘ mul-Monoid' M x ~ id is-retraction-right-div-is-invertible-element-Monoid H y = ( associative-mul-Monoid M _ _ _) ∙ ( ap ( mul-Monoid M y) ( is-right-inverse-inv-is-invertible-element-Monoid M H)) ∙ ( right-unit-law-mul-Monoid M y) is-equiv-mul-is-invertible-element-Monoid' : is-invertible-element-Monoid M x → is-equiv (mul-Monoid' M x) is-equiv-mul-is-invertible-element-Monoid' H = is-equiv-is-invertible ( right-div-is-invertible-element-Monoid H) ( is-section-right-div-is-invertible-element-Monoid H) ( is-retraction-right-div-is-invertible-element-Monoid H)
See also
- The core of a monoid is defined in
group-theory.cores-monoids.