Inner automorphisms #

In this file we prove that any algebraic automorphism is an inner automorphism.

We work in a field is_R_or_C 𝕜 and finite dimensional vector spaces and matrix algebras.

main definition #

def linear_equiv.matrix_conj_of: this defines an algebraic automorphism over $Mₙ$ given by $x \mapsto yxy^{-1}$ for some linear automorphism $y$ over $\mathbb{k}^n$

main result #

automorphism_matrix_inner''': given an algebraic automorphism $f$ over a non-trivial finite-dimensional matrix algebra $M_n(\mathbb{k})$, we have that there exists a linear automorphism $T$ over the vector space $\mathbb{k}^n$ such that f = T.matrix_conj_of

source

theorem automorphism_matrix_inner {n : Type u_1} {R : Type u_2} [fintype n] [field R] [decidable_eq n] [nonempty n] (f : matrix n n R ≃ₐ[R] matrix n n R) :

∃ (T : matrix n n R), (∀ (a : matrix n n R), (⇑f a).mul T = T.mul a) ∧ function.bijective ⇑(⇑matrix.to_lin' T)

any automorphism of Mₙ is inner given by 𝕜ⁿ, in particular, given a bijective linear map f ∈ L(Mₙ) such that f(ab)=f(a)f(b), we have that there exists a matrix T ∈ Mₙ such that ∀ a ∈ Mₙ : f(a) * T = T * a and T is invertible

source

theorem automorphism_matrix_inner'' {n : Type u_1} {𝕜 : Type u_3} [field 𝕜] [fintype n] [decidable_eq n] [nonempty n] (f : matrix n n 𝕜 ≃ₐ[𝕜] matrix n n 𝕜) :

∃ (T : (n → 𝕜) ≃ₗ[𝕜] n → 𝕜), ∀ (a : matrix n n 𝕜), ⇑f a = ((⇑linear_map.to_matrix' T.to_linear_map).mul a).mul (⇑linear_map.to_matrix' T.symm.to_linear_map)

given an automorphic algebraic equivalence f on Mₙ, we have that there exists a linear equivalence T such that f(a) = M(T) * a * M(⅟ T), i.e., any automorphic algebraic equivalence on Mₙ is inner

source

def algebra.aut_inner {R : Type u_1} {E : Type u_2} [comm_semiring R] [semiring E] [algebra R E] (x : E) [invertible x] :

E ≃ₐ[R] E

Equations

algebra.aut_inner x = {to_fun := λ (y : E), x * y * ⅟ x, inv_fun := λ (y : E), ⅟ x * y * x, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

theorem algebra.aut_inner_apply {R : Type u_1} {E : Type u_2} [comm_semiring R] [semiring E] [algebra R E] (x : E) [invertible x] (y : E) :

⇑(algebra.aut_inner x) y = x * y * ⅟ x

source

theorem algebra.aut_inner_symm_apply {R : Type u_1} {E : Type u_2} [comm_semiring R] [semiring E] [algebra R E] (x : E) [invertible x] (y : E) :

⇑((algebra.aut_inner x).symm) y = ⅟ x * y * x

source

theorem algebra.aut_inner_mul_aut_inner {R : Type u_1} {E : Type u_2} [comm_semiring R] [semiring E] [algebra R E] (x y : E) [invertible x] [invertible y] :

algebra.aut_inner x * algebra.aut_inner y = algebra.aut_inner (x * y)

source

theorem aut_mat_inner {n : Type u_1} {𝕜 : Type u_3} [field 𝕜] [fintype n] [decidable_eq n] (f : matrix n n 𝕜 ≃ₐ[𝕜] matrix n n 𝕜) :

∃ (T : (n → 𝕜) ≃ₗ[𝕜] n → 𝕜), f = algebra.aut_inner (⇑linear_map.to_matrix' ↑T)

source

theorem aut_mat_inner' {n : Type u_1} {𝕜 : Type u_3} [field 𝕜] [fintype n] [decidable_eq n] (f : matrix n n 𝕜 ≃ₐ[𝕜] matrix n n 𝕜) :

∃ (T : GL n 𝕜), f = algebra.aut_inner ⇑T

source

theorem aut_mat_inner_trace_preserving {n : Type u_1} {𝕜 : Type u_3} [field 𝕜] [fintype n] [decidable_eq n] (f : matrix n n 𝕜 ≃ₐ[𝕜] matrix n n 𝕜) (x : matrix n n 𝕜) :

(⇑f x).trace = x.trace

source

theorem matrix.commutes_with_all_iff {n : Type u_1} [fintype n] {R : Type u_2} [comm_semiring R] [decidable_eq n] {x : matrix n n R} :

(∀ (y : matrix n n R), commute y x) ↔ ∃ (α : R), x = α • 1

if a matrix commutes with all matrices, then it is equal to a scalar multiplied by the identity

source

theorem matrix.commutes_with_all_iff_of_ne_zero {n : Type u_1} {𝕜 : Type u_3} [field 𝕜] [fintype n] [decidable_eq n] [nonempty n] {x : matrix n n 𝕜} (hx : x ≠ 0) :

(∀ (y : matrix n n 𝕜), commute y x) ↔ ∃! (α : 𝕜ˣ), x = ↑α • 1

source

theorem algebra.aut_inner_eq_aut_inner_iff {n : Type u_1} {𝕜 : Type u_3} [field 𝕜] [fintype n] [decidable_eq n] (x y : matrix n n 𝕜) [invertible x] [invertible y] :

algebra.aut_inner x = algebra.aut_inner y ↔ ∃ (α : 𝕜), y = α • x