Failed to ext in AddMonoid.End ℤ ?

Stream: mathlib4

[Zhu]

Hi!
I'm writing a prove that the endomorphism ring of ℤ is isomorphic to ℤ.
Specifically, I'm aiming to set up an equivalence AddMonoid.End ℤ ≃+* ℤ where:

• toFun maps f : AddMonoid.End ℤ to f 1
• invFun maps an integer n to the endomorphism that sends each integer x to n * x.

I'm encountering a problem with proving left_inv in my code. The ext tactic fails to work as expected.
Here's the relevant code:

import Mathlib


abbrev zEnd := AddMonoid.End ℤ

lemma l_1 (f : AddMonoid.End ℤ) : ∀ n, f n = n * f 1 := by
  intro n
  let g : (ℤ →+ ℤ) := f
  have : g n = n * g 1 := by apply AddMonoidHom.apply_int
  exact this

instance : AddMonoid.End ℤ ≃+* ℤ where

  toFun f := f 1

  invFun n := {
      toFun := fun x => n * x
      map_zero' := by simp
      map_add' := by intros; ring }

  left_inv := by
    intro f
    simp
    simp [mul_comm, ← l_1 f]
    -- ext failed
    sorry

  right_inv := by
    intro n
    simp
    sorry

  map_mul' := by
    intro f g
    simp [l_1 f (g 1), mul_comm]

  map_add' := by
    intro f g
    simp
    rfl

Any insights into why ext isn't working in this context, or suggestions on alternative approaches for this proof, would be very helpful. Thanks!

[Zhu]

image.png
This is the goal of left_inv after simp.

[Adam Topaz]

does AddMonoid.End have an ext lemma?

[Adam Topaz]

you could apply AddMonoidHom.ext.

[Adam Topaz]

Also, using instance to define this equivalence is not the right approach. instance is used to define instances of type classes.

[Kevin Buzzard]

    unfold AddMonoid.End
    ext
    simp

also works for the first sorry.

[Kevin Buzzard]

Also, I note that the unfold approach is somehow more powerful than apply AddMonoidHom.ext because after unfolding, ext somehow knows that it suffices to check equality after evaluation at 1 whereas AddMonoidHom.ext still demands that you check equality at all inputs.

[Zhu]

Thanks for the help! I’ve updated the code based on your suggestions, and it’s working now. :grinning:

import Mathlib


abbrev zEnd := AddMonoid.End ℤ

lemma l_1 (f : AddMonoid.End ℤ) : ∀ n, f n = n * f 1 := by
  intro n
  let g : (ℤ →+ ℤ) := f
  have : g n = n * g 1 := by apply AddMonoidHom.apply_int
  exact this

example : AddMonoid.End ℤ ≃+* ℤ where

  toFun f := f 1

  invFun n := {
      toFun := fun x => n * x
      map_zero' := by simp
      map_add' := by intros; ring }


  left_inv f := by
    /- old approach
    apply AddMonoidHom.ext
    simp [mul_comm, ← l_1 f]
    -/
    unfold AddMonoid.End
    ext
    simp


  right_inv n := by
    /- old approach
    simp
    conv =>
      rhs
      rw [Eq.symm (Int.mul_one n)]
    rfl
    -/
    unfold AddMonoid.End
    simp


  map_mul' f g := by
    simp [l_1 f (g 1), mul_comm]

  map_add' f g := by
    simp
    rfl

[Zhu]

l_1 can also be written more concisely using unfold.

lemma l_1 (f : AddMonoid.End ℤ) : ∀ n, f n = n * f 1 := by
  unfold AddMonoid.End at f
  apply AddMonoidHom.apply_int

[Kyle Miller]

Kevin Buzzard said:

ext somehow knows that it suffices to check equality after evaluation at 1

This is probably the difference between ext1 and ext. The first applies a single ext lemma, and the second chains them.

[Ruben Van de Velde]

I would instead think it's a specialized ext lemma that uses the monoid hom structure