Zulip Chat Archive

Stream: new members

Topic: Coercion not properly recognized


view this post on Zulip Nicolò Cavalleri (Aug 01 2020 at 10:18):

I can't make the following example work with coercions (i.e. by removing to_fun). Does anybody have tips?

import ring_theory.algebra

open algebra

variables (R : Type*) (A : Type*) [comm_semiring R] [semiring A] [algebra R A]
  (M : Type*) [add_comm_monoid M] [semimodule A M]

def transitive_scalar (R : Type*) (A : Type*) (M : Type*)
  [comm_semiring R] [semiring A] [algebra R A]
  [add_comm_monoid M] [semimodule A M] : has_scalar R M :=
{ smul := λ r m, ((algebra_map R A).to_fun r)  m, }

def transitive_module (R : Type*) (A : Type*) (M : Type*)
  [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [semimodule A M] :
  semimodule R M :=
{ smul := λ r m, ((algebra_map R A).to_fun r)  m, /- if I remove to_fun it does not work. Why? -/
  smul_add := λ r x y, smul_add _ _ _,
  smul_zero := λ r, smul_zero _,
  zero_smul := λ r, by simp only [(algebra_map R A).map_zero']; exact zero_smul _ _,
  one_smul := λ x, by simp only [(algebra_map R A).map_one']; exact one_smul _ _,
  mul_smul := λ r s x, by simp only [(algebra_map R A).map_mul']; exact mul_smul _ _ _,
  add_smul := λ r s x, by simp only [(algebra_map R A).map_add']; exact add_smul _ _ _, }

view this post on Zulip Kenny Lau (Aug 01 2020 at 10:23):

perche le versione con ' non devono stare usate

import ring_theory.algebra

open algebra

variables (R : Type*) (A : Type*) [comm_semiring R] [semiring A] [algebra R A]
  (M : Type*) [add_comm_monoid M] [semimodule A M]

def transitive_scalar (R : Type*) (A : Type*) (M : Type*)
  [comm_semiring R] [semiring A] [algebra R A]
  [add_comm_monoid M] [semimodule A M] : has_scalar R M :=
{ smul := λ r m, ((algebra_map R A) r)  m, }

def transitive_module (R : Type*) (A : Type*) (M : Type*)
  [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [semimodule A M] :
  semimodule R M :=
{ smul := λ r m, ((algebra_map R A) r)  m, /- if I remove to_fun it does not work. Why? -/
  smul_add := λ r x y, smul_add _ _ _,
  smul_zero := λ r, smul_zero _,
  zero_smul := λ r, by simp only [(algebra_map R A).map_zero]; exact zero_smul _ _,
  one_smul := λ x, by simp only [(algebra_map R A).map_one]; exact one_smul _ _,
  mul_smul := λ r s x, by simp only [(algebra_map R A).map_mul]; exact mul_smul _ _ _,
  add_smul := λ r s x, by simp only [(algebra_map R A).map_add]; exact add_smul _ _ _, }

view this post on Zulip Kenny Lau (Aug 01 2020 at 10:23):

(algebra_map R A).map_one non (algebra_map R A).map_one'

view this post on Zulip Kenny Lau (Aug 01 2020 at 10:24):

#check ring_hom.map_one -- ring_hom.map_one : ∀ (f : ?M_1 →+* ?M_2), ⇑f 1 = 1
#check ring_hom.map_one' -- ring_hom.map_one' : ∀ (c : ?M_1 →+* ?M_2), c.to_fun 1 = 1

view this post on Zulip Kenny Lau (Aug 01 2020 at 10:28):

@Nicolò Cavalleri

view this post on Zulip Nicolò Cavalleri (Aug 01 2020 at 11:27):

Ok grazie! Moreover I also cannot manage to substitute smul := ..., with ..transitive_scalar R A M, you know why?

view this post on Zulip Kenny Lau (Aug 01 2020 at 12:42):

@Gabriel Ebner #mwe

class foo :=
(foo : )

class bar extends foo :=
(bar : foo = 0)

axiom one_eq_zero : 1 = 0

def foo_instance : foo :=
{ foo := 1 }

def bar_instance₁ : bar :=
{ foo := 1,
  bar := by simp only [one_eq_zero] } -- works

def bar_instance₂ : bar :=
{ bar := by simp only [one_eq_zero],  -- ⊢ foo.foo = 0
  .. foo_instance }

view this post on Zulip Kenny Lau (Aug 01 2020 at 12:50):

@Nicolò Cavalleri these nested instances can have unpredictable behaviour, so the safest way is to do this:

import ring_theory.algebra

open algebra

variables (R : Type*) (A : Type*) [comm_semiring R] [semiring A] [algebra R A]
  (M : Type*) [add_comm_monoid M] [semimodule A M]

def transitive_scalar (R : Type*) (A : Type*) (M : Type*)
  [comm_semiring R] [semiring A] [algebra R A]
  [add_comm_monoid M] [semimodule A M] : has_scalar R M :=
{ smul := λ r m, algebra_map R A r  m, }

open ring_hom
def transitive_module (R : Type*) (A : Type*) (M : Type*)
  [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [semimodule A M] :
  semimodule R M :=
{ smul_add := λ r x y, smul_add _ _ _,
  smul_zero := λ r, smul_zero _,
  zero_smul := λ x, show algebra_map R A 0  x = 0, by rw [map_zero, zero_smul],
  one_smul := λ x, show algebra_map R A 1  x = x, by rw [map_one, one_smul],
  mul_smul := λ r s x, show algebra_map R A (r * s)  x =
    algebra_map R A r  algebra_map R A s  x, by rw [map_mul, mul_smul],
  add_smul := λ r s x, show algebra_map R A (r + s)  x =
    algebra_map R A r  x + algebra_map R A s  x, by rw [map_add, add_smul],
  .. transitive_scalar R A M }

view this post on Zulip Kenny Lau (Aug 01 2020 at 12:50):

i.e. use show

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 14:27):

Ok thanks! And does anybody know why lean does not recognize automatically this coercion:

import ring_theory.algebra

open algebra ring_hom

variables (R : Type*) (A : Type*) [comm_semiring R] [comm_semiring A] [algebra R A]
  (M : Type*) [add_comm_monoid M] [semimodule A M]

class compatible_semimodule (R : Type*) (A : Type*) [comm_semiring R] [semiring A]
  [algebra R A] (M : Type*) [add_comm_monoid M] [semimodule A M] [semimodule R M] :=
(compatible {r : R} {m : M} : r  m = ((algebra_map R A) r)  m)

structure derivation [semimodule A M] [semimodule R M] [compatible_semimodule R A M]
  extends A [R] M :=
(leibniz' (a b : A) : to_fun (a * b) = a  to_fun b + b  to_fun a)

section

variables {R} {A} {M} [semimodule R M] [compatible_semimodule R A M]

namespace derivation

instance : has_coe_to_fun (derivation R A M) := ⟨_, λ D, D.to_linear_map.to_fun

lemma one_mul_one (M : Type*) [monoid M] : 1 * 1 = 1 := one_mul 1

section
variables {R A} (D : derivation R A M) (r : R) (a b : A)
@[simp] lemma map_algebra_map : D (algebra_map R A r) = 0 :=
begin
  rw [mul_one r, monoid_hom.map_mul (algebra_map R A) r 1], -- not recognizing coercion to monoid_hom
  sorry,
end

view this post on Zulip Adam Topaz (Aug 02 2020 at 14:46):

Just to be clear, a linear map does not induce a multiplicative monoid morphism. A module is, in particular, a commutative additive monoid. You probably want to use something like mul_smul or something that's named similarly.

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 14:50):

What is add_cancel_comm_monoid? This code doesn't compile for me

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 14:53):

Sorry I'm confused isn't algebra_map a ring homomorphism? Why linear map?

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 14:53):

Kevin Buzzard said:

What is add_cancel_comm_monoid? This code doesn't compile for me

Sorry I got the mwe wrong, that's only on my local branch! It chould be fixed now, let me know if something else is wrong

view this post on Zulip Adam Topaz (Aug 02 2020 at 14:54):

D is linear

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 14:54):

What's the question? The error is clear, a →+* is not a →*

view this post on Zulip Reid Barton (Aug 02 2020 at 14:55):

extends doesn't create a coercion

view this post on Zulip Adam Topaz (Aug 02 2020 at 14:55):

Oh I see. You can use ring_hom.map_mul, I guess...

view this post on Zulip Reid Barton (Aug 02 2020 at 14:55):

or (just guessing from context) (algebra_map R A).map_mul?

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 14:55):

( Your code still doesn't compile, you should perhaps cut and paste into a new file before posting. But it's easy to fix -- you need add_comm_monoid )

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 14:57):

Reid Barton said:

extends doesn't create a coercion

Does it not? I have been convinced all the times it did

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 14:58):

It creates a function, but not a coercion

view this post on Zulip Reid Barton (Aug 02 2020 at 14:58):

for classes, it also creates an instance

view this post on Zulip Reid Barton (Aug 02 2020 at 14:58):

and it affects the working of the . syntax

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 14:58):

Oh then that's why I believed it did then because things worked with classes

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 14:58):

Mistery solved thanks to all

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 15:01):

Is it in general a good idea to write a coercion for structures extending other structures? Like for linear map if I make it extend add_monoid_hom?

view this post on Zulip Reid Barton (Aug 02 2020 at 15:08):

In general we don't know whether anything is a good idea

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 15:09):

If we knew what the good ideas were the first time around, I wouldn't have just spent the last two weeks refactoring subgroups.

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 15:12):

Well in any case this:

@[priority 1000]
instance {α : Type*} {β : Type*} { : semiring α} { : semiring β} : has_coe (α →+* β) (α →* β) :=
ring_hom.to_monoid_hom

seems to be in mathlib already, so I still wonder why did not things work before...

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 15:13):

The rewrite tactic works up to syntactic equality so would not apply the coercion

view this post on Zulip Adam Topaz (Aug 02 2020 at 15:14):

The structure map of an algebra extends a ring hom, so you can use the ring_hom fields for the structure map of an algebra.

view this post on Zulip Adam Topaz (Aug 02 2020 at 15:15):

So when you combine this with Kevin's comment above, you get the issue.

view this post on Zulip Adam Topaz (Aug 02 2020 at 15:20):

Actually I'm probably wrong.

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 15:21):

Well what you said works it was just that I still wanted to understand why what I did did not work

view this post on Zulip Adam Topaz (Aug 02 2020 at 15:25):

Yeah I'm not sure, because (I think) ring hom extends monoid hom.

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 15:28):

Adam Topaz said:

Yeah I'm not sure, because (I think) ring hom extends monoid hom.

It does and there is a coercion from one to the other

view this post on Zulip Adam Topaz (Aug 02 2020 at 15:30):

Ok I understand now. algebra is a class, which has a ring_hom as a field, so that's why you can use ring_hom.map_mul.

view this post on Zulip Adam Topaz (Aug 02 2020 at 15:31):

The algebra_map is the ring_hom.

view this post on Zulip Adam Topaz (Aug 02 2020 at 15:36):

BTW: this works:

@[simp] lemma map_algebra_map : D (algebra_map R A r) = 0 :=
begin
  rw [mul_one r, map_mul],
  sorry,
end

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 15:56):

Nicolò Cavalleri said:

Well what you said works it was just that I still wanted to understand why what I did did not work

The rewrite doesn't work because of the error given when the rewrite fails. Is this the answer to your question?

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 15:58):

Oh OK I do see your point

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 16:10):

OK so the way to answer this question is to explicitly make Lean do the coercion and see what the problem is:

rw [mul_one r, monoid_hom.map_mul (algebra_map R A : R →* A) r 1],

and now we see the issue: if you make the coercion so that monoid_hom.map_mul works, the error is

rewrite tactic failed, did not find instance of the pattern in the target expression
  ⇑↑(algebra_map R A) (r * 1)
state:
...
⊢ ⇑D (⇑(algebra_map R A) (r * 1)) = 0

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 16:11):

and these things aren't syntactically equal so the rewrite fails.

view this post on Zulip Gabriel Ebner (Aug 02 2020 at 17:32):

@Kenny Lau Didn't read the whole thread, but this behavior is intentional. You write foo_instance, you get foo_instance.foo (or the type class equivalent here). In general foo_instance might not be a foo.mk, so it doesn't make sense to extract the arguments.

view this post on Zulip Kenny Lau (Aug 02 2020 at 17:32):

ok thanks

view this post on Zulip Nicolò Cavalleri (Aug 02 2020 at 18:07):

Kevin Buzzard said:

and these things aren't syntactically equal so the rewrite fails.

What does ⇑↑(algebra_map R A) (r * 1) exactly mean? I mean why two arrows?

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 18:08):

The first is the coercion from a ring hom to a monoid hom, and the second is a coercion-to-function from the monoid hom to the actual function underlying the monoid hom.

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 18:09):

It's defeq, but not syntactically equal, to ⇑(algebra_map R A)

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 18:14):

You could use change to change the goal into something for which the rewrite works of course -- but you have a ring hom and the theorem ring_hom.map_mul exists so you may as well use that.

view this post on Zulip Nicolò Cavalleri (Aug 03 2020 at 09:05):

I'm having a really hard time with coercions haha every single new one does not work for a different reason... What about this one?

import ring_theory.algebra

variables (R : Type*) (A : Type*) [comm_semiring R] [comm_semiring A] [algebra R A]
  (M : Type*) [add_comm_monoid M] [semimodule A M]

class compatible_semimodule (R : Type*) (A : Type*) [comm_semiring R] [semiring A]
  [algebra R A] (M : Type*) [add_comm_monoid M] [semimodule A M] [semimodule R M] :=
(compatible {r : R} {m : M} : r  m = ((algebra_map R A) r)  m)

structure derivation [semimodule A M] [semimodule R M] [compatible_semimodule R A M]
  extends A [R] M :=
(leibniz' (a b : A) : to_fun (a * b) = a  to_fun b + b  to_fun a)

section

variables {R} {A} {M} [semimodule R M] [compatible_semimodule R A M]

namespace derivation

instance : has_coe_to_fun (derivation R A M) := ⟨_, λ D, D.to_linear_map.to_fun

instance has_coe_to_linear_map : has_coe (derivation R A M) (A [R] M) :=
  ⟨λ D, D.to_linear_map

variables (D : derivation R A M) (r : R) (a b : A)

@[simp] lemma map_smul : D (r  a) = r  D a := linear_map.map_smul D r a /- This works... -/

variables [comm_ring R] [ring A] [algebra R A] [add_comm_group M] [module A M] [module R M]

@[simp] lemma map_neg : D (-a) = -D a := linear_map.map_neg D a /- ...but this does not, and neither
                                                                   does D.to_linear_map.map_neg a.
                                                                   Why?? I checked instances a
                                                                   hundred times! -/

end derivation

end

view this post on Zulip Anne Baanen (Aug 03 2020 at 09:54):

With set_option pp.all true, we get the error:

type mismatch at application
  @linear_map.map_neg.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6 ?m_7 ?m_8 ?m_9 ?m_10 ?m_11
    (@derivation.to_linear_map.{u_1 u_2 u_3} R A _inst_1 _inst_2 _inst_3 M _inst_4 _inst_5 _inst_5 _inst_6 _inst_7 D)
term
  @derivation.to_linear_map.{u_1 u_2 u_3} R A _inst_1 _inst_2 _inst_3 M _inst_4 _inst_5 _inst_5 _inst_6 _inst_7 D
has type
  @linear_map.{u_1 u_2 u_3} R A M (@comm_semiring.to_semiring.{u_1} R _inst_1)
    (@semiring.to_add_comm_monoid.{u_2} A (@comm_semiring.to_semiring.{u_2} A _inst_2))
    _inst_4
    (@algebra.to_semimodule.{u_1 u_2} R A _inst_1 (@comm_semiring.to_semiring.{u_2} A _inst_2) _inst_3)
    _inst_6 : Type (max u_2 u_3)
but is expected to have type
  @linear_map.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6 ?m_7 (@add_comm_group.to_add_comm_monoid.{?l_2} ?m_5 ?m_8)
    (@add_comm_group.to_add_comm_monoid.{?l_3} ?m_6 ?m_9)
    ?m_10
    ?m_11 : Type (max ?l_1 ?l_2)

So apparently there are still comm_semiring istances floating around for R and A that are being picked up by derivation. If you have a [comm_semiring R] variable and later say [comm_ring R], then this gives two different ring structures on R, not that the previous instance gets a new - operator.

view this post on Zulip Anne Baanen (Aug 03 2020 at 09:57):

It works if we put all the instances in their own section:

import ring_theory.algebra

variables (R A M : Type*)

section
variables [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [semimodule A M]

class compatible_semimodule (R : Type*) (A : Type*) [comm_semiring R] [semiring A]
  [algebra R A] (M : Type*) [add_comm_monoid M] [semimodule A M] [semimodule R M] :=
(compatible {r : R} {m : M} : r  m = ((algebra_map R A) r)  m)

structure derivation [semimodule A M] [semimodule R M] [compatible_semimodule R A M]
  extends A [R] M :=
(leibniz' (a b : A) : to_fun (a * b) = a  to_fun b + b  to_fun a)

section

variables {R} {A} {M} [semimodule R M] [compatible_semimodule R A M]

namespace derivation

instance : has_coe_to_fun (derivation R A M) := ⟨_, λ D, D.to_linear_map.to_fun

instance has_coe_to_linear_map : has_coe (derivation R A M) (A [R] M) :=
  ⟨λ D, D.to_linear_map

variables (D : derivation R A M) (r : R) (a b : A)

@[simp] lemma map_smul : D (r  a) = r  D a := linear_map.map_smul D r a /- This works... -/

end derivation

end

end

variables [comm_ring R] [comm_ring A] [algebra R A] [add_comm_group M] [module A M] [module R M] [compatible_semimodule R A M] (D : derivation R A M) (r : R) (a b : A)

@[simp] lemma map_neg : D (-a) = -D a := linear_map.map_neg D a

view this post on Zulip Anne Baanen (Aug 03 2020 at 10:00):

The above solution is rather ugly, though. When I want to switch between semiring and ring structures, I generally put them on different variables, for instance variables {R₀ R₁ : Type*} [semiring R₀] [ring R₁].


Last updated: May 10 2021 at 19:16 UTC