Division monoids

This file defines additive and multiplicative structures with division, inversion, subtraction, or negation, up to DivisionCommMonoid and SubtractionCommMonoid. Group structures are defined in Mathlib.Algebra.Group.Defs.

def zpowRec {G : Type u_1} [One G] [Mul G] [Inv G] (npow : ℕ → G → G := npowRec) : ℤ → G → G

The fundamental power operation in a group. zpowRec n a = a*a*...*a n times, for integer n. Use instead a ^ n, which has better definitional behavior.

Equations

• zpowRec npow (Int.ofNat n) x✝ = npow n x✝
• zpowRec npow (Int.negSucc n) x✝ = (npow n.succ x✝)⁻¹

def zsmulRec {G : Type u_1} [Zero G] [Add G] [Neg G] (nsmul : ℕ → G → G := nsmulRec) : ℤ → G → G

The fundamental scalar multiplication in an additive group. zpowRec n a = a+a+...+a n times, for integer n. Use instead n • a, which has better definitional behavior.

Equations

• zsmulRec nsmul (Int.ofNat n) x✝ = nsmul n x✝
• zsmulRec nsmul (Int.negSucc n) x✝ = -nsmul n.succ x✝

class InvolutiveNeg (A : Type u_2) extends Neg A : Type u_2

Auxiliary typeclass for types with an involutive Neg.

• neg : A → A
• neg_neg (x : A) : - -x = x

class InvolutiveInv (G : Type u_2) extends Inv G : Type u_2

Auxiliary typeclass for types with an involutive Inv.

• inv : G → G
• inv_inv (x : G) : x⁻¹⁻¹ = x

@[simp]

theorem inv_inv {G : Type u_1} [InvolutiveInv G] (a : G) : a⁻¹⁻¹ = a

@[simp]

theorem neg_neg {G : Type u_1} [InvolutiveNeg G] (a : G) : - -a = a

Design note on DivInvMonoid/SubNegMonoid and DivisionMonoid/SubtractionMonoid

Those two pairs of made-up classes fulfill slightly different roles.

DivInvMonoid/SubNegMonoid provides the minimum amount of information to define the ℤ action (zpow or zsmul). Further, it provides a div field, matching the forgetful inheritance pattern. This is useful to shorten extension clauses of stronger structures (Group, GroupWithZero, DivisionRing, Field) and for a few structures with a rather weak pseudo-inverse (Matrix).

DivisionMonoid/SubtractionMonoid is targeted at structures with stronger pseudo-inverses. It is an ad hoc collection of axioms that are mainly respected by three things:

• Groups
• Groups with zero
• The pointwise monoids Set α, Finset α, Filter α

It acts as a middle ground for structures with an inversion operator that plays well with multiplication, except for the fact that it might not be a true inverse (a / a ≠ 1 in general). The axioms are pretty arbitrary (many other combinations are equivalent to it), but they are independent:

• Without DivisionMonoid.div_eq_mul_inv, you can define / arbitrarily.
• Without DivisionMonoid.inv_inv, you can consider WithTop Unit with a⁻¹ = ⊤ for all a.
• Without DivisionMonoid.mul_inv_rev, you can consider WithTop α with a⁻¹ = a for all a where α noncommutative.
• Without DivisionMonoid.inv_eq_of_mul, you can consider any CommMonoid with a⁻¹ = a for all a.

As a consequence, a few natural structures do not fit in this framework. For example, ENNReal respects everything except for the fact that (0 * ∞)⁻¹ = 0⁻¹ = ∞ while ∞⁻¹ * 0⁻¹ = 0 * ∞ = 0.

def DivInvMonoid.div' {G : Type u_2} [Monoid G] [Inv G] (a b : G) : G

In a class equipped with instances of both Monoid and Inv, this definition records what the default definition for Div would be: a * b⁻¹. This is later provided as the default value for the Div instance in DivInvMonoid.

We keep it as a separate definition rather than inlining it in DivInvMonoid so that the Div field of individual DivInvMonoids constructed using that default value will not be unfolded at .instance transparency.

Equations

• DivInvMonoid.div' a b = a * b⁻¹

class ZSMul (G : Type u_2) : Type u_2

ZSMul is an implementation detail of SubNegMonoid. It is needed because it is impossible to extend SMUl ℕ M and SMul ℤ M at the same time.

• zsmul : ℤ → G → G

  Multiplication by an integer. Set this to zsmulRec unless Module diamonds are possible.

class ZPow (G : Type u_2) : Type u_2

ZPow is an implementation detail of DivInvMonoid. It is needed because it is impossible to extend Pow M ℕ and Pow M ℤ at the same time.

• zpow : ℤ → G → G

  The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

@[instance_reducible]

instance ZPow.toPow {M : Type u_2} [ZPow M] : Pow M ℤ

Equations

• ZPow.toPow = { pow := fun (x : M) (n : ℤ) => ZPow.zpow n x }

@[instance_reducible]

instance ZSMul.toSMul {M : Type u_2} [ZSMul M] : SMul ℤ M

Equations

• ZSMul.toSMul = { smul := fun (n : ℤ) (x : M) => ZSMul.zsmul n x }

@[instance_reducible]

instance ZPow.ofPow {M : Type u_2} [Pow M ℤ] : ZPow M

Equations

• ZPow.ofPow = { zpow := fun (n : ℤ) (x : M) => Pow.pow x n }

@[instance_reducible]

instance ZSMul.ofSMul {M : Type u_2} [SMul ℤ M] : ZSMul M

Equations

• ZSMul.ofSMul = { zsmul := fun (n : ℤ) (x : M) => SMul.smul n x }

class DivInvMonoid (G : Type u_2) extends Monoid G, Inv G, Div G, ZPow G : Type u_2

A DivInvMonoid is a Monoid with operations / and ⁻¹ satisfying div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹.

This deduplicates the name div_eq_mul_inv. The default for div is such that a / b = a * b⁻¹ holds by definition.

Adding div as a field rather than defining a / b := a * b⁻¹ allows us to avoid certain classes of unification failures, for example: Let Foo X be a type with a ∀ X, Div (Foo X) instance but no ∀ X, Inv (Foo X), e.g. when Foo X is a EuclideanDomain. Suppose we also have an instance ∀ X [Cromulent X], GroupWithZero (Foo X). Then the (/) coming from GroupWithZero.div cannot be definitionally equal to the (/) coming from Foo.Div.

In the same way, adding a zpow field makes it possible to avoid definitional failures in diamonds. See the definition of Monoid and Note [forgetful inheritance] for more explanations on this.

• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• one : G
• one_mul (a : G) : 1 * a = a
• mul_one (a : G) : a * 1 = a
• npow : ℕ → G → G
• npow_zero (x : G) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : G) : x ^ (n + 1) = x ^ n * x
• inv : G → G
• div : G → G → G
• zpow : ℤ → G → G
• div_eq_mul_inv (a b : G) : a / b = a * b⁻¹

  a / b := a * b⁻¹

• zpow_zero' (a : G) : a ^ 0 = 1

  a ^ 0 = 1

• zpow_succ' (n : ℕ) (a : G) : a ^ ↑n.succ = a ^ ↑n * a

  a ^ (n + 1) = a ^ n * a

• zpow_neg' (n : ℕ) (a : G) : a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹

  a ^ -(n + 1) = (a ^ (n + 1))⁻¹

def SubNegMonoid.sub' {G : Type u_2} [AddMonoid G] [Neg G] (a b : G) : G

In a class equipped with instances of both AddMonoid and Neg, this definition records what the default definition for Sub would be: a + -b. This is later provided as the default value for the Sub instance in SubNegMonoid.

We keep it as a separate definition rather than inlining it in SubNegMonoid so that the Sub field of individual SubNegMonoids constructed using that default value will not be unfolded at .instance transparency.

Equations

• SubNegMonoid.sub' a b = a + -b

class SubNegMonoid (G : Type u_2) extends AddMonoid G, Neg G, Sub G, ZSMul G : Type u_2

A SubNegMonoid is an AddMonoid with unary - and binary - operations satisfying sub_eq_add_neg : ∀ a b, a - b = a + -b.

The default for sub is such that a - b = a + -b holds by definition.

Adding sub as a field rather than defining a - b := a + -b allows us to avoid certain classes of unification failures, for example: Let foo X be a type with a ∀ X, Sub (Foo X) instance but no ∀ X, Neg (Foo X). Suppose we also have an instance ∀ X [Cromulent X], AddGroup (Foo X). Then the (-) coming from AddGroup.sub cannot be definitionally equal to the (-) coming from Foo.Sub.

In the same way, adding a zsmul field makes it possible to avoid definitional failures in diamonds. See the definition of AddMonoid and Note [forgetful inheritance] for more explanations on this.

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• zero : G
• zero_add (a : G) : 0 + a = a
• add_zero (a : G) : a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero (x : G) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : G) : (n + 1) • x = n • x + x
• neg : G → G
• sub : G → G → G
• zsmul : ℤ → G → G
• sub_eq_add_neg (a b : G) : a - b = a + -b
• zsmul_zero' (a : G) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : G) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : G) : Int.negSucc n • a = -(↑n.succ • a)

class IsAddCyclic (G : Type u_2) [SMul ℤ G] : Prop

A group is called cyclic if it is generated by a single element.

Wikidata Q245462

• exists_zsmul_surjective : ∃ (g : G), Function.Surjective fun (x : ℤ) => x • g

class IsCyclic (G : Type u_2) [Pow G ℤ] : Prop

A group is called cyclic if it is generated by a single element.

Wikidata Q245462

• exists_zpow_surjective : ∃ (g : G), Function.Surjective fun (x : ℤ) => g ^ x

theorem exists_zpow_surjective (G : Type u_2) [Pow G ℤ] [IsCyclic G] : ∃ (g : G), Function.Surjective fun (x : ℤ) => g ^ x

theorem exists_zsmul_surjective (G : Type u_2) [SMul ℤ G] [IsAddCyclic G] : ∃ (g : G), Function.Surjective fun (x : ℤ) => x • g

@[simp]

theorem zpow_eq_pow {G : Type u_1} [DivInvMonoid G] (n : ℤ) (x : G) : ZPow.zpow n x = x ^ n

@[simp]

theorem zsmul_eq_smul {G : Type u_1} [SubNegMonoid G] (n : ℤ) (x : G) : ZSMul.zsmul n x = n • x

theorem zpow_zero {G : Type u_1} [DivInvMonoid G] (a : G) : a ^ 0 = 1

@[simp]

theorem zero_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) : 0 • a = 0

@[simp]

theorem zpow_natCast {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) : a ^ ↑n = a ^ n

@[simp]

theorem natCast_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ℕ) : ↑n • a = n • a

@[simp]

theorem zpow_ofNat {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) : a ^ OfNat.ofNat n = a ^ OfNat.ofNat n

theorem ofNat_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ℕ) : OfNat.ofNat n • a = OfNat.ofNat n • a

@[simp]

theorem zpow_negSucc {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) : a ^ Int.negSucc n = (a ^ (n + 1))⁻¹

@[simp]

theorem negSucc_zsmul {G : Type u_2} [SubNegMonoid G] (a : G) (n : ℕ) : Int.negSucc n • a = -((n + 1) • a)

theorem div_eq_mul_inv {G : Type u_1} [DivInvMonoid G] (a b : G) : a / b = a * b⁻¹

Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of DivInvMonoid.div_eq_mul_inv ensuring that the types unfold better.

theorem sub_eq_add_neg {G : Type u_1} [SubNegMonoid G] (a b : G) : a - b = a + -b

Subtracting an element is the same as adding by its negative. This is a duplicate of SubNegMonoid.sub_eq_add_neg ensuring that the types unfold better.

theorem division_def {G : Type u_1} [DivInvMonoid G] (a b : G) : a / b = a * b⁻¹

Alias of div_eq_mul_inv.

---

Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of DivInvMonoid.div_eq_mul_inv ensuring that the types unfold better.

theorem inv_eq_one_div {G : Type u_1} [DivInvMonoid G] (x : G) : x⁻¹ = 1 / x

theorem neg_eq_zero_sub {G : Type u_1} [SubNegMonoid G] (x : G) : -x = 0 - x

theorem mul_div_assoc {G : Type u_1} [DivInvMonoid G] (a b c : G) : a * b / c = a * (b / c)

theorem add_sub_assoc {G : Type u_1} [SubNegMonoid G] (a b c : G) : a + b - c = a + (b - c)

@[simp]

theorem one_div {G : Type u_1} [DivInvMonoid G] (a : G) : 1 / a = a⁻¹

@[simp]

theorem zero_sub {G : Type u_1} [SubNegMonoid G] (a : G) : 0 - a = -a

theorem zpow_one {G : Type u_1} [DivInvMonoid G] (a : G) : a ^ 1 = a

@[simp]

theorem one_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) : 1 • a = a

theorem zpow_two {G : Type u_1} [DivInvMonoid G] (a : G) : a ^ 2 = a * a

theorem two_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) : 2 • a = a + a

theorem zpow_neg_one {G : Type u_1} [DivInvMonoid G] (x : G) : x ^ (-1) = x⁻¹

theorem neg_one_zsmul {G : Type u_1} [SubNegMonoid G] (x : G) : -1 • x = -x

theorem zpow_neg_coe_of_pos {G : Type u_1} [DivInvMonoid G] (a : G) {n : ℕ} : 0 < n → a ^ (-↑n) = (a ^ n)⁻¹

theorem zsmul_neg_coe_of_pos {G : Type u_1} [SubNegMonoid G] (a : G) {n : ℕ} : 0 < n → -↑n • a = -(n • a)

class NegZeroClass (G : Type u_2) extends Zero G, Neg G : Type u_2

Typeclass for expressing that -0 = 0.

• zero : G
• neg : G → G
• neg_zero : -0 = 0

class SubNegZeroMonoid (G : Type u_2) extends SubNegMonoid G, NegZeroClass G : Type u_2

A SubNegMonoid where -0 = 0.

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• zero : G
• zero_add (a : G) : 0 + a = a
• add_zero (a : G) : a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero (x : G) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : G) : (n + 1) • x = n • x + x
• neg : G → G
• sub : G → G → G
• zsmul : ℤ → G → G
• sub_eq_add_neg (a b : G) : a - b = a + -b
• zsmul_zero' (a : G) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : G) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : G) : Int.negSucc n • a = -(↑n.succ • a)
• neg_zero : -0 = 0

class InvOneClass (G : Type u_2) extends One G, Inv G : Type u_2

Typeclass for expressing that 1⁻¹ = 1.

• one : G
• inv : G → G
• inv_one : 1⁻¹ = 1

class DivInvOneMonoid (G : Type u_2) extends DivInvMonoid G, InvOneClass G : Type u_2

A DivInvMonoid where 1⁻¹ = 1.

• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• one : G
• one_mul (a : G) : 1 * a = a
• mul_one (a : G) : a * 1 = a
• npow : ℕ → G → G
• npow_zero (x : G) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : G) : x ^ (n + 1) = x ^ n * x
• inv : G → G
• div : G → G → G
• zpow : ℤ → G → G
• div_eq_mul_inv (a b : G) : a / b = a * b⁻¹
• zpow_zero' (a : G) : a ^ 0 = 1
• zpow_succ' (n : ℕ) (a : G) : a ^ ↑n.succ = a ^ ↑n * a
• zpow_neg' (n : ℕ) (a : G) : a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
• inv_one : 1⁻¹ = 1

@[simp]

theorem inv_one {G : Type u_1} [InvOneClass G] : 1⁻¹ = 1

@[simp]

theorem neg_zero {G : Type u_1} [NegZeroClass G] : -0 = 0

class SubtractionMonoid (G : Type u_2) extends SubNegMonoid G, InvolutiveNeg G : Type u_2

A SubtractionMonoid is a SubNegMonoid with involutive negation and such that -(a + b) = -b + -a and a + b = 0 → -a = b.

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• zero : G
• zero_add (a : G) : 0 + a = a
• add_zero (a : G) : a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero (x : G) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : G) : (n + 1) • x = n • x + x
• neg : G → G
• sub : G → G → G
• zsmul : ℤ → G → G
• sub_eq_add_neg (a b : G) : a - b = a + -b
• zsmul_zero' (a : G) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : G) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : G) : Int.negSucc n • a = -(↑n.succ • a)
• neg_neg (x : G) : - -x = x
• neg_add_rev (a b : G) : -(a + b) = -b + -a
• neg_eq_of_add (a b : G) : a + b = 0 → -a = b

  Despite the asymmetry of neg_eq_of_add, the symmetric version is true thanks to the involutivity of negation.

class DivisionMonoid (G : Type u_2) extends DivInvMonoid G, InvolutiveInv G : Type u_2

A DivisionMonoid is a DivInvMonoid with involutive inversion and such that (a * b)⁻¹ = b⁻¹ * a⁻¹ and a * b = 1 → a⁻¹ = b.

This is the immediate common ancestor of Group and GroupWithZero.

• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• one : G
• one_mul (a : G) : 1 * a = a
• mul_one (a : G) : a * 1 = a
• npow : ℕ → G → G
• npow_zero (x : G) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : G) : x ^ (n + 1) = x ^ n * x
• inv : G → G
• div : G → G → G
• zpow : ℤ → G → G
• div_eq_mul_inv (a b : G) : a / b = a * b⁻¹
• zpow_zero' (a : G) : a ^ 0 = 1
• zpow_succ' (n : ℕ) (a : G) : a ^ ↑n.succ = a ^ ↑n * a
• zpow_neg' (n : ℕ) (a : G) : a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
• inv_inv (x : G) : x⁻¹⁻¹ = x
• mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹
• inv_eq_of_mul (a b : G) : a * b = 1 → a⁻¹ = b

  Despite the asymmetry of inv_eq_of_mul, the symmetric version is true thanks to the involutivity of inversion.

@[simp]

theorem mul_inv_rev {G : Type u_1} [DivisionMonoid G] (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹

@[simp]

theorem neg_add_rev {G : Type u_1} [SubtractionMonoid G] (a b : G) : -(a + b) = -b + -a

theorem inv_eq_of_mul_eq_one_right {G : Type u_1} [DivisionMonoid G] {a b : G} : a * b = 1 → a⁻¹ = b

theorem neg_eq_of_add_eq_zero_right {G : Type u_1} [SubtractionMonoid G] {a b : G} : a + b = 0 → -a = b

theorem inv_eq_of_mul_eq_one_left {G : Type u_1} [DivisionMonoid G] {a b : G} (h : a * b = 1) : b⁻¹ = a

theorem neg_eq_of_add_eq_zero_left {G : Type u_1} [SubtractionMonoid G] {a b : G} (h : a + b = 0) : -b = a

theorem eq_inv_of_mul_eq_one_left {G : Type u_1} [DivisionMonoid G] {a b : G} (h : a * b = 1) : a = b⁻¹

theorem eq_neg_of_add_eq_zero_left {G : Type u_1} [SubtractionMonoid G] {a b : G} (h : a + b = 0) : a = -b

class SubtractionCommMonoid (G : Type u_2) extends SubtractionMonoid G, AddCommMonoid G : Type u_2

Commutative SubtractionMonoid.

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• zero : G
• zero_add (a : G) : 0 + a = a
• add_zero (a : G) : a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero (x : G) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : G) : (n + 1) • x = n • x + x
• neg : G → G
• sub : G → G → G
• zsmul : ℤ → G → G
• sub_eq_add_neg (a b : G) : a - b = a + -b
• zsmul_zero' (a : G) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : G) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : G) : Int.negSucc n • a = -(↑n.succ • a)
• neg_neg (x : G) : - -x = x
• neg_add_rev (a b : G) : -(a + b) = -b + -a
• neg_eq_of_add (a b : G) : a + b = 0 → -a = b
• add_comm (a b : G) : a + b = b + a

class DivisionCommMonoid (G : Type u_2) extends DivisionMonoid G, CommMonoid G : Type u_2

Commutative DivisionMonoid.

This is the immediate common ancestor of CommGroup and CommGroupWithZero.

• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• one : G
• one_mul (a : G) : 1 * a = a
• mul_one (a : G) : a * 1 = a
• npow : ℕ → G → G
• npow_zero (x : G) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : G) : x ^ (n + 1) = x ^ n * x
• inv : G → G
• div : G → G → G
• zpow : ℤ → G → G
• div_eq_mul_inv (a b : G) : a / b = a * b⁻¹
• zpow_zero' (a : G) : a ^ 0 = 1
• zpow_succ' (n : ℕ) (a : G) : a ^ ↑n.succ = a ^ ↑n * a
• zpow_neg' (n : ℕ) (a : G) : a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
• inv_inv (x : G) : x⁻¹⁻¹ = x
• mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹
• inv_eq_of_mul (a b : G) : a * b = 1 → a⁻¹ = b
• mul_comm (a b : G) : a * b = b * a

We initialize the projections for the group structures for @[simps] here.

The lemmas generated for the npow/zpow projections will not apply to x ^ y, since the argument order of these projections does not match the argument order of ^. The nsmul/zsmul lemmas are correct.