Stream: maths

Topic: ring hom -> unit group hom?

Kevin Buzzard (Mar 02 2019 at 13:10):

If $f:A\to B$ is a homomorphism of commutative rings, do we have the induced map $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.

Kevin Buzzard (Mar 02 2019 at 13:11):

gaargh is it a theorem about monoids?

Chris Hughes (Mar 02 2019 at 13:12):

It's called units.map

Chris Hughes (Mar 02 2019 at 13:13):

Probably algebra.group

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.

Kevin Buzzard (Mar 02 2019 at 13:13):

Thanks by the way.

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?

Chris Hughes (Mar 02 2019 at 13:21):

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

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.

Kevin Buzzard (Mar 02 2019 at 13:22):

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

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]

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

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