The convolutive star ring on matrices

In this file, we provide the star algebra instance on WithConv (Matrix m n R) given by the Hadamard product and intrinsic star (i.e., the star of each element in the matrix).

@[implicit_reducible]

instance instMulWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [Mul α] : Mul (WithConv (Matrix m n α))

Equations

• instMulWithConvMatrix = { mul := fun (a b : WithConv (Matrix m n α)) => WithConv.toConv (a.ofConv.hadamard b.ofConv) }

theorem convMul_def {m : Type u_1} {n : Type u_2} {α : Type u_3} [Mul α] (x y : WithConv (Matrix m n α)) : x * y = WithConv.toConv (x.ofConv.hadamard y.ofConv)

@[implicit_reducible]

instance instSemigroupWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [Semigroup α] : Semigroup (WithConv (Matrix m n α))

Equations

• instSemigroupWithConvMatrix = { toMul := instMulWithConvMatrix, mul_assoc := ⋯ }

@[implicit_reducible]

instance instNonUnitalNonAssocSemiringWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring (WithConv (Matrix m n α))

Equations

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

@[implicit_reducible]

instance instCommMagmaWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [CommMagma α] : CommMagma (WithConv (Matrix m n α))

Equations

• instCommMagmaWithConvMatrix = { toMul := instMulWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instOneWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [One α] : One (WithConv (Matrix m n α))

Equations

• instOneWithConvMatrix = { one := WithConv.toConv (Matrix.of 1) }

theorem convOne_def {m : Type u_1} {n : Type u_2} {α : Type u_3} [One α] : 1 = WithConv.toConv (Matrix.of 1)

@[implicit_reducible]

instance instMulOneClassWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [MulOneClass α] : MulOneClass (WithConv (Matrix m n α))

Equations

• instMulOneClassWithConvMatrix = { toOne := instOneWithConvMatrix, toMul := instMulWithConvMatrix, one_mul := ⋯, mul_one := ⋯ }

@[implicit_reducible]

instance instMonoidWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [Monoid α] : Monoid (WithConv (Matrix m n α))

Equations

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

@[implicit_reducible]

instance instCommMonoidWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [CommMonoid α] : CommMonoid (WithConv (Matrix m n α))

Equations

• instCommMonoidWithConvMatrix = { toMonoid := instMonoidWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instNonAssocSemiringWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonAssocSemiring α] : NonAssocSemiring (WithConv (Matrix m n α))

Equations

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

@[implicit_reducible]

instance instNonUnitalSemiringWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalSemiring α] : NonUnitalSemiring (WithConv (Matrix m n α))

Equations

• instNonUnitalSemiringWithConvMatrix = { toNonUnitalNonAssocSemiring := instNonUnitalNonAssocSemiringWithConvMatrix, mul_assoc := ⋯ }

@[implicit_reducible]

instance instNonUnitalNonAssocCommSemiringWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalNonAssocCommSemiring α] : NonUnitalNonAssocCommSemiring (WithConv (Matrix m n α))

Equations

• instNonUnitalNonAssocCommSemiringWithConvMatrix = { toNonUnitalNonAssocSemiring := instNonUnitalNonAssocSemiringWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instNonUnitalCommSemiringWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalCommSemiring α] : NonUnitalCommSemiring (WithConv (Matrix m n α))

Equations

• instNonUnitalCommSemiringWithConvMatrix = { toNonUnitalSemiring := instNonUnitalSemiringWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instNonAssocCommSemiringWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonAssocCommSemiring α] : NonAssocCommSemiring (WithConv (Matrix m n α))

Equations

• instNonAssocCommSemiringWithConvMatrix = { toNonAssocSemiring := instNonAssocSemiringWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instSemiringWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [Semiring α] : Semiring (WithConv (Matrix m n α))

Equations

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

@[implicit_reducible]

instance instCommSemiringWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [CommSemiring α] : CommSemiring (WithConv (Matrix m n α))

Equations

• instCommSemiringWithConvMatrix = { toSemiring := instSemiringWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instNonUnitalNonAssocRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing (WithConv (Matrix m n α))

Equations

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

@[implicit_reducible]

instance instNonUnitalNonAssocCommRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalNonAssocCommRing α] : NonUnitalNonAssocCommRing (WithConv (Matrix m n α))

Equations

• instNonUnitalNonAssocCommRingWithConvMatrix = { toNonUnitalNonAssocRing := instNonUnitalNonAssocRingWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instNonUnitalRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalRing α] : NonUnitalRing (WithConv (Matrix m n α))

Equations

• instNonUnitalRingWithConvMatrix = { toNonUnitalNonAssocRing := instNonUnitalNonAssocRingWithConvMatrix, mul_assoc := ⋯ }

@[implicit_reducible]

instance instNonUnitalCommRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalCommRing α] : NonUnitalCommRing (WithConv (Matrix m n α))

Equations

• instNonUnitalCommRingWithConvMatrix = { toNonUnitalRing := instNonUnitalRingWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instNonAssocRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonAssocRing α] : NonAssocRing (WithConv (Matrix m n α))

Equations

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

@[implicit_reducible]

instance instNonAssocCommRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonAssocCommRing α] : NonAssocCommRing (WithConv (Matrix m n α))

Equations

• instNonAssocCommRingWithConvMatrix = { toNonAssocRing := instNonAssocRingWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [Ring α] : Ring (WithConv (Matrix m n α))

Equations

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

@[implicit_reducible]

instance instCommRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [CommRing α] : CommRing (WithConv (Matrix m n α))

Equations

• instCommRingWithConvMatrix = { toRing := instRingWithConvMatrix, mul_comm := ⋯ }

@[implicit_reducible]

instance instStarWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [Star α] : Star (WithConv (Matrix m n α))

Equations

• instStarWithConvMatrix = { star := fun (x : WithConv (Matrix m n α)) => WithConv.toConv (x.ofConv.map star) }

theorem intrinsicStar_def {m : Type u_1} {n : Type u_2} {α : Type u_3} [Star α] (x : WithConv (Matrix m n α)) : star x = WithConv.toConv (x.ofConv.map star)

@[implicit_reducible]

instance instInvolutiveStarWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [InvolutiveStar α] : InvolutiveStar (WithConv (Matrix m n α))

Equations

• instInvolutiveStarWithConvMatrix = { toStar := instStarWithConvMatrix, star_involutive := ⋯ }

@[implicit_reducible]

instance instStarAddMonoidWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [AddMonoid α] [StarAddMonoid α] : StarAddMonoid (WithConv (Matrix m n α))

Equations

• instStarAddMonoidWithConvMatrix = { toInvolutiveStar := instInvolutiveStarWithConvMatrix, star_add := ⋯ }

@[implicit_reducible]

instance instStarMulWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [Mul α] [StarMul α] : StarMul (WithConv (Matrix m n α))

Equations

• instStarMulWithConvMatrix = { toInvolutiveStar := instInvolutiveStarWithConvMatrix, star_mul := ⋯ }

@[implicit_reducible]

instance instStarRingWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [NonUnitalNonAssocSemiring α] [StarRing α] : StarRing (WithConv (Matrix m n α))

Equations

• instStarRingWithConvMatrix = { toStarMul := instStarMulWithConvMatrix, star_add := ⋯ }

instance instSMulCommClassWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} {β : Type u_4} [Monoid β] [MulAction β α] [Mul α] [SMulCommClass β α α] : SMulCommClass β (WithConv (Matrix m n α)) (WithConv (Matrix m n α))

instance instIsScalarTowerWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} {β : Type u_4} [Monoid β] [MulAction β α] [Mul α] [IsScalarTower β α α] : IsScalarTower β (WithConv (Matrix m n α)) (WithConv (Matrix m n α))

@[implicit_reducible]

instance instAlgebraWithConvMatrix {m : Type u_1} {n : Type u_2} {α : Type u_3} {β : Type u_4} [CommSemiring β] [Semiring α] [Algebra β α] : Algebra β (WithConv (Matrix m n α))

Equations

• instAlgebraWithConvMatrix = Algebra.ofModule ⋯ ⋯

theorem Matrix.WithConv.IsIdempotentElem.isSelfAdjoint {m : Type u_1} {n : Type u_2} {α : Type u_3} [Semiring α] [IsLeftCancelMulZero α] [StarRing α] {f : WithConv (Matrix m n α)} (hf : IsIdempotentElem f) : IsSelfAdjoint f

All matrices are intrinsically self-adjoint if they are convolutively idempotent.

def WithConv.matrixToLin'StarAlgEquiv (m : Type u_1) (n : Type u_2) (α : Type u_3) [CommSemiring α] [StarRing α] [Fintype n] [DecidableEq n] : WithConv (Matrix m n α) ≃⋆ₐ[α] WithConv ((n → α) →ₗ[α] m → α)

WithConv (Matrix m n α) is ⋆-algebraically equivalent to WithConv ((n → α) →ₗ m → α).

In particular, the convolutive product on linear maps corresponds to the Hadamard product on matrices and the intrinsic star on linear maps corresponds to taking the star of each element in the matrix.

Equations

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

@[simp]

theorem WithConv.matrixToLin'StarAlgEquiv_apply {m : Type u_1} {n : Type u_2} {α : Type u_3} [CommSemiring α] [StarRing α] [Fintype n] [DecidableEq n] (x : WithConv (Matrix m n α)) : (matrixToLin'StarAlgEquiv m n α) x = toConv (Matrix.toLin' x.ofConv)

@[simp]

theorem WithConv.symm_matrixToLin'StarAlgEquiv_apply {m : Type u_1} {n : Type u_2} {α : Type u_3} [CommSemiring α] [StarRing α] [Fintype n] [DecidableEq n] (x : WithConv ((n → α) →ₗ[α] m → α)) : (matrixToLin'StarAlgEquiv m n α).symm x = toConv (LinearMap.toMatrix' x.ofConv)

theorem Matrix.toLin'_hadamard {m : Type u_1} {n : Type u_2} {α : Type u_3} [CommSemiring α] [Fintype n] [DecidableEq n] (x y : Matrix m n α) : toLin' (x.hadamard y) = (WithConv.toConv (toLin' x) * WithConv.toConv (toLin' y)).ofConv

theorem Matrix.isSymm_iff_intrinsicStar_toLin' {n : Type u_2} {α : Type u_3} [CommSemiring α] [StarRing α] [Fintype n] [DecidableEq n] {A : Matrix n n α} : A.IsSymm ↔ star (WithConv.toConv (toLin' A)) = WithConv.toConv (toLin' (star A))