# Zulip Chat Archive

## Stream: new members

### Topic: misunderstanding coe?

#### Alex Mathers (Mar 30 2020 at 18:04):

I currently have the following two lines of code

instance (R : Type*) [comm_ring R] {A : Type*} [comm_ring A] [algebra R A] : has_coe (subalgebra R A) (set A) := ⟨λ S, S.carrier⟩ instance (R : Type*) [comm_ring R] {A : Type*} [comm_ring A] [algebra R A] (S : subalgebra R A) : is_subring S := S.subring

returning the error message

type mismatch at application is_subring S term S has type subalgebra R A : Type ? but is expected to have type set ?m_1 : Type ?

am I misunderstanding how the coercion should be working?

#### Reid Barton (Mar 30 2020 at 18:20):

It doesn't know yet what `S`

is supposed to be a subring of

#### Alex Mathers (Mar 30 2020 at 18:24):

How can I make it explicit? In the definition of `is_subring`

the ambient ring is not explicit, i.e. it looks like

class is_subring {R : Type*} [ring R] (S : set R) extends is_add_subgroup S, is_submonoid S : Prop.

#### Reid Barton (Mar 30 2020 at 18:24):

I guess you could claim it should be able to infer it from the definition `S.subring`

, but I think the coercion will not fire soon enough for that to work.

#### Reid Barton (Mar 30 2020 at 18:24):

Maybe `is_subring (S : set A)`

for example.

#### Alex Mathers (Mar 30 2020 at 18:25):

I see. That fixes it!

#### Reid Barton (Mar 30 2020 at 18:25):

Just because you have written this first `has_coe`

instance doesn't mean Lean has to use it.

#### Alex Mathers (Mar 30 2020 at 18:25):

is there a simple explanation of what Lean is doing for why it doesn't "use" it?

#### Reid Barton (Mar 30 2020 at 18:26):

It isn't doing anything because it has no way to know what the `?m_1`

is in the error message.

#### Reid Barton (Mar 30 2020 at 18:28):

For example, someone else could add an `instance : has_coe (subalgebra R A) (set R)`

(never mind that it would be nonsense) and then what do you expect to happen?

#### Alex Mathers (Mar 30 2020 at 18:29):

Ah, I see

#### Alex Mathers (Mar 30 2020 at 19:46):

I guess this is related to my previous question: my code

instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] : integral_domain (integral_closure R A) := subring.domain ((integral_closure R A) : set A)

is giving the error message

failed to synthesize type class instance for R : Type ?, _inst_1 : comm_ring R, A : Type ?, _inst_2 : integral_domain A, _inst_3 : algebra R A ⊢ is_subring (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)))

while the code from the previous question is supposed to be giving the instance of `(integral_closure R A) : subalgebra R A`

as a subring of `A`

. How can I "remind" Lean that this does have an instance of `is_subring`

?

#### Alex Mathers (Mar 30 2020 at 19:50):

also it seems from the error message that Lean isn't actually using the coercion I set up, rather I guess it's using the sequence of coercions `subalgebra R A → submodule R A → set A`

. Is there a possibility that this is related to my issue?

#### Kevin Buzzard (Mar 30 2020 at 20:01):

What happens if you remove your coercion and then attempt to coerce anyway?

#### Kevin Buzzard (Mar 30 2020 at 20:02):

If it still works then you should trust that the people who set it up knew what they were doing and don't add the coercion

#### Alex Mathers (Mar 30 2020 at 20:02):

It has the same error message

#### Kevin Buzzard (Mar 30 2020 at 20:02):

Sure

#### Kevin Buzzard (Mar 30 2020 at 20:02):

But I'm asking just about whether the coercion succeeds

#### Kevin Buzzard (Mar 30 2020 at 20:03):

From subalgebra to set

#### Kevin Buzzard (Mar 30 2020 at 20:03):

My guess is that you shouldn't be creating that instance but this is not the answer to your problem

#### Kevin Buzzard (Mar 30 2020 at 20:05):

You should also see if the second instance is solved by `by apply_instance`

#### Kevin Buzzard (Mar 30 2020 at 20:05):

It would surprise me if there were important coercions which were not there already

#### Kevin Buzzard (Mar 30 2020 at 20:06):

The inbuilt coercions might have subtle priorities set, for example

#### Kevin Buzzard (Mar 30 2020 at 20:08):

And what happens if you just remove the explicit coercion to set A in your error? Mathlib might have solved all your problems already

#### Kevin Buzzard (Mar 30 2020 at 20:08):

I'll get to a computer and stop guessing in a sec

#### Kevin Buzzard (Mar 30 2020 at 20:21):

I'm still working out the imports :-(

#### Kevin Buzzard (Mar 30 2020 at 20:22):

I think we should have a bot which just flags all posted code which doesn't actually compile and either kicks the poster or suggests imports and opens which will fix it.

#### Kevin Buzzard (Mar 30 2020 at 20:24):

Right. This succeeds

import ring_theory.algebra ring_theory.subring instance (R : Type*) [comm_ring R] {A : Type*} [comm_ring A] [algebra R A] : has_coe (subalgebra R A) (set A) := by apply_instance

so don't add a new one.

#### Alex Mathers (Mar 30 2020 at 20:24):

sorry for the delay. These imports should be the necessary ones:

import ring_theory.integral_closure import ring_theory.localization import ring_theory.algebra import ring_theory.subring

#### Patrick Massot (Mar 30 2020 at 20:24):

A more realistic idea would be to try someone who could write a web page explaining what is a MWE, so that we can paste a link to that web page each it's needed.

#### Kevin Buzzard (Mar 30 2020 at 20:25):

So do we not have bundled subrings?

#### Kevin Buzzard (Mar 30 2020 at 20:25):

Where are my undergraduates?

#### Alex Mathers (Mar 30 2020 at 20:27):

This is the only definition I see on the subring document:

class is_subring (S : set R) extends is_add_subgroup S, is_submonoid S : Prop.

#### Kevin Buzzard (Mar 30 2020 at 20:27):

Yeah, I think we don't have bundled subrings. Shame. I bet it would be easier with those.

#### Kevin Buzzard (Mar 30 2020 at 20:27):

And this doesn't work:

instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] : integral_domain (integral_closure R A) := by apply_instance

#### Alex Mathers (Mar 30 2020 at 20:30):

Unfortunate :/

#### Kevin Buzzard (Mar 30 2020 at 20:32):

Did you see the Artin-Tate thread?

#### Alex Mathers (Mar 30 2020 at 20:32):

No I didn't

#### Kevin Buzzard (Mar 30 2020 at 20:32):

This whole algebra, subring thing drives me nuts

#### Alex Mathers (Mar 30 2020 at 20:33):

I saw a conversation about difficulties with "triangles" of rings in commutative algebra, not sure if that's the thread you mean but yeah it seems to be an annoying issue

#### Kevin Buzzard (Mar 30 2020 at 20:34):

import ring_theory.integral_closure import ring_theory.localization import ring_theory.algebra import ring_theory.subring instance foo (R : Type*) [comm_ring R] {A : Type*} [comm_ring A] [algebra R A] (S : subalgebra R A) : is_subring (S : set A) := S.subring instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] : integral_domain (integral_closure R A) := @subring.domain A _ _ (foo _ _)

works

#### Kevin Buzzard (Mar 30 2020 at 20:35):

i.e. I just feed it the things it can't find

#### Alex Mathers (Mar 30 2020 at 20:36):

Nice! what purpose does the `@`

character serve?

#### Kevin Buzzard (Mar 30 2020 at 20:36):

instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] : integral_domain (integral_closure R A) := @subring.domain A _ (integral_closure R A) _

`@`

means "forget `{}`

and `[]`

and just tell me every input"

#### Alex Mathers (Mar 30 2020 at 20:37):

Ohh that makes sense

#### Kevin Buzzard (Mar 30 2020 at 20:37):

It's exactly the same problem as before. You want to prove `integral_domain (integral_closure R A)`

and you want to use `subring.domain`

.

#check @subring.domain /- subring.domain : Π {D : Type u_1} [_inst_3 : integral_domain D] (S : set D) [_inst_4 : is_subring S], integral_domain ↥S -/

#### Kevin Buzzard (Mar 30 2020 at 20:39):

Lean asks you for `S`

which is in your case some kind of coercion of `integral_closure R A`

to a set, i.e. to a term of type `set D`

for some `D`

, but Lean doesn't have a clue what `D`

is.

#### Kevin Buzzard (Mar 30 2020 at 20:39):

If it knew it had to find a coercion to `set A`

it could do it (indeed, my second solution is doing just that).

#### Kevin Buzzard (Mar 30 2020 at 20:41):

But until you tell it it's looking for a coercion to `set ?m_1`

and it can't find one for some reason.

#### Alex Mathers (Mar 30 2020 at 20:42):

I see. so by using @ you are allowed to enter the first implicit argument A which I guess basically tells Lean that we are meant to consider `integral_closure R A`

as an element of `set A`

, then it finds the previously defined coercion to do this on its own

#### Kevin Buzzard (Mar 30 2020 at 20:45):

Exactly. And using my new toy

set_option trace.type_context.is_def_eq true set_option trace.type_context.is_def_eq_detail true instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] : integral_domain (integral_closure R A) := subring.domain (integral_closure R A) -- fails

we can see from the debugging output that indeed the unifier is failing to find the coercion when the metavariable is in place:

[type_context.is_def_eq_detail] [1]: subalgebra R A =?= set ?m_1 [type_context.is_def_eq_detail] unfold right: set [type_context.is_def_eq_detail] [2]: subalgebra R A =?= ?m_1 → Prop [type_context.is_def_eq_detail] on failure: subalgebra R A =?= ?m_1 → Prop [type_context.is_def_eq] subalgebra R A =?= set ?m_1 ... failed (approximate mode)

#### Reid Barton (Mar 30 2020 at 20:47):

Is that failing to find a coercion or simply checking that the two sides are not defeq (without a coercion)?

#### Kevin Buzzard (Mar 30 2020 at 20:48):

Oh man, looking at this debugging output it even seems to get so close!

[type_context.is_def_eq_detail] [7]: has_coe_to_sort.coe (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))) =?= {x // x ∈ ?m_2} [type_context.is_def_eq_detail] [8]: (λ (s : set A), {x // x ∈ s}) (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))) =?= {x // x ∈ ?m_2} [type_context.is_def_eq_detail] after whnf_core: {x // x ∈ has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))} =?= {x // x ∈ ?m_2} [type_context.is_def_eq_detail] process_assignment ?m_1 := A [type_context.is_def_eq_detail] assign: ?m_1 := A [type_context.is_def_eq_detail] [9]: x ∈ has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= x ∈ ?m_2 [type_context.is_def_eq_detail] process_assignment ?m_1 := has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) [type_context.is_def_eq_detail] [10]: set ?m_1 =?= set A [type_context.is_def_eq_detail] assign: ?m_1 := has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) [type_context.is_def_eq] integral_domain ↥(integral_closure R A) =?= integral_domain ↥?m_2 ... success (approximate mode)

#### Kevin Buzzard (Mar 30 2020 at 20:49):

I don't know how to read these logs, I only started looking at them today.

#### Kevin Buzzard (Mar 30 2020 at 20:51):

https://gist.github.com/kbuzzard/b8c86cfd46b5253c4888979078ba1f00

Last updated: May 11 2021 at 12:15 UTC