# Documentation

Mathlib.GroupTheory.Divisible

# Divisible Group and rootable group #

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

## Main definition #

• DivisibleBy 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 ∈ α.
• RootableBy 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 #

• divisibleByOfSMulRightSurj : 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_divisibleBy : the constructive definition of divisiblity implies the condition that n • x = a has solutions for all n ≠ 0 and a ∈ A.
• Prod.divisibleBy : A × B is divisible for any two divisible additive monoids.
• Pi.divisibleBy : any product of divisible additive monoids is divisible.
• AddGroup.divisibleByIntOfDivisibleByNat : for additive groups, int divisiblity is implied by nat divisiblity.
• AddGroup.divisibleByNatOfDivisibleByInt : for additive groups, nat divisiblity is implied by int divisiblity.
• AddCommGroup.divisibleByIntOfSmulTopEqTop: the constructive definition of divisiblity is implied by the condition that n • A = A for all n ≠ 0.
• AddCommGroup.smul_top_eq_top_of_divisibleBy_int: the constructive definition of divisiblity implies the condition that n • A = A for all n ≠ 0.
• divisibleByIntOfCharZero : any field of characteristic zero is divisible.
• QuotientAddGroup.divisibleBy : quotient group of divisible group is divisible.
• Function.Surjective.divisibleBy : if A is divisible and A →+ B is surjective, then B is divisible.

and their multiplicative counterparts:

• rootableByOfPowLeftSurj : 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_rootableBy : the constructive definition of rootablity implies the condition that xⁿ = y has solutions for all n ≠ 0 and a ∈ A.
• Prod.rootableBy : any product of two rootable monoids is rootable.
• Pi.rootableBy : any product of rootable monoids is rootable.
• Group.rootableByIntOfRootableByNat : in groups, int rootablity is implied by nat rootablity.
• Group.rootableByNatOfRootableByInt : in groups, nat rootablity is implied by int rootablity.
• QuotientGroup.rootableBy : quotient group of rootable group is rootable.
• Function.Surjective.rootableBy : 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 DivisibleBy (A : Type u_1) (α : Type u_2) [] [SMul α A] [Zero α] :
Type (max u_1 u_2)
• div : AαA
• div_zero : ∀ (a : A), = 0
• div_cancel : ∀ {n : α} (a : A), n 0n = a

An AddMonoid 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
class RootableBy (A : Type u_1) (α : Type u_2) [] [Pow A α] [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
theorem smul_right_surj_of_divisibleBy (A : Type u_1) (α : Type u_2) [] [SMul α A] [Zero α] [] {n : α} (hn : n 0) :
theorem pow_left_surj_of_rootableBy (A : Type u_1) (α : Type u_2) [] [Pow A α] [Zero α] [] {n : α} (hn : n 0) :
Function.Surjective fun a => a ^ n
theorem divisibleByOfSMulRightSurj.proof_2 (A : Type u_2) (α : Type u_1) [] [SMul α A] [Zero α] (H : ∀ {n : α}, n 0Function.Surjective fun a => n a) :
∀ {n : α} (a : A), n 0n (fun a n => if x : n = 0 then 0 else Exists.choose (H n x a)) a n = a
theorem divisibleByOfSMulRightSurj.proof_1 (A : Type u_1) (α : Type u_2) [] [SMul α A] [Zero α] (H : ∀ {n : α}, n 0Function.Surjective fun a => n a) :
∀ (x : A), (if x : 0 = 0 then 0 else Exists.choose (H 0 x x)) = 0
noncomputable def divisibleByOfSMulRightSurj (A : Type u_1) (α : Type u_2) [] [SMul α A] [Zero α] (H : ∀ {n : α}, n 0Function.Surjective fun a => n a) :

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

Instances For
noncomputable def rootableByOfPowLeftSurj (A : Type u_1) (α : Type u_2) [] [Pow A α] [Zero α] (H : ∀ {n : α}, n 0Function.Surjective fun a => a ^ n) :

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

Instances For
theorem Pi.divisibleBy.proof_1 {ι : Type u_1} {β : Type u_3} (B : ιType u_2) [(i : ι) → SMul β (B i)] [Zero β] [(i : ι) → AddMonoid (B i)] [(i : ι) → DivisibleBy (B i) β] (_x : (i : ι) → B i) :
(fun x n i => DivisibleBy.div (x i) n) _x 0 = 0
theorem Pi.divisibleBy.proof_2 {ι : Type u_2} {β : Type u_1} (B : ιType u_3) [(i : ι) → SMul β (B i)] [Zero β] [(i : ι) → AddMonoid (B i)] [(i : ι) → DivisibleBy (B i) β] :
∀ {n : β} (_x : (i : ι) → B i), n 0n (fun x n i => DivisibleBy.div (x i) n) _x n = _x
instance Pi.divisibleBy {ι : Type u_3} {β : Type u_4} (B : ιType u_5) [(i : ι) → SMul β (B i)] [Zero β] [(i : ι) → AddMonoid (B i)] [(i : ι) → DivisibleBy (B i) β] :
DivisibleBy ((i : ι) → B i) β
instance Pi.rootableBy {ι : Type u_3} {β : Type u_4} (B : ιType u_5) [(i : ι) → Pow (B i) β] [Zero β] [(i : ι) → Monoid (B i)] [(i : ι) → RootableBy (B i) β] :
RootableBy ((i : ι) → B i) β
theorem Prod.divisibleBy.proof_2 {β : Type u_3} {B : Type u_1} {B' : Type u_2} [SMul β B] [SMul β B'] [Zero β] [] [] [] [DivisibleBy B' β] :
∀ {n : β} (_p : B × B'), n 0n (fun p n => (DivisibleBy.div p.fst n, DivisibleBy.div p.snd n)) _p n = _p
theorem Prod.divisibleBy.proof_1 {β : Type u_3} {B : Type u_1} {B' : Type u_2} [SMul β B] [SMul β B'] [Zero β] [] [] [] [DivisibleBy B' β] (_p : B × B') :
(fun p n => (DivisibleBy.div p.fst n, DivisibleBy.div p.snd n)) _p 0 = 0
instance Prod.divisibleBy {β : Type u_3} {B : Type u_4} {B' : Type u_5} [SMul β B] [SMul β B'] [Zero β] [] [] [] [DivisibleBy B' β] :
DivisibleBy (B × B') β
instance Prod.rootableBy {β : Type u_3} {B : Type u_4} {B' : Type u_5} [Pow B β] [Pow B' β] [Zero β] [] [Monoid B'] [] [RootableBy B' β] :
RootableBy (B × B') β
instance ULift.instDivisibleBy (A : Type u_1) (α : Type u_2) [] [SMul α A] [Zero α] [] :
theorem ULift.instDivisibleBy.proof_1 (A : Type u_2) (α : Type u_3) [] [SMul α A] [Zero α] [] (x : ) :
(fun x a => { down := DivisibleBy.div x.down a }) x 0 = 0
theorem ULift.instDivisibleBy.proof_2 (A : Type u_2) (α : Type u_3) [] [SMul α A] [Zero α] [] :
∀ {n : α} (x : ), n 0n (fun x a => { down := DivisibleBy.div x.down a }) x n = x
instance ULift.instRootableBy (A : Type u_1) (α : Type u_2) [] [Pow A α] [Zero α] [] :
theorem AddCommGroup.smul_top_eq_top_of_divisibleBy_int (A : Type u_1) [] [] {n : } (hn : n 0) :
noncomputable def AddCommGroup.divisibleByIntOfSmulTopEqTop (A : Type u_1) [] (H : ∀ {n : }, n 0n = ) :

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

Instances For
instance divisibleByIntOfCharZero {𝕜 : Type u_1} [] [] :
theorem AddGroup.divisibleByIntOfDivisibleByNat.proof_2 (A : Type u_1) [] [] {n : } (a : A) (hn : n 0) :
n (fun a z => AddGroup.divisibleByIntOfDivisibleByNat.match_1 (fun z => A) z (fun n => ) fun n => -DivisibleBy.div a (n + 1)) a n = a

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

Instances For
abbrev AddGroup.divisibleByIntOfDivisibleByNat.match_1 (motive : Sort u_1) :
(z : ) → ((n : ) → motive ()) → ((n : ) → motive ()) → motive z
Instances For

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

Instances For
theorem AddGroup.divisibleByNatOfDivisibleByInt.proof_2 (A : Type u_1) [] [] {n : } (a : A) (hn : n 0) :
n (fun a n => ) a n = a

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

Instances For

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

Instances For
theorem Function.Surjective.divisibleBy.proof_1 {A : Type u_3} {B : Type u_2} {α : Type u_1} [Zero α] [] [SMul α A] [SMul α B] [] (f : AB) (hf : ) (hpow : ∀ (a : A) (n : α), f (n a) = n f a) {n : α} (hn : n 0) (x : B) :
a, (fun a => n a) a = x
noncomputable def Function.Surjective.divisibleBy {A : Type u_1} {B : Type u_2} {α : Type u_3} [Zero α] [] [] [SMul α A] [SMul α B] [] (f : AB) (hf : ) (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.

Instances For
abbrev Function.Surjective.divisibleBy.match_1 {A : Type u_1} {B : Type u_2} (f : AB) (x : B) (motive : (a, f a = x) → Prop) :
(x : a, f a = x) → ((y : A) → (hy : f y = x) → motive (_ : a, f a = x)) → motive x
Instances For
noncomputable def Function.Surjective.rootableBy {A : Type u_1} {B : Type u_2} {α : Type u_3} [Zero α] [] [] [Pow A α] [Pow B α] [] (f : AB) (hf : ) (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.

Instances For
theorem DivisibleBy.surjective_smul (A : Type u_4) (α : Type u_5) [] [SMul α A] [Zero α] [] {n : α} (hn : n 0) :
theorem RootableBy.surjective_pow (A : Type u_4) (α : Type u_5) [] [Pow A α] [Zero α] [] {n : α} (hn : n 0) :
Function.Surjective fun a => a ^ n
theorem QuotientAddGroup.divisibleBy.proof_1 {A : Type u_1} [] (B : ) :