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

theorem automorphism_matrix_inner {n : Type u_2} {R : Type u_1} [Fintype n] [Field R] [DecidableEq n] [h5 : Nonempty n] (f : Matrix n n R ≃ₐ[R] Matrix n n R) : ∃ (T : Matrix n n R), (∀ (a : Matrix n n R), f a * T = T * a) ∧ Function.Bijective ⇑(Matrix.toLin' 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

theorem automorphism_matrix_inner'' {n : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [Fintype n] [DecidableEq n] [Nonempty n] (f : Matrix n n 𝕜 ≃ₐ[𝕜] Matrix n n 𝕜) : ∃ (T : (n → 𝕜) ≃ₗ[𝕜] n → 𝕜), ∀ (a : Matrix n n 𝕜), f a = LinearMap.toMatrix' ↑T * a * LinearMap.toMatrix' ↑T.symm

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

def Algebra.autInner {R : Type u_1} {E : Type u_2} [CommSemiring R] [Semiring E] [Algebra R E] (x : E) [Invertible x] : E ≃ₐ[R] E

Equations

• Algebra.autInner x = { toFun := fun (y : E) => x * y * ⅟ x, invFun := fun (y : E) => ⅟ x * y * x, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem Algebra.autInner_apply {R : Type u_1} {E : Type u_2} [CommSemiring R] [Semiring E] [Algebra R E] (x : E) [Invertible x] (y : E) : (autInner x) y = x * y * ⅟ x

theorem Algebra.autInner_symm_apply {R : Type u_1} {E : Type u_2} [CommSemiring R] [Semiring E] [Algebra R E] (x : E) [Invertible x] (y : E) : (autInner x).symm y = ⅟ x * y * x

theorem Algebra.coe_autInner_eq_rmul_comp_lmul {R : Type u_1} {E : Type u_2} [CommSemiring R] [Semiring E] [Algebra R E] (x : E) [Invertible x] : ⇑(autInner x) = ⇑(_root_.lmul x) ∘ ⇑(rmul ⅟ x)

theorem Algebra.coe_autInner_symm_eq_rmul_comp_lmul {R : Type u_1} {E : Type u_2} [CommSemiring R] [Semiring E] [Algebra R E] (x : E) [Invertible x] : ⇑(autInner x).symm = ⇑(_root_.lmul ⅟ x) ∘ ⇑(rmul x)

theorem lmul_comp_rmul_eq_mulLeftRight {R : Type u_1} {E : Type u_2} [CommSemiring R] [NonUnitalSemiring E] [Module R E] [SMulCommClass R E E] [IsScalarTower R E E] (a b : E) : lmul a ∘ₗ rmul b = LinearMap.mulLeftRight R (a, b)

theorem lmul_comp_rmul_eq_coe_mulLeftRight {R : Type u_1} {E : Type u_2} [CommSemiring R] [NonUnitalSemiring E] [Module R E] [SMulCommClass R E E] [IsScalarTower R E E] (a b : E) : ⇑(lmul a) ∘ ⇑(rmul b) = ⇑(LinearMap.mulLeftRight R (a, b))

theorem Algebra.autInner_hMul_autInner {R : Type u_1} {E : Type u_2} [CommSemiring R] [Semiring E] [Algebra R E] (x y : E) [hx : Invertible x] [hy : Invertible y] : autInner x * autInner y = autInner (x * y)

def AlgEquiv.IsInner {R : Type u_1} {E : Type u_2} [CommSemiring R] [Semiring E] [Algebra R E] (f : E ≃ₐ[R] E) : Prop

Equations

• f.IsInner = ∃ (a : E) (x : Invertible a), f = Algebra.autInner a

def AlgEquiv.prod_map {K : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Algebra K R₁] [Algebra K R₂] [Algebra K R₃] [Algebra K R₄] (f : R₁ ≃ₐ[K] R₂) (g : R₃ ≃ₐ[K] R₄) : (R₁ × R₃) ≃ₐ[K] R₂ × R₄

Equations

• f.prod_map g = { toFun := Prod.map ⇑f ⇑g, invFun := Prod.map ⇑f.symm ⇑g.symm, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgEquiv.prod_map_symm_apply {K : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Algebra K R₁] [Algebra K R₂] [Algebra K R₃] [Algebra K R₄] (f : R₁ ≃ₐ[K] R₂) (g : R₃ ≃ₐ[K] R₄) (a✝ : R₂ × R₄) : (f.prod_map g).symm a✝ = Prod.map (⇑f.symm) (⇑g.symm) a✝

@[simp]

theorem AlgEquiv.prod_map_apply {K : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Algebra K R₁] [Algebra K R₂] [Algebra K R₃] [Algebra K R₄] (f : R₁ ≃ₐ[K] R₂) (g : R₃ ≃ₐ[K] R₄) (a✝ : R₁ × R₃) : (f.prod_map g) a✝ = Prod.map (⇑f) (⇑g) a✝

def AlgEquiv.Pi {K : Type u_1} {ι : Type u_2} [CommSemiring K] {R : ι → Type u_3} [(i : ι) → Semiring (R i)] [(i : ι) → Algebra K (R i)] (f : (i : ι) → R i ≃ₐ[K] R i) : ((i : ι) → R i) ≃ₐ[K] (i : ι) → R i

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgEquiv.Pi_symm_apply {K : Type u_1} {ι : Type u_2} [CommSemiring K] {R : ι → Type u_3} [(i : ι) → Semiring (R i)] [(i : ι) → Algebra K (R i)] (f : (i : ι) → R i ≃ₐ[K] R i) (x : (i : ι) → R i) (i : ι) : (Pi f).symm x i = (f i).symm (x i)

@[simp]

theorem AlgEquiv.Pi_apply {K : Type u_1} {ι : Type u_2} [CommSemiring K] {R : ι → Type u_3} [(i : ι) → Semiring (R i)] [(i : ι) → Algebra K (R i)] (f : (i : ι) → R i ≃ₐ[K] R i) (x : (i : ι) → R i) (i : ι) : (Pi f) x i = (f i) (x i)

instance Prod.invertible_fst {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {a : R₁ × R₂} [ha : Invertible a] : Invertible a.1

Equations

• Prod.invertible_fst = { invOf := (⅟ a).1, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

instance Prod.invertible_snd {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {a : R₁ × R₂} [ha : Invertible a] : Invertible a.2

Equations

• Prod.invertible_snd = { invOf := (⅟ a).2, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

instance Prod.invertible {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {a : R₁} {b : R₂} [ha : Invertible a] [hb : Invertible b] : Invertible (a, b)

Equations

• Prod.invertible = { invOf := (⅟ a, ⅟ b), invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

instance Pi.invertible_i {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Semiring (R i)] [(i : ι) → Semiring (R i)] {a : (i : ι) → R i} [ha : Invertible a] (i : ι) : Invertible (a i)

Equations

• Pi.invertible_i i = { invOf := ⅟ a i, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

instance Pi.invertible {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Semiring (R i)] [(i : ι) → Semiring (R i)] {a : (i : ι) → R i} [ha : (i : ι) → Invertible (a i)] : Invertible a

Equations

• Pi.invertible = { invOf := fun (i : ι) => ⅟ (a i), invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem AlgEquiv.prod_isInner_iff_prod_map {K : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Algebra K R₁] [Algebra K R₂] (f : (R₁ × R₂) ≃ₐ[K] R₁ × R₂) : f.IsInner ↔ ∃ (a : R₁) (_ha : Invertible a) (b : R₂) (_hb : Invertible b), f = (Algebra.autInner a).prod_map (Algebra.autInner b)

theorem AlgEquiv.pi_isInner_iff_pi_map {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [CommSemiring K] [(i : ι) → Semiring (R i)] [(i : ι) → Algebra K (R i)] (f : ((i : ι) → R i) ≃ₐ[K] (i : ι) → R i) : f.IsInner ↔ ∃ (a : (i : ι) → R i) (_ha : (i : ι) → Invertible (a i)), f = Pi fun (i : ι) => Algebra.autInner (a i)

theorem AlgEquiv.pi_isInner_iff_pi_map' {K : Type u_1} {ι : Type u_2} {n : ι → Type u_3} [CommSemiring K] [Fintype ι] [(i : ι) → Fintype (n i)] [(i : ι) → DecidableEq (n i)] (f : PiMat K ι n ≃ₐ[K] PiMat K ι n) : f.IsInner ↔ ∃ (a : PiMat K ι n) (x : (i : ι) → Invertible (a i)), f = Pi fun (i : ι) => Algebra.autInner (a i)

theorem aut_mat_inner {n : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [Fintype n] [DecidableEq n] (f : Matrix n n 𝕜 ≃ₐ[𝕜] Matrix n n 𝕜) : ∃ (T : (n → 𝕜) ≃ₗ[𝕜] n → 𝕜), f = Algebra.autInner (LinearMap.toMatrix' ↑T)

theorem aut_mat_inner' {n : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [Fintype n] [DecidableEq n] (f : Matrix n n 𝕜 ≃ₐ[𝕜] Matrix n n 𝕜) : ∃ (T : GL n 𝕜), f = Algebra.autInner ↑T

theorem aut_mat_inner_trace_preserving {n : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [Fintype n] [DecidableEq n] (f : Matrix n n 𝕜 ≃ₐ[𝕜] Matrix n n 𝕜) (x : Matrix n n 𝕜) : (f x).trace = x.trace

theorem AlgEquiv.apply_matrix_trace {n : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [Fintype n] [DecidableEq n] (f : Matrix n n 𝕜 ≃ₐ[𝕜] Matrix n n 𝕜) (x : Matrix n n 𝕜) : (f x).trace = x.trace

Alias of aut_mat_inner_trace_preserving.

theorem Matrix.commutes_with_all_iff {n : Type u_2} [Fintype n] {R : Type u_1} [CommSemiring R] [DecidableEq 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

theorem Matrix.center {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] : Set.center (Matrix n n R) = ↑(Submodule.span R {1})

theorem Matrix.prod_center {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] : Set.center (Matrix n n R × Matrix m m R) = ↑(Submodule.span R {(1, 0), (0, 1)})

theorem Matrix.pi_center {R : Type u_1} {ι : Type u_2} [CommSemiring R] [DecidableEq ι] [Fintype ι] {n : ι → Type u_3} [(i : ι) → DecidableEq (n i)] [(i : ι) → Fintype (n i)] : Set.center ((i : ι) → Matrix (n i) (n i) R) = {x : (i : ι) → Matrix (n i) (n i) R | ∀ (i : ι), x i ∈ Set.center (Matrix (n i) (n i) R)}

theorem PiMat.center {R : Type u_1} {ι : Type u_2} [CommSemiring R] [DecidableEq ι] [Fintype ι] {n : ι → Type u_3} [(i : ι) → DecidableEq (n i)] [(i : ι) → Fintype (n i)] : Set.center (PiMat R ι n) = {x : PiMat R ι n | ∀ (i : ι), x i ∈ Set.center (Matrix (n i) (n i) R)}

theorem Matrix.commutes_with_all_iff_of_ne_zero {n : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [Fintype n] [DecidableEq n] [Nonempty n] {x : Matrix n n 𝕜} (hx : x ≠ 0) : (∀ (y : Matrix n n 𝕜), Commute y x) ↔ ∃! α : 𝕜ˣ, x = ↑α • 1

theorem Algebra.autInner_eq_autInner_iff {n : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [Fintype n] [DecidableEq n] (x y : Matrix n n 𝕜) [Invertible x] [Invertible y] : autInner x = autInner y ↔ ∃ (α : 𝕜), y = α • x

theorem Matrix.one_ne_zero_iff {𝕜 : Type u_1} {n : Type u_2} [DecidableEq n] [Zero 𝕜] [One 𝕜] [NeZero 1] : 1 ≠ 0 ↔ Nonempty n

theorem Matrix.one_eq_zero_iff {𝕜 : Type u_1} {n : Type u_2} [DecidableEq n] [Zero 𝕜] [One 𝕜] [NeZero 1] : 1 = 0 ↔ IsEmpty n

theorem AlgEquiv.matrix_prod_aut {𝕜 : Type u_1} {n : Type u_2} {m : Type u_3} [Field 𝕜] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (f : (Mat 𝕜 n × Mat 𝕜 m) ≃ₐ[𝕜] Mat 𝕜 n × Mat 𝕜 m) : f (1, 0) = (1, 0) ∧ f (0, 1) = (0, 1) ∨ f (1, 0) = (0, 1) ∧ f (0, 1) = (1, 0)

theorem Fin.fintwo_of_neZero {i : Fin 2} (hi : i ≠ 0) : i = 1

def matrixPiFin_algEquiv_PiFinTwo {𝕜 : Type u_1} [CommSemiring 𝕜] {k : ℕ} {n : Fin (k + 1) → Type u_2} [(i : Fin (k + 1)) → Fintype (n i)] [(i : Fin (k + 1)) → DecidableEq (n i)] : ((i : Fin (k + 1)) → Mat 𝕜 (n i)) ≃ₐ[𝕜] Mat 𝕜 (n ⟨0, ⋯⟩) × ((j : Fin k) → Mat 𝕜 (n j.succ))

Equations

• One or more equations did not get rendered due to their size.

theorem matrixPiFin_algEquiv_PiFinTwo_apply {𝕜 : Type u_1} [CommSemiring 𝕜] {k : ℕ} {n : Fin (k + 1) → Type u_2} [(i : Fin (k + 1)) → Fintype (n i)] [(i : Fin (k + 1)) → DecidableEq (n i)] (x : (i : Fin (k + 1)) → Mat 𝕜 (n i)) : matrixPiFin_algEquiv_PiFinTwo x = (x 0, fun (j : Fin k) => x j.succ)

theorem matrixPiFin_algEquiv_PiFinTwo_symm_apply {𝕜 : Type u_1} [CommSemiring 𝕜] {k : ℕ} {n : Fin (k + 1) → Type u_2} [(i : Fin (k + 1)) → Fintype (n i)] [(i : Fin (k + 1)) → DecidableEq (n i)] (x : Mat 𝕜 (n 0) × ((j : Fin k) → Mat 𝕜 (n j.succ))) (i : Fin (k + 1)) : matrixPiFin_algEquiv_PiFinTwo.symm x i = if h : i = 0 then fun (a b : n i) => x.1 (⋯.mpr a) (⋯.mpr b) else ⋯.mpr (x.2 (i.pred h))

def matrixPiFinTwo_algEquiv_prod {𝕜 : Type u_1} [CommSemiring 𝕜] {n : Fin 2 → Type u_2} [(i : Fin 2) → Fintype (n i)] [(i : Fin 2) → DecidableEq (n i)] : ((i : Fin 2) → Mat 𝕜 (n i)) ≃ₐ[𝕜] Mat 𝕜 (n 0) × Mat 𝕜 (n 1)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem matrixPiFinTwo_algEquiv_prod_apply {𝕜 : Type u_1} [CommSemiring 𝕜] {n : Fin 2 → Type u_2} [(i : Fin 2) → Fintype (n i)] [(i : Fin 2) → DecidableEq (n i)] (x : (i : Fin 2) → Mat 𝕜 (n i)) : matrixPiFinTwo_algEquiv_prod x = (x 0, x 1)

@[simp]

theorem matrixPiFinTwo_algEquiv_prod_symm_apply {𝕜 : Type u_1} [CommSemiring 𝕜] {n : Fin 2 → Type u_2} [(i : Fin 2) → Fintype (n i)] [(i : Fin 2) → DecidableEq (n i)] (x : Mat 𝕜 (n 0) × Mat 𝕜 (n 1)) (i : Fin 2) : matrixPiFinTwo_algEquiv_prod.symm x i = if h : i = 0 then fun (a b : n i) => x.1 (⋯.mpr a) (⋯.mpr b) else fun (a b : n i) => x.2 (⋯.mpr a) (⋯.mpr b)

theorem matrixPiFinTwo_algAut_apply_piSingle {𝕜 : Type u_1} [Field 𝕜] {n : Fin 2 → Type u_2} [(i : Fin 2) → Fintype (n i)] [(i : Fin 2) → DecidableEq (n i)] (f : ((i : Fin 2) → Mat 𝕜 (n i)) ≃ₐ[𝕜] (i : Fin 2) → Mat 𝕜 (n i)) : ∃ (σ : Equiv.Perm (Fin 2)), ∀ (i : Fin 2), f (Pi.single (σ i) 1) = Pi.single i 1

theorem matrix_linearEquiv_iff_fintype_equiv {R : Type u_1} {n : Type u_2} {m : Type u_3} [Ring R] [StrongRankCondition R] [Fintype n] [Fintype m] : Nonempty (Mat R m ≃ₗ[R] Mat R n) ↔ Nonempty (m ≃ n)

theorem LinearEquiv.nonempty_of_equiv {K : Type u_1} {R : Type u_2} {S : Type u_3} {T : Type u_4} [Ring K] [StrongRankCondition K] [AddCommGroup R] [Module K R] [Module.Free K R] [AddCommGroup S] [Module K S] [Module.Free K S] [AddCommGroup T] [Module K T] [Module.Free K T] [Module.Finite K R] [Module.Finite K S] [Module.Finite K T] (h : R ≃ₗ[K] T) : Nonempty (R ≃ₗ[K] S) ↔ Nonempty (T ≃ₗ[K] S)

def OrderedPiMat (R : Type u_1) (k : Type u_2) (t : k → Type u_3) (n : k → Type u_4) : (∀ (i j : k), Nonempty (n i ≃ n j) ↔ i = j) → Type (max (max (max u_2 u_3) u_4) u_1)

Equations

• OrderedPiMat R k t n x✝ = ((i : k) → t i → Mat R (n i))

theorem Algebra.prod_one_zero_mul {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (a : R₁ × R₂) : (1, 0) * a = (a.1, 0)

theorem Algebra.prod_zero_one_mul {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (a : R₁ × R₂) : (0, 1) * a = (0, a.2)

def tacticProd_map_add : Lean.ParserDescr

Equations

• tacticProd_map_add = Lean.ParserDescr.node `tacticProd_map_add 1024 (Lean.ParserDescr.nonReservedSymbol "prod_map_add" false)

def tacticProd_map_mul : Lean.ParserDescr

Equations

• tacticProd_map_mul = Lean.ParserDescr.node `tacticProd_map_mul 1024 (Lean.ParserDescr.nonReservedSymbol "prod_map_mul" false)

def AlgEquiv.of_prod_map₁₁ {K : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Algebra K R₁] [Algebra K R₂] [Algebra K R₃] [Algebra K R₄] (f : (R₁ × R₂) ≃ₐ[K] R₃ × R₄) (hf : f (1, 0) = (1, 0)) : R₁ ≃ₐ[K] R₃

Equations

• f.of_prod_map₁₁ hf = { toFun := fun (a : R₁) => (f (a, 0)).1, invFun := fun (a : R₃) => (f.symm (a, 0)).1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def AlgEquiv.of_prod_map₂₂ {K : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Algebra K R₁] [Algebra K R₂] [Algebra K R₃] [Algebra K R₄] (f : (R₁ × R₂) ≃ₐ[K] R₃ × R₄) (hf : f (0, 1) = (0, 1)) : R₂ ≃ₐ[K] R₄

Equations

• f.of_prod_map₂₂ hf = { toFun := fun (a : R₂) => (f (0, a)).2, invFun := fun (a : R₄) => (f.symm (0, a)).2, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def AlgEquiv.of_prod_map₁₂ {K : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Algebra K R₁] [Algebra K R₂] [Algebra K R₃] [Algebra K R₄] (f : (R₁ × R₂) ≃ₐ[K] R₃ × R₄) (hf : f (1, 0) = (0, 1)) : R₁ ≃ₐ[K] R₄

Equations

• f.of_prod_map₁₂ hf = { toFun := fun (x : R₁) => (f (x, 0)).2, invFun := fun (x : R₄) => (f.symm (0, x)).1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def AlgEquiv.of_prod_map₂₁ {K : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Algebra K R₁] [Algebra K R₂] [Algebra K R₃] [Algebra K R₄] (f : (R₁ × R₂) ≃ₐ[K] R₃ × R₄) (hf : f (0, 1) = (1, 0)) : R₂ ≃ₐ[K] R₃

Equations

• f.of_prod_map₂₁ hf = { toFun := fun (x : R₂) => (f (0, x)).1, invFun := fun (x : R₃) => (f.symm (x, 0)).2, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem AlgEquiv.matrix_prod_aut' {𝕜 : Type u_1} {n : Type u_2} {m : Type u_3} [Field 𝕜] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (f : (Matrix n n 𝕜 × Matrix m m 𝕜) ≃ₐ[𝕜] Matrix n n 𝕜 × Matrix m m 𝕜) : (∃ (f₁ : Matrix n n 𝕜 ≃ₐ[𝕜] Matrix n n 𝕜) (f₂ : Matrix m m 𝕜 ≃ₐ[𝕜] Matrix m m 𝕜), f = f₁.prod_map f₂) ∨ ∃ (g₁ : Matrix m m 𝕜 ≃ₐ[𝕜] Matrix n n 𝕜) (g₂ : Matrix n n 𝕜 ≃ₐ[𝕜] Matrix m m 𝕜), ⇑f = ⇑(g₁.prod_map g₂) ∘ Prod.swap

theorem AlgEquiv.matrix_fintype_card_eq_of {𝕜 : Type u_1} {n : Type u_2} {m : Type u_3} [Field 𝕜] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {f : (Matrix n n 𝕜 × Matrix m m 𝕜) ≃ₐ[𝕜] Matrix n n 𝕜 × Matrix m m 𝕜} (hf : f (0, 1) = (1, 0)) : Fintype.card n = Fintype.card m