Instances of DivisibleBy

Stream: mathlib4

[Stepan Nesterov]

I am confused as to how the instances of DivisibleBy are set up.

import Mathlib

#synth DivisibleBy ℚ ℤ -- works
#synth DivisibleBy ℚ ℕ -- fails

section divZ

variable (A : Type*) [AddCommGroup A] [DivisibleBy A ℤ] (B : AddSubgroup A)

#synth DivisibleBy (A ⧸ B) ℤ -- fails

end divZ

section divN

variable (A : Type*) [AddCommGroup A] [DivisibleBy A ℕ] (B : AddSubgroup A)

#synth DivisibleBy (A ⧸ B) ℕ -- works

end divN

#synth DivisibleBy (ℚ ⧸ (Int.castAddHom ℚ).range) ℕ -- fails to synthesize `DivisibleBy ℚ ℕ`
#synth DivisibleBy (ℚ ⧸ (Int.castAddHom ℚ).range) ℤ -- fails to synthesize `DivisibleBy (A ⧸ B) ℤ`

Because ℚ is only divisible by ℤ and the quotient group only inherits divisibility by ℕ, mathlib can not infer that $\mathbb{Q}/\mathbb{Z}$ is a divisible group. Is there a reason for why it works like that?

[Ruben Van de Velde]

docs#DivisibleBy

[Kevin Buzzard]

Youch, this is a constructive definition, so it doesn't surprise me that there are some missing instances: adding them might cause diamonds. Are you sure you want to be using it at all? This doesn't just say "there's a $y$ such that $ny=x$", it says "we give a $y$ such that $ny=x$ and you'd better hope that nobody else gives another one even when there are many choices for $y$".

[Stepan Nesterov]

Kevin Buzzard said:

Youch, this is a constructive definition, so it doesn't surprise me that there are some missing instances: adding them might cause diamonds. Are you sure you want to be using it at all? This doesn't just say "there's a $y$ such that $ny=x$", it says "we give a $y$ such that $ny=x$ and you'd better hope that nobody else gives another one even when there are many choices for $y$".

Is there a non-constructive counterpart that I could use?

[Kevin Buzzard]

You could make IsDivisibleBy, define it as Nonempty (DivisbleBy ...) and then you could beef up

/-- A group is `ℤ`-rootable if it is `ℕ`-rootable.
-/
@[to_additive /-- An additive group is `ℤ`-divisible if it is `ℕ`-divisible. -/]
def rootableByIntOfRootableByNat [RootableBy A ℕ] : RootableBy A ℤ

and

/-- A group is `ℕ`-rootable if it is `ℤ`-rootable
-/
@[to_additive /-- An additive group is `ℕ`-divisible if it `ℤ`-divisible. -/]
def rootableByNatOfRootableByInt [RootableBy A ℤ] : RootableBy A ℕ where

into instances (right now they're not instances because I guess they'll cause diamonds?)

[Kevin Buzzard]

This sounds like a fun exercise, let me try knocking something up. For all I know there's already a standard way of talking about divisible abelian groups already though (although I don't know one and couldn't immediately spot one).

[Kevin Buzzard]

import Mathlib

class IsDivisibleBy (A α : Type*) [AddMonoid A] [SMul α A] [Zero α] : Prop where
  nonemptyDivisibleBy : Nonempty (DivisibleBy A α)

section monoid

variable {A α : Type*} [AddMonoid A] [SMul α A] [Zero α]

theorem isDivisibleBy_def : IsDivisibleBy A α ↔ ∀ {n : α} (a : A), n ≠ 0 → ∃ y, n • y = a := by
  constructor
  · rintro ⟨div, div_zero, div_cancel⟩ n a hn
    exact ⟨div a n, div_cancel _ hn⟩
  · intro h
    classical
    let div : A → α → A := fun a n ↦ if hn : n = 0 then 0 else (h a hn).choose
    refine ⟨div, ?_, ?_⟩
    · intro a
      exact dif_pos rfl
    · intro n a hn
      convert (h a hn).choose_spec
      exact dif_neg hn

instance [h : DivisibleBy A α] : IsDivisibleBy A α := ⟨⟨h⟩⟩

end monoid

section group

variable {A α : Type*} [AddGroup A] [SMul α A] [Zero α]

instance [h : IsDivisibleBy A ℕ] : IsDivisibleBy A ℤ := by
  obtain ⟨⟨h⟩⟩ := h
  exact ⟨⟨AddGroup.divisibleByIntOfDivisibleByNat A⟩⟩

instance [h : IsDivisibleBy A ℤ] : IsDivisibleBy A ℕ := by
  obtain ⟨⟨h⟩⟩ := h
  exact ⟨⟨AddGroup.divisibleByNatOfDivisibleByInt A⟩⟩

#synth IsDivisibleBy ℚ ℤ -- works
#synth IsDivisibleBy ℚ ℕ -- works

end group

section commgroup

variable {A α : Type*} [AddCommGroup A] [SMul α A] [Zero α]

noncomputable instance AddQuotientGroup.isDivisibleBy
  [h : IsDivisibleBy A ℤ] (B : AddSubgroup A): IsDivisibleBy (A ⧸ B) ℤ := by
  obtain ⟨⟨h⟩⟩ := h
  exact ⟨⟨QuotientAddGroup.mk_surjective.divisibleBy _ fun _ _ => rfl⟩⟩

section divZ

variable (A : Type*) [AddCommGroup A] [IsDivisibleBy A ℤ] (B : AddSubgroup A)

#synth IsDivisibleBy (A ⧸ B) ℤ -- works

end divZ

section divN

variable (A : Type*) [AddCommGroup A] [IsDivisibleBy A ℕ] (B : AddSubgroup A)

#synth IsDivisibleBy (A ⧸ B) ℕ -- works

end divN

#synth IsDivisibleBy (ℚ ⧸ (Int.castAddHom ℚ).range) ℕ -- works
#synth IsDivisibleBy (ℚ ⧸ (Int.castAddHom ℚ).range) ℤ -- works

Don't know if mathlib will be interested. For sure, if it is, it will want IsRootableBy with all proofs multiplicativised.