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