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

For additive monoids and groups:

• 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) [AddMonoid A] [SMul α A] [Zero α] : Type (max u_1 u_2)

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.

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

theorem DivisibleBy.div_zero {A : Type u_1} {α : Type u_2} [AddMonoid A] [SMul α A] [Zero α] [self : DivisibleBy A α] (a : A) : DivisibleBy.div a 0 = 0

theorem DivisibleBy.div_cancel {A : Type u_1} {α : Type u_2} [AddMonoid A] [SMul α A] [Zero α] [self : DivisibleBy A α] {n : α} (a : A) : n ≠ 0 → n • DivisibleBy.div a n = a

class RootableBy (A : Type u_1) (α : Type u_2) [Monoid A] [Pow A α] [Zero α] : Type (max u_1 u_2)

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.

• root : A → α → A
• root_zero : ∀ (a : A), RootableBy.root a 0 = 1
• root_cancel : ∀ {n : α} (a : A), n ≠ 0 → RootableBy.root a n ^ n = a

theorem RootableBy.root_zero {A : Type u_1} {α : Type u_2} [Monoid A] [Pow A α] [Zero α] [self : RootableBy A α] (a : A) : RootableBy.root a 0 = 1

theorem RootableBy.root_cancel {A : Type u_1} {α : Type u_2} [Monoid A] [Pow A α] [Zero α] [self : RootableBy A α] {n : α} (a : A) : n ≠ 0 → RootableBy.root a n ^ n = a

theorem smul_right_surj_of_divisibleBy (A : Type u_1) (α : Type u_2) [AddMonoid A] [SMul α A] [Zero α] [DivisibleBy A α] {n : α} (hn : n ≠ 0) : Function.Surjective fun (a : A) => n • a

theorem pow_left_surj_of_rootableBy (A : Type u_1) (α : Type u_2) [Monoid A] [Pow A α] [Zero α] [RootableBy A α] {n : α} (hn : n ≠ 0) : Function.Surjective fun (a : A) => a ^ n

theorem divisibleByOfSMulRightSurj.proof_2 (A : Type u_2) (α : Type u_1) [AddMonoid A] [SMul α A] [Zero α] (H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun (a : A) => n • a) : ∀ {n : α} (a : A), n ≠ 0 → n • (fun (a : A) (n : α) => if x : n = 0 then 0 else ⋯.choose) a n = a

noncomputable def divisibleByOfSMulRightSurj (A : Type u_1) (α : Type u_2) [AddMonoid A] [SMul α A] [Zero α] (H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun (a : A) => n • a) : DivisibleBy A α

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

Equations

• divisibleByOfSMulRightSurj A α H = { div := fun (a : A) (n : α) => if x : n = 0 then 0 else ⋯.choose, div_zero := ⋯, div_cancel := ⋯ }

theorem divisibleByOfSMulRightSurj.proof_1 (A : Type u_1) (α : Type u_2) [AddMonoid A] [SMul α A] [Zero α] (H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun (a : A) => n • a) : ∀ (x : A), (if x : 0 = 0 then 0 else ⋯.choose) = 0

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

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

Equations

• rootableByOfPowLeftSurj A α H = { root := fun (a : A) (n : α) => if x : n = 0 then 1 else ⋯.choose, root_zero := ⋯, root_cancel := ⋯ }

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) β

Equations

• Pi.divisibleBy B = { div := fun (x : (i : ι) → B i) (n : β) (i : ι) => DivisibleBy.div (x i) n, div_zero := ⋯, div_cancel := ⋯ }

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 : (i : ι) → B i) (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 ≠ 0 → n • (fun (x : (i : ι) → B i) (n : β) (i : ι) => DivisibleBy.div (x i) n) _x n = _x

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) β

Equations

• Pi.rootableBy B = { root := fun (x : (i : ι) → B i) (n : β) (i : ι) => RootableBy.root (x i) n, root_zero := ⋯, root_cancel := ⋯ }

theorem Prod.divisibleBy.proof_1 {β : Type u_3} {B : Type u_1} {B' : Type u_2} [SMul β B] [SMul β B'] [Zero β] [AddMonoid B] [AddMonoid B'] [DivisibleBy B β] [DivisibleBy B' β] (_p : B × B') : (fun (p : B × B') (n : β) => (DivisibleBy.div p.1 n, DivisibleBy.div p.2 n)) _p 0 = 0

instance Prod.divisibleBy {β : Type u_3} {B : Type u_4} {B' : Type u_5} [SMul β B] [SMul β B'] [Zero β] [AddMonoid B] [AddMonoid B'] [DivisibleBy B β] [DivisibleBy B' β] : DivisibleBy (B × B') β

Equations

• Prod.divisibleBy = { div := fun (p : B × B') (n : β) => (DivisibleBy.div p.1 n, DivisibleBy.div p.2 n), div_zero := ⋯, div_cancel := ⋯ }

theorem Prod.divisibleBy.proof_2 {β : Type u_3} {B : Type u_1} {B' : Type u_2} [SMul β B] [SMul β B'] [Zero β] [AddMonoid B] [AddMonoid B'] [DivisibleBy B β] [DivisibleBy B' β] : ∀ {n : β} (_p : B × B'), n ≠ 0 → n • (fun (p : B × B') (n : β) => (DivisibleBy.div p.1 n, DivisibleBy.div p.2 n)) _p n = _p

instance Prod.rootableBy {β : Type u_3} {B : Type u_4} {B' : Type u_5} [Pow B β] [Pow B' β] [Zero β] [Monoid B] [Monoid B'] [RootableBy B β] [RootableBy B' β] : RootableBy (B × B') β

Equations

• Prod.rootableBy = { root := fun (p : B × B') (n : β) => (RootableBy.root p.1 n, RootableBy.root p.2 n), root_zero := ⋯, root_cancel := ⋯ }

theorem ULift.instDivisibleBy.proof_1 (A : Type u_2) (α : Type u_3) [AddMonoid A] [SMul α A] [Zero α] [DivisibleBy A α] (x : ULift.{u_1, u_2} A) : (fun (x : ULift.{u_1, u_2} A) (a : α) => { down := DivisibleBy.div x.down a }) x 0 = 0

theorem ULift.instDivisibleBy.proof_2 (A : Type u_2) (α : Type u_3) [AddMonoid A] [SMul α A] [Zero α] [DivisibleBy A α] : ∀ {n : α} (x : ULift.{u_1, u_2} A), n ≠ 0 → n • (fun (x : ULift.{u_1, u_2} A) (a : α) => { down := DivisibleBy.div x.down a }) x n = x

instance ULift.instDivisibleBy (A : Type u_1) (α : Type u_2) [AddMonoid A] [SMul α A] [Zero α] [DivisibleBy A α] : DivisibleBy (ULift.{u_3, u_1} A) α

Equations

• ULift.instDivisibleBy A α = { div := fun (x : ULift.{?u.7, ?u.8} A) (a : α) => { down := DivisibleBy.div x.down a }, div_zero := ⋯, div_cancel := ⋯ }

instance ULift.instRootableBy (A : Type u_1) (α : Type u_2) [Monoid A] [Pow A α] [Zero α] [RootableBy A α] : RootableBy (ULift.{u_3, u_1} A) α

Equations

• ULift.instRootableBy A α = { root := fun (x : ULift.{?u.7, ?u.8} A) (a : α) => { down := RootableBy.root x.down a }, root_zero := ⋯, root_cancel := ⋯ }

theorem AddCommGroup.smul_top_eq_top_of_divisibleBy_int (A : Type u_1) [AddCommGroup A] [DivisibleBy A ℤ] {n : ℤ} (hn : n ≠ 0) : n • ⊤ = ⊤

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

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

Equations

• AddCommGroup.divisibleByIntOfSMulTopEqTop A H = { div := fun (a : A) (n : ℤ) => if hn : n = 0 then 0 else Exists.choose ⋯, div_zero := ⋯, div_cancel := ⋯ }

@[instance 100]

instance divisibleByIntOfCharZero {𝕜 : Type u_1} [DivisionRing 𝕜] [CharZero 𝕜] : DivisibleBy 𝕜 ℤ

Equations

• divisibleByIntOfCharZero = { div := fun (q : 𝕜) (n : ℤ) => q / ↑n, div_zero := ⋯, div_cancel := ⋯ }

theorem AddGroup.divisibleByIntOfDivisibleByNat.proof_1 (A : Type u_1) [AddGroup A] [DivisibleBy A ℕ] (a : A) : DivisibleBy.div a 0 = 0

abbrev AddGroup.divisibleByIntOfDivisibleByNat.match_1 (motive : ℤ → Sort u_1) : (z : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive z

Equations

• AddGroup.divisibleByIntOfDivisibleByNat.match_1 motive z h_1 h_2 = Int.casesOn z (fun (a : ℕ) => h_1 a) fun (a : ℕ) => h_2 a

def AddGroup.divisibleByIntOfDivisibleByNat (A : Type u_1) [AddGroup A] [DivisibleBy A ℕ] : DivisibleBy A ℤ

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

Equations

• One or more equations did not get rendered due to their size.

theorem AddGroup.divisibleByIntOfDivisibleByNat.proof_2 (A : Type u_1) [AddGroup A] [DivisibleBy A ℕ] {n : ℤ} (a : A) (hn : n ≠ 0) : n • (fun (a : A) (z : ℤ) => AddGroup.divisibleByIntOfDivisibleByNat.match_1 (fun (z : ℤ) => A) z (fun (n : ℕ) => DivisibleBy.div a n) fun (n : ℕ) => -DivisibleBy.div a (n + 1)) a n = a

def Group.rootableByIntOfRootableByNat (A : Type u_1) [Group A] [RootableBy A ℕ] : RootableBy A ℤ

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

Equations

• One or more equations did not get rendered due to their size.

theorem AddGroup.divisibleByNatOfDivisibleByInt.proof_2 (A : Type u_1) [AddGroup A] [DivisibleBy A ℤ] {n : ℕ} (a : A) (hn : n ≠ 0) : n • (fun (a : A) (n : ℕ) => DivisibleBy.div a ↑n) a n = a

theorem AddGroup.divisibleByNatOfDivisibleByInt.proof_1 (A : Type u_1) [AddGroup A] [DivisibleBy A ℤ] (a : A) : DivisibleBy.div a 0 = 0

def AddGroup.divisibleByNatOfDivisibleByInt (A : Type u_1) [AddGroup A] [DivisibleBy A ℤ] : DivisibleBy A ℕ

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

Equations

• AddGroup.divisibleByNatOfDivisibleByInt A = { div := fun (a : A) (n : ℕ) => DivisibleBy.div a ↑n, div_zero := ⋯, div_cancel := ⋯ }

def Group.rootableByNatOfRootableByInt (A : Type u_1) [Group A] [RootableBy A ℤ] : RootableBy A ℕ

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

Equations

• Group.rootableByNatOfRootableByInt A = { root := fun (a : A) (n : ℕ) => RootableBy.root a ↑n, root_zero := ⋯, root_cancel := ⋯ }

theorem Function.Surjective.divisibleBy.proof_1 {A : Type u_3} {B : Type u_2} {α : Type u_1} [Zero α] [AddMonoid A] [SMul α A] [SMul α B] [DivisibleBy A α] (f : A → B) (hf : Function.Surjective f) (hpow : ∀ (a : A) (n : α), f (n • a) = n • f a) {n : α} (hn : n ≠ 0) (x : B) : ∃ (a : B), (fun (a : B) => n • a) a = x

abbrev Function.Surjective.divisibleBy.match_1 {A : Type u_1} {B : Type u_2} (f : A → B) (x : B) (motive : (∃ (a : A), f a = x) → Prop) : ∀ (x_1 : ∃ (a : A), f a = x), (∀ (y : A) (hy : f y = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

noncomputable def Function.Surjective.divisibleBy {A : Type u_1} {B : Type u_2} {α : Type u_3} [Zero α] [AddMonoid A] [AddMonoid B] [SMul α A] [SMul α B] [DivisibleBy A α] (f : A → B) (hf : Function.Surjective f) (hpow : ∀ (a : A) (n : α), f (n • a) = n • f a) : DivisibleBy B α

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

Equations

• Function.Surjective.divisibleBy f hf hpow = divisibleByOfSMulRightSurj B α ⋯

noncomputable def Function.Surjective.rootableBy {A : Type u_1} {B : Type u_2} {α : Type u_3} [Zero α] [Monoid A] [Monoid B] [Pow A α] [Pow B α] [RootableBy A α] (f : A → B) (hf : Function.Surjective f) (hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n) : RootableBy B α

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

Equations

• Function.Surjective.rootableBy f hf hpow = rootableByOfPowLeftSurj B α ⋯

theorem DivisibleBy.surjective_smul (A : Type u_4) (α : Type u_5) [AddMonoid A] [SMul α A] [Zero α] [DivisibleBy A α] {n : α} (hn : n ≠ 0) : Function.Surjective fun (a : A) => n • a

theorem RootableBy.surjective_pow (A : Type u_4) (α : Type u_5) [Monoid A] [Pow A α] [Zero α] [RootableBy A α] {n : α} (hn : n ≠ 0) : Function.Surjective fun (a : A) => a ^ n

noncomputable instance QuotientAddGroup.divisibleBy {A : Type u_2} [AddCommGroup A] (B : AddSubgroup A) [DivisibleBy A ℕ] : DivisibleBy (A ⧸ B) ℕ

Any quotient group of a divisible group is divisible

Equations

• QuotientAddGroup.divisibleBy B = Function.Surjective.divisibleBy QuotientAddGroup.mk ⋯ ⋯

theorem QuotientAddGroup.divisibleBy.proof_2 {A : Type u_1} [AddCommGroup A] (B : AddSubgroup A) : ∀ (x : A) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem QuotientAddGroup.divisibleBy.proof_1 {A : Type u_1} [AddCommGroup A] (B : AddSubgroup A) : Function.Surjective QuotientAddGroup.mk

noncomputable instance QuotientGroup.rootableBy {A : Type u_2} [CommGroup A] (B : Subgroup A) [RootableBy A ℕ] : RootableBy (A ⧸ B) ℕ

Any quotient group of a rootable group is rootable.

Equations

• QuotientGroup.rootableBy B = Function.Surjective.rootableBy QuotientGroup.mk ⋯ ⋯