# Zulip Chat Archive

## 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