coe_fn

Stream: maths

[Ashvni Narayanan]

I have that for x, an element of an integral domain A, under the localization map f (wrt non-zero divisors of A), f(x) = f(1), and I want to show that x = 1.

x : A,
k' : ⇑(localization_map.to_map (fraction_ring.of A)) x = ⇑(localization_map.to_map (fraction_ring.of A)) 1
⊢ x = 1

I tried

      apply (localization_map.to_map_injective k'),

but I get the error:

type mismatch at application
  localization_map.to_map_injective k'
term
  k'
has type
  ⇑(localization_map.to_map (fraction_ring.of A)) x = ⇑(localization_map.to_map (fraction_ring.of A)) 1
but is expected to have type
  ?m_6.to_map = ?m_7.to_map

Isn't it the same thing? The change tactic does not seem to work. I don't know what coe_fn does.

Any help is appreciated, thank you very much!

[Ashvni Narayanan]

Here is the link to the line : https://github.com/leanprover-community/mathlib/blob/314cdc531d565aa836143d2c44af9d510dda36cd/src/ring_theory/dedekind_domain.lean#L314

[Reid Barton]

I think your question is the same as this one: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/injectivity.20of.20localization.20map/near/209630168

[Kevin Buzzard]

has_coe_to_fun is a typeclass which we attach to things which aren't strictly speaking functions, but which we want to treat as functions anyway. The ⇑ notation is used for this. A great example of this is group homomorphisms (or ring homomorphisms, monoid homomorphisms...). A (bundled) monoid homomorphism in Lean is a package of data: the function, and the proof that it's a monoid homomorphism. Shortly after the definition of monoid_hom in algebra.group.hom there's the line

instance {mM : monoid M} {mN : monoid N} : has_coe_to_fun (M →* N) :=
⟨_, monoid_hom.to_fun⟩

which says "given a monoid hom from M to N, pretend it's a function by (unsurprisingly) using the function which is part of this package". Whenever Lean does this, it will insert that funny little arrow to let you know. This is some subtlety which is essentially completely overlooked by mathematicians in practice, who would argue that the group homomorphism and the underlying function were the same object. Because proofs are "things" in Lean, and in particular things which can get bundled up and attached to other stuff, we see a difference between the function and the group hom; the group hom isn't a function, it's a package. This trick enables us to treat it as a function.

In your example, this to_map thing just unfolds to to_monoid_hom so you have a monoid hom and you're evaluating it at x so you're treating it like a function.

[Kevin Buzzard]

That's what coe_fn is, but I agree with Reid about the error :-)

[Ashvni Narayanan]

Kevin Buzzard said:

has_coe_to_fun is a typeclass which we attach to things which aren't strictly speaking functions, but which we want to treat as functions anyway. The ⇑ notation is used for this. A great example of this is group homomorphisms (or ring homomorphisms, monoid homomorphisms...). A (bundled) monoid homomorphism in Lean is a package of data: the function, and the proof that it's a monoid homomorphism. Shortly after the definition of monoid_hom in algebra.group.hom there's the line

instance {mM : monoid M} {mN : monoid N} : has_coe_to_fun (M →* N) :=
⟨_, monoid_hom.to_fun⟩

which says "given a monoid hom from M to N, pretend it's a function by (unsurprisingly) using the function which is part of this package". Whenever Lean does this, it will insert that funny little arrow to let you know. This is some subtlety which is essentially completely overlooked by mathematicians in practice, who would argue that the group homomorphism and the underlying function were the same object. Because proofs are "things" in Lean, and in particular things which can get bundled up and attached to other stuff, we see a difference between the function and the group hom; the group hom isn't a function, it's a package. This trick enables us to treat it as a function.

In your example, this to_map thing just unfolds to to_monoid_hom so you have a monoid hom and you're evaluating it at x so you're treating it like a function.

Ah ok, I understand. It seems to be similar to .val.

[Ashvni Narayanan]

Reid Barton said:

I think your question is the same as this one: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/injectivity.20of.20localization.20map/near/209630168

Also, this worked! Thank you very much!

[Kevin Buzzard]

If you're talking about how sometimes a pair (val,property) "magically" becomes val even when you don't write .val, this could well also be a coercion -- this time not to a function, so a different kind of up-arrow. There's also a third kind, when you have an object which isn't a type but want to treat it as a type. See Theorem Proving In Lean for more info.

[Ashvni Narayanan]

Will do, thank you!