## Stream: general

### Topic: structure unification fails

#### Yury G. Kudryashov (Apr 25 2020 at 06:15):

Yet another unification problem. I'm trying to define subsemiring reusing submonoid. The following code fails in the definition of comap. It fails to unify different carriers coming from to_submonoid and to_add_submonoid.

import group_theory.submonoid algebra.ring

universes u v

variables {R : Type u} {S : Type v} [semiring R] [semiring S]

set_option old_structure_cmd true

structure subsemiring (R : Type u) [semiring R] extends submonoid R, add_submonoid R

namespace subsemiring

instance : has_coe (subsemiring R) (set R) := ⟨subsemiring.carrier⟩

instance : has_coe_to_sort (subsemiring R) := ⟨Type*, λ S, S.carrier⟩

instance : has_mem R (subsemiring R) := ⟨λ m S, m ∈ (S:set R)⟩

@[simp, norm_cast]
lemma mem_coe {S : subsemiring R} {m : R} : m ∈ (S : set R) ↔ m ∈ S := iff.rfl

@[simp, norm_cast]
lemma coe_coe (s : subsemiring R) : ↥(s : set R) = s := rfl

/-- The preimage of a subsemiring along a monoid homomorphism is a subsemiring. -/
def comap (f : R →+* S) (s : subsemiring S) : subsemiring R :=
{ carrier := (f ⁻¹' s),
.. s.to_submonoid.comap ↑f, .. s.to_add_submonoid.comap ↑f }

end subsemiring


Ping here

#### Yury G. Kudryashov (May 10 2020 at 19:02):

Solved by using (f : R →* S) instead of coe f.

#### Kevin Buzzard (May 10 2020 at 19:12):

the randomness of Lean

#### Kenny Lau (May 10 2020 at 19:17):

magic doesn't work in Lean

#### Chris Hughes (May 10 2020 at 19:19):

It's the wrong sort of arrow right? It should be \u=

#### Yury G. Kudryashov (May 10 2020 at 19:22):

No, it is a conversion to monoid_hom / add_monoid_hom, so it is a correct type of arrow. I guess that Lean failed to figure out the target type of this coercion.

Last updated: May 14 2021 at 13:24 UTC