diamond

Stream: new members

[Yakov Pechersky]

On my branch#pechersky/ordered-module-smul, I am hitting a diamond on smul actions on order_dual. But it seems that the data (the actual smul) is the same. What's going on here? Is this another instance of how use of defeq of R and order_dual R causes issues later on?

import algebra.module.ordered

section semiring

variables (k E : Type*)
  [hr : semiring k] [hc : ordered_add_comm_group E] [hm : module k E]

def LHS :=
  (@order_dual.smul_with_zero k E hr
    (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid E
      (@ordered_add_comm_group.to_ordered_cancel_add_comm_monoid E hc))
    (@mul_action_with_zero.to_smul_with_zero k E
      (@semiring.to_monoid_with_zero k hr)
      (@add_zero_class.to_has_zero E
          (@add_monoid.to_add_zero_class E
            (@add_comm_monoid.to_add_monoid E
                (@ordered_add_comm_monoid.to_add_comm_monoid E
                  (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid E
                      (@ordered_add_comm_group.to_ordered_cancel_add_comm_monoid E hc))))))
      (@module.to_mul_action_with_zero k E hr
          (@add_comm_group.to_add_comm_monoid E (@ordered_add_comm_group.to_add_comm_group E hc))
          hm)))

def RHS :=
  (@mul_action_with_zero.to_smul_with_zero k (order_dual E)
      (@semiring.to_monoid_with_zero k hr)
      (@add_zero_class.to_has_zero (order_dual E)
        (@add_monoid.to_add_zero_class (order_dual E)
            (@add_comm_monoid.to_add_monoid (order_dual E)
              (@ordered_add_comm_monoid.to_add_comm_monoid (order_dual E)
                  (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid (order_dual E)
                    (@ordered_add_comm_group.to_ordered_cancel_add_comm_monoid (order_dual E)
                        (@order_dual.ordered_add_comm_group E hc)))))))
      (@module.to_mul_action_with_zero k (order_dual E) hr
        (@add_comm_group.to_add_comm_monoid (order_dual E)
            (@ordered_add_comm_group.to_add_comm_group (order_dual E)
              (@order_dual.ordered_add_comm_group E hc)))
        (@order_dual.module k E hr
            (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid E
              (@ordered_add_comm_group.to_ordered_cancel_add_comm_monoid E hc))
            hm)))

#check @LHS k E hr hc hm
/-
LHS k E : smul_with_zero k (order_dual E)
-/

#check @RHS k E hr hc hm
/-
RHS k E : smul_with_zero k (order_dual E)
-/

attribute [ext] smul_with_zero has_scalar

lemma fails : @LHS k E hr hc hm = @RHS k E hr hc hm := rfl

lemma succeed : @LHS k E hr hc hm = @RHS k E hr hc hm :=
begin
  ext1,
  ext1,
  refl
end

end semiring

[Yakov Pechersky]

Yes, seems so. Being less defeq-y, one avoids it. #8930, #8938