gpow on `matrix n n K`

Stream: general

[Yakov Pechersky]

Thanks to linear_algebra.matrix.nonsingular_inverse, we have a has_inv (matrix n n K). However, that does not provide a has_pow (matrix n n K) int. What is the right way to provide that? Directly? What's the correct algebraic structure to give here?

[Eric Wieser]

I think that instance requires a group

[Eric Wieser]

There's also fpow instead of gpow which requires a group_with_zero

[Yakov Pechersky]

You can define it by casing on the int, and for things that are truly invertible, (units.coe_hom _).map_pow will work on the two cases. But it monoid_hom.map_gpow won't work, of course, due to the restriction to groups...

[Yakov Pechersky]

Can one give matrix n n K group_with_zero then?

[Eric Wieser]

Only when n=unit

[Eric Wieser]

There are non-invertible non-zero matrices

[Yakov Pechersky]

I see -- the issue is evident below

import linear_algebra.matrix.nonsingular_inverse

open_locale matrix
open matrix

variables {n α : Type*} [fintype n] [decidable_eq n] [comm_ring α]

noncomputable instance : div_inv_monoid (matrix n n α) :=
{ ..matrix.has_inv,
  ..(show monoid (matrix n n α), by apply_instance) }

lemma matrix.inv_def (M : matrix n n α) : M⁻¹ = nonsing_inv M := rfl

lemma matrix.nonsing_inv_of_not_is_unit {M : matrix n n α} (h : ¬ is_unit M) :
  M⁻¹ = 0 :=
begin
  rw is_unit_iff_is_unit_det at h,
  simp [matrix.inv_def, nonsing_inv, h]
end

lemma matrix.inv_zero [nontrivial n] [nontrivial α] : (0 : matrix n n α)⁻¹ = 0 :=
matrix.nonsing_inv_of_not_is_unit (by simp)

noncomputable instance [nontrivial n] [nontrivial α] : group_with_zero (matrix n n α) :=
{ zero_mul := λ _, matrix.zero_mul _,
  mul_zero := λ _, matrix.mul_zero _,
  inv_zero := matrix.inv_zero,
  mul_inv_cancel := λ M hM, sorry, -- if `¬ is_unit M` then `0 = 1`
  ..(show has_zero (matrix n n α), by apply_instance),
  ..(show nontrivial (matrix n n α), by apply_instance),
  ..(show div_inv_monoid (matrix n n α), by apply_instance) }

[Kevin Buzzard]

Square matrices over a semiring are a monoid with zero

[Yury G. Kudryashov]

You can try to generalize the gpow instance to a monoid+has_inv but it won't have many nice properties.

[Yury G. Kudryashov]

So, it might be better to copy definition from fpow or gpow, then prove lemmas that are true for matrices (or operators).

[Kevin Buzzard]

Square matrices over a field shouldn't really have an inv, because of matrices like $\begin{pmatrix}01\\00\end{pmatrix}$.

[Anne Baanen]

My proposal was to define has_inv as (some choice of) pseudoinverse, which would give sensible results for a few more matrices. But that might actually have less nice properties than the nonsingular inverse.

[Yakov Pechersky]

Are there any lemmas about monoid_with_zero that are worth having for matrices? I can do the specialized fpow approach for matrices.

[Eric Wieser]

I assume you mean group_with_zero, monoid_with_zero is already true for matrices

[Yakov Pechersky]

Sorry, I was trying to parse Kevin's statement

[Kevin Buzzard]

"Monoids with zero shouldn't have an inv"