Zulip Chat Archive

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

Yury G. Kudryashov (May 10 2020 at 18:58):

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: Aug 03 2023 at 10:10 UTC