Compare inverses

Stream: Is there code for X?

[Antoine Chambert-Loir]

if $A$ is an $R$-algebra, it is not true that the image in $A$ of Ring.inverse r, for $r \in R$, coincides with Ring.inverse (r : A) (because $r$ might be noninverstible in $A$ while its image in $R$ is invertible), but this holds if $R=\mathbf Q$.
However, the following proof seems fairly complicated.

import Mathlib.Algebra.Algebra.Basic

example {A : Type _} [CommRing A] [Algebra ℚ A] (n : ℕ) (a : A) :
  Ring.inverse (n : ℚ) • a = Ring.inverse (n : A) * a := by
  cases' Nat.eq_zero_or_pos n with hn hn
  . simp only [hn, Nat.cast_zero, isUnit_zero_iff, not_false_eq_true, Ring.inverse_non_unit, zero_smul,
    Ring.inverse_zero, zero_mul]
  . suffices hn' : IsUnit (n : ℚ)
    simp only [Algebra.smul_def, ← map_natCast (algebraMap ℚ A)]
    apply symm
    rw [Ring.inverse_mul_eq_iff_eq_mul, ← mul_assoc]
    apply symm
    convert @one_mul A _ _
    simp only [← map_mul, ← map_one (algebraMap ℚ A)]
    apply congr_arg
    apply symm
    rw [Ring.eq_mul_inverse_iff_mul_eq, one_mul]
    . exact hn'
    . apply RingHom.isUnit_map
      exact hn'
    rw [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero]
    exact Nat.ne_of_gt hn

[Anatole Dedecker]

This works for any field right? The proof being "either $r$ is zero, then it works by junk values, or $r$ is invertible in $R$, hence in $A$ with the same inverse. Am I missing something obvious?

[Anatole Dedecker]

Sorry that doesn't answer your question at all :sweat_smile: My first guess would be to try using docs#Units.map, but maybe switching between the different inverse APIs will make it hard.

[Anatole Dedecker]

import Mathlib.Algebra.Algebra.Basic

open Ring algebraMap

lemma foo {R S F : Type _} [GroupWithZero R] [MonoidWithZero S] [MonoidWithZeroHomClass F R S]
    (f : F) (x : R) :
    Ring.inverse (f x) = f (Ring.inverse x) := by
  rcases GroupWithZero.eq_zero_or_unit x with (rfl|⟨u, rfl⟩)
  · rw [inverse_zero, map_zero, inverse_zero]
  · change inverse ((f : R →* S) u) = (f : R →* S) (inverse u)
    rw [← Units.coe_map, inverse_unit, ← map_inv, Units.coe_map, inverse_unit]

example {R A : Type _} [Field R] [CommRing A] [Algebra R A] (r : R) (a : A) :
    Ring.inverse r • a = Ring.inverse (r : A) * a := by
  rw [Algebra.smul_def, ← foo (algebraMap R A)]
  rfl

[Eric Rodriguez]

example [CommRing A] [CommRing K] [Algebra K A] (x : K) :
  Ring.inverse (algebraMap K A x) = algebraMap K A (Ring.inverse x) := by
cases' em (IsUnit x) with h h
· lift x to Kˣ using h
  have : ((algebraMap K A).toMonoidHom : K → A) = algebraMap K A := rfl
  simp only [not_true, Ring.inverse_unit]
  rw [←this, ←Units.coe_map_inv (algebraMap K A).toMonoidHom, ←Ring.inverse_unit]
  simp
· sorry

I have this skeleton of something that may be more useful generally

[Eric Rodriguez]

but the right condition so that the sorry holds I don't know

[Eric Rodriguez]

the API here doesn't seem to be great

[Eric Wieser]

It's annoying that Ring.inverse_unit doesn't take is_unit

[Eric Rodriguez]

also that Units.map needs monoidhom instead of monoidhomclass

[Eric Wieser]

I think that might have been deliberate on my part

[Eric Rodriguez]

why?

[Anatole Dedecker]

I don't think this can work with so little assumptions on K, because as Antoine said it doesn't work if x is not invertible in K but is invertible in A. I'd guess my version is essentially the more general you can get (EDIT: without extra assumption like what Antoine describes below).

[Antoine Chambert-Loir]

The most general version would be that of a $R$ algebra $A$ such that an element of $R$ is a unit in $A$ if and only if it is already a unit in $R$. These algebras have a name, but I don't remember it.

[Eric Wieser]

Eric, here's a slightly longer version of yours:

lemma map_inverse {R S F : Type _} [MonoidWithZero R] [MonoidWithZero S] [MonoidWithZeroHomClass F R S]
    (f : F) (x : R) :
    f (Ring.inverse x) = Ring.inverse (f x) := by
  rcases em (IsUnit x) with (⟨u, rfl⟩|hu)
  · have : ((f : R →* S) : R → S) = f := rfl
    simp only [not_true, Ring.inverse_unit]
    rw [←this, ←Units.coe_map_inv (f : R →* S), ←Ring.inverse_unit]
    simp
  · rw [inverse_non_unit _ hu, map_zero, inverse_non_unit]
    intro h
    apply hu; clear hu
    sorry -- `h: IsUnit (↑f x) ⊢ IsUnit x`

[Eric Wieser]

Eric Rodriguez said:

why?

Something to do with the fact that you still end up with a MonoidHom anyway; it feels a bit like deciding you're going to generalize the arguments to MonoidHom.comp.

[Anatole Dedecker]

Good luck proving that last sorry :sweat_smile:

[Eric Wieser]

docs#ExteriorAlgebra.isUnit_algebraMap shows one example of when it's true outside GroupWithZero...

[Anatole Dedecker]

Yes, but I don't think we have any way to state it generally right now

[Eric Rodriguez]

Eric Wieser said:

Eric Rodriguez said:

why?

Something to do with the fact that you still end up with a MonoidHom anyway; it feels a bit like deciding you're going to generalize the arguments to MonoidHom.comp.

the issue with this is that it now forces you to work with double coercions and it starts being ugly; even if the output isn't polymorphic (and it can't be anyways) it's nice that the input is

[Kevin Buzzard]

Anatole Dedecker said:

I don't think this can work with so little assumptions on K, because as Antoine said it doesn't work if x is not invertible in K but is invertible in A. I'd guess my version is essentially the more general you can get (EDIT: without extra assumption like what Antoine describes below).

If it's any help, one way to spell "if f(x) is a unit then x is a unit" in mathlib is IsLocalRingHom f.

[Antoine Chambert-Loir]

I had never seen the terminology of a local homomorphism of rings outside of the context of local rings, but this makes sense. For categories, a functor reflecting isomorphisms is called conservative.

[Eric Rodriguez]

docs#LocalRing.surjective_units_map_of_local_ringHom

[Eric Rodriguez]

Weird name...

[Eric Rodriguez]

But I don't think there's anything there about this, I do think this could be added to that API

[Kevin Buzzard]

Antoine Chambert-Loir said:

I had never seen the terminology of a local homomorphism of rings outside of the context of local rings, but this makes sense. For categories, a functor reflecting isomorphisms is called conservative.

yes this was funny: the point is reflecting units makes sense even if the rings aren't local. I asked de Jong about it and he suggested that a better definition (in the sense that it might be a more useful concept in the non-local case) was "Spec(f) sends closed points to closed points, and the image of Spec(f) contains all closed points" (which implies that f reflects units) but we took the simpler route.

[Kevin Buzzard]

Here's the route via IsLocalRingHom: I had to bash it out becuse it's funny :-)

import Mathlib.Algebra.Algebra.Basic
import Mathlib.RingTheory.Ideal.LocalRing

open Ring algebraMap

-- missing?
lemma Ring.inverse_unit' {M₀ : Type _} [MonoidWithZero M₀] (x : M₀) (h : IsUnit x) :
  inverse x = ((h.unit⁻¹ : M₀ˣ) : M₀) := dif_pos h

lemma baz {R S : Type _} [Semiring R] [Semiring S] (f : R →+* S)
    [IsLocalRingHom f] (x : R) : Ring.inverse (f x) = f (Ring.inverse x) := by
  by_cases IsUnit (f x)
  · rw [inverse_unit' _ h, inverse_unit' _ (isUnit_of_map_unit f x h)]
    change _ = (f : R →* S) _
    rw [← Units.coe_map, map_inv]
    congr
    ext
    simp
  · simp [inverse_non_unit _ h, inverse_non_unit _ (mt (IsUnit.map f) h) ]

instance bar {R S : Type _} [Field R] [Ring S] [Nontrivial S]
    (f : R →+* S) : IsLocalRingHom f where
      map_nonunit a _ := by
        rcases eq_or_ne a 0 with (rfl | h)
        · simp_all
        · exact ⟨⟨a, a⁻¹, mul_inv_cancel h, inv_mul_cancel h⟩, rfl⟩

example {R A : Type _} [Field R] [CommRing A] [Algebra R A] (r : R) (a : A) :
    Ring.inverse r • a = Ring.inverse (r : A) * a := by
  by_cases Nontrivial A
  · rw [Algebra.smul_def, ← baz (algebraMap R A)]
    rfl
  · rw [not_nontrivial_iff_subsingleton] at h
    simp [h]

[Eric Rodriguez]

Eric Wieser said:

docs#ExteriorAlgebra.isUnit_algebraMap shows one example of when it's true outside GroupWithZero...

is this a local ring hom in Kevin's "stronger proper" sense?

[Eric Rodriguez]

I'm considering a refactor to condense all these lemmas together but I don't want to base this off what is arguably a "bad" definition

[Matthew Ballard]

Kevin can correct me but I think his definition is implicitly commutative

[Eric Rodriguez]

Oh, of course

[Kevin Buzzard]

The definition is in mathlib so we can just have a look :-)

[Kevin Buzzard]

docs#IsLocalRingHom

[Eric Rodriguez]

I meant your definition with Spec, Kevin, in case we want to refactor to de Jong's suggestion in the future

[Kevin Buzzard]

Oh yeah the Spec version is definitely commutative only but I'm not sure that we're ever going to change our definition (which allows noncommutative rings by the looks of things), which we're seeing show up in other situations anyway

[Adam Topaz]

Why isn't this definition made for monoids?

[Kevin Buzzard]

I don't see why it shouldn't be! The name is getting weirder and weirder but hey...

[Matthew Ballard]

It looks like it gets specialized to commutative things quickly

[Adam Topaz]

I think this is an actual thing people consider the context of monoids. I remember seeing some paper using this a few years ago in the context of stuff "under spec Z" in the sense of Toen-Vaquie.

[Kevin Buzzard]

IsLocalRingHom. Library note: "they don't have to be local, or rings." I don't even know why we're restricting to homomorphisms either :-)

[Matthew Ballard]

docs#isUnit_map_of_leftInverse is for monoids

[Matthew Ballard]

So some easy connections are lying around

[Jireh Loreaux]

Here's a (noncommutative!) example of IsLocalRingHom showing up with the current definition: the spectral permanence property for C⋆-algebras can be phrased as, "If S is a closed star subalgebra of a C⋆-algebra A, then IsLocalRingHom ((↑) : S → A)." This phrasing doesn't exist in mathlib currently, but it could with about 10 lines of work,

[Jireh Loreaux]

If IsLocalRingHom were stated for MonoidHomClass instead that might be convenient.

[Eric Wieser]

Isn't IsLocalRingHom already true for algebra_map R (exterior_algebra R M)?

[Matthew Ballard]

That is mildly noncommutative :stuck_out_tongue_wink:

[Eric Wieser]

IsLocalRingHom is defined without assuming commutativity though

[Matthew Ballard]

Yes

[Matthew Ballard]

Eric Wieser said:

Isn't IsLocalRingHom already true for algebra_map R (exterior_algebra R M)?

Sorry, I interpreted this as "we already have a noncommutative example"

[Eric Wieser]

Ah, my mistake. That was indeed what I meant to mean!

[Jireh Loreaux]

Sorry, my example wasn't meant to be the only noncommutative one, just another and I wanted to emphasize that fact since there was talk of a commutative-only definition.

[Eric Rodriguez]

#6045 makes a start on this

[Eric Rodriguez]

[I will tag it with proper stuff when we have refactor tags in mathlib4!]

[Eric Rodriguez]

#6045 is now ready for a first round of reviews :)