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.

source

@[class]

structure divisible_by (A : Type u_1) (α : Type u_2) [add_monoid A] [has_smul α A] [has_zero α] :

Type (max u_1 u_2)

div : A → α → A
div_zero : ∀ (a : A), divisible_by.div a 0 = 0
div_cancel : ∀ {n : α} (a : A), n ≠ 0 → n • divisible_by.div a n = a

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

source

@[class]

structure rootable_by (A : Type u_1) (α : Type u_2) [monoid A] [has_pow A α] [has_zero α] :

Type (max u_1 u_2)

root : A → α → A
root_zero : ∀ (a : A), rootable_by.root a 0 = 1
root_cancel : ∀ {n : α} (a : A), n ≠ 0 → rootable_by.root a n ^ 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

source

theorem pow_left_surj_of_rootable_by (A : Type u_1) (α : Type u_2) [monoid A] [has_pow A α] [has_zero α] [rootable_by A α] {n : α} (hn : n ≠ 0) :

function.surjective (λ (a : A), a ^ n)

source

theorem smul_right_surj_of_divisible_by (A : Type u_1) (α : Type u_2) [add_monoid A] [has_smul α A] [has_zero α] [divisible_by A α] {n : α} (hn : n ≠ 0) :

function.surjective (λ (a : A), n • a)

source

noncomputable def rootable_by_of_pow_left_surj (A : Type u_1) (α : Type u_2) [monoid A] [has_pow A α] [has_zero α] (H : ∀ {n : α}, n ≠ 0 → function.surjective (λ (a : A), a ^ n)) :

rootable_by A α

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

Equations

rootable_by_of_pow_left_surj A α H = {root := λ (a : A) (n : α), dite (n = 0) (λ (_x : n = 0), 1) (λ (hn : ¬n = 0), _.some), root_zero := _, root_cancel := _}

source

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

divisible_by A α

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

Equations

divisible_by_of_smul_right_surj A α H = {div := λ (a : A) (n : α), dite (n = 0) (λ (_x : n = 0), 0) (λ (hn : ¬n = 0), _.some), div_zero := _, div_cancel := _}

source

@[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

pi.rootable_by B = {root := λ (x : Π (i : ι), B i) (n : β) (i : ι), rootable_by.root (x i) n, root_zero := _, root_cancel := _}

source

@[protected, instance]

def pi.divisible_by {ι : Type u_3} {β : Type u_4} (B : ι → Type u_5) [Π (i : ι), has_smul β (B i)] [has_zero β] [Π (i : ι), add_monoid (B i)] [Π (i : ι), divisible_by (B i) β] :

divisible_by (Π (i : ι), B i) β

Equations

pi.divisible_by B = {div := λ (x : Π (i : ι), B i) (n : β) (i : ι), divisible_by.div (x i) n, div_zero := _, div_cancel := _}

source

@[protected, instance]

def prod.divisible_by {β : Type u_3} {B : Type u_4} {B' : Type u_5} [has_smul β B] [has_smul β B'] [has_zero β] [add_monoid B] [add_monoid B'] [divisible_by B β] [divisible_by B' β] :

divisible_by (B × B') β

Equations

prod.divisible_by = {div := λ (p : B × B') (n : β), (divisible_by.div p.fst n, divisible_by.div p.snd n), div_zero := _, div_cancel := _}

source

@[protected, instance]

def prod.rootable_by {β : Type u_3} {B : Type u_4} {B' : Type u_5} [has_pow B β] [has_pow B' β] [has_zero β] [monoid B] [monoid B'] [rootable_by B β] [rootable_by B' β] :

rootable_by (B × B') β

Equations

prod.rootable_by = {root := λ (p : B × B') (n : β), (rootable_by.root p.fst n, rootable_by.root p.snd n), root_zero := _, root_cancel := _}

source

theorem add_comm_group.smul_top_eq_top_of_divisible_by_int (A : Type u_1) [add_comm_group A] [divisible_by A ℤ] {n : ℤ} (hn : n ≠ 0) :

n • ⊤ = ⊤

source

noncomputable def add_comm_group.divisible_by_int_of_smul_top_eq_top (A : Type u_1) [add_comm_group A] (H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤) :

divisible_by A ℤ

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

Equations

add_comm_group.divisible_by_int_of_smul_top_eq_top A H = {div := λ (a : A) (n : ℤ), dite (n = 0) (λ (hn : n = 0), 0) (λ (hn : ¬n = 0), Exists.some _), div_zero := _, div_cancel := _}

source

@[protected, instance]

def divisible_by_int_of_char_zero {𝕜 : Type u_1} [division_ring 𝕜] [char_zero 𝕜] :

divisible_by 𝕜 ℤ

Equations

divisible_by_int_of_char_zero = {div := λ (q : 𝕜) (n : ℤ), q / ↑n, div_zero := _, div_cancel := _}

source

def group.rootable_by_int_of_rootable_by_nat (A : Type u_1) [group A] [rootable_by A ℕ] :

rootable_by A ℤ

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

Equations

group.rootable_by_int_of_rootable_by_nat A = {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 -[1+ n] = (rootable_by.root a (n + 1))⁻¹
group.rootable_by_int_of_rootable_by_nat._match_1 A a ↑n = rootable_by.root a n

source

def add_group.divisible_by_int_of_divisible_by_nat (A : Type u_1) [add_group A] [divisible_by A ℕ] :

divisible_by A ℤ

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

Equations

add_group.divisible_by_int_of_divisible_by_nat A = {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 = divisible_by.div a n
add_group.divisible_by_int_of_divisible_by_nat._match_1 A a -[1+ n] = -divisible_by.div a (n + 1)

source

def group.rootable_by_nat_of_rootable_by_int (A : Type u_1) [group A] [rootable_by A ℤ] :

rootable_by A ℕ

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

Equations

group.rootable_by_nat_of_rootable_by_int A = {root := λ (a : A) (n : ℕ), rootable_by.root a ↑n, root_zero := _, root_cancel := _}

source

def add_group.divisible_by_nat_of_divisible_by_int (A : Type u_1) [add_group A] [divisible_by A ℤ] :

divisible_by A ℕ

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

Equations

add_group.divisible_by_nat_of_divisible_by_int A = {div := λ (a : A) (n : ℕ), divisible_by.div a ↑n, div_zero := _, div_cancel := _}

source

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

rootable_by B α

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

Equations

function.surjective.rootable_by f hf hpow = rootable_by_of_pow_left_surj B α _

source

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] [has_smul α A] [has_smul α B] [divisible_by A α] (f : A → B) (hf : function.surjective f) (hpow : ∀ (a : A) (n : α), f (n • a) = n • f a) :

divisible_by B α

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

Equations

function.surjective.divisible_by f hf hpow = divisible_by_of_smul_right_surj B α _

source

theorem rootable_by.surjective_pow (A : Type u_1) (α : Type u_2) [monoid A] [has_pow A α] [has_zero α] [rootable_by A α] {n : α} (hn : n ≠ 0) :

function.surjective (λ (a : A), a ^ n)

source

theorem divisible_by.surjective_smul (A : Type u_1) (α : Type u_2) [add_monoid A] [has_smul α A] [has_zero α] [divisible_by A α] {n : α} (hn : n ≠ 0) :

function.surjective (λ (a : A), n • a)

source

@[protected, instance]

noncomputable def quotient_add_group.divisible_by {A : Type u_2} [add_comm_group A] (B : add_subgroup A) [divisible_by A ℕ] :

divisible_by (A ⧸ B) ℕ

Any quotient group of a divisible group is divisible

Equations

quotient_add_group.divisible_by B = function.surjective.divisible_by quotient_add_group.mk _ _

source

@[protected, instance]

noncomputable def quotient_group.rootable_by {A : Type u_2} [comm_group A] (B : subgroup A) [rootable_by A ℕ] :

rootable_by (A ⧸ B) ℕ

Any quotient group of a rootable group is rootable.

Equations

quotient_group.rootable_by B = function.surjective.rootable_by quotient_group.mk _ _