misunderstanding coe?

Stream: new members

[Alex Mathers]

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]

It doesn't know yet what S is supposed to be a subring of

[Alex Mathers]

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]

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]

Maybe is_subring (S : set A) for example.

[Alex Mathers]

I see. That fixes it!

[Reid Barton]

Just because you have written this first has_coe instance doesn't mean Lean has to use it.

[Alex Mathers]

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

[Reid Barton]

It isn't doing anything because it has no way to know what the ?m_1 is in the error message.

[Reid Barton]

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]

Ah, I see

[Alex Mathers]

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]

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]

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

[Kevin Buzzard]

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]

It has the same error message

[Kevin Buzzard]

Sure

[Kevin Buzzard]

But I'm asking just about whether the coercion succeeds

[Kevin Buzzard]

From subalgebra to set

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The inbuilt coercions might have subtle priorities set, for example

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

I'm still working out the imports :-(

[Kevin Buzzard]

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]

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]

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]

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]

So do we not have bundled subrings?

[Kevin Buzzard]

Where are my undergraduates?

[Alex Mathers]

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]

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

[Kevin Buzzard]

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]

Unfortunate :/

[Kevin Buzzard]

Did you see the Artin-Tate thread?

[Alex Mathers]

No I didn't

[Kevin Buzzard]

This whole algebra, subring thing drives me nuts

[Alex Mathers]

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]

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]

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

[Alex Mathers]

Nice! what purpose does the @ character serve?

[Kevin Buzzard]

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]

Ohh that makes sense

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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