Coercion not properly recognized

Stream: new members

[Nicolò Cavalleri]

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]

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]

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

[Kenny Lau]

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

@Nicolò Cavalleri

[Nicolò Cavalleri]

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

[Kenny Lau]

@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]

@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]

i.e. use show

[Nicolò Cavalleri]

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]

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]

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

[Nicolò Cavalleri]

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

[Nicolò Cavalleri]

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]

D is linear

[Kevin Buzzard]

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

[Reid Barton]

extends doesn't create a coercion

[Adam Topaz]

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

[Reid Barton]

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

[Kevin Buzzard]

( 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]

Reid Barton said:

extends doesn't create a coercion

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

[Kevin Buzzard]

It creates a function, but not a coercion

[Reid Barton]

for classes, it also creates an instance

[Reid Barton]

and it affects the working of the . syntax

[Nicolò Cavalleri]

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

[Nicolò Cavalleri]

Mistery solved thanks to all

[Nicolò Cavalleri]

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]

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

[Kevin Buzzard]

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]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

Actually I'm probably wrong.

[Nicolò Cavalleri]

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

[Adam Topaz]

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

[Nicolò Cavalleri]

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]

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]

The algebra_map is the ring_hom.

[Adam Topaz]

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]

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]

Oh OK I do see your point

[Kevin Buzzard]

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]

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

[Gabriel Ebner]

@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]

ok thanks

[Nicolò Cavalleri]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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₁].