ring.inverse is continuous

Stream: Is there code for X?

[Eric Wieser]

Is this true? Do we have it somewhere with stronger assumptions?

example {R} [monoid_with_zero R] [topological_space R] [has_continuous_mul R] :
  continuous_on (λ A : R, ring.inverse A) {A : R | is_unit A} := by library_search

[Heather Macbeth]

It's true for the group of units of a complete normed ring.

[Patrick Massot]

docs#normed_ring.inverse_continuous_at

[Heather Macbeth]

Note also that units R is given a topology in docs#units.topological_space, but it's not always the same as the subspace topology from R

[Heather Macbeth]

(Instead, it's precisely the topology which also makes inversion continuous.)

[Heather Macbeth]

docs#units.topological_group

[Eric Wieser]

I guess it's also true in a topological field too?

[Heather Macbeth]

It would be worth stating both the ring.inverse lemma and the fact is_open_map (coe : units k → k) for a topological field.

[Heather Macbeth]

By analogy with docs#normed_ring.inverse_continuous_at and docs#units.is_open_map_coe

[Eric Wieser]

I ask because I was trying to show that the matrix inverse is continuous around the units

[Eric Wieser]

And I'm not sure what assumptions I should be taking

[Eric Wieser]

It sounds like I need multiple copies of the lemma for the topological_field vs normed_ring cases?

[Heather Macbeth]

You can apply it to the normed ring of square matrices over a normed field directly.

[Eric Wieser]

Matrices aren't (yet) a normed ring

[Eric Wieser]

(in mathlib)

[Heather Macbeth]

I think establishing that instance will be by far the fastest way to prove that fact.

[Eric Wieser]

I'm already 90% of the way there

[Eric Wieser]

It's the pesky ring.inverse A.det that's left

[Heather Macbeth]

But the abstract proof is also the "right" one -- eg it's what I've used before to prove that the "inversion" map on endomorphisms is continuous.

[Eric Wieser]

Besides, going this way fills out missing API

[Heather Macbeth]

Why do you need this? Is it maybe a fact about endomorphisms in disguise?

[Eric Wieser]

Oh, I'm sure it is a statement about endomorphisms in disguise

[Eric Wieser]

I was trying to state https://en.wikipedia.org/wiki/Jacobi%27s_formula, and just filling out various API

[Heather Macbeth]

Yes, this is a fact about endomorphisms!

[Eric Wieser]

Last time I tried that translation, I got stumped by trying to translate matrix.adjugate to endomorphisms

[Eric Wieser]

Eric Wieser said:

I'm already 90% of the way there

#13009 is the PR.

[Heather Macbeth]

Eric Wieser said:

Last time I tried that translation, I got stumped by trying to translate matrix.adjugate to endomorphisms

If $f : E \to E$ is your endomorphism, and $E$ has dimension $n$, then the adjugate is the induced map between exterior powers $f^{\wedge (n-1)}:E^{\wedge (n-1)}\to E^{\wedge (n-1)}$.

[Eric Wieser]

Maybe I need to pick back up my tensor powers PR that got stalled on fin nonsense

[Eric Wieser]

Although I guess (exterior_algebra.\io R M).range ^ (n - 1) could work there

[Heather Macbeth]

@Eric Wieser

import analysis.normed_space.units
import analysis.normed_space.pi_Lp

noncomputable theory
open_locale nnreal

section
variables (𝕜 : Type*) [uniform_space 𝕜]
variables (n : Type*) [fintype n] [decidable_eq n] (m : Type*) [fintype m] [decidable_eq m]

-- should add this instance
instance : uniform_space (matrix n m 𝕜) := Pi.uniform_space (λ i, m → 𝕜)

instance [complete_space 𝕜] : complete_space (matrix n m 𝕜) := Pi.complete (λ i, m → 𝕜)

end

variables (𝕜 : Type*) [normed_field 𝕜]
variables (n : Type*) [fintype n] [decidable_eq n] (m : Type*) [fintype m] [decidable_eq m]

-- check that `L∞-L∞` normed group definition matches the standard uniform space instance.
example : (matrix.normed_group : normed_group (matrix n m 𝕜)).to_uniform_space
  = matrix.uniform_space 𝕜 n m :=
rfl

/-- The `L1-L∞` norm on matrices. -/
def matrix.normed_group' : normed_group (matrix n m 𝕜) :=
@pi.normed_group n (λ i, pi_Lp 1 (λ j, 𝕜)) _ (λ i, pi_Lp.normed_group 1 (λ j, 𝕜))

-- check that `L1-L∞` normed group definition matches the standard uniform space instance.
example : (matrix.normed_group' 𝕜 n m).to_uniform_space = matrix.uniform_space 𝕜 n m := rfl

/-- Matrices are a normed ring wrt the `L1-to-L∞` norm. -/
def matrix.normed_ring : normed_ring (matrix n n 𝕜) :=
{ norm_mul := sorry,
  .. matrix.ring,
  .. matrix.normed_group' 𝕜 n n }

variables [complete_space 𝕜]

example (A : units (matrix n n 𝕜)) : continuous_at ring.inverse (A : matrix n n 𝕜) :=
begin
  convert @normed_ring.inverse_continuous_at (matrix n n 𝕜) (matrix.normed_ring 𝕜 n) _ A,
  -- apparently unrelated diamond:
  -- `pi.monoid_with_zero = semiring.to_monoid_with_zero (matrix n n 𝕜)`
end

[Eric Wieser]

That's a real diamond, it's telling you that you've mixed up elementwise and matrix multiplication somehow

[Eric Wieser]

I can't see where though

[Heather Macbeth]

Ah, indeed. This works:

example (A : units (matrix n n 𝕜)) : continuous_at ring.inverse (id A : matrix n n 𝕜) :=
@normed_ring.inverse_continuous_at (matrix n n 𝕜) (matrix.normed_ring 𝕜 n) _ A

[Heather Macbeth]

The cast from units (matrix n n 𝕜) to matrix n n 𝕜 went too far and turned it just to n → n → 𝕜.

[Eric Wieser]

That coercion behavior has been causing trouble in some of the modular forms PRs too

[Eric Wieser]

I think lean inserts a coe_fn too eagerly?

[Eric Wieser]

@Heather Macbeth, is there any reason to pick the L1-to-L∞ norm over say the operator norm or the frobenius norm? Do you have a feel for which will be easiest to show submulltiplicity of?

[Eric Wieser]

Answer: Yes, the L1-to-L∞ norm imposes much weaker typeclass requirements than the frobenius norm!

I've PR'd a proof of your norm_mul := sorry in #13518