# mathlib3documentation

group_theory.divisible

# Divisible Group and rootable group #

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

In this file, we define a divisible add monoid and a rootable monoid with some basic properties.

## Main definition #

• divisible_by A α: An additive monoid A is said to be divisible by α iff for all n ≠ 0 ∈ α and y ∈ A, there is an x ∈ A such that n • x = y. In this file, we adopt a constructive approach, i.e. we ask for an explicit div : A → α → A function such that div a 0 = 0 and n • div a n = a for all n ≠ 0 ∈ α.
• rootable_by A α: A monoid A is said to be rootable by α iff for all n ≠ 0 ∈ α and y ∈ A, there is an x ∈ A such that x^n = y. In this file, we adopt a constructive approach, i.e. we ask for an explicit root : A → α → A function such that root a 0 = 1 and (root a n)ⁿ = a for all n ≠ 0 ∈ α.

## Main results #

For additive monoids and groups:

• divisible_by_of_smul_right_surj : the constructive definition of divisiblity is implied by the condition that n • x = a has solutions for all n ≠ 0 and a ∈ A.
• smul_right_surj_of_divisible_by : the constructive definition of divisiblity implies the condition that n • x = a has solutions for all n ≠ 0 and a ∈ A.
• prod.divisible_by : A × B is divisible for any two divisible additive monoids.
• pi.divisible_by : any product of divisble additive monoids is divisible.
• add_group.divisible_by_int_of_divisible_by_nat : for additive groups, int divisiblity is implied by nat divisiblity.
• add_group.divisible_by_nat_of_divisible_by_int : for additive groups, nat divisiblity is implied by int divisiblity.
• add_comm_group.divisible_by_int_of_smul_top_eq_top: the constructive definition of divisiblity is implied by the condition that n • A = A for all n ≠ 0.
• add_comm_group.smul_top_eq_top_of_divisible_by_int: the constructive definition of divisiblity implies the condition that n • A = A for all n ≠ 0.
• divisible_by_int_of_char_zero : any field of characteristic zero is divisible.
• quotient_add_group.divisible_by : quotient group of divisible group is divisible.
• function.surjective.divisible_by : if A is divisible and A →+ B is surjective, then B is divisible.

and their multiplicative counterparts:

• rootable_by_of_pow_left_surj : the constructive definition of rootablity is implied by the condition that xⁿ = y has solutions for all n ≠ 0 and a ∈ A.
• pow_left_surj_of_rootable_by : the constructive definition of rootablity implies the condition that xⁿ = y has solutions for all n ≠ 0 and a ∈ A.
• prod.rootable_by : any product of two rootable monoids is rootable.
• pi.rootable_by : any product of rootable monoids is rootable.
• group.rootable_by_int_of_rootable_by_nat : in groups, int rootablity is implied by nat rootablity.
• group.rootable_by_nat_of_rootable_by_int : in groups, nat rootablity is implied by int rootablity.
• quotient_group.rootable_by : quotient group of rootable group is rootable.
• function.surjective.rootable_by : if A is rootable and A →* B is surjective, then B is rootable.

TODO: Show that divisibility implies injectivity in the category of AddCommGroup.

@[class]
structure divisible_by (A : Type u_1) (α : Type u_2) [add_monoid A] [ A] [has_zero α] :
Type (max u_1 u_2)

An add_monoid A is α-divisible iff n • x = a has a solution for all n ≠ 0 ∈ α and a ∈ A. Here we adopt a constructive approach where we ask an explicit div : A → α → A function such that

• div a 0 = 0 for all a ∈ A
• n • div a n = a for all n ≠ 0 ∈ α and a ∈ A.
Instances of this typeclass
Instances of other typeclasses for divisible_by
• divisible_by.has_sizeof_inst
@[class]
structure rootable_by (A : Type u_1) (α : Type u_2) [monoid A] [ α] [has_zero α] :
Type (max u_1 u_2)
• root : A α A
• root_zero : (a : A), = 1
• root_cancel : {n : α} (a : A), n 0 ^ n = a

A monoid A is α-rootable iff xⁿ = a has a solution for all n ≠ 0 ∈ α and a ∈ A. Here we adopt a constructive approach where we ask an explicit root : A → α → A function such that

• root a 0 = 1 for all a ∈ A
• (root a n)ⁿ = a for all n ≠ 0 ∈ α and a ∈ A.
Instances of this typeclass
Instances of other typeclasses for rootable_by
• rootable_by.has_sizeof_inst
theorem pow_left_surj_of_rootable_by (A : Type u_1) (α : Type u_2) [monoid A] [ α] [has_zero α] [ α] {n : α} (hn : n 0) :
function.surjective (λ (a : A), a ^ n)
theorem smul_right_surj_of_divisible_by (A : Type u_1) (α : Type u_2) [add_monoid A] [ A] [has_zero α] [ α] {n : α} (hn : n 0) :
function.surjective (λ (a : A), n a)
noncomputable def rootable_by_of_pow_left_surj (A : Type u_1) (α : Type u_2) [monoid A] [ α] [has_zero α] (H : {n : α}, n 0 function.surjective (λ (a : A), a ^ n)) :
α

A monoid A is α-rootable iff the pow _ n function is surjective, i.e. the constructive version implies the textbook approach.

Equations
noncomputable def divisible_by_of_smul_right_surj (A : Type u_1) (α : Type u_2) [add_monoid A] [ A] [has_zero α] (H : {n : α}, n 0 function.surjective (λ (a : A), n a)) :
α

An add_monoid A is α-divisible iff n • _ is a surjective function, i.e. the constructive version implies the textbook approach.

Equations
@[protected, instance]
def pi.rootable_by {ι : Type u_3} {β : Type u_4} (B : ι Type u_5) [Π (i : ι), has_pow (B i) β] [has_zero β] [Π (i : ι), monoid (B i)] [Π (i : ι), rootable_by (B i) β] :
rootable_by (Π (i : ι), B i) β
Equations
@[protected, instance]
def pi.divisible_by {ι : Type u_3} {β : Type u_4} (B : ι Type u_5) [Π (i : ι), (B i)] [has_zero β] [Π (i : ι), add_monoid (B i)] [Π (i : ι), divisible_by (B i) β] :
divisible_by (Π (i : ι), B i) β
Equations
@[protected, instance]
def prod.divisible_by {β : Type u_3} {B : Type u_4} {B' : Type u_5} [ B] [ B'] [has_zero β] [add_monoid B] [add_monoid B'] [ β] [ β] :
divisible_by (B × B') β
Equations
@[protected, instance]
def prod.rootable_by {β : Type u_3} {B : Type u_4} {B' : Type u_5} [ β] [has_pow B' β] [has_zero β] [monoid B] [monoid B'] [ β] [ β] :
rootable_by (B × B') β
Equations
theorem add_comm_group.smul_top_eq_top_of_divisible_by_int (A : Type u_1) [ ] {n : } (hn : n 0) :
noncomputable def add_comm_group.divisible_by_int_of_smul_top_eq_top (A : Type u_1) (H : {n : }, n 0 n = ) :

If for all n ≠ 0 ∈ ℤ, n • A = A, then A is divisible.

Equations
@[protected, instance]
def divisible_by_int_of_char_zero {𝕜 : Type u_1} [char_zero 𝕜] :
Equations

A group is ℤ-rootable if it is ℕ-rootable.

Equations
• = {root := λ (a : A) (z : ), group.rootable_by_int_of_rootable_by_nat._match_1 A a z, root_zero := _, root_cancel := _}
• group.rootable_by_int_of_rootable_by_nat._match_1 A a = (n + 1))⁻¹
• group.rootable_by_int_of_rootable_by_nat._match_1 A a n =

An additive group is ℤ-divisible if it is ℕ-divisible.

Equations
• = {div := λ (a : A) (z : ), add_group.divisible_by_int_of_divisible_by_nat._match_1 A a z, div_zero := _, div_cancel := _}
• add_group.divisible_by_int_of_divisible_by_nat._match_1 A a n =
• add_group.divisible_by_int_of_divisible_by_nat._match_1 A a = - (n + 1)

A group is ℕ-rootable if it is ℤ-rootable

Equations

An additive group is ℕ-divisible if it ℤ-divisible.

Equations
noncomputable def function.surjective.rootable_by {α : Type u_1} {A : Type u_2} {B : Type u_3} [has_zero α] [monoid A] [monoid B] [ α] [ α] [ α] (f : A B) (hf : function.surjective f) (hpow : (a : A) (n : α), f (a ^ n) = f a ^ n) :
α

If f : A → B is a surjective homomorphism and A is α-rootable, then B is also α-rootable.

Equations
• hpow =
noncomputable def function.surjective.divisible_by {α : Type u_1} {A : Type u_2} {B : Type u_3} [has_zero α] [add_monoid A] [add_monoid B] [ A] [ B] [ α] (f : A B) (hf : function.surjective f) (hpow : (a : A) (n : α), f (n a) = n f a) :
α

If f : A → B is a surjective homomorphism and A is α-divisible, then B is also α-divisible.

Equations
• hpow =
theorem rootable_by.surjective_pow (A : Type u_1) (α : Type u_2) [monoid A] [ α] [has_zero α] [ α] {n : α} (hn : n 0) :
function.surjective (λ (a : A), a ^ n)
theorem divisible_by.surjective_smul (A : Type u_1) (α : Type u_2) [add_monoid A] [ A] [has_zero α] [ α] {n : α} (hn : n 0) :
function.surjective (λ (a : A), n a)
@[protected, instance]
noncomputable def quotient_add_group.divisible_by {A : Type u_2} (B : add_subgroup A) [ ] :

Any quotient group of a divisible group is divisible

Equations
@[protected, instance]
noncomputable def quotient_group.rootable_by {A : Type u_2} [comm_group A] (B : subgroup A) [ ] :

Any quotient group of a rootable group is rootable.

Equations