mathlib feat(group_theory/divisible): definition of divisible group

This PR defines divisible group and proves that the set of rationals is divisible and product of divisible group is divisible. Future PR will be opened to prove that divisibility implies injectivity and hence category of abelian group has enough injective and an adjoint functor will transfer enough invectiveness in Ab to R-Mod.

[x] depends on: #15478

Jun 28 '22 15:06 jjaassoonn

I think we might want a multiplicative group version of this too? with the one here generated by to_additive? Certainly there are nice examples like algebraically closed fields that are multiplicative groups.

Jun 30 '22 15:06 alexjbest

What's the difference between module ℚ A and divisible A? Is the following true?

/-- Any rat-module is divisible -/
def divisible_of_rat_module [module ℚ A] : divisible A :=
{ div_int := λ q n, (n : ℚ)⁻¹ • q,
  div_zero := λ q, by norm_num,
  div_cancel := λ n q hn, by {
    rw [zsmul_eq_smul_cast ℚ, smul_inv_smul₀],
    exact (int.cast_ne_zero.mpr hn : _) }

/-- Any divisible additive group is a rat-module -/
def rat_module_of_divisible [divisible A] : module ℚ A :=
{ smul := λ q a, q.num • divisible.div_int a q.denom ,
  one_smul := λ a, by {dsimp, refine divisible.div_cancel _ one_ne_zero },
  mul_smul := λ q r a, sorry,
  smul_add := λ q a b, sorry,
  smul_zero := λ q, by {
    dsimp, sorry },
  add_smul := λ q r a, by {dsimp, sorry},
  zero_smul := λ a, by simp }

attribute [ext] divisible

def divisible_is_pointless : divisible A ≃ module ℚ A :=
{ to_fun := @add_comm_group.rat_module_of_divisible _ _,
  inv_fun := @add_comm_group.divisible_of_rat_module _ _,
  left_inv := λ d, begin
    resetI,
    ext a z,
    dsimp [add_comm_group.divisible_of_rat_module, rat_module_of_divisible],
    obtain rfl | hz := eq_or_ne z 0,
    { simp [divisible.div_zero] },
    rw inv_smul_eq_iff₀,
    unfold_projs,
    dsimp,
    sorry,
    exact int.cast_ne_zero.mpr hz,
  end,
  right_inv := _ }

Not really, think about abelian groups with torsion, for example Q/Z, this is divisible but not a Q module. If an Ab is torsion free then it is a Q-module.

Jun 30 '22 15:06 jjaassoonn

I think we might want a multiplicative group version of this too? with the one here generated by to_additive? Certainly there are nice examples like algebraically closed fields that are multiplicative groups.

Do you mean something like this

namespace comm_group

variables (A : Type*) [comm_group A]

@[to_additive "add_comm_group.divisible"]
class rootable :=
(root_int : A → ℤ → A)
(root_zero : ∀ a, root_int a 0 = 1)
(root_pow : ∀ {n : ℤ} (a : A), n ≠ 0 → (root_int a n)^n = a)

end comm_group

Jun 30 '22 15:06 jjaassoonn

I also think this notion could be more useful when defined for comm_monoids, so we cover groups_with_zero too, (such as fields again), the property of nat divisibility implies int divisibility in a group after all. We could then maybe refactor a bunch of things about nth roots in terms of this new notion.

Jun 30 '22 15:06 alexjbest

I think we might want a multiplicative group version of this too? with the one here generated by to_additive? Certainly there are nice examples like algebraically closed fields that are multiplicative groups.

Do you mean something like this
namespace comm_group

variables (A : Type*) [comm_group A]

@[to_additive "add_comm_group.divisible"]
class rootable :=
(root_int : A → ℤ → A)
(root_zero : ∀ a, root_int a 0 = 1)
(root_pow : ∀ {n : ℤ} (a : A), n ≠ 0 → (root_int a n)^n = a)

end comm_group

Yeah something like that, unfortunately it messes up your nice notation though :(

Jun 30 '22 15:06 alexjbest

I also think this notion could be more useful when defined for comm_monoids, so we cover groups_with_zero too, (such as fields again), the property of nat divisibility implies int divisibility in a group after all. We could then maybe refactor a bunch of things about nth roots in terms of this new notion.

Is the current form of this pr what you have in mind @alexjbest

Jul 15 '22 22:07 jjaassoonn

This PR/issue depends on: