# Zulip Chat Archive

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

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

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

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

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

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

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

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

#### Kenny Lau (Aug 02 2020 at 17:32):

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)
(@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.

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