Zulip Chat Archive

Stream: general

Topic: normed_division_ring


Jireh Loreaux (Feb 18 2022 at 08:18):

I think I have a problem because mathlib doesn't have a normed_division_ring, but I'm not sure. I think I reduced my problem to the following:

problem

If I understand the error message correctly, the problem is that the term I constructed is a unit in the monoid coming from the fact that R is a division_ring, but it was expecting a unit in the monoid coming form the fact that R is a normed_ring.

  1. Did I interpret correctly?
  2. I really do need both hypotheses as I am trying to define the Gelfand-Mazur isomorphism
  3. How do I deal with this?

Kevin Buzzard (Feb 18 2022 at 08:22):

docs#division_ring docs#normed_ring docs#is_field docs#is_division_ring (sorry, on mobile!)

Damiano Testa (Feb 18 2022 at 08:24):

Doing convert (@is_unit_iff_ne_zero _ _ r).mpr _ produces a goal of

R: Type u_1
_inst_1: division_ring R
_inst_2: normed_ring R
r: R
h: r  0
 ring.to_monoid R = monoid_with_zero.to_monoid R

Maybe this means that there are issues with going from ring to monoid? I do not really know whether this is a diamond or not...

Kevin Buzzard (Feb 18 2022 at 08:25):

(deleted)

Kevin Buzzard (Feb 18 2022 at 08:27):

is_field is an example, which is there, but if your ring is not commutative you'll need is_division_ring which is not, but which should be easy to add (just copy is_field and drop stuff)

Kevin Buzzard (Feb 18 2022 at 08:28):

Aargh on mobile, accidentally just deleted post saying "it's not a diamond, you do indeed have two ring structures, fix it with a mixin"

Damiano Testa (Feb 18 2022 at 08:29):

Kevin said:
So yeah you're right -- division_ring R puts a ring structure on R and normed_ring R puts a different ring structure on it (so it's not diamond). You'll have to use what I think they call a Prop-valued mixin.

Damiano Testa (Feb 18 2022 at 08:29):

(Kevin, I hope that you wanted to actually recover what you had said!)

Jireh Loreaux (Feb 18 2022 at 08:41):

I think there's a problem with this idea, namely, is_division_ring can't just be Prop-valued mixin because division_ring needs an inv and div, whereas rings don't have this. :sad:

Jireh Loreaux (Feb 18 2022 at 08:42):

(and yes, my rings are noncommutative, until they aren't via the isomorphism)

Damiano Testa (Feb 18 2022 at 08:43):

I have not looked at this much, so I might be wrong, but is_field also takes a ring and produces something with inverses. Does asserting the existence of a left/right inverse (without using the \inv notation, simply an element of the ring) not work for division_ring as well?

Jireh Loreaux (Feb 18 2022 at 08:43):

ah, good point, let me check out docs#is_field.to_field

Kevin Buzzard (Feb 18 2022 at 08:45):

It's noncomputable but that's where the data is added

Jireh Loreaux (Feb 18 2022 at 08:46):

If I truly cared about computability, I don't know how I could have ended up in functional analysis. :laughing:

Jireh Loreaux (Feb 18 2022 at 09:24):

docs#division_ring_of_is_unit_or_eq_zero

Jireh Loreaux (Feb 18 2022 at 09:38):

So, I guess I don't understand how to actually use this. If I have a ring, and I have a Prop-valued mixin for division ring, how do I conclude some group_with_zero property? Because if I use haveI to construct my division ring, then I'm just back where I started (with 2 ring structures), but without the division ring type class instance, how do I get Lean to recognize the group_with_zero instance so I can use is_unit_iff_ne_zero?

Anne Baanen (Feb 18 2022 at 09:40):

If you use letI, then the two instances should be definitionally equal

Anne Baanen (Feb 18 2022 at 09:41):

(have and haveI forget the definition of the new hypothesis, let and letI preserve it)

Jireh Loreaux (Feb 18 2022 at 09:41):

ah, of course, it's data. Stupid me.

Kevin Buzzard (Feb 18 2022 at 11:33):

This is a highly non-mathematical issue which took me some time to get used to! This even goes back to the definition of group -- we often write the definition as "a group is a set plus a multiplication plus some axioms" and the axioms imply "there exists a unique identity" so the mathematicians say "let's now call it 1" and I think that in ZFC there is no issue here but for Lean some magic has to occur to get the data from the prop, so instead of invoking magic all the time they just add 1 to the data in the definition -- and then we end up with both field and is_field etc etc. In some sense I'm surprised we don't have an is_group predicate on monoids -- perhaps the reason we don't is that in practice either the monoids we have are obviously not groups or obviously groups?

Eric Wieser (Feb 18 2022 at 11:39):

Since I don't see it mentioned here, another solution here is just "define normed_division_ring in the obvious way". Chances are we don't have it yet because no one needed it

Eric Wieser (Feb 18 2022 at 11:40):

One reason why is_field is useful is that it allows you express "this ring structure is not a field"; is_empty (field α) means something quite different to ¬is_field α, and only the latter really expresses something mathematically interesting.

Mario Carneiro (Feb 18 2022 at 12:26):

not to diminish the point, but is_empty (field α) (or better, nonempty (field α)) is slightly mathematically interesting: it's a cardinality constraint which I believe is true iff is either a prime power or an infinite cardinal

Mario Carneiro (Feb 18 2022 at 12:27):

I'm not sure we have that proved though (maybe we know the first part?)

Mario Carneiro (Feb 18 2022 at 12:28):

come to think of it, do we have the existence of prime power fields? A computable definition would be extra cool

Eric Rodriguez (Feb 18 2022 at 12:32):

docs#galois_field

Eric Rodriguez (Feb 18 2022 at 12:33):

seems to not be constructive

Mario Carneiro (Feb 18 2022 at 12:33):

(for the infinite case I think it's quite accessible from current mathlib: you use the fraction field of mv_polynomial α ℚ)

Eric Rodriguez (Feb 18 2022 at 14:11):

i've just finished the finite case:

import field_theory.finite.galois_field
import algebra.is_prime_pow
import data.equiv.transfer_instance

local notation `‖` x `‖` := fintype.card x

lemma nat.prime.is_prime_pow {p : } (hp : p.prime) : is_prime_pow p :=
(is_prime_pow_nat_iff p).mpr p, 1, hp, one_pos, pow_one p

example {α} [fintype α] : nonempty (field α)  is_prime_pow (fintype.card α) :=
begin
  split,
  swap,
  { rintros p, n, hp, hn, ⟩,
    haveI := fact.mk (nat.prime_iff.mpr hp),
    exact ⟨(fintype.equiv_of_card_eq ((galois_field.card p n hn.ne').trans )).symm.field },
  rintro h⟩,
  casesI char_p.exists α with p _,
  haveI hp := fact.mk (char_p.char_is_prime α p),
  let b := is_noetherian.finset_basis (zmod p) α,
  rw [module.card_fintype b, zmod.card, is_prime_pow_pow_iff],
  exact hp.1.is_prime_pow,
  rw finite_dimensional.finrank_eq_card_basis b,
  exact finite_dimensional.finrank_pos.ne'
end

I don't see the equiv α ≃ fraction_ring (mv_polynomial α ℚ); how do you make it?

Eric Rodriguez (Feb 18 2022 at 14:12):

sorry, we should probably move this to another thread

Alex J. Best (Feb 18 2022 at 14:25):

you probably need some facts about cardinal of mv_polynomial (file#data/mv_polynomial/cardinal) and fraction_ring (not sure we have those)

Alex J. Best (Feb 18 2022 at 14:27):

I guess using that the localization map is surjective it shouldn't be too hard to get those?

Kevin Buzzard (Feb 18 2022 at 14:34):

I guess you need facts about cardinality of finsupp too. Would be a nice Friday afternoon exercise!

Jireh Loreaux (Feb 18 2022 at 14:40):

so do we want is_division_ring as a mix in, or do we just wanted to define a normed_division_ring? Tossing around the hypothesis (h : ∀ b : A, is_unit b ∨ b = 0) for everything related to Gelfand-Mazur is just silly. See here for the mixin version (you must be on the j-loreaux/spectrum-nonempty branch for the second half of this to compile):

Should I PR the mixin or define normed_division_algebra, or both?

Kevin Buzzard (Feb 18 2022 at 14:41):

People who understand this sort of thing now start talking about quadratic growth of typeclass inference search or something; hopefully someone who understands the internals will chime in.

Yaël Dillies (Feb 18 2022 at 15:10):

The pattern here is to define normed_division_ring. The question of whether it should be a mixin belongs to another discussion as mathlib already has weaker and stronger typeclasses which are not mixins, namely normed_ring and normed_field.

Kevin Buzzard (Feb 18 2022 at 15:29):

Oh! If they're there then it's probably case closed: we seem to want a new object normed_division_ring. Is it still OK to use old_structure_cmd or should it extend one structure and then add the fields for the other?

Yaël Dillies (Feb 18 2022 at 16:08):

Oh, I think we don't care much about that. I suspect all the other ones use old_structure_cmd happily.

Gabriel Ebner (Feb 18 2022 at 16:17):

The whole normed_* hierarchy doesn't use old_structure_cmd (but it should).

Gabriel Ebner (Feb 18 2022 at 16:18):

(Slightly related: I'm currently working on adding a typeclass for nat.cast&int.cast and had to refactor normed_* to old_structure_cmd. I should probably extract that to a separate PR.)

Yaël Dillies (Feb 18 2022 at 16:38):

I don't understand. Are you using old structures more? I thought the plan was to get rid of them?

Gabriel Ebner (Feb 18 2022 at 16:48):

The plan is to use them again, since Lean 4 now uses a mixture of old/new structures (i.e., new whenever possible, old as an automatic fallback). Looking over normed_*, there's lots of ugly hacks that can be removed by switching to old structures.

Yaël Dillies (Feb 18 2022 at 16:49):

Oh, that's good to know, since I've been going round the library to remove old structures.

Yaël Dillies (Feb 18 2022 at 16:49):

What I'm most complaining about the current situation is that new structures really could be as easy to declare as old ones, but for some reason they are not.

Yaël Dillies (Feb 18 2022 at 16:50):

It seems to be that this is an implementation detail that leaked through.

Yaël Dillies (Feb 18 2022 at 16:52):

What I want is to be able to declare new structures the same way as old ones, namely you put as many extends clauses as you want, with conflicting fields if you want.

Yaël Dillies (Feb 18 2022 at 16:54):

And it would generate the structure in the new style, namely the first parent is taken as a field and every parent that wants to add a conflicting field is blown up and we instead get a separate instance/projection.

Gabriel Ebner (Feb 18 2022 at 16:57):

That's what's happening in Lean 4.

Yaël Dillies (Feb 18 2022 at 16:57):

That might not always do what you want, namely if foo has a and b, bar has b and c, baz has c and d, then

structure qux extends foo, bar, baz

would generate

structure qux :=
(to_foo : foo)
(c : ...)
(d : ...)

def qux.to_bar (x : qux) : bar := { ..x}

def qux.to_baz (x : qux) : baz := { ..x}

instead of the more optimal

structure qux :=
(to_foo : foo)
(to_baz : baz)

def qux.to_bar (x : qux) : bar := { ..x}

Yaël Dillies (Feb 18 2022 at 16:58):

And this gets worse with bigger structures which have more complicated conflicting fields, but arguably rearranging the clauses would solve what it can.

Yaël Dillies (Feb 18 2022 at 16:59):

Is that possible, Gabriel, or am I daydreaming?

Gabriel Ebner (Feb 18 2022 at 17:00):

It works if you write extends Foo, Baz, Bar.

Yaël Dillies (Feb 18 2022 at 17:00):

Sorry, that was my point :upside_down:

Yaël Dillies (Feb 18 2022 at 17:01):

But it doesn't currently generate qux.to_bar automatically, right?

Gabriel Ebner (Feb 18 2022 at 17:07):

If you write extends Foo, Baz, Bar it does create a projection to Bar. I can't vouch for the name though.

Yaël Dillies (Feb 18 2022 at 17:09):

In Lean 3 too?

Gabriel Ebner (Feb 18 2022 at 17:14):

No, but that's only a temporary issue.

Jireh Loreaux (Feb 18 2022 at 19:55):

#12132: introduces division rings. For the moment I just copied the stuff that worked (i.e., didn't use commutativity) from normed fields. Should I in another PR refactor to only use the normed_division_ring versions and rely on type class inference for the rest? Obviously that could touch a lot of files, and it's not that much code duplication right now anyway.

Yaël Dillies (Feb 18 2022 at 20:06):

docs#normed_field.norm_mul, docs#norm_mul

Yaël Dillies (Feb 18 2022 at 20:07):

Hmm... that's weird. Why is it not just called norm_mul?

Yaël Dillies (Feb 18 2022 at 20:08):

In any case I think you should replace the lemmas right away. This really fits with the rest of the PR.

Jireh Loreaux (Feb 18 2022 at 21:17):

norm_mul for fields and division rings is an equality, not an inequality like for (semi)normed rings. That's the reason for the difference.

Eric Wieser (Feb 18 2022 at 21:19):

Probably we should call the inequality version norm_mul_le

Eric Wieser (Feb 18 2022 at 21:19):

If that's more work though, we could have norm_mul' for the division_ring / field versions

Jireh Loreaux (Feb 18 2022 at 21:20):

I'm just worried about touching 30 or 40 files in one PR. The amount of work is not a huge deal, as long as it's feasible.

Jireh Loreaux (Feb 18 2022 at 21:24):

grepping for normed_field.norm_mul alone hit 13 different files. I'm willing to do it, but someone has to explain to me how to go about it without making my life miserable.

Jireh Loreaux (Feb 18 2022 at 21:25):

Eric Wieser said:

Probably we should call the inequality version norm_mul_le

Interestingly, the API for it includes the le, it's just the structure projection that doesn't have it.

Eric Wieser (Feb 18 2022 at 21:31):

Well nothing should be using the structure projection anyway

Eric Wieser (Feb 18 2022 at 21:32):

docs#norm_mul_le exists then?

Eric Wieser (Feb 18 2022 at 21:32):

Does docs#norm_mul too?

Eric Wieser (Feb 18 2022 at 21:33):

Alright, easy - rename normed_field.norm_mul' to norm_mul (by adding an API lemma to unwrap it) and you're done

Jireh Loreaux (Feb 19 2022 at 22:34):

Sorry, @Eric Wieser, I think we were talking past each other. Here is the situation:

  1. normed_ring has a norm_mul structure projection (which is actually an inequality), and an API wrapper norm_mul_le (root namespace)
  2. normed_field has a norm_mul' structure projection (which is an equality), and a namespaced API wrapper normed_field.norm_mul

I think @Yaël Dillies was asking why the latter is namespaced, but the former isn't. When I followed up with the (in)equality comment, I had thought the namespacing was required because the ring version was called norm_mul, but it isn't, that's only the name of the structure projection.

My worry about deleting all these normed field lemmas (and only keeping the division ring versions) is that they're all in the normed_field namespace, and of course the division ring versions don't want to be in that namespace (right? I'm not crazy). So should I really delete them, and then go around into all the files that broke and add an open normed_division_ring? This was my concern about touching 30 or 40 files.

Yaël Dillies (Feb 19 2022 at 22:39):

The projection from normed_ring really should be called normed_ring.norm_mul_le. Changing it shouldn't be too hard as it's supposedly called exactly once (to prove norm_mul_le). The projection from normed_field should be called normed_field.norm_mul and the API lemma should be called norm_mul (either by exporting it or declaring it separately). Almost no lemma should be in the normed_field namespace.

Yaël Dillies (Feb 19 2022 at 22:40):

Similarly, no lemma should be in the normed_division_ring namespace.

Jireh Loreaux (Feb 19 2022 at 22:42):

That makes sense to me, but do we need someone (@Yury G. Kudryashov because git blame) to weigh in about why they were originally put into the normed_field namespace?

Yury G. Kudryashov (Feb 19 2022 at 22:44):

normed_field was there long before me.

Yaël Dillies (Feb 19 2022 at 22:46):

I suspect this namespace is an historical accident.

Yury G. Kudryashov (Feb 19 2022 at 22:46):

I agree that it should be in the root namespace.

Jireh Loreaux (Feb 19 2022 at 22:49):

okay, I'll change it.

Jireh Loreaux (Feb 19 2022 at 23:09):

I think we have a diamond problem. A normed field is both a normed division ring and a normed commutative ring.

Jireh Loreaux (Feb 19 2022 at 23:14):

Sorry, I didn't explain enough: both of these have instances of normed group.

Yaël Dillies (Feb 19 2022 at 23:14):

But are they not defeq?

Yaël Dillies (Feb 19 2022 at 23:15):

There are diamonds everywhere. The real trouble is non-defeq diamonds.

Jireh Loreaux (Feb 19 2022 at 23:16):

well, I think not because I was getting problems with the lemma norm_norm which to me looked like a diamond, but perhaps I misinterpreted the reason. Let me see if I can get the file back to that state and post the error.

Yaël Dillies (Feb 19 2022 at 23:18):

Don't hesitate to post the code either here or on the branch. I'll be happy to diagnose.

Jireh Loreaux (Feb 19 2022 at 23:34):

nevermind, I think I'm an idiot. There was a namespace normed_field and a section normed_field and I think I deleted the wrong corresponding end normed_field which caused there to be a [normed_field α] and a [nondiscrete_normed_field α] at the same time, hence two norms.

Jireh Loreaux (Feb 19 2022 at 23:40):

Wait, no, it's back. I don't understand. Here's the current file. Line 462: basic.lean

Jireh Loreaux (Feb 19 2022 at 23:41):

When I instantiate the metavariable from the hole with x, I get this error:

type mismatch at application
  real.norm_of_nonneg (norm_nonneg x)
term
  norm_nonneg x
has type
  @has_le.le real real.has_le 0 (@has_norm.norm α (@semi_normed_group.to_has_norm α _inst_2) x)
but is expected to have type
  @has_le.le real real.has_le 0
    (@has_norm.norm α (@normed_field.to_has_norm α (@nondiscrete_normed_field.to_normed_field α _inst_1)) x)

Jireh Loreaux (Feb 19 2022 at 23:49):

oh wait, it's seeing a seminormed group from the declaration and a nondiscrete normed field from earlier

Jireh Loreaux (Feb 19 2022 at 23:54):

okay, I made this file happy, thanks.

Jireh Loreaux (Feb 20 2022 at 04:05):

Can someone diagnose why my changes in #12132 broke the usage of ac_refl on line 975 of analysis/asymptotics/asymtopotics.lean? Replacing it with ring solves the goal. My guess is something to do with instance priority for normed_division_ring and it is getting stuck there and failing to recognize commutativity, but I'm not sure.

Eric Wieser (Feb 20 2022 at 10:34):

Perhaps it would be best to split this into a "rename the normed_field stuff" PR followed by the division_ring stuff - that would make it easier to isolate the problem

Jireh Loreaux (Feb 20 2022 at 14:07):

#12163: moves normed field lemmas into root namespace. We'll see how CI goes.

Jireh Loreaux (Feb 20 2022 at 15:49):

Success

Jireh Loreaux (Feb 22 2022 at 03:45):

Anyone want to try to understand why ac_refl fails in commit 94b0b05 on branch j-loreaux/normed-division-ring (file analysis/asymptotics/asymptotics line 975)? I just pushed another commit to workaround it, but it might be good to understand why it's not working. I don't have the knowledge to know where to start.


Last updated: Dec 20 2023 at 11:08 UTC