Zulip Chat Archive

Stream: maths

Topic: Perfect Numbers


view this post on Zulip Aaron Anderson (Jun 17 2020 at 03:30):

I have a rough but working proof of the Perfect Number/Euclid-Euler Theorem, Freek 70, at https://github.com/awainverse/perfect_number

view this post on Zulip Aaron Anderson (Jun 17 2020 at 03:31):

I’m interested in people’s input on several things. One thing that comes to mind is whether some of the nat variables should be replaced with pnats.

view this post on Zulip Johan Commelin (Jun 17 2020 at 05:05):

@Aaron Anderson Interesting! I will write some feedback after breakfast.

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 05:07):

If it builds, then we can add it to our list.

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 05:09):

Could you please open a PR to mathlib/archive? We'll probably want to merge some parts to src/ but it would be nice to have a green light from CI before adding a link to this PR to the website.

view this post on Zulip Aaron Anderson (Jun 17 2020 at 05:56):

I'm trying to figure out how, but creating my own repository to host this today was already stretching my understanding of github...

view this post on Zulip Bryan Gin-ge Chen (Jun 17 2020 at 05:58):

I just downloaded the repo and it built locally with no warnings or errors.

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:02):

@Aaron Anderson We can coach you through it.

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:03):

Are you on windows or linux?

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:03):

(Or mac...)

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:04):

Linux.

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:04):

Ooh great, than it's easy-peasy

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:05):

You should have just received an email with an invitation for write access to mathlib.

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:05):

I know a few of the basic git commands at this point

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:05):

Do you by chance have leanproject installed?

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:05):

Yes, and I used that to create my perfect_number repo

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:08):

Ok, great.

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:08):

(I've accepted the email invitation)

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:09):

@Aaron Anderson so if you accept that invitation, and then leanproject get mathlib (in a directory where you do not yet have a copy of mathlib), then you are halfway there.

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:12):

Ok, I've done that, and have a "mathlib" folder on my computer.

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:12):

After that, you can write

git checkout -b freek-70

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:12):

This creates a new branch, for your PR

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:13):

After that, you have to copy your file to
archive/100-theorems-list/70_perfect_numbers.lean

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:13):

(Or something like that)

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:13):

And then

git add archive/100-theorems-list/70_perfect_numbers.lean
git commit

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:14):

In the commit message, you can use something like

feat(archive/100-theorems-list): perfect numbers (nr 70)

or something better (-;

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:15):

Once you have done that:

git push

and this will give an error message, saying that you need to set an upstream thingy. It will tell you which command to execute instead. Do that.

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:16):

This last command will give you a URL in it's output. You can visit that URL to open a PR.
(Alternatively, just go to the mathlib page on github, and it will recognise that you recently pushed a branch, and suggest to open a PR.)

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:17):

Finally, you can (if you want :stuck_out_tongue_wink:) post a message here of the form #3057 where 3057 is the PR number on the github page, and Zulip will automatically turn it into a link that we can click on to see your latest creation.

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:22):

Now for some feedback on the code. I've gone through the first 100 lines or so.

import data.nat.totient

open_locale classical
open_locale big_operators

section definitions

variable (n : )

def divisors : finset  :=
finset.filter (λ x : , x  n) (finset.Ico 1 (n + 1))

def proper_divisors : finset  :=
finset.filter (λ x : , x  n) (finset.Ico 1 n)

lemma not_proper_self :
  n  proper_divisors n :=
by simp [proper_divisors]

lemma mem_divisors {m : } :
n  divisors m  n  m  m  0:=
begin
  suffices : n  m  1  n  n < m + 1  n  m  ¬m = 0,
  by simpa only [divisors, finset.Ico.mem, ne.def, finset.mem_filter, and_comm],
  split,
  { intro hyp, refine hyp.left, _⟩, have h1 := hyp.right, omega },
  { intro hyp, refine hyp.left, _⟩,
    rcases hyp with ⟨⟨c, rfl, nonzero,
    split,
    { cases n,
      { simpa using nonzero },
      { exact nat.le_add_left _ _, }, },
    { cases c,
      { simpa using nonzero },
      { calc n = n * 1           : by rw mul_one
           ...  n * (c + 1)     : nat.mul_le_mul_left _ (nat.le_add_left _ _)
           ... < n * (c + 1) + 1 : nat.lt_succ_self _, } } }
end

variable {n}

lemma le_of_mem_divisors {m : } (h : n  divisors m) : n  m :=
by { rw [mem_divisors,  nat.pos_iff_ne_zero] at h, apply nat.le_of_dvd h.2 h.1 }

variable (n)

--lemma mem_proper_divisors : sorry := sorry

lemma divisors_eq_proper_divisors_insert_self (posn : 0 < n) :
  divisors n = insert n (proper_divisors n) :=
begin
  ext,
  simp only [finset.mem_insert, divisors, proper_divisors, finset.Ico.succ_top posn,
    finset.filter_insert, if_true, dvd_refl, finset.mem_insert],
end

def sum_divisors :  :=
 i in divisors n, i

def sum_proper_divisors :  :=
 i in proper_divisors n, i

@[simp] lemma divisors_zero : divisors 0 =  := dec_trivial

@[simp] lemma proper_divisors_zero : proper_divisors 0 =  := dec_trivial

@[simp] lemma sum_divisors_zero : sum_divisors 0 = 0 := dec_trivial

@[simp] lemma sum_proper_divisors_zero : sum_proper_divisors 0 = 0 := dec_trivial

lemma sum_divisors_eq_sum_proper_divisors_add_self :
sum_divisors n = sum_proper_divisors n + n :=
begin
  by_cases h : n = 0, { simp [h] },
  replace h : 0 < n := nat.pos_iff_ne_zero.mpr h,
  rw [sum_divisors, sum_proper_divisors, divisors_eq_proper_divisors_insert_self _ h,
    finset.sum_insert (not_proper_self _), add_comm],
end

def perfect : Prop :=
sum_proper_divisors n = n

end definitions

section basic_lemmas

lemma perfect_iff_sum_divisors_twice {n : } :
  perfect n  sum_divisors n = 2 * n :=
by { rw [sum_divisors_eq_sum_proper_divisors_add_self, perfect], omega }

@[simp] lemma divisors_one : divisors 1 = ({1} : finset ) :=
by { ext, rw mem_divisors, simp }

lemma one_mem_divisors {n : } (nonzero : n  0):
1  divisors n :=
by simp [mem_divisors, nonzero]

lemma self_mem_divisors {n : } (nonzero : n  0):
  n  divisors n :=
by simp [mem_divisors, nonzero]

lemma pos_sum_divisors {n : } (posn : 0 < n) :
  0 < sum_divisors n :=
begin
  rw nat.pos_iff_ne_zero at posn,
  calc 0 =  i in divisors n, 0 : finset.sum_const_zero.symm
     ... < sum_divisors n       : finset.sum_lt_sum (λ _ _, nat.zero_le _) _,
  use 1, exact one_mem_divisors posn, nat.zero_lt_one,
end

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:22):

#3094

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:22):

I should say that I think the code was already really good!

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:23):

@Aaron Anderson Nice!

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:24):

Another thing that can make your life easier: you often need to exclude n = 0. Sometimes you use 0 < n, sometimes 0 ≠ n. You should choose one, and use it everywhere. It will make it a lot easier to pass the assumption back and forth.
Now you constantly need to convert between the two versions.

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:25):

I'm still wondering if I do anything that'd make it difficult to just shift to pnats

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:26):

It might help a bit... But I'm not sure if it will matter much

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 06:27):

I think the correct thing to say here is "sure, just switch to pnats, and when you find holes in the pnat library just make a PR to mathlib which fixes them"

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:27):

Another thing:

src/number_theory/lucas_lehmer.lean:def mersenne (p : ℕ) : ℕ := 2^p - 1

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:27):

You could import that file.

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:27):

Maybe it even contains some lemmas that you could reuse.

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 06:27):

I think pnats deserve some more love

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:29):

@Aaron Anderson and there is also

src/data/padics/padic_norm.lean:def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=

which can help with the multiplicity lemmas

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:33):

@Yury G. Kudryashov Don't you think that 95% of the code should go into src/?

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:34):

@Aaron Anderson A lot of your lemmas seem useful and reusable. So we might want to butcher your file into tiny pieces that end up in 10 different places in mathlib.

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:35):

Awesome.

view this post on Zulip Aaron Anderson (Jun 17 2020 at 06:35):

I think pnats might be good for defining multiplicative functions in general

view this post on Zulip Johan Commelin (Jun 17 2020 at 06:36):

Feel free to experiment!

view this post on Zulip Johan Commelin (Jun 17 2020 at 07:04):

@Aaron Anderson By the way, probably relevant: if you want to make changes to the code in the PR, just edit the files in your clone of mathlib, and then git commit -a, write a message, and git push. That's it.

view this post on Zulip Kenny Lau (Jun 17 2020 at 07:23):

I use git commit -am "message"

view this post on Zulip Patrick Massot (Jun 17 2020 at 07:36):

Johan, if you don't have a convenient link you could have used instead of writing all those git explanations then you're welcome to copy paste this into our contributing guide, or a new file linked from our contributing guide.

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 07:43):

Johan Commelin said:

Yury G. Kudryashov Don't you think that 95% of the code should go into src/?

I didn't look at the code yet.

view this post on Zulip Aaron Anderson (Jun 18 2020 at 06:13):

I've started refactoring to pnats. Proving inequalities is easier, but the tactics seem much weaker. Along the way, I found that having to switch between pnats and nats made me want to use nat.primes for my prime numbers, but this is maybe too cumbersome...

view this post on Zulip Aaron Anderson (Jun 18 2020 at 06:13):

It's in a new file here https://github.com/awainverse/perfect_number

view this post on Zulip Aaron Anderson (Jun 18 2020 at 06:17):

I'd like to be able to talk about multiplicative functions in general, and prove something to the effect of ∀ n : ℕ+, f(n) = (factorisation n).prod (λ p : nat.primes, λ k : ℕ, f (p ^ k)) for a multiplicative function f, and factorisation a finsupp of multiplicities

view this post on Zulip Aaron Anderson (Jun 18 2020 at 06:18):

I think this is a good argument that I should keep going on pnats, and maybe nat.primes?

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 06:31):

The reason I would not use pnats if I were knocking off this sort of proof is precisely that they're not as well developed as nats, and the reason they're not as well developed is precisely because people don't use them. This vicious circle is not there for any particular reason and that's why I think keeping going on pnats is a good idea. Any factoring stuff will work better with pnats than nats the moment pnats have the right infrastructure. Pnats are a monoid with cancellation; monoids with 0 are a different thing somehow

view this post on Zulip Aaron Anderson (Jun 18 2020 at 17:45):

Well, I have no idea how the omega tactic works, other than sometimes it solves my problems with nats, but as I go I'm designating which lemmas about pnats maybe should be simp lemmas

view this post on Zulip Aaron Anderson (Jun 20 2020 at 01:09):

I'm proving (usually 2-line proofs or so) a lot of lemmas about pnats which are basically wrappers for existing nat lemmas. I think pnats would be way more useful if there was a common generalization of some kind of divisibility-structure, and facts about coprime and gcd were proved for that.

view this post on Zulip Aaron Anderson (Jun 20 2020 at 01:10):

I know that ring_theory/coprime exists, but pnats aren't a semiring, and gcd doesn't seem to be defined in that context.

view this post on Zulip Aaron Anderson (Jun 20 2020 at 01:11):

This probably wants some definition of a divisibilty poset?

view this post on Zulip Aaron Anderson (Jun 20 2020 at 01:12):

(Not at all necessary just to get this project in mathlib, but it'd be cool to start proving things about multiplicative functions, Dirichlet convolution, and even incidence algebras)

view this post on Zulip Johan Commelin (Jun 20 2020 at 05:05):

@Aaron Anderson Do you have any idea what kind of structure you need (weaker than semiring) in which you can prove your facts?

view this post on Zulip Johan Commelin (Jun 20 2020 at 05:07):

I guess (tongue in cheek) you might need a canonically_ordered_semirig

view this post on Zulip Aaron Anderson (Jun 20 2020 at 05:18):

I think that addition is unnecessary, a comm_monoid should be enough context

view this post on Zulip Aaron Anderson (Jun 20 2020 at 05:21):

Or perhaps has_dvd

view this post on Zulip Bryan Gin-ge Chen (Jun 20 2020 at 05:21):

Incidence algebras would be great!

view this post on Zulip Aaron Anderson (Jun 20 2020 at 05:22):

Something like “if you have an operation called gcd, which is provably equivalent to the sup in the poset with relation dvd, which has sensible properties, then you have these lemmas”

view this post on Zulip Alex J. Best (Jun 20 2020 at 05:26):

I did a tiny bit on incidence algebras a long time ago, its completely broken now :sad: (but I guess this means mathlib has advanced a lot) (and it was badly written / experimental to begin with) but just in case you are curious here is what I had:

import tactic
import data.rat.basic
import data.set.intervals
import data.set.finite
import init.algebra.order

open nat set

variable (α : Type*)

class locally_finite extends partial_order α :=
(fin_Icc :  x y : α, fintype (Icc x y))

def my_Icc (n m : ) : list  := list.range' n (m - n + 1)
def Icc_multi (n m : ) : multiset  := my_Icc n m
theorem nodup (n m : ) : list.nodup (my_Icc n m) :=
by dsimp [my_Icc]; simp [list.nodup_range']

theorem my_nodup (n m : ) : multiset.nodup (Icc_multi n m) := nodup _ _
def tIcc (n m : ) : finset  := ⟨_, my_nodup n m

instance Icc_ℕ_fintype (l u : ) : fintype (Icc l u) :=
fintype.of_finset (tIcc l u) (λ x,
begin split, intro h,simp [h], split, {simp [()] at h, sorry},sorry,sorry, end)

instance : partial_order  := by apply_instance

instance : locally_finite  :=
{ fin_Icc := λ x y, Icc_ℕ_fintype x y,
  ..nat.partial_order }

variables [locally_finite α] (R : Type*) [comm_ring R]

def incidence_algebra := α  α  R

def δ [decidable_eq α] : incidence_algebra α R :=
λ x y, if x = y then 1 else 0

#check δ  
#eval δ   1 0

def ζ [@decidable_rel α ()] : incidence_algebra α R :=
λ x y, if x  y then 1 else 0

#check ζ  
#eval ζ   1 3
#eval ζ   1 0

instance [decidable_eq α] : has_one (incidence_algebra α R) := δ α R

instance : has_mul (incidence_algebra α R) :=
⟨λ f g x y, finset.sum ((locally_finite.fin_Icc x y).elems) (λ z, f x z * g z y)

#check (δ   * δ  )
#eval (δ   * δ  ) 1 1
#eval (δ   * ζ  ) 1 1

instance [decidable_eq α] : monoid (incidence_algebra α R) :=
{ mul := (*),
  mul_assoc := λ x y z, begin sorry end,
  one := (1),
  one_mul := λ a, begin ext x y, simp [(*),has_one.one,δ],sorry end,
  mul_one := sorry }

instance (x y : α) : fintype (Icc x y) := locally_finite.fin_Icc x y

lemma card_Icc_lt_card_Icc_of_lt (x y z : α) (hxz : x  z) (hzy : z < y) : fintype.card (Icc x z) < fintype.card (Icc x y) :=
begin
   have hxy : x  y := le_of_lt (lt_of_le_of_lt hxz hzy),
   have y_not_mem : y  Icc x z := λ h, begin
      simp only [hxy, true_and, mem_Icc] at h,
      exact lt_irrefl _ (lt_of_le_of_lt h hzy),
   end,
   have y_mem : y  Icc x y := by simp [hxy],
   have : Icc x z  Icc x y := Icc_subset_Icc_right (le_of_lt hzy),
   exact card_lt_card this, λ h, by cc,
end

def μaux [decidable_eq α] (x : α) : α  R
| y := if x = y then 1 else begin
   haveI : fintype (Ico x y) := sorry,
   exact -finset.sum (fintype.elems (Ico x y)) (λ z,
      have fintype.card (Icc x z) < fintype.card (Icc x y) :=
         card_Icc_lt_card_Icc_of_lt α x y z.1 z.2.1 z.2.2,
      μaux z),
end
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ y,
   fintype.card (Icc x y)
)]}

def μ [decidable_eq α] : incidence_algebra α R := λ x, μaux α R x

set_option pp.all false

example : μ   = λ x y, if x = y then 1 else (if y = x + 1 then -1 else 0) :=
begin
   ext x y,
   split_ifs,
   {dsimp [μ], rwa [μaux, if_pos], },
   {dsimp [μ], rwa [μaux], rwa [if_neg, h_1], simp,
   have : Ico x (x + 1) = {x} := sorry,
   conv_lhs
   {
      rw [this],
      congr,
      skip,
      funext,
      rw [μaux],
      rw [if_pos (sorry  : x =  z)],
   }, simp, have := (locally_finite.fin_Icc x (x+1)).complete, simp at this,
   norm_cast,
   rw finset.card_eq_one,
   use x,
   simp,
   dsimp,
   dunfold coe_sort,
   dunfold has_coe_to_sort.coe,dsimp,
   simp,
   ext,
   simp at a,
   split,
   intro h,

   have := this x (by simp),
   erw [(sorry : Icc x (x+1) = {x})] at this,  },
end
#eval μ   1 1
#check set.has_coe_to_sort
lemma (p) :  finset.sum (fintype.elems {x_1 : α // p x}) f

lemma μ_inv_ζ_eq_one [decidable_eq α] [@decidable_rel α ()] : μ α R * ζ α R = 1 := begin
ext x y,
dsimp,
simp [(*)],
unfold_coes,
   dunfold coe_sort,
   dunfold has_coe_to_sort.coe,dsimp,
   simp,
end


#lint

view this post on Zulip Alex J. Best (Jun 20 2020 at 05:31):

Looks like list.Icc still isn't in mathlib, maybe we should add this as a (help wanted / easy) issue on github rather than just a comment in https://github.com/leanprover-community/mathlib/blob/fbc9592788fe71b15bdefc972a98f40b79d29bab/src/data/list/intervals.lean#L19 so people can find it?

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 08:37):

Isn't pnat a canonically ordered comm monoid with a lattice structure? Won't this be enough for most things?

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 08:40):

Note that nat isn't because of zero. But nat might well be a monoid with 0 with good factorisation properties. I was talking to @Chris Hughes about this the other day. The ideals in a commutative ring are a monoid and the ideals in a Dedekind domain are a monoid with a zero and, other than that, good factorisation properties. This all very much reminds me of @Johan Commelin 's group with 0 insight. There's some natural structure here that we're missing and we would like, but mathematicians didn't spot it yet. Is it an incidence algebra? I don't know what they are

view this post on Zulip Bryan Gin-ge Chen (Jun 20 2020 at 08:45):

Incidence algebras are what you define to generalize the Mobius inversion formula to settings like finite subsets where it becomes inclusion-exclusion.

view this post on Zulip David Wärn (Jun 20 2020 at 08:48):

Isn't nat a "canonically ordered comm monoid with lattice structure", where 0 is the maximal element? I think the problem with nat is that Dirichlet convolutions make no sense at 0, since a * b = 0 has infinitely many solutions

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 09:08):

If the axioms work out for nat too then the situation is even better than I expected

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 09:13):

The concept of a UFD generalises to monoids, was Chris' observation. And then there's this dichotomy depending on whether there's a 0 or not. At the end of the day the answer to the original question is that pnat as a monoid has the property that it is free, so you get all the juicy consequences of the universal property including a lattice structure with arbitrary nonzero infs. Does pnat have a lattice instance? Probably not because if there's an order it will be the usual one, not divisibility

view this post on Zulip David Wärn (Jun 20 2020 at 10:28):

I think there are at least three things happening with pnat that we can try to generalize:

  • Dirichlet convolutions of arithmetic functions. Incidence algebras sort of make sense of this, but an element of the incidence algebra contains superfluous information. Another concept is this: given a ring R and a category C, such that every arrow in C has only finitely many factorisations into two arrows, we can form the "category algebra", which assigns a scalar in R to every arrow, and where convolution makes sense because of the finiteness condition. Given a monoid like pnat (but unlike nat under multiplication!) we can thus form the category algebra on the single object category, and get the usual notion of arithmetic function & Dirichlet convolution. We also get incidence algebras, since posets are categories. We get a "Zeta function" by assigning 1 to every arrow, and a "delta function" (identity for convolution) by assigning 1 to identity arrows and 0 to everything else.

  • Multiplicative functions. Over "sufficiently nice" monoids (in particular free monoids like pnat), we can talk about multiplicative functions. I think for perfect numbers the relevant facts are "Zeta function is multiplicative", "the coercion pnat -> int is multiplicative", and "convolution of multiplicative functions is multiplicative".

  • Möbius inversion.Sometimes we can find a Möbius function, inverse to the Zeta function. In particular it always exists in an incidence algebra.

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 10:45):

It sounds like this incidence stuff is useful for the theory of so-called "multiplicative functions" (f(ab)=f(a)f(b) if gcd(a,b)=1), which do I think work on nat (f(0) can be anything). I wonder to what extent mobius inversion is useful though? I don't think you need it for perfect numbers

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 10:49):

Note that the standard usage of the phrase in number theory books has this gcd condition -- a monoid hom is called a strictly multiplicative function in the number theory literature. Coefficients of certain modular forms are multiplicative but not monoid homs, somehow the weaker notion was isolated as being useful

view this post on Zulip David Wärn (Jun 20 2020 at 10:58):

Yes, multiplicative function is a good concept, but I'm not sure how it generalizes. Presumably there's a connection to be made with measures, which are only additive when your sets are disjoint

view this post on Zulip David Wärn (Jun 20 2020 at 11:01):

Meanwhile, the concept of category algebra generalizes matrix algebras (which I unsuccessfully tried to make sense of a while ago) as well, via indiscrete categories. What a concept!

view this post on Zulip David Wärn (Jun 20 2020 at 11:29):

I also don't think you need Möbius inversion for Perfect numbers -- but of course it's often useful for counting things. As far as I can see the main (only?) advantage of incidence algebras over category algebras is that you always have a Möbius function (the upshot of the category algebra is that you get the usual notion of arithmetic function).

view this post on Zulip Aaron Anderson (Jun 20 2020 at 16:25):

All you need right now for perfect numbers to work for pnats are some duplicate lemmas about gcd and stuff, which I’ve written, and an alteration of the fin_mult and coprime_part ideas to work with pnat.factors rather than multiplicity, which needs a semiring

view this post on Zulip Aaron Anderson (Jun 20 2020 at 16:26):

But I’m just thinking about how to avoid writing so many duplicate lemmas if I (or someone else) keeps writing related elementary number theory

view this post on Zulip Aaron Anderson (Jun 20 2020 at 18:09):

Kevin Buzzard said:

Isn't pnat a canonically ordered comm monoid with a lattice structure? Won't this be enough for most things?

This is likely what I'm looking for. There's no definition yet of a multiplicative canonically_ordered_comm_monoid, and maybe that's what I'm looking for... one problem I wouldn't know how to deal with is how to recognize dvd as a partial order, without interfering with the linear order le from the additive structure. Then also I'm not sure syntactically it'd be easy to prove things about the gcd function without just repeatedly rewriting gcd_eq_sup_dvd or something

view this post on Zulip Yury G. Kudryashov (Jun 20 2020 at 18:22):

AFAIR there is some theory about "dvd as a partial order" in algebra/associated.

view this post on Zulip Aaron Anderson (Jun 20 2020 at 19:54):

Yury G. Kudryashov said:

AFAIR there is some theory about "dvd as a partial order" in algebra/associated.

That does seem useful. I'd want to prove things about the special case where associates is a partial order, in bijection with the original monoid, because there's only one unit.

view this post on Zulip Aaron Anderson (Jun 21 2020 at 22:41):

I've retrofitted most of my file to deal with pnats, and created a new file, multiplicity_vectors.lean, that introduces yet another kind of prime factorisation (as a finsupp), but contains a lot of sorries

view this post on Zulip Aaron Anderson (Jun 21 2020 at 22:44):

This new factorisation would be pretty useful for talking about multiplicative functions, and maybe other things, I'm interested to see if anyone else is interested in it. Probably the next thing to do with that would be to show that it's order isomorphic and add_monoid isomorphic to factor_multiset, and then a bunch of the sorried properties will probably be reduced to lemmas saying that lattices respect order isomorphisms, which either should exist or do already

view this post on Zulip Johan Commelin (Jun 22 2020 at 05:03):

@Aaron Anderson Note that there is already an isomorphism between multiset X and finsupp X nat. You could use that to transport the definition and a bunch of lemmas...
Alternatively, we might decide that the finsupp approach is the more flexible point of view, and just ditch the multiset approach completely.

view this post on Zulip Aaron Anderson (Jun 22 2020 at 05:07):

I’ve used .to_multiset to define it, and I know that’s invertible and a strict_mono. Is that the isomorphism you’re referring to?

view this post on Zulip Johan Commelin (Jun 22 2020 at 05:08):

Yup, exactly

view this post on Zulip Johan Commelin (Jun 22 2020 at 05:08):

The inverse is .to_finsupp

view this post on Zulip Aaron Anderson (Jul 01 2020 at 04:21):

I made a new commit, and started a PR review thread for 3094.


Last updated: May 14 2021 at 18:28 UTC