Skip to content

Instantly share code, notes, and snippets.

@eric-wieser
Last active January 28, 2021 09:59
Show Gist options
  • Save eric-wieser/66022bcfd708091799bc86e80404b504 to your computer and use it in GitHub Desktop.
Save eric-wieser/66022bcfd708091799bc86e80404b504 to your computer and use it in GitHub Desktop.
Failed to synthesize typeclass instance

The error is

failed to synthesize type class instance for
A : Type u_1,
_inst_1 : semiring A,
ι : Type u_2,
_inst_2 : add_comm_monoid ι,
_inst_3 : decidable_eq ι,
carriers : ι → add_submonoid A,
_inst_4 : semiring_add_gradation carriers,
x : ⨁ (i : ι), ↥(carriers i),
_inst : Π (i : ι) (x : (λ (i : ι), ↥(carriers i)) i), decidable (x ≠ 0)
⊢ Π (i : ι) (x : (λ (i : ι), ↥(carriers i)) i), decidable (x ≠ 0)
import algebra.direct_sum
import ring_theory.subsemiring
variables
{A : Type*} [semiring A]
{ι : Type*} [add_comm_monoid ι] [decidable_eq ι]
namespace direct_sum
class semiring_add_gradation (carriers : ι → add_submonoid A) :=
(one_mem : (1 : A) ∈ carriers 0)
(mul_mem : ∀ {i j} (gi : carriers i) (gj : carriers j), (gi * gj : A) ∈ carriers (i + j))
variables (carriers : ι → add_submonoid A) [semiring_add_gradation carriers]
open_locale direct_sum
/-! First, define multiplication and 1 on the individual carriers, and show they form a
heq-monoid-/
def hmul {i j} : carriers i →+ carriers j →+ carriers (i + j) :=
{ to_fun := λ a,
{ to_fun := λ b, ⟨(a * b : A), semiring_add_gradation.mul_mem a b⟩,
map_add' := λ _ _, subtype.ext (mul_add _ _ _),
map_zero' := subtype.ext (mul_zero _), },
map_add' := λ _ _, add_monoid_hom.ext $ λ _, subtype.ext (add_mul _ _ _),
map_zero' := add_monoid_hom.ext $ λ _, subtype.ext (zero_mul _) }
def hone : carriers 0 := ⟨1, semiring_add_gradation.one_mem⟩
lemma hone_hmul {i} (a : carriers i) : hmul carriers (hone carriers) a == a :=
begin
rw subtype.heq_iff_coe_eq,
{ exact one_mul _ },
{ exact λ x, (zero_add i).symm ▸ iff.rfl, }
end
lemma hmul_hone {i} (a : carriers i) : hmul carriers a (hone carriers) == a :=
begin
rw subtype.heq_iff_coe_eq,
exact mul_one _,
exact λ x, (add_zero i).symm ▸ iff.rfl,
end
lemma hmul_assoc {i j k} (a : carriers i) (b : carriers j) (c : carriers k) :
hmul carriers (hmul carriers a b) c == hmul carriers a (hmul carriers b c) :=
begin
rw subtype.heq_iff_coe_eq,
exact mul_assoc _ _ _,
exact λ x, (add_assoc i j k).symm ▸ iff.rfl,
end
/-! Next, compose them with `direct_sum.of`. -/
def mul_def' {i j} : carriers i →+ carriers j →+ ⨁ i, carriers i :=
{ to_fun := λ a,
add_monoid_hom.comp_hom (direct_sum.of (λ i, carriers i) $ i + j) (hmul carriers a),
map_add' := λ a b, by simp only [add_monoid_hom.map_add],
map_zero' := by simp only [add_monoid_hom.map_zero] }
def one_def' : ⨁ i, carriers i := direct_sum.of (λ i, carriers i) 0 (hone carriers)
instance : has_one (⨁ i, carriers i) :=
{ one := direct_sum.of (λ i, carriers i) 0 (hone carriers)}
instance : has_mul (⨁ i, carriers i) :=
{ mul := λ a b, begin
refine direct_sum.to_add_monoid (λ j,
direct_sum.to_add_monoid (λ i,
_
) a
) b,
exact mul_def' carriers,
end }
/-! Now the fun begins! -/
lemma one_mul (x : ⨁ i, carriers i) : 1 * x = x :=
begin
unfold has_one.one has_mul.mul one_def' mul_def',
simp only [add_monoid_hom.coe_mk, to_add_monoid_of, add_monoid_hom.comp_hom_apply_apply],
rw [direct_sum.to_add_monoid, dfinsupp.lift_add_hom_apply],
haveI : Π (i : ι) (x : (λ i, ↥(carriers i)) i), decidable (x ≠ 0) := λ i x, classical.dec _,
rw @dfinsupp.sum_add_hom_apply ι (λ i, ↥(carriers i)) _ _ _ ‹_›,
simp [add_monoid_hom.coe_comp, function.comp, direct_sum.of],
convert dfinsupp.sum_single,
ext1 i, ext1 xi,
congr,
exact zero_add _,
exact hone_hmul _ xi,
assumption
end
lemma mul_one (x : ⨁ i, carriers i) : x * 1 = x :=
begin
unfold has_one.one has_mul.mul one_def' mul_def',
simp only [add_monoid_hom.coe_mk, to_add_monoid_of, add_monoid_hom.comp_hom_apply_apply],
rw [direct_sum.to_add_monoid, dfinsupp.lift_add_hom_apply],
haveI : Π (i : ι) (x : (λ i, ↥(carriers i)) i), decidable (x ≠ 0) := λ i x, classical.dec _,
rw @dfinsupp.sum_add_hom_apply ι (λ i, ↥(carriers i)) _ _ _ ‹_›,
simp [add_monoid_hom.coe_comp, function.comp, direct_sum.of, dfinsupp.single_add_hom,
add_monoid_hom.coe_dfinsupp_sum],
resetI,
rw add_monoid_hom.coe_dfinsupp_sum x,
-- dunfold add_monoid_hom.comp,
-- convert dfinsupp.sum_single,
-- simp [add_monoid_hom.dfinsupp_sum_apply],
-- ext1 i, ext1 xi,
-- congr,
-- exact zero_add _,
-- have := hone_hmul _ xi,
-- exact this,
-- assumption
end
#print direct_sum.has_mul
#check dfinsupp.sum
end direct_sum
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment