mul_inv_rev for ring_hom.inverse

Stream: Is there code for X?

[Eric Wieser]

I couldn't find this statement; is it true?

lemma ring.mul_inverse_rev {R} [ring R] (a b : R) :
  ring.inverse (a * b) = ring.inverse b * ring.inverse a :=

I can work out a proof for comm_ring, but can't find any obvious lemmas to get it for ring.

[Eric Wieser]

I get stuck at:

ha: ¬is_unit a
hb: ¬is_unit b
h: is_unit (a * b)
⊢ false

which I suspect isn't provable

[Kevin Buzzard]

Yeah I think you're right, it's not provable.

[Kevin Buzzard]

Let M be ℕ → ℤ with pointwise addition, and let R be M→+ M with pointwise addition and composition as multiplication (so R is the endomorphism ring of the abelian group M). If f : M then define a.f : M by $a.f(n)=f(n+1)$ and b.f : Mby $b.f(n+1)=f(n)$ and $b.f(0)=0$. I claim that neither a nor b are units in $R$ because if $u$ is a unit of $R$ then the induced map $M\to M$ must be a bijection (because it has a two-sided inverse). However $b$ is not surjective (because $bf(0)=0$) and $a$ is not injective (because $a$ sends the function mapping $0$ to $1$ and everything else to $0$, to zero). However the composite $a\circ b$ is the identity function so in particular is a unit.

[Alex J. Best]

I think this should be true in a Dedekind finite ring (one where a * b = 1 -> b * a = 1), which is the subject of my oldest still open PR #1822, I did start cleaning it up to get it merged recently, but I can't find the branch now lol. The upshot of that PR is that many nice properties (e.g Noetherian imply Dedekind finite)

EDIT: refreshed branch is at https://github.com/leanprover-community/mathlib/tree/alexjbest/dedekind-finite

[Kevin Buzzard]

My example is basically the simplest ring I know with elements a,b such that ab=1 and ba!=1

[Kevin Buzzard]

One can make a "universal" such ring, i.e. look at polynomials in two non-commuting variables A and B, and then quotient out by the bi-ideal generated by AB-1 to get some quotient ring over which I have very little control. But for this quotient ring (the "universal ring") I don't really see how to prove that BA!=1. The proof I know involves writing down a concrete ring for which the equality doesn't hold and noting that there will be a map from the universal ring to the concrete ring so BA can't have been 1 in the universal ring because then it would have to be 1 in the concrete ring. But then you may as well just use the concrete ring anyway.

[Eric Wieser]

I pr'd the easy version in #9863

[Eric Wieser]

Does this version look true?

lemma ring.inverse_mul_self {R} [semiring R] (r : R) :
  ring.inverse (r * r) = ring.inverse r * ring.inverse r :=
begin
  by_cases hr : is_unit r,
  { obtain ⟨u, rfl⟩ := hr,
    rw [←units.coe_mul, ring.inverse_unit, ring.inverse_unit, ←units.coe_mul, mul_inv_rev], },
  rw [ring.inverse_non_unit _ hr, zero_mul],
  apply ring.inverse_non_unit,
  intro hrr,
  apply hr,
  sorry
end

It feels like maybe commutativity isn't relevant if the two argument are the same

[Reid Barton]

Yes, because if $r^2$ has an inverse (say $w$) then $r$ has a left inverse $wr$ and a right inverse $rw$, which then have to be equal

[Eric Wieser]

Any golfing ideas?

lemma is_unit_mul_self_iff {M} [monoid M] {m : M} : is_unit (m * m) ↔ is_unit m :=
begin
  refine ⟨λ h, _, λ h, h.mul h⟩,
  obtain ⟨u, hu⟩ := h,
  have same : ↑u⁻¹ * m = m * ↑u⁻¹,
  { rw [units.inv_mul_eq_iff_eq_mul, ←mul_assoc, units.eq_mul_inv_iff_mul_eq, hu, mul_assoc], },
  refine ⟨⟨m, ↑u⁻¹ * m, _, _⟩, rfl⟩,
  { rw [same, ←mul_assoc, ←hu, units.mul_inv], },
  { rw [mul_assoc, ←hu, units.inv_mul], },
end

lemma ring.inverse_mul_self {M₀} [monoid_with_zero M₀] (r : M₀) :
  ring.inverse (r * r) = ring.inverse r * ring.inverse r :=
begin
  by_cases h : is_unit r,
  { obtain ⟨u, rfl⟩ := h,
    rw [←units.coe_mul, ring.inverse_unit, ring.inverse_unit, ←units.coe_mul, mul_inv_rev], },
  { rw [ring.inverse_non_unit _ h, zero_mul,
        ring.inverse_non_unit _ (mt is_unit_mul_self_iff.mp h)], }
end

[Eric Wieser]

Ah, we have docs#is_unit_pos_pow_iff but it's not general enough

[Eric Wieser]

#10041

[Yakov Pechersky]

Thanks for generalizing it, I hadn't been able to use the units api to juggle the terms when I tried it.

[Yury G. Kudryashov]

lemma commute.is_unit_mul {M : Type*} [monoid M] {a b : M} (h : commute a b) :
  is_unit (a * b) ↔ is_unit a ∧ is_unit b :=
begin
  refine ⟨_, λ H, H.1.mul H.2⟩,
  rintro ⟨u, hu⟩,
  have : b * ↑u⁻¹ * a = 1,
  { have := (commute.refl _).mul_right h, rw ← hu at this,
    rw [← this.units_inv_right.right_comm, ← h.eq, ← hu, u.mul_inv] },
  split,
  { refine ⟨⟨a, b * ↑u⁻¹, _, this⟩, rfl⟩,
    rw [← mul_assoc, ← hu, u.mul_inv] },
  { refine ⟨⟨b, ↑u⁻¹ * a, _, _⟩, rfl⟩,
    { rwa ← mul_assoc },
    { rw [mul_assoc, ← hu, u.inv_mul] } }
end

[Yury G. Kudryashov]

You can use this to get is_unit_mul_self as well as is_unit_pow in a non-commutative monoid.

[Yury G. Kudryashov]

#10042

[Eric Wieser]

Nice! Can you use your PR to generalize is_unit_pos_pow_iff too so that mine can be closed?

[Yury G. Kudryashov]

Done.