mathlib3 documentation

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 #

Main results #

For additive monoids and groups:

and their multiplicative counterparts:

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] [has_smul α 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_pow A α] [has_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.
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_pow A α] [has_zero α] [rootable_by A α] {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] [has_smul α A] [has_zero α] [divisible_by A α] {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_pow 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] [has_smul α 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 : ι), has_smul β (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} [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
@[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
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 = ) :

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

Equations
@[protected, instance]
Equations

A group is -rootable if it is -rootable.

Equations

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

Equations

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] [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) :

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

Equations
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) :

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

Equations
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)
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)
@[protected, instance]
noncomputable def quotient_add_group.divisible_by {A : Type u_2} [add_comm_group A] (B : add_subgroup A) [divisible_by 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) [rootable_by A ] :

Any quotient group of a rootable group is rootable.

Equations