normed_division_ring

Stream: general

[Jireh Loreaux]

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

import analysis.normed_space.basic

variables {R : Type*} [division_ring R] [normed_ring R]

lemma problem (r : R) (h : r ≠ 0) : is_unit r :=
(@is_unit_iff_ne_zero R _ r).mpr h

/-
type mismatch at application
  is_unit_iff_ne_zero.mpr h
term
  h
has type
  r ≠ 0
but is expected to have type
  r ≠ 0
Additional information:
context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    is_unit_iff_ne_zero.mpr ?m_1
  has type
    @is_unit R
      (@monoid_with_zero.to_monoid R
         (@group_with_zero.to_monoid_with_zero R (@division_ring.to_group_with_zero R _inst_1)))
      r
  but is expected to have type
    @is_unit R (@ring.to_monoid R (@normed_ring.to_ring R _inst_2)) r
-/

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]

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

[Damiano Testa]

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]

(deleted)

[Kevin Buzzard]

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]

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]

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]

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

[Jireh Loreaux]

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]

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

[Damiano Testa]

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]

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

[Kevin Buzzard]

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

[Jireh Loreaux]

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

[Jireh Loreaux]

docs#division_ring_of_is_unit_or_eq_zero

[Jireh Loreaux]

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]

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

[Anne Baanen]

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

[Jireh Loreaux]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Eric Rodriguez]

docs#galois_field

[Eric Rodriguez]

seems to not be constructive

[Mario Carneiro]

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

[Eric Rodriguez]

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, hα⟩,
    haveI := fact.mk (nat.prime_iff.mpr hp),
    exact ⟨(fintype.equiv_of_card_eq ((galois_field.card p n hn.ne').trans hα)).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]

sorry, we should probably move this to another thread

[Alex J. Best]

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]

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

[Kevin Buzzard]

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

[Jireh Loreaux]

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):

import analysis.normed_space.spectrum

universe u

section division_ring -- goes in `algebra.field.basic`

open_locale classical

/-- A predicate to express that a ring is a division ring.
This is mainly useful because such a predicate does not contain data,
and can therefore be easily transported along ring isomorphisms.
Additionaly, this is useful when trying to prove that
a particular ring structure extends to a division ring. -/
structure is_division_ring (R : Type u) [ring R] : Prop :=
(exists_pair_ne : ∃ (x y : R), x ≠ y)
(mul_inv_cancel : ∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1)

/-- Transferring from division_ring to is_division_ring -/
lemma division_ring.to_is_division_ring (R : Type u) [division_ring R] : is_division_ring R :=
{ mul_inv_cancel := λ a ha, ⟨a⁻¹, division_ring.mul_inv_cancel ha⟩,
  ..‹division_ring R› }

/-- Transferring from is_division_ring to division_ring -/
noncomputable def is_division_ring.to_division_ring (R : Type u) [ring R] (h : is_division_ring R) :
  division_ring R :=
{ inv := λ a, if ha : a = 0 then 0 else classical.some (is_division_ring.mul_inv_cancel h ha),
  inv_zero := dif_pos rfl,
  mul_inv_cancel := λ a ha,
    begin
      convert classical.some_spec (is_division_ring.mul_inv_cancel h ha),
      exact dif_neg ha
    end,
  .. ‹ring R›, ..h }

end division_ring

section gelfand_mazur_isomorphism

variables {A : Type*} [normed_ring A] [normed_algebra ℂ A] [complete_space A] [nontrivial A]
[measurable_space A] [borel_space A] [topological_space.second_countable_topology A]

local notation `σ` := spectrum ℂ

open spectrum

/-- Choose an arbitrary element of the spectrum of each element in a nontrivial complex Banach
algebra. -/
noncomputable def spectrum.some (a : A) : ℂ :=
set.nonempty.some (spectrum.nonempty a)

lemma spectrum.some_spec (a : A) : spectrum.some a ∈ spectrum ℂ a :=
set.nonempty.some_mem (spectrum.nonempty a)

lemma spectrum.unique_mem (h : is_division_ring A) {a : A} {x y : ℂ}
  (hx : x ∈ σ a) (hy : y ∈ σ a) : x = y :=
begin
  letI := is_division_ring.to_division_ring A h,
  rw [mem_iff, not_iff_not.mpr is_unit_iff_ne_zero, not_not, sub_eq_iff_eq_add, zero_add] at hx hy,
  exact no_zero_smul_divisors.algebra_map_injective ℂ A (hy.symm ▸ hx),
end

lemma spectrum.unique_of_mem (h : is_division_ring A) {x : ℂ} {a b : A}
  (ha : x ∈ σ a) (hb : x ∈ σ b) : a = b :=
begin
  letI := is_division_ring.to_division_ring A h,
  rw [mem_iff, not_iff_not.mpr is_unit_iff_ne_zero, not_not, sub_eq_iff_eq_add, zero_add] at ha hb,
  exact ha ▸ hb,
end

lemma spectrum.exists_some_singleton (h : is_division_ring A) (a : A) :
  ∃ z, spectrum ℂ a = {z} :=
set.exists_eq_singleton_iff_nonempty_unique_mem.mpr
  ⟨spectrum.nonempty a, (λ x hx y hy, spectrum.unique_mem h hx hy)⟩

/-- **Gelfand-Mazur theorem**: A complex Banach division algebra is isomorphic to `ℂ`, registered
as an algebra equivalence. -/
@[simps]
noncomputable def alg_equiv.complex_complete_normed_division_ring
  (h : is_division_ring A) : ℂ ≃ₐ[ℂ] A :=
{ to_fun := algebra_map ℂ A,
  inv_fun := spectrum.some,
  left_inv := λ z, by simpa only [scalar_eq] using spectrum.some_spec ((algebra_map ℂ A) z),
  right_inv := λ a,
  begin
    letI := is_division_ring.to_division_ring A h,
    have h₁ := spectrum.some_spec (algebra_map ℂ A (spectrum.some a)),
    have h₂ := not_not.mp ((not_iff_not.mpr is_unit_iff_ne_zero).mp (mem_iff.mp h₁)),
    rw [sub_eq_iff_eq_add, zero_add] at h₂,
    rw [no_zero_smul_divisors.algebra_map_injective ℂ A h₂] at h₁,
    exact spectrum.unique_of_mem h h₁ (spectrum.some_spec a),
  end,
  map_mul' := (algebra_map ℂ A).map_mul,
  map_add' := (algebra_map ℂ A).map_add,
  commutes' := λ _, rfl }

end gelfand_mazur_isomorphism

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

[Kevin Buzzard]

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]

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]

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]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

(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]

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

[Gabriel Ebner]

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]

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

[Yaël Dillies]

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]

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

[Yaël Dillies]

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]

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]

That's what's happening in Lean 4.

[Yaël Dillies]

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]

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]

Is that possible, Gabriel, or am I daydreaming?

[Gabriel Ebner]

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

[Yaël Dillies]

Sorry, that was my point :upside_down:

[Yaël Dillies]

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

[Gabriel Ebner]

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]

In Lean 3 too?

[Gabriel Ebner]

No, but that's only a temporary issue.

[Jireh Loreaux]

#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]

docs#normed_field.norm_mul, docs#norm_mul

[Yaël Dillies]

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

[Yaël Dillies]

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

[Jireh Loreaux]

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]

Probably we should call the inequality version norm_mul_le

[Eric Wieser]

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

[Jireh Loreaux]

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]

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]

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]

Well nothing should be using the structure projection anyway

[Eric Wieser]

docs#norm_mul_le exists then?

[Eric Wieser]

Does docs#norm_mul too?

[Eric Wieser]

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

[Jireh Loreaux]

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]

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]

Similarly, no lemma should be in the normed_division_ring namespace.

[Jireh Loreaux]

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]

normed_field was there long before me.

[Yaël Dillies]

I suspect this namespace is an historical accident.

[Yury G. Kudryashov]

I agree that it should be in the root namespace.

[Jireh Loreaux]

okay, I'll change it.

[Jireh Loreaux]

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

[Jireh Loreaux]

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

[Yaël Dillies]

But are they not defeq?

[Yaël Dillies]

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

[Jireh Loreaux]

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]

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

[Jireh Loreaux]

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]

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

[Jireh Loreaux]

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]

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

[Jireh Loreaux]

okay, I made this file happy, thanks.

[Jireh Loreaux]

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]

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]

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

[Jireh Loreaux]

Success

[Jireh Loreaux]

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.