Inner automorphisms of matrix algebras

This file ports the upstream monlib4 theorem that every automorphism of a finite, nontrivial matrix algebra over a field is inner. The downstream corollaries package the implementing matrix as a linear equivalence or as an element of the general linear group.

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

Every automorphism of a finite nontrivial matrix algebra is inner.

theorem Matrix.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

Version of automorphism_matrix_inner using a linear equivalence.

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

Inner automorphism by conjugation with an invertible algebra element.

Equations

• Matrix.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 Matrix.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 Matrix.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)

Any automorphism of a finite matrix algebra is implemented by conjugation.

theorem Matrix.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

Any automorphism of a finite matrix algebra is conjugation by GL n 𝕜.

theorem Matrix.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

Automorphisms of finite matrix algebras preserve trace.

theorem Matrix.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 Matrix.aut_mat_inner_trace_preserving.

---

Automorphisms of finite matrix algebras preserve trace.

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

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

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 = Matrix.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 = Matrix.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

@[reducible, inline]

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

Root-name compatibility wrapper for upstream monlib4 inner automorphisms.

Equations

• Algebra.autInner x = Matrix.Algebra.autInner x

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

An algebra automorphism is inner if it is conjugation by an invertible element.

Equations

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

def AlgEquiv.prodMap {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₄

Product of algebra equivalences, acting componentwise on a product algebra.

Equations

• f.prodMap 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.prodMap_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.prodMap g) a✝ = Prod.map (⇑f) (⇑g) a✝

@[simp]

theorem AlgEquiv.prodMap_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.prodMap g).symm a✝ = Prod.map (⇑f.symm) (⇑g.symm) 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

Dependent-function algebra equivalence induced by pointwise algebra equivalences.

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)

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

Square matrix algebras of finite types are linearly equivalent exactly when their index types have the same cardinality.

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) (h : ∀ (i j : k), Nonempty (n i ≃ n j) ↔ i = j) : Type (max (max (max u_2 u_3) u_4) u_1)

A dependent product of matrix blocks indexed by an ordered block type.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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 := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Pi.invertible {ι : Type u_1} {R : ι → Type u_2} [(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_prodMap {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).prodMap (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] [(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 Matrix.commutes_with_all_iff {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {x : Matrix n n R} : (∀ (y : Matrix n n R), Commute y x) ↔ ∃ (α : R), x = α • 1

A matrix that commutes with every matrix is scalar.

theorem Matrix.center {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] : Set.center (Matrix n n R) = ↑(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] {n : ι → Type u_3} [(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] {n : ι → Type u_3} [(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 matrixPiFinAlgEquivPiFinTwo {𝕜 : 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))

Split a nonempty finite dependent product of matrix algebras into its head and tail.

Equations

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

theorem matrixPiFinAlgEquivPiFinTwo_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)) : matrixPiFinAlgEquivPiFinTwo x = (x 0, fun (j : Fin k) => x j.succ)

theorem matrixPiFinAlgEquivPiFinTwo_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)) : matrixPiFinAlgEquivPiFinTwo.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 matrixPiFinTwoAlgEquivProd {𝕜 : 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)

Identify a two-term dependent product of matrix algebras with a binary product.

Equations

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

@[simp]

theorem matrixPiFinTwoAlgEquivProd_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)) : matrixPiFinTwoAlgEquivProd x = (x 0, x 1)

@[simp]

theorem matrixPiFinTwoAlgEquivProd_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) : matrixPiFinTwoAlgEquivProd.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 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 AlgEquiv.ofProdMap₁₁ {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₃

Extract the first component of a product algebra equivalence that fixes (1, 0).

Equations

• f.ofProdMap₁₁ 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.ofProdMap₂₂ {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₄

Extract the second component of a product algebra equivalence that fixes (0, 1).

Equations

• f.ofProdMap₂₂ 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.ofProdMap₁₂ {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₄

Extract the off-diagonal component of a product algebra equivalence that sends (1, 0) to (0, 1).

Equations

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

def AlgEquiv.ofProdMap₂₁ {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₃

Extract the off-diagonal component of a product algebra equivalence that sends (0, 1) to (1, 0).

Equations

• f.ofProdMap₂₁ hf = { toFun := fun (a : R₂) => (f (0, a)).1, invFun := fun (a : R₃) => (f.symm (a, 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₁.prodMap f₂) ∨ ∃ (g₁ : Matrix m m 𝕜 ≃ₐ[𝕜] Matrix n n 𝕜) (g₂ : Matrix n n 𝕜 ≃ₐ[𝕜] Matrix m m 𝕜), ⇑f = ⇑(g₁.prodMap 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