with_zero (multiplicative A) ≃* multiplicative (with_bot A)

Stream: Is there code for X?

[Eric Wieser]

Do we have something like this anywhere?

section
local attribute [reducible] with_zero

def with_zero.to_additive {A} [add_monoid A] :
  with_zero (multiplicative A) ≃* multiplicative (with_bot A) :=
by exact mul_equiv.refl _
end

@[simp] lemma with_zero.to_additive_zero {A} [add_monoid A] :
  with_zero.to_additive (0 : with_zero (multiplicative A)) = multiplicative.of_add ⊥ := rfl
@[simp] lemma with_zero.to_additive_coe {A} [add_monoid A] (x : multiplicative A) :
  with_zero.to_additive ↑x = multiplicative.of_add (x.to_add : with_bot A) := rfl
@[simp] lemma with_zero.to_additive_symm_bot {A} [add_monoid A] :
  with_zero.to_additive.symm (multiplicative.of_add (⊥ : with_bot A)) = 0 := rfl
@[simp] lemma with_zero.to_additive_coe_of_add {A} [add_monoid A] (x : A) :
  with_zero.to_additive.symm (multiplicative.of_add (x : with_bot A)) =
    multiplicative.of_add x := rfl

[Eric Wieser]

I ask because this combined with #8889 gives an if-free definition of #12245's

def infty_valuation_def (r : ratfunc Fq) : with_zero (multiplicative ℤ) :=
with_zero.to_additive.symm $
  multiplicative.of_add (r.num.degree.map coe - r.denom.degree.map coe : with_bot ℤ)

(cc @María Inés de Frutos Fernández)

[María Inés de Frutos Fernández]

As far as I know this is not in mathlib.
I think it would be nice to have the with_top version of this:

def with_zero.to_additive {A} [add_monoid A] :
  with_zero (multiplicative A) ≃* multiplicative (with_top A) :=
by exact mul_equiv.refl _

It might help to easily relate the valuation infty_valuation with its associated add_valuation (and more generally for other nonarchimedean valuations).

[María Inés de Frutos Fernández]

Currently in mathlib we seem to have more API for valuation and with_zero than for add_valuation and with_top, so I just use valuation, but it would be nice if there were a simple way to convert from one to the other.

[Eric Wieser]

You're right, with_top is probably the right choice, not with_bot, since that also makes this preserve the ordering relation.

[Eric Wieser]

I retract that comment, with_bot is the one that preserves order after all

[Kevin Buzzard]

With valuations in particular, Maria's convention is the useful one, because additive valuations like "v(n) = the highest power of p dividing n" have v(0)=+∞ and when converting to a multiplicative valuation you reverse the order.

[Kevin Buzzard]

v_mult(n)=e^v_add(n) with 0<e<1 (traditionally e=1/p)

[Eric Wieser]

I can't quite make the precise connection between your comment and my isomorphism above, although I can believe it's there

[Kevin Buzzard]

If G is a totally ordered abelian group then with_bot G and with_top G are order isomorphic via inv.

[Eric Wieser]

Yes, so I think I'd argue you should be chaining the equiv I suggest above with such an inv order isomorphism

[Eric Wieser]

I guess we have docs#order_iso.inv but no with_* version?

[Eric Wieser]

Hmm, I still think I'm missing something - order_iso.inv : G ≃o order_dual G, so either the total order changes things in a way I can't see, or you mean that with_top G ≃o with_bot (order_dual G) via inv.

[Kevin Buzzard]

You're rght -- there is an unsolvable "op" problem here. Additive valuations have the axiom v(ab)>= min v(a) v(b) and multiplicative valuations have the axiom v(ab) <= max v(a) v(b) and this is already culturally embedded. This is what's behind Maria's comment.

[Eric Wieser]

Right, so there's an order_dual hiding in the difference too

[Eric Wieser]

It took me forever, but I think you're describing foo or bar in:

import algebra.order.group
import control.equiv_functor

def order_iso.with_bot_dual {G : Type*} [has_le G] :
  order_dual (with_top G) ≃o with_bot (order_dual G) :=
order_iso.refl _

def order_iso.with_top_dual {G : Type*} [has_le G] :
  order_dual (with_bot G) ≃o with_top (order_dual G) :=
order_iso.refl _

def order_iso.with_top {α β} [partial_order α] [partial_order β] (e : α ≃o β) :
  with_top α ≃o with_top β :=
{ to_equiv := show option α ≃ option β, from equiv_functor.map_equiv _ e,
  map_rel_iff' := λ x y, begin
    cases x; cases y;
      dsimp [equiv_functor.map_equiv, equiv_functor.map];
      dsimp [with_top.none_eq_top, with_top.some_eq_coe];
      try {simp},
    exact e.map_rel_iff,
  end }

variables {G : Type*} [group G] [partial_order G]
  [covariant_class G G (*) (≤)]
  [covariant_class G G (function.swap (*)) (≤)]

def bar : with_top G ≃o with_top (order_dual G) :=
order_iso.with_top (order_iso.inv G)

def foo : with_top G ≃o order_dual (with_bot G) :=
bar.trans order_iso.with_top_dual.symm

[Kevin Buzzard]

Right! We use foo and then to_additive when translating from mult to add

[Yaël Dillies]

Oh duh, did I forget to add the above with_top/with_bot equivalences?

[Eric Wieser]

The other important one we're missing is:

def order_iso.with_top {α β} [has_le α] [has_le β] (e : α ≃o β) :
  with_top α ≃o with_top β :=

[Yaël Dillies]

Have a look at #11677 :wink:

[Yaël Dillies]

I needed those for docs#lattice_hom in order to construct the free functor from Lattice to BoundedLattice.

[Eric Wieser]

I don't see the order_iso version there

[Yaël Dillies]

No, it's not there, but I was about to add it

[Eric Wieser]

I edited it above

[Eric Wieser]

The proof is gross, we should probably have an equiv_functor instance for with_top

[Eric Wieser]

Eric Wieser said:

It took me forever, but I think you're describing foo or bar in:
<snip>

I PR'd these three isos in #12264

[Eric Wieser]

The last pieces are in #12275. I'm not sure exactly how useful these are, but I think with all of them together you can push the type tags around while preserving structure.

[Yaël Dillies]

You should definitely have a look at branch#GroupWithZero

[Eric Wieser]

Is there any overlap? I don't see it

[Yaël Dillies]

My monoid_hom.with_zero is very close to your mul_equiv.with_zero_congr.

[Eric Wieser]

It's also very close to the docs#with_zero.map we already have, right?

[Yaël Dillies]

Yeah