Mathlib.Algebra.Group.Commute.Hom

SemiconjBy.map theorem

[MulHomClass F M N] (h : SemiconjBy a x y) (f : F) : SemiconjBy (f a) (f x) (f y)

Full source

@[to_additive (attr := simp)]
protected theorem SemiconjBy.map [MulHomClass F M N] (h : SemiconjBy a x y) (f : F) :
    SemiconjBy (f a) (f x) (f y) := by simpa only [SemiconjBy, map_mul] using congr_arg f h

Homomorphic Image Preserves Semiconjugation Relation

Informal description

Let $M$ and $N$ be multiplicative structures, and let $F$ be a type of homomorphisms from $M$ to $N$ that preserve multiplication. If $a, x, y \in M$ satisfy the semiconjugation relation $a * x = y * a$, then for any homomorphism $f \colon M \to N$ in $F$, the images satisfy the semiconjugation relation $f(a) * f(x) = f(y) * f(a)$.

Commute.map theorem

[MulHomClass F M N] (h : Commute x y) (f : F) : Commute (f x) (f y)

Full source

@[to_additive (attr := simp)]
protected theorem Commute.map [MulHomClass F M N] (h : Commute x y) (f : F) : Commute (f x) (f y) :=
  SemiconjBy.map h f

Homomorphic Image Preserves Commutation Relation

Informal description

Let $M$ and $N$ be multiplicative structures, and let $F$ be a type of homomorphisms from $M$ to $N$ that preserve multiplication. If $x, y \in M$ commute (i.e., $x * y = y * x$), then for any homomorphism $f \colon M \to N$ in $F$, the images $f(x)$ and $f(y)$ also commute (i.e., $f(x) * f(y) = f(y) * f(x)$).

SemiconjBy.of_map theorem

[MulHomClass F M N] (f : F) (hf : Function.Injective f) (h : SemiconjBy (f a) (f x) (f y)) : SemiconjBy a x y

Full source

@[to_additive (attr := simp)]
protected theorem SemiconjBy.of_map [MulHomClass F M N] (f : F) (hf : Function.Injective f)
    (h : SemiconjBy (f a) (f x) (f y)) : SemiconjBy a x y :=
  hf (by simpa only [SemiconjBy, map_mul] using h)

Lifting of Semiconjugation Relation via Injective Multiplicative Homomorphism

Informal description

Let $M$ and $N$ be multiplicative structures, and let $F$ be a type of homomorphisms from $M$ to $N$ that preserve multiplication. Given an injective homomorphism $f \colon M \to N$ in $F$, if elements $f(a), f(x), f(y) \in N$ satisfy the semiconjugation relation $f(a) * f(x) = f(y) * f(a)$, then the original elements $a, x, y \in M$ satisfy the semiconjugation relation $a * x = y * a$.

Commute.of_map theorem

[MulHomClass F M N] {f : F} (hf : Function.Injective f) (h : Commute (f x) (f y)) : Commute x y

Full source

@[to_additive (attr := simp)]
theorem Commute.of_map [MulHomClass F M N] {f : F} (hf : Function.Injective f)
    (h : Commute (f x) (f y)) : Commute x y :=
  hf (by simpa only [map_mul] using h.eq)

Inverse Image of Commuting Elements under Injective Multiplicative Homomorphism

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f \colon M \to N$ be an injective multiplicative homomorphism. If the images $f(x)$ and $f(y)$ commute in $N$, then $x$ and $y$ commute in $M$. That is, if $f(x) * f(y) = f(y) * f(x)$, then $x * y = y * x$.