Zulip Chat Archive

Stream: new members

Topic: MonoidHomClass₂ and AddMonoidHom₁ in MIL chapter 7 section2


Shanghe Chen (Mar 27 2024 at 16:30):

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 (Mar 27 2024 at 16:30):

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 (Mar 27 2024 at 16:31):

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 (Mar 27 2024 at 16:33):

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 (Mar 27 2024 at 16:50):

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]

Last updated: May 02 2025 at 03:31 UTC