Zulip Chat Archive

Stream: maths

Topic: coe_fn


view this post on Zulip Ashvni Narayanan (Oct 21 2020 at 20:54):

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!

view this post on Zulip Ashvni Narayanan (Oct 21 2020 at 20:55):

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

view this post on Zulip Reid Barton (Oct 21 2020 at 20:56):

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

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 21:08):

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.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 21:08):

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

view this post on Zulip Ashvni Narayanan (Oct 21 2020 at 21:20):

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.

view this post on Zulip Ashvni Narayanan (Oct 21 2020 at 21:20):

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!

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 21:22):

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.

view this post on Zulip Ashvni Narayanan (Oct 21 2020 at 21:24):

Will do, thank you!


Last updated: May 12 2021 at 08:14 UTC