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

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

Sure

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

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


Unfortunate :/

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

Did you see the Artin-Tate thread?

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