Multiplicative homomorphisms respect semiconjugation and commutation. #
@[simp]
theorem
AddSemiconjBy.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
{a : M}
{x : M}
{y : M}
[AddHomClass F M N]
(h : AddSemiconjBy a x y)
(f : F)
:
AddSemiconjBy (↑f a) (↑f x) (↑f y)
@[simp]
theorem
SemiconjBy.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
{a : M}
{x : M}
{y : M}
[MulHomClass F M N]
(h : SemiconjBy a x y)
(f : F)
:
SemiconjBy (↑f a) (↑f x) (↑f y)
@[simp]
theorem
AddCommute.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
{x : M}
{y : M}
[AddHomClass F M N]
(h : AddCommute x y)
(f : F)
:
AddCommute (↑f x) (↑f y)
@[simp]
theorem
Commute.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
{x : M}
{y : M}
[MulHomClass F M N]
(h : Commute x y)
(f : F)
:
Commute (↑f x) (↑f y)
@[simp]
theorem
AddSemiconjBy.of_map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
{a : M}
{x : M}
{y : M}
[AddHomClass F M N]
(f : F)
(hf : Function.Injective ↑f)
(h : AddSemiconjBy (↑f a) (↑f x) (↑f y))
:
AddSemiconjBy a x y
@[simp]
theorem
SemiconjBy.of_map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
{a : M}
{x : M}
{y : M}
[MulHomClass F M N]
(f : F)
(hf : Function.Injective ↑f)
(h : SemiconjBy (↑f a) (↑f x) (↑f y))
:
SemiconjBy a x y
@[simp]
theorem
AddCommute.of_map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
{x : M}
{y : M}
[AddHomClass F M N]
{f : F}
(hf : Function.Injective ↑f)
(h : AddCommute (↑f x) (↑f y))
:
AddCommute x y
@[simp]
theorem
Commute.of_map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
{x : M}
{y : M}
[MulHomClass F M N]
{f : F}
(hf : Function.Injective ↑f)
(h : Commute (↑f x) (↑f y))
:
Commute x y