ring hom -> unit group hom?

Stream: maths

[Kevin Buzzard]

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]

gaargh is it a theorem about monoids?

[Chris Hughes]

It's called units.map

[Chris Hughes]

Probably algebra.group

[Kevin Buzzard]

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

[Kevin Buzzard]

Thanks by the way.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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?