One by one matrices

This file proves that one by one matrices over a base are equivalent to the base itself under the canonical map that sends a one by one matrix !![a] to a.

Main results

• Matrix.uniqueRingEquiv
• Matrix.uniqueAlgEquiv

Tags

Matrix, Unique, AlgEquiv

def Matrix.uniqueEquiv {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] : Matrix m n A ≃ A

The isomorphism between the type of all one by one matrices and the base type.

Equations

• Matrix.uniqueEquiv = { toFun := fun (M : Matrix m n A) => M default default, invFun := fun (a : A) => Matrix.of fun (x : m) (x_1 : n) => a, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matrix.uniqueEquiv_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] (M : Matrix m n A) : uniqueEquiv M = M default default

@[simp]

theorem Matrix.uniqueEquiv_symm_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] (a : A) : uniqueEquiv.symm a = of fun (x : m) (x_1 : n) => a

def Matrix.uniqueAddEquiv {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] [Add A] : Matrix m n A ≃+ A

The obvious additive isomorphism between M₁(A) and A, if A has an addition.

Equations

• Matrix.uniqueAddEquiv = { toEquiv := Matrix.uniqueEquiv, map_add' := ⋯ }

@[simp]

theorem Matrix.uniqueAddEquiv_symm_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] [Add A] (a : A) : uniqueAddEquiv.symm a = of fun (x : m) (x_1 : n) => a

@[simp]

theorem Matrix.uniqueAddEquiv_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] [Add A] (M : Matrix m n A) : uniqueAddEquiv M = M default default

def Matrix.uniqueLinearEquiv {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_4} [Unique m] [Unique n] [Semiring R] [AddCommMonoid A] [Module R A] : Matrix m n A ≃ₗ[R] A

M₁(A) is linearly equivalent to A as an R-module where R is a semiring.

Equations

• Matrix.uniqueLinearEquiv = { toFun := Matrix.uniqueAddEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := Matrix.uniqueAddEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matrix.uniqueLinearEquiv_symm_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_4} [Unique m] [Unique n] [Semiring R] [AddCommMonoid A] [Module R A] (a✝ : A) : uniqueLinearEquiv.symm a✝ = uniqueAddEquiv.invFun a✝

@[simp]

theorem Matrix.uniqueLinearEquiv_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_4} [Unique m] [Unique n] [Semiring R] [AddCommMonoid A] [Module R A] (a✝ : Matrix m n A) : uniqueLinearEquiv a✝ = uniqueAddEquiv.toFun a✝

def Matrix.uniqueRingEquiv {m : Type u_1} {A : Type u_3} [Unique m] [NonUnitalNonAssocSemiring A] : Matrix m m A ≃+* A

M₁(A) and A are equivalent as rings.

Equations

• Matrix.uniqueRingEquiv = { toEquiv := Matrix.uniqueAddEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.uniqueRingEquiv_symm_apply {m : Type u_1} {A : Type u_3} [Unique m] [NonUnitalNonAssocSemiring A] (a : A) : uniqueRingEquiv.symm a = of fun (x x_1 : m) => a

@[simp]

theorem Matrix.uniqueRingEquiv_apply {m : Type u_1} {A : Type u_3} [Unique m] [NonUnitalNonAssocSemiring A] (M : Matrix m m A) : uniqueRingEquiv M = M default default

def Matrix.uniqueAlgEquiv {m : Type u_1} {A : Type u_3} {R : Type u_4} [Unique m] [Semiring A] [CommSemiring R] [Algebra R A] : Matrix m m A ≃ₐ[R] A

M₁(A) is equivalent to A as an R-algebra.

Equations

• Matrix.uniqueAlgEquiv = { toEquiv := Matrix.uniqueRingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Matrix.uniqueAlgEquiv_symm_apply {m : Type u_1} {A : Type u_3} {R : Type u_4} [Unique m] [Semiring A] [CommSemiring R] [Algebra R A] (a : A) : uniqueAlgEquiv.symm a = of fun (x x_1 : m) => a

@[simp]

theorem Matrix.uniqueAlgEquiv_apply {m : Type u_1} {A : Type u_3} {R : Type u_4} [Unique m] [Semiring A] [CommSemiring R] [Algebra R A] (M : Matrix m m A) : uniqueAlgEquiv M = M default default