scilib documentation

algebra.invertible

Invertible elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines a typeclass invertible a for elements a with a two-sided multiplicative inverse.

The intent of the typeclass is to provide a way to write e.g. ⅟2 in a ring like ℤ[1/2] where some inverses exist but there is no general ⁻¹ operator; or to specify that a field has characteristic ≠ 2. It is the Type-valued analogue to the Prop-valued is_unit.

For constructions of the invertible element given a characteristic, see algebra/char_p/invertible and other lemmas in that file.

Notation #

⅟a is invertible.inv_of a, the inverse of a

Implementation notes #

The invertible class lives in Type, not Prop, to make computation easier. If multiplication is associative, invertible is a subsingleton anyway.

The simp normal form tries to normalize ⅟a to a ⁻¹. Otherwise, it pushes ⅟ inside the expression as much as possible.

Since invertible a is not a Prop (but it is a subsingleton), we have to be careful about coherence issues: we should avoid having multiple non-defeq instances for invertible a in the same context. This file plays it safe and uses def rather than instance for most definitions, users can choose which instances to use at the point of use.

For example, here's how you can use an invertible 1 instance:

variables {α : Type*} [monoid α]

def something_that_needs_inverses (x : α) [invertible x] := sorry

section
local attribute [instance] invertible_one
def something_one := something_that_needs_inverses 1
end

Tags #

invertible, inverse element, inv_of, a half, one half, a third, one third, ½, ⅓

@[class]

structure invertible {α : Type u} [has_mul α] [has_one α] (a : α) :

Type u

inv_of : α
inv_of_mul_self : ⅟ a * a = 1
mul_inv_of_self : a * ⅟ a = 1

invertible a gives a two-sided multiplicative inverse of a.

Instances of this typeclass

Instances of other typeclasses for invertible

invertible.has_sizeof_inst
invertible.subsingleton

@[simp]

theorem inv_of_mul_self {α : Type u} [has_mul α] [has_one α] (a : α) [invertible a] :

⅟ a * a = 1

@[simp]

theorem mul_inv_of_self {α : Type u} [has_mul α] [has_one α] (a : α) [invertible a] :

a * ⅟ a = 1

@[simp]

theorem inv_of_mul_self_assoc {α : Type u} [monoid α] (a b : α) [invertible a] :

⅟ a * (a * b) = b

@[simp]

theorem mul_inv_of_self_assoc {α : Type u} [monoid α] (a b : α) [invertible a] :

a * (⅟ a * b) = b

@[simp]

theorem mul_inv_of_mul_self_cancel {α : Type u} [monoid α] (a b : α) [invertible b] :

a * ⅟ b * b = a

@[simp]

theorem mul_mul_inv_of_self_cancel {α : Type u} [monoid α] (a b : α) [invertible b] :

a * b * ⅟ b = a

theorem inv_of_eq_right_inv {α : Type u} [monoid α] {a b : α} [invertible a] (hac : a * b = 1) :

⅟ a = b

theorem inv_of_eq_left_inv {α : Type u} [monoid α] {a b : α} [invertible a] (hac : b * a = 1) :

⅟ a = b

theorem invertible_unique {α : Type u} [monoid α] (a b : α) [invertible a] [invertible b] (h : a = b) :

@[protected, instance]

def invertible.subsingleton {α : Type u} [monoid α] (a : α) :

subsingleton (invertible a)

def invertible.copy {α : Type u} [mul_one_class α] {r : α} (hr : invertible r) (s : α) (hs : s = r) :

If r is invertible and s = r, then s is invertible.

Equations

hr.copy s hs = {inv_of := ⅟ r hr, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem coe_unit_of_invertible {α : Type u} [monoid α] (a : α) [invertible a] :

↑(unit_of_invertible a) = a

def unit_of_invertible {α : Type u} [monoid α] (a : α) [invertible a] :

αˣ

An invertible element is a unit.

Equations

unit_of_invertible a = {val := a, inv := ⅟ a _inst_2, val_inv := _, inv_val := _}

@[simp]

theorem coe_inv_unit_of_invertible {α : Type u} [monoid α] (a : α) [invertible a] :

↑(unit_of_invertible a)⁻¹ = ⅟ a

theorem is_unit_of_invertible {α : Type u} [monoid α] (a : α) [invertible a] :

def units.invertible {α : Type u} [monoid α] (u : αˣ) :

invertible ↑u

Units are invertible in their associated monoid.

Equations

u.invertible = {inv_of := ↑u⁻¹, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_units {α : Type u} [monoid α] (u : αˣ) [invertible ↑u] :

⅟ ↑u = ↑u⁻¹

theorem is_unit.nonempty_invertible {α : Type u} [monoid α] {a : α} (h : is_unit a) :

nonempty (invertible a)

noncomputable def is_unit.invertible {α : Type u} [monoid α] {a : α} (h : is_unit a) :

Convert is_unit to invertible using classical.choice.

Prefer casesI h.nonempty_invertible over letI := h.invertible if you want to avoid choice.

Equations

h.invertible = classical.choice _

@[simp]

theorem nonempty_invertible_iff_is_unit {α : Type u} [monoid α] (a : α) :

nonempty (invertible a) ↔ is_unit a

def invertible_of_group {α : Type u} [group α] (a : α) :

Each element of a group is invertible.

Equations

invertible_of_group a = {inv_of := a⁻¹, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_eq_group_inv {α : Type u} [group α] (a : α) [invertible a] :

def invertible_one {α : Type u} [monoid α] :

1 is the inverse of itself

Equations

invertible_one = {inv_of := 1, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_one {α : Type u} [monoid α] [invertible 1] :

⅟ 1 = 1

def invertible_neg {α : Type u} [has_mul α] [has_one α] [has_distrib_neg α] (a : α) [invertible a] :

invertible (-a)

-⅟a is the inverse of -a

Equations

invertible_neg a = {inv_of := -⅟ a, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_neg {α : Type u} [monoid α] [has_distrib_neg α] (a : α) [invertible a] [invertible (-a)] :

⅟ (-a) = -⅟ a

@[simp]

theorem one_sub_inv_of_two {α : Type u} [ring α] [invertible 2] :

1 - ⅟ 2 = ⅟ 2

@[simp]

theorem inv_of_two_add_inv_of_two {α : Type u} [non_assoc_semiring α] [invertible 2] :

⅟ 2 + ⅟ 2 = 1

@[protected, instance]

def invertible_inv_of {α : Type u} [has_one α] [has_mul α] {a : α} [invertible a] :

invertible (⅟ a)

a is the inverse of ⅟a.

Equations

invertible_inv_of = {inv_of := a, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_inv_of {α : Type u} [monoid α] (a : α) [invertible a] [invertible (⅟ a)] :

⅟ (⅟ a) = a

@[simp]

theorem inv_of_inj {α : Type u} [monoid α] {a b : α} [invertible a] [invertible b] :

⅟ a = ⅟ b ↔ a = b

def invertible_mul {α : Type u} [monoid α] (a b : α) [invertible a] [invertible b] :

invertible (a * b)

⅟b * ⅟a is the inverse of a * b

Equations

invertible_mul a b = {inv_of := ⅟ b * ⅟ a, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_mul {α : Type u} [monoid α] (a b : α) [invertible a] [invertible b] [invertible (a * b)] :

⅟ (a * b) = ⅟ b * ⅟ a

theorem commute.inv_of_right {α : Type u} [monoid α] {a b : α} [invertible b] (h : commute a b) :

commute a (⅟ b)

theorem commute.inv_of_left {α : Type u} [monoid α] {a b : α} [invertible b] (h : commute b a) :

commute (⅟ b) a

theorem commute_inv_of {M : Type u_1} [has_one M] [has_mul M] (m : M) [invertible m] :

commute m (⅟ m)

theorem nonzero_of_invertible {α : Type u} [mul_zero_one_class α] (a : α) [nontrivial α] [invertible a] :

a ≠ 0

@[protected, instance]

def invertible.ne_zero {α : Type u} [mul_zero_one_class α] [nontrivial α] (a : α) [invertible a] :

@[simp]

theorem ring.inverse_invertible {α : Type u} [monoid_with_zero α] (x : α) [invertible x] :

ring.inverse x = ⅟ x

A variant of ring.inverse_unit.

def invertible_of_nonzero {α : Type u} [group_with_zero α] {a : α} (h : a ≠ 0) :

a⁻¹ is an inverse of a if a ≠ 0

Equations

invertible_of_nonzero h = {inv_of := a⁻¹, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_eq_inv {α : Type u} [group_with_zero α] (a : α) [invertible a] :

@[simp]

theorem inv_mul_cancel_of_invertible {α : Type u} [group_with_zero α] (a : α) [invertible a] :

a⁻¹ * a = 1

@[simp]

theorem mul_inv_cancel_of_invertible {α : Type u} [group_with_zero α] (a : α) [invertible a] :

a * a⁻¹ = 1

@[simp]

theorem div_mul_cancel_of_invertible {α : Type u} [group_with_zero α] (a b : α) [invertible b] :

a / b * b = a

@[simp]

theorem mul_div_cancel_of_invertible {α : Type u} [group_with_zero α] (a b : α) [invertible b] :

a * b / b = a

@[simp]

theorem div_self_of_invertible {α : Type u} [group_with_zero α] (a : α) [invertible a] :

a / a = 1

def invertible_div {α : Type u} [group_with_zero α] (a b : α) [invertible a] [invertible b] :

invertible (a / b)

b / a is the inverse of a / b

Equations

invertible_div a b = {inv_of := b / a, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_div {α : Type u} [group_with_zero α] (a b : α) [invertible a] [invertible b] [invertible (a / b)] :

⅟ (a / b) = b / a

def invertible_inv {α : Type u} [group_with_zero α] {a : α} [invertible a] :

invertible a⁻¹

a is the inverse of a⁻¹

Equations

invertible_inv = {inv_of := a, inv_of_mul_self := _, mul_inv_of_self := _}

def invertible.map {R : Type u_1} {S : Type u_2} {F : Type u_3} [mul_one_class R] [mul_one_class S] [monoid_hom_class F R S] (f : F) (r : R) [invertible r] :

invertible (⇑f r)

Monoid homs preserve invertibility.

Equations

invertible.map f r = {inv_of := ⇑f (⅟ r), inv_of_mul_self := _, mul_inv_of_self := _}

theorem map_inv_of {R : Type u_1} {S : Type u_2} {F : Type u_3} [mul_one_class R] [monoid S] [monoid_hom_class F R S] (f : F) (r : R) [invertible r] [invertible (⇑f r)] :

⇑f (⅟ r) = ⅟ (⇑f r)

Note that the invertible (f r) argument can be satisfied by using letI := invertible.map f r before applying this lemma.

def invertible.of_left_inverse {R : Type u_1} {S : Type u_2} {G : Type u_3} [mul_one_class R] [mul_one_class S] [monoid_hom_class G S R] (f : R → S) (g : G) (r : R) (h : function.left_inverse ⇑g f) [invertible (f r)] :

If a function f : R → S has a left-inverse that is a monoid hom, then r : R is invertible if f r is.

The inverse is computed as g (⅟(f r))

Equations

invertible.of_left_inverse f g r h = (invertible.map g (f r)).copy r _

theorem invertible.of_left_inverse_inv_of {R : Type u_1} {S : Type u_2} {G : Type u_3} [mul_one_class R] [mul_one_class S] [monoid_hom_class G S R] (f : R → S) (g : G) (r : R) (h : function.left_inverse ⇑g f) [invertible (f r)] :

⅟ r = ⅟ (⇑g (f r))

@[simp]

theorem invertible_equiv_of_left_inverse_symm_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [monoid R] [monoid S] [monoid_hom_class F R S] [monoid_hom_class G S R] (f : F) (g : G) (r : R) (h : function.left_inverse ⇑g ⇑f) (_x : invertible r) :

⇑((invertible_equiv_of_left_inverse f g r h).symm) _x = invertible.map f r

@[simp]

theorem invertible_equiv_of_left_inverse_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [monoid R] [monoid S] [monoid_hom_class F R S] [monoid_hom_class G S R] (f : F) (g : G) (r : R) (h : function.left_inverse ⇑g ⇑f) (_x : invertible (⇑f r)) :

⇑(invertible_equiv_of_left_inverse f g r h) _x = invertible.of_left_inverse ⇑f g r h

def invertible_equiv_of_left_inverse {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [monoid R] [monoid S] [monoid_hom_class F R S] [monoid_hom_class G S R] (f : F) (g : G) (r : R) (h : function.left_inverse ⇑g ⇑f) :

invertible (⇑f r) ≃ invertible r

Invertibility on either side of a monoid hom with a left-inverse is equivalent.

Equations

invertible_equiv_of_left_inverse f g r h = {to_fun := λ (_x : invertible (⇑f r)), invertible.of_left_inverse ⇑f g r h, inv_fun := λ (_x : invertible r), invertible.map f r, left_inv := _, right_inv := _}