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 #

Main results #

For additive monoids and groups:

and their multiplicative counterparts:

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.
Instances
    theorem DivisibleBy.div_zero {A : Type u_1} {α : Type u_2} :
    ∀ {inst : AddMonoid A} {inst_1 : SMul α A} {inst_2 : Zero α} [self : DivisibleBy A α] (a : A), DivisibleBy.div a 0 = 0
    theorem DivisibleBy.div_cancel {A : Type u_1} {α : Type u_2} :
    ∀ {inst : AddMonoid A} {inst_1 : SMul α A} {inst_2 : Zero α} [self : DivisibleBy A α] {n : α} (a : A), n 0n 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.
    Instances
      theorem RootableBy.root_zero {A : Type u_1} {α : Type u_2} :
      ∀ {inst : Monoid A} {inst_1 : Pow A α} {inst_2 : Zero α} [self : RootableBy A α] (a : A), RootableBy.root a 0 = 1
      theorem RootableBy.root_cancel {A : Type u_1} {α : Type u_2} :
      ∀ {inst : Monoid A} {inst_1 : Pow A α} {inst_2 : Zero α} [self : RootableBy A α] {n : α} (a : A), n 0RootableBy.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 0Function.Surjective fun (a : A) => n a) :
      ∀ {n : α} (a : A), n 0n (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 0Function.Surjective fun (a : A) => n 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 := }
      Instances For
        theorem divisibleByOfSMulRightSurj.proof_1 (A : Type u_1) (α : Type u_2) [AddMonoid A] [SMul α A] [Zero α] (H : ∀ {n : α}, n 0Function.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 0Function.Surjective fun (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
        • rootableByOfPowLeftSurj A α H = { root := fun (a : A) (n : α) => if x : n = 0 then 1 else .choose, root_zero := , root_cancel := }
        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 : (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 0n (fun (x : (i : ι) → B i) (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) β
          Equations
          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
          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 0n (fun (p : B × B') (n : β) => (DivisibleBy.div p.1 n, DivisibleBy.div p.2 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 β] [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
          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
          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 0n (fun (x : ULift.{u_1, u_2} A) (a : α) => { down := DivisibleBy.div x.down a }) x n = x
          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
          instance ULift.instDivisibleBy (A : Type u_1) (α : Type u_2) [AddMonoid A] [SMul α A] [Zero α] [DivisibleBy A α] :
          Equations
          instance ULift.instRootableBy (A : Type u_1) (α : Type u_2) [Monoid A] [Pow A α] [Zero α] [RootableBy A α] :
          Equations
          noncomputable def AddCommGroup.divisibleByIntOfSMulTopEqTop (A : Type u_1) [AddCommGroup A] (H : ∀ {n : }, n 0n = ) :

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

          Equations
          Instances For
            @[instance 100]
            instance divisibleByIntOfCharZero {𝕜 : Type u_1} [DivisionRing 𝕜] [CharZero 𝕜] :
            Equations
            • divisibleByIntOfCharZero = { div := fun (q : 𝕜) (n : ) => q / n, div_zero := , div_cancel := }
            theorem AddGroup.divisibleByIntOfDivisibleByNat.proof_2 (A : Type u_1) [AddGroup A] [DivisibleBy A ] {n : } (a : A) (hn : n 0) :
            n (fun (a : A) (z : ) => match z with | Int.ofNat n => DivisibleBy.div a n | Int.negSucc n => -DivisibleBy.div a (n + 1)) a n = a

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

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

              A group is -rootable if it is -rootable.

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

                An additive group is -divisible if it -divisible.

                Equations
                Instances For
                  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

                  A group is -rootable if it is -rootable

                  Equations
                  Instances For
                    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 : AB) (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
                    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 : AB) (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
                    Instances For
                      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 : AB) (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
                      Instances For
                        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
                        theorem QuotientAddGroup.divisibleBy.proof_2 {A : Type u_1} [AddCommGroup A] (B : AddSubgroup A) :
                        ∀ (x : A) (x_1 : ), (x_1 x) = (x_1 x)
                        noncomputable instance QuotientAddGroup.divisibleBy {A : Type u_2} [AddCommGroup A] (B : AddSubgroup A) [DivisibleBy A ] :

                        Any quotient group of a divisible group is divisible

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

                        Any quotient group of a rootable group is rootable.

                        Equations