## Stream: new members

### Topic: Coercion not properly recognized

#### 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_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 _ _ _, }


#### 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_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 _ _ _, }


#### Kenny Lau (Aug 01 2020 at 10:23):

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

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


#### Kenny Lau (Aug 01 2020 at 10:28):

@Nicolò Cavalleri

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

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


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


#### Kenny Lau (Aug 01 2020 at 12:50):

i.e. use show

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


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

#### Kevin Buzzard (Aug 02 2020 at 14:50):

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

#### Nicolò Cavalleri (Aug 02 2020 at 14:53):

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

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

D is linear

#### Kevin Buzzard (Aug 02 2020 at 14:54):

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

#### Reid Barton (Aug 02 2020 at 14:55):

extends doesn't create a coercion

#### Adam Topaz (Aug 02 2020 at 14:55):

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

#### Reid Barton (Aug 02 2020 at 14:55):

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

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

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

#### Kevin Buzzard (Aug 02 2020 at 14:58):

It creates a function, but not a coercion

#### Reid Barton (Aug 02 2020 at 14:58):

for classes, it also creates an instance

#### Reid Barton (Aug 02 2020 at 14:58):

and it affects the working of the . syntax

#### Nicolò Cavalleri (Aug 02 2020 at 14:58):

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

#### Nicolò Cavalleri (Aug 02 2020 at 14:58):

Mistery solved thanks to all

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

#### Reid Barton (Aug 02 2020 at 15:08):

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

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

#### Nicolò Cavalleri (Aug 02 2020 at 15:12):

Well in any case this:

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


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

#### Kevin Buzzard (Aug 02 2020 at 15:13):

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

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

#### Adam Topaz (Aug 02 2020 at 15:15):

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

#### Adam Topaz (Aug 02 2020 at 15:20):

Actually I'm probably wrong.

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

#### Adam Topaz (Aug 02 2020 at 15:25):

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

#### Nicolò Cavalleri (Aug 02 2020 at 15:28):

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

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

#### Adam Topaz (Aug 02 2020 at 15:31):

The algebra_map is the ring_hom.

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


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

#### Kevin Buzzard (Aug 02 2020 at 15:58):

Oh OK I do see your point

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


#### Kevin Buzzard (Aug 02 2020 at 16:11):

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

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

ok thanks

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

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

#### Kevin Buzzard (Aug 02 2020 at 18:09):

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

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

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


#### 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)
_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
?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.

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


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