mul_action and has_scalar diamond

Stream: general

[Yakov Pechersky]

Consider the following lemma. At the end, I have a diamond on two smul instances. What's the right way to avoid these?

import linear_algebra.matrix.nonsingular_inverse

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

open matrix

lemma det_eq_elem_of_subsingleton' [subsingleton n] (A : matrix n n α) (k : n) :
  det A = A k k := sorry

lemma adjugate_subsingleton' [subsingleton n] (A : matrix n n α) : adjugate A = 1 := sorry

lemma adjugate_adjugate' [subsingleton n] (A : matrix n n α) (h : is_unit A.det) :
  A.adjugate.adjugate = h.unit ^ ((fintype.card n : ℤ) - 2) • A :=
begin
  rw adjugate_subsingleton',
  ext i j,
  have hj : i = j := subsingleton.elim i j,
  subst hj,
  have : fintype.card n = 1,
  { rw fintype.card_eq_one_iff,
    use i,
    simp },
  have hd : A i i = h.unit,
  { rw [h.unit_spec, det_eq_elem_of_subsingleton' _ i] },
  have hc : h.unit⁻¹ • h.unit = 1,
  { simp },
  rw [pi.smul_apply, pi.smul_apply, hd, this, gpow_sub, gpow_bit0,
      ←units.coe_smul],
  simp only [mul_inv_rev, mul_inv_cancel_comm_assoc, gpow_one, int.coe_nat_zero, int.coe_nat_succ,
              one_apply_eq, zero_add],
  convert units.ext_iff.mp hc.symm,
  sorry -- diamond here
end

[Yakov Pechersky]

In particular, I made the hc hypothesis because smul_eq_mul wouldn't work.

[Yakov Pechersky]

One way, of course, is to avoid using h.unit in the lemma statement, and have only nat powers.

[Eric Wieser]

Can you reduce this any further?

[Eric Wieser]

This diamond is weird - if I do local attribute [ext] has_scalar, then I can close your goal with ext, refl

[Eric Wieser]

Which suggests that the two smul actions are defeq

[Eric Wieser]

Ah, here's the MWE:

import group_theory.group_action.units

example {α : Type*} [comm_monoid α] :
  (units.mul_action' : mul_action (units α) (units α)) = monoid.to_mul_action _ :=
rfl -- fails

attribute [ext] mul_action has_scalar

example {α : Type*} [comm_monoid α] :
  (units.mul_action' : mul_action (units α) (units α)) = monoid.to_mul_action _ :=
begin
  ext,
  refl,
end  -- succeeds

[Eric Wieser]

Ah, and this reveals what's going wrong:

example {α : Type*} [comm_monoid α] :
  (units.mul_action' : mul_action (units α) (units α)) = monoid.to_mul_action (units α) :=
begin
  dunfold monoid.to_mul_action units.mul_action',
  congr,
  { dunfold has_mul.mul mul_one_class.mul monoid.mul div_inv_monoid.mul ,
    dunfold group.mul,
    dsimp [units.smul_def],
    dunfold has_inv.inv div_inv_monoid.inv group.inv,
    dsimp only,
    unfold_coes,
    ext : 2,
    dsimp only,
    -- {val := x.val * x_1.val, inv := x.inv * x_1.inv, val_inv := _, inv_val := _} =
    -- {val := x.val * x_1.val, inv := x_1.inv * x.inv, val_inv := _, inv_val := _}
    sorry
    },
  sorry,
  sorry
end

The actions agree on val, but disagree on inv

[Eric Wieser]

So src#units.mul_action' is at fault here

[Yakov Pechersky]

What would the inv be then for that definition?

[Eric Wieser]

I think it should be using a right action, opposite.op r⁻¹ • m⁻¹

[Eric Wieser]

I can investigate tomorrow

[Eric Wieser]

I've almost fixed this, but I think the typeclass I need doesn't exist. What additional assumptions does the sorry below need?

import group_theory.group_action.units
import algebra.opposites

-- turn off the bad instance we're tring to fix
local attribute [-instance] units.mul_action'

namespace units

open opposite

variables {G M α : Type*}

/-! Right actions on units - I can't think if a good way to inherit these from anything we already
have -/

instance units.op_has_scalar [monoid M] [has_scalar Mᵒᵖ α] : has_scalar (units M)ᵒᵖ α :=
{ smul := λ um a, op (um.unop : M) • a }

instance units.op_mul_action [monoid M] [mul_action Mᵒᵖ α] : mul_action (units M)ᵒᵖ α :=
{ smul := λ um a, op (um.unop : M) • a,
  one_smul := (one_smul Mᵒᵖ : _),
  mul_smul := λ um un, mul_smul (op (um.unop : M)) (op (un.unop : M)), }

/-! Notation just to make the intent behind the sorried lemma clear. -/

notation g` •> `:73 m:72 := g • m
notation m` <• `:73 g:72 := opposite.op g • m

variables [group G] [monoid M] [mul_action G M] [mul_action Gᵒᵖ M]

lemma smul_mul_inv_smul (g : G) (m : units M) : (g •> (m : M)) * (↑(m⁻¹) <• g⁻¹) = 1 :=
sorry

lemma inv_smul_mul_smul (g : G) (m : units M) : (↑(m⁻¹) <• g⁻¹) * (g •> (m : M)) = 1 :=
opposite.op_injective $ smul_mul_inv_smul g (units.op_equiv.symm (op m))

/-- A fixed version of `units.mul_action'`. -/
instance better_mul_action' : mul_action G (units M) :=
{ smul := λ g m, ⟨g •> (m : M), ↑(m⁻¹) <• g⁻¹, smul_mul_inv_smul _ _, inv_smul_mul_smul _ _⟩,
  one_smul := λ m, units.ext $ one_smul _ _,
  mul_smul := λ g₁ g₂ m, units.ext $ mul_smul _ _ _ }

-- note: now only needs monoid not comm_monoid!
example {α : Type*} [monoid α] :
  (units.better_mul_action' : mul_action (units α) (units α)) = monoid.to_mul_action _ :=
rfl -- ok, no diamond any more

end units

[Eric Wieser]

I think the sorry can be expanded as:

lemma smul_mul_inv_smul [is_scalar_tower G M M] (g : G) (m : units M)
  : (g •> (m : M)) * (↑(m⁻¹) <• g⁻¹) = 1 :=
calc (g •> (m : M)) * (↑(m⁻¹) <• g⁻¹)
    = g •> ((m : M) * (↑(m⁻¹) <• g⁻¹)) : by rw [←smul_eq_mul, ←smul_eq_mul, smul_assoc]
... = g •> ((m : M) * ↑(m⁻¹)) <• g⁻¹ : by {
    congr' 1,
    rw [←op_smul_eq_mul, ←op_smul_eq_mul],
    sorry -- we need `is_scalar_tower` for right actions
    }
... = g •> 1 <• g⁻¹ : by rw units.mul_inv
... = (g * g⁻¹) •> 1 : sorry  -- `smul_comm_class` is too strong here
... = 1 : by rw [mul_right_inv, one_smul]

[Yakov Pechersky]

Does <-units.coe_mul help here?

[Eric Wieser]

I doubt it, that step is folded into the by rw units.mul_inv

[Eric Wieser]

I think the statement at the first sorry is a general statement of m1 * (m2 <• g2) = (m1 * m2) <• g2 which may or may not be something that can be expressed with existing typeclasses.

[Eric Wieser]

It follows from docs#smul_mul_assoc and docs#mul_smul_comm, but the requirements for those lemmas are stricter than we need as they go through the intermediate state m1 * (m2 <• g2) = (m1 <• g2) * m2 which isn't true when M and G are the same non-commutative monoid (and therefore (<•) = (*)).

[Yakov Pechersky]

Here is another related clash:

import linear_algebra.matrix.determinant
import data.polynomial.monic

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

open polynomial matrix finset equiv.perm

lemma coeff_finset_prod_zero {β : Type*} (f : β → polynomial α) (l : finset β) :
  coeff (l.prod f) 0 = l.prod (λ p, coeff (f p) 0) :=
let g : polynomial α →+* α := ring_hom.mk (λ p : polynomial α, coeff p 0)
  (by simp) (by simp) (by simp) (by simp) in g.map_prod f l

lemma coeff_finset_sum_zero {β : Type*} (f : β → polynomial α) (l : finset β) :
  coeff (l.sum f) 0 = l.sum (λ p, coeff (f p) 0) :=
let g : polynomial α →+* α := ring_hom.mk (λ p : polynomial α, coeff p 0)
  (by simp) (by simp) (by simp) (by simp) in g.map_sum f l

lemma coeff_det_X_add_C_zero (A B : matrix n n α) :
  coeff (det ((X : polynomial α) • C.map_matrix A + (C.map_matrix B))) 0 =
    det B :=
begin
  rw [det_apply, coeff_finset_sum_zero, det_apply],
  refine finset.sum_congr rfl _,
  simp only [algebra.id.smul_eq_mul, mem_univ, ring_hom.map_matrix_apply, forall_true_left,
             map_apply, dmatrix.add_apply, pi.smul_apply],
  intros g,
  convert coeff_smul (sign g) _ 0, -- really this should be a rewrite
  { sorry },                       -- if not for this diamond
  { rw coeff_finset_prod_zero,
    refine finset.prod_congr rfl _,
    simp },
end

[Eric Wieser]

(just to check: docs#polynomial.coeff_smul)

[Eric Wieser]

What's the type of the term in the strings m diamond?

[Eric Wieser]

Ah, discord clarifies the diamond is docs#units.has_scalar (introduced in #7438) vs docs#polynomial.has_scalar