MonoidHomClass₂ and AddMonoidHom₁ in MIL chapter 7 section2

Stream: new members

[Shanghe Chen]

Hi in MIL the example about coersion of ring homomorphism to function of types, how is it handle the part of adding equality?

[Shanghe Chen]

As in MIL the setup is

import Mathlib.Tactic
set_option autoImplicit true

@[ext]
structure MonoidHom₁ (G H : Type) [Monoid G] [Monoid H] where
  toFun : G → H
  map_one : toFun 1 = 1
  map_mul : ∀ g g', toFun (g * g') = toFun g * toFun g'

instance [Monoid G] [Monoid H] : CoeFun (MonoidHom₁ G H) (fun _ ↦ G → H) where
  coe := MonoidHom₁.toFun

attribute [coe] MonoidHom₁.toFun

@[ext]
structure AddMonoidHom₁ (G H : Type) [AddMonoid G] [AddMonoid H] where
  toFun : G → H
  map_zero : toFun 0 = 0
  map_add : ∀ g g', toFun (g+g') = toFun g + toFun g'

@[ext]
structure RingHom₁ (R S : Type) [Ring R] [Ring S] extends MonoidHom₁ R S, AddMonoidHom₁ R S

class MonoidHomClass₂ (F : Type) (M N: outParam Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

instance [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₂.toFun

attribute [coe] MonoidHomClass₂.toFun

instance (R S : Type) [Ring R] [Ring S] : MonoidHomClass₂ (RingHom₁ R S) R S where
  toFun := fun f ↦ f.toMonoidHom₁.toFun
  map_one := fun f ↦ f.toMonoidHom₁.map_one
  map_mul := fun f ↦ f.toMonoidHom₁.map_mul

[Shanghe Chen]

Then I added an example:

example [Ring R] [Ring S] (f : RingHom₁ R S) {r r' : R} (h : r + r' = 0) : f r + f r' = 0 := by
  have g:=f.map_add r r'
  simp at g
  have e : f r = f.toMonoidHom₁ r := by rfl
  have e' : f r' = f.toMonoidHom₁ r' := by rfl
  rw [e, e', ←g, h, f.map_zero]

[Shanghe Chen]

If I understood correctly, the purpose of class MonoidHomClass₂ is for avoiding explicit f.toMonoidHom₁. But in the example related to the addition operation, is it still necessarily explicit? I cannot simplify the above example for removing e and e'

[Shanghe Chen]

Why is it not implemented that handles both addition and multiplication like the following (It seems that RingHomClass is defined)

class RingHomClass₁ (F : Type) (M N: outParam Type) [Ring M] [Ring N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'
  map_zero : ∀ f, toFun f 0 = 0
  map_add : ∀ f g g', toFun f (g+g') = toFun f g + toFun f g'

instance (R S : Type) [Ring R] [Ring S] : RingHomClass₁ (RingHom₁ R S) R S where
  toFun := fun f ↦ f.toMonoidHom₁.toFun
  map_one := fun f ↦ f.toMonoidHom₁.map_one
  map_mul := fun f ↦ f.toMonoidHom₁.map_mul
  map_zero := fun f ↦ f.toAddMonoidHom₁.map_zero
  map_add := fun f ↦ f.toAddMonoidHom₁.map_add

instance [Ring M] [Ring N] [RingHomClass₁ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := RingHomClass₁.toFun

attribute [coe] RingHomClass₁.toFun

example [Ring R] [Ring S] (f : RingHom₁ R S) {r r' : R} (h : r + r' = 0) : f r + f r' = 0 := by
  rw [←RingHomClass₁.map_add, h, RingHomClass₁.map_zero]

example [Ring R] [Ring S] (f : RingHom₁ R S) {r r' : R} (h : r * r' = 1) : f r * f r' = 1 := by
  rw [←RingHomClass₁.map_mul f r r', h, RingHomClass₁.map_one]