Zulip Chat Archive

Stream: maths

Topic: ring hom -> unit group hom?


view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:10):

If f:ABf:A\to B is a homomorphism of commutative rings, do we have the induced map A×B×A^\times\to B^\times plus the proof that it's a group homomorphism? It feels like it should sit in algebra.ring but I can't spot it in there.

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:11):

gaargh is it a theorem about monoids?

view this post on Zulip Chris Hughes (Mar 02 2019 at 13:12):

It's called units.map

view this post on Zulip Chris Hughes (Mar 02 2019 at 13:13):

Probably algebra.group

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:13):

Yes I just found it after you replied. I was looking in the wrong place. Bloody monoids.

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:13):

Thanks by the way.

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:20):

set_option class.instance_max_depth 35

def valfield_units_of_valfield_units_of_eq_supp (h : supp v₁ = supp v₂) :
  units (valuation_field v₁)  units (valuation_field v₂) :=
units.map $ valfield_of_valfield_of_eq_supp h

I have a field hom K -> L and I want a map on the units; I've just had to set_option class.instance_max_depth 35 to make it happen. I don't like it when this starts. Is there some way to persuade type class resolution that life isn't so difficult?

view this post on Zulip Chris Hughes (Mar 02 2019 at 13:21):

I guess maybe just introduce a bunch of instances for valuation_field is a semiring etc.

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:22):

instance (h : supp v₁ = supp v₂) : is_field_hom (valfield_of_valfield_of_eq_supp h) :=
by delta valfield_of_valfield_of_eq_supp; apply_instance

--set_option class.instance_max_depth 35

instance (h : supp v₁ = supp v₂) : is_monoid_hom (valfield_of_valfield_of_eq_supp h) :=
by apply_instance

This fails without the set_option.

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:22):

Getting from a field hom to a monoid hom is too hard for Lean

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:25):

instance (h : supp v₁ = supp v₂) : is_field_hom (valfield_of_valfield_of_eq_supp h) :=
by delta valfield_of_valfield_of_eq_supp; apply_instance

instance meh (h : supp v₁ = supp v₂) : is_ring_hom (valfield_of_valfield_of_eq_supp h) :=
by apply_instance

set_option class.instance_max_depth 44

instance (h : supp v₁ = supp v₂) : is_monoid_hom (valfield_of_valfield_of_eq_supp h) :=
by delta valfield_of_valfield_of_eq_supp; apply_instance

Things are getting worse not better :-/ [the numbers are minimal in each case]

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:25):

I can get back down to 35 if I don't do the delta first before apply_instance

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 13:30):

instance (h : supp v₁ = supp v₂) : is_field_hom (valfield_of_valfield_of_eq_supp h) :=
by delta valfield_of_valfield_of_eq_supp; apply_instance

instance (h : supp v₁ = supp v₂) : is_monoid_hom (valfield_of_valfield_of_eq_supp h) :=
is_semiring_hom.is_monoid_hom (valfield_of_valfield_of_eq_supp h)

OK so there's my fix; just supply the term directly. Now I don't need to change the max depth. Is this good practice or should I be using another solution?


Last updated: May 14 2021 at 20:13 UTC