mul_pos

Stream: maths

[Johan Commelin]

import algebra.linear_ordered_comm_group_with_zero

open_locale classical

lemma mul_pos'''' {M : Type*} [linear_ordered_comm_monoid_with_zero M]
  (a b : M) (ha : 0 < a) (hb : 0 < b) :
  0 < a * b :=
begin
  admit,
end

Is this true?

[Johan Commelin]

#xy:

example {ι : Type*} (s : finset ι) (f : ι → ℕ) (h : ∀ i, 0 < f i) :
  0 < ∏ i in s, f i :=
begin
  sorry
end

[Kevin Buzzard]

Yes it's true update: erm...

[Johan Commelin]

I know I can prove the second example by passing to int or pnat, but that feels like a hack around a hole in the library.

[Johan Commelin]

I don't understant the contortion linear_ordered_comm_monoid_with_zero well enough to know whether my set of examples covers its behaviour...

[Kevin Buzzard]

I've got it down to a,b!=0 implies ab!=0 and this is surely true for any linearly ordered structure

[Johan Commelin]

Right, I got that far as well...

[Damiano Testa]

I am not sure that there is a proof in Lean that a linear order has no non-trivial zero divisors... seems like a job for the new notion of regular! :stuck_out_tongue_wink:

[Rémy Degenne]

I see no reference to a linear order in the instances of docs#no_zero_divisors

[Kevin Buzzard]

So how about {0,eps,1} with eps^2=0 and all other multiplications the obvious ones?

[Kevin Buzzard]

:-/

[Damiano Testa]

Should this go in the counterexamples folder? :smile:

[Kevin Buzzard]

Is it definitely a counterexample?

[Kevin Buzzard]

I need to prepare my class :-(

[Damiano Testa]

I am not sure: of course, the weird thing is eps^2 not being positive, but I do not know if this is precluded by the axioms of linear...

[Kevin Buzzard]

It sounds right though. I've even seen this example before. The valuation on Z_p takes values in [0,1], and now if you want to quotient and get some kind of valuation on Z/p^nZ then you need to quotient the target too, and get {0} union (1/p^n,1], and this comes up in tilting and is precisely the reason I wanted to switch from linear_ordered_comm_group_with_zero as the target of a valuation to linear_ordered_comm_monoid_with_zero.

[Kevin Buzzard]

Update on this: I think I did all the groundwork for making that change (e.g. I made the class!) but I never did the switch for the target of a valuation IIRC.

[Rémy Degenne]

going through the fields of linear_ordered_comm_monoid_with_zero one by one, it looks like it fits. I did not code anything to verify though.

[Kevin Buzzard]

If it doesn't fit then I need to completely re-evaluate the "change group to monoid" idea for valuations, because my understanding of what is going on is wrong. I was completely wrong when I claimed 0<a -> 0<b -> 0<ab was true, I even knew this counterexample.

[Johan Commelin]

import algebra.ordered_monoid

@[derive [decidable_eq]]
inductive foo
| zero
| eps
| one

namespace foo

instance : has_zero foo := ⟨zero⟩
instance : has_one foo := ⟨one⟩
notation `ε` := eps

def aux1 : foo → ℕ
| 0 := 0
| ε := 1
| 1 := 2

meta def boom : tactic unit :=
`[repeat {rintro ⟨⟩}; dec_trivial]

lemma aux1_inj : function.injective aux1 :=
by boom

instance : linear_order foo :=
linear_order.lift aux1 $ aux1_inj

def mul : foo → foo → foo
| 0 _ := 0
| ε 1 := ε
| ε _ := 0
| 1 x := x

instance : comm_monoid foo :=
{ mul := mul,
  one := 1,
  one_mul := by boom,
  mul_one := by boom,
  mul_comm := by boom,
  mul_assoc := by boom }

instance : linear_ordered_comm_monoid_with_zero foo :=
{ zero := 0,
  zero_mul := by boom,
  mul_zero := by boom,
  mul_le_mul_left := by { rintro ⟨⟩ ⟨⟩ h ⟨⟩; revert h; dec_trivial },
  lt_of_mul_lt_mul_left := by { rintro ⟨⟩ ⟨⟩ ⟨⟩; dec_trivial },
  zero_le_one := dec_trivial,
  .. foo.linear_order,
  .. foo.comm_monoid }

end foo

[Johan Commelin]

Thanks for the counterexample Kevin!

[Kevin Buzzard]

Good to know that my global understanding was correct and my local error was just that!

[Kevin Buzzard]

PR it to the counterexamples directory!

[Johan Commelin]

That directory doesn't exist yet, right?

[Damiano Testa]

it does in the branch counterexamples

[Damiano Testa]

but i never created a PR...

[Damiano Testa]

because I am not sure that what I wrote there would actually be acceptable for mathlib, even in the counterexamples directory!

[Damiano Testa]

https://github.com/leanprover-community/mathlib/tree/counterexamples

[Kevin Buzzard]

I dream of a linter which, for any ordered pair of distinct prop-valued classes, checks that either there's an instance showing that one implies the other, or a counterexample showing that it doesn't :-)

[Damiano Testa]

You can golf your multiplication as follows:

def mul1 : foo → foo → foo
| 1 x := x
| x 1 := x
| _ _ := 0

lemma muleq : mul = mul1 :=
begin
  ext1 a, ext1 b,
  cases a;cases b;
  boom,
end

(This is simply me trying to learn how to use the equation compiler.)

[Johan Commelin]

aah, good catch (-;

[Damiano Testa]

Kevin, your linter seems great! I hope that it will exist one day!

The counterexamples folder is a home-remedy for it...

[Damiano Testa]

Johan, given that you wrote down a fully formalized proof of the example, it will be very little work to add it to counterexamples: there is a non-existent review process for that branch!

If you want, I can push it, but feel free to do so yourself, if you prefer!

[Johan Commelin]

Ooh, feel free to add it

[Johan Commelin]

We should have a journal "Counterexamples of Mathematics" with a nonexistent review process. Sounds like an awesome place to publish :rofl:

[Damiano Testa]

Ahaha

In the meanwhile, the CI is working on it: I guess this counts as one of the most thorough refereeing processes, after actually getting into mathlib!

[Damiano Testa]

Johan, the referee report is back: your proof is correct!

[Christian Merten]

Sorry for bumping this very old thread, but this counterexample is currently deleted in #31749 (because with the new proposed docs#LinearOrderedCommMonoidWithZero mul_pos is a theorem), so I read the discussion here. One comment confuses me:
Kevin Buzzard said:

It sounds right though. I've even seen this example before. The valuation on Z_p takes values in [0,1], and now if you want to quotient and get some kind of valuation on Z/p^nZ then you need to quotient the target too, and get {0} union (1/p^n,1], and this comes up in tilting and is precisely the reason I wanted to switch from linear_ordered_comm_group_with_zero as the target of a valuation to linear_ordered_comm_monoid_with_zero.

From the context, it seems to me that you are suggesting that $\{0\} \cup (1/p^n,1]$ is a natural example of a "linearly ordered commutative monoid with zero" that has $\epsilon ^ 2 = 0$. Am I misunderstanding you or what is $\epsilon$ here?
(cc @Yaël Dillies and for reference the more recent thread where this change was discussed is here: #mathlib4 > Should linear ordered comm monoids with zero be torsion-free )

[Yaël Dillies]

I assume $\epsilon$ here would be anything between $p^{-n}$ and $p^{-n/2}$?

[Kevin Buzzard]

Yeah this is supposed to be a quotient of the multiplicative monoid [0,1] by the equivalence relation "make everything in [0,1/p^n] equivalent and call it 0" (corresponding to the quotient "make everything with norm at most 1/p^n equal to zero" on the ring side). Note the quotient map is an example of a non-injective morphism of monoids with trivial kernel.

[Christian Merten]

So then the question is: How important is this example? Because if #31749 is merged, this can no longer be the codomain of a valuation.

[Kevin Buzzard]

I can't remember what I was thinking of when I said "this comes up in tilting". @Kenny Lau I was probably supervising your MSc project on tilting at that time. Do you have any memories of this?

[Christian Merten]

Coming back to this: We should get to a decision on #31749 so that Yaël does not have to keep fixing merge conflicts.
Am I correct that no one seems to remember the use case of the $\{0\} \cup (1/p^n, 1]$ example?

[Kevin Buzzard]

Whatever reason I had for using monoids as a target would, even if I could remember it, need to be seriously re-evaluated now we have docs#ValuativeRel which IMO is the way to do adic spaces now. Am I right in thinking that we'd still be able to put a ValuativeRel structure on the integers corresponding to this funky thing which is about to be banned as a valuation?

[Yaël Dillies]

I doubt so: docs#ValuativeRel.vle_mul_cancel seems to forbid it

[Kevin Buzzard]

I guess this would not be valid because the axiom vle_mul_cancel would not be satisfied. My instinct is that we should do one of the following: (a) forget my concerns and go ahead, or (b) someone should actively try and get in touch with Kenny and see if he remembers anything. I'll start on (b).

[Kenny Lau]

#30989 is Teichmuller, and I promised a future PR where I would prove Perfection R ≅ Perfection (R/I), and then we won't need a valuation on R/I anymore, right? I don't remember anything about this valuation.

[Kevin Buzzard]

I have no objections to the refactor. I don't think it's reasonable to hold this up based on some conversation from 6 years ago which nobody remembers the details of. All I know for sure is that mathlib is far more mature now.