Multiplicative homomorphisms respect semiconjugation and commutation. #
@[simp]
theorem
SemiconjBy.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
{a x y : M}
[FunLike F M N]
[MulHomClass F M N]
(h : SemiconjBy a x y)
(f : F)
:
SemiconjBy (f a) (f x) (f y)
@[simp]
theorem
AddSemiconjBy.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
{a x y : M}
[FunLike F M N]
[AddHomClass F M N]
(h : AddSemiconjBy a x y)
(f : F)
:
AddSemiconjBy (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 y : M}
[FunLike F M N]
[AddHomClass F M N]
(h : AddCommute x y)
(f : F)
:
AddCommute (f x) (f y)
theorem
SemiconjBy.of_map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
{a x y : M}
[FunLike F M N]
[MulHomClass F M N]
{f : F}
(hf : Function.Injective ⇑f)
(h : SemiconjBy (f a) (f x) (f y))
:
SemiconjBy a x y
theorem
AddSemiconjBy.of_map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
{a x y : M}
[FunLike F M N]
[AddHomClass F M N]
{f : F}
(hf : Function.Injective ⇑f)
(h : AddSemiconjBy (f a) (f x) (f y))
:
AddSemiconjBy a x y
theorem
Commute.of_map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
{x y : M}
[FunLike F M N]
[MulHomClass F M N]
{f : F}
(hf : Function.Injective ⇑f)
(h : Commute (f x) (f y))
:
Commute x y
theorem
AddCommute.of_map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
{x y : M}
[FunLike F M N]
[AddHomClass F M N]
{f : F}
(hf : Function.Injective ⇑f)
(h : AddCommute (f x) (f y))
:
AddCommute x y
theorem
semiconjBy_map_iff
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
{a : M}
[FunLike F M N]
[MulHomClass F M N]
{f : F}
(hf : Function.Injective ⇑f)
{x y : M}
:
theorem
addSemiconjBy_map_iff
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
{a : M}
[FunLike F M N]
[AddHomClass F M N]
{f : F}
(hf : Function.Injective ⇑f)
{x y : M}
:
theorem
commute_map_iff
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Mul M]
[Mul N]
[FunLike F M N]
[MulHomClass F M N]
{f : F}
(hf : Function.Injective ⇑f)
{x y : M}
:
theorem
addCommute_map_iff
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[Add M]
[Add N]
[FunLike F M N]
[AddHomClass F M N]
{f : F}
(hf : Function.Injective ⇑f)
{x y : M}
: