works in web editor, not locally

Stream: general

[Kevin Buzzard]

There's some subtlety I don't understand in the below code:

import Mathlib.RingTheory.TensorProduct

open scoped TensorProduct

def Coalgebra.id' (R : Type) (A : Type)
  [CommRing R] [AddCommGroup A] [Module R A] : A →ₗ[R] A := LinearMap.id

class Coalgebra (R : Type) (A : Type) [CommRing R] [AddCommGroup A] [Module R A] where
  Δ : A →ₗ[R] A ⊗[R] A
  ε : A →ₗ[R] R
  coassoc : ∀ a : A, (TensorProduct.assoc R A A A) ((TensorProduct.map Δ id') (Δ a)) = ((TensorProduct.map id' Δ) (Δ a))
  ε_id : ∀ a : A, (TensorProduct.lid R A) ((TensorProduct.map ε id') (Δ a)) = id' a
  id_ε : ∀ a : A, (TensorProduct.lid R A) ((TensorProduct.comm R A R) ((TensorProduct.map id' ε) (Δ a))) = id' a

It works fine in the web editor, but when I run it locally (clarification: in a scratch file in mathlib) I get unknown identifier 'id'' in the definition of Coalgebra. What is going on?

[Adam Topaz]

It probably has something to do with autoImplicit.

[Adam Topaz]

E.g. this fails in the web editor:

import Mathlib.RingTheory.TensorProduct

open scoped TensorProduct

def Coalgebra.id' (R : Type) (A : Type)
  [CommRing R] [AddCommGroup A] [Module R A] : A →ₗ[R] A := LinearMap.id

set_option autoImplicit false


class Coalgebra (R : Type) (A : Type) [CommRing R] [AddCommGroup A] [Module R A] where
  Δ : A →ₗ[R] A ⊗[R] A
  ε : A →ₗ[R] R
  coassoc : ∀ a : A, (TensorProduct.assoc R A A A) ((TensorProduct.map Δ id') (Δ a)) = ((TensorProduct.map id' Δ) (Δ a))
  ε_id : ∀ a : A, (TensorProduct.lid R A) ((TensorProduct.map ε id') (Δ a)) = id' a
  id_ε : ∀ a : A, (TensorProduct.lid R A) ((TensorProduct.comm R A R) ((TensorProduct.map id' ε) (Δ a))) = id' a

[Adam Topaz]

My guess is that the web editor doesn't turn off auto implicit by default.

[Adam Topaz]

But mathlib4 does: https://github.com/leanprover-community/mathlib4/blob/d030880f14fc5219d77c688b9c42e367c588c805/lakefile.lean#L8

[Adam Topaz]

When you say "open locally", are you opening a copy a mathlib? Or are you working in a project which depends on mathlib?

[Eric Wieser]

Adam Topaz said:

My guess is that the web editor doesn't turn off auto implicit by default.

This constantly bites me, and I wish it would; but I'm sure there are people who have the opposite opinion

[Kevin Buzzard]

I should have said that I tried adding set_option autoImplicit true locally and this didn't fix the local error. (so we have established that it's possible to break working code in the web editor, but I still don't know how to get my non-working local code to work)

[Adam Topaz]

does go to definition work on id' in the definition of Coalgebra your web editor?

[Kevin Buzzard]

id' is an unknown identifier locally.

[Adam Topaz]

sorry, I meant web

[Adam Topaz]

well, it doesn't for me. so it's unknown also for the web editor.

[Kevin Buzzard]

jump to definition doesn't work in the web editor as far as I know?

[Adam Topaz]

If I put your original code in a fresh file in a fresh project which depends on mathlib, then I get no errors locally.

[Kevin Buzzard]

Oh interesting! Yes, I was dumping it in mathlib. So what other option is mathlib setting which is messing this code up?

[Adam Topaz]

I suppose the global option in the lakefile overrides the option in the file?

[Ruben Van de Velde]

It shouldn't

[Adam Topaz]

right, so something is still wrong.

[Kevin Buzzard]

yeah indeed the code works fine in NNG :-)

[Kevin Buzzard]

The option in the file is working fine in mathlib, you can e.g. change Type to Type u and this works fine with autoImplicit true. But id' still doesn't work.

[Adam Topaz]

I got it, it's not autoImplicit, but rather relaxedAutoImplicit. This should work:

import Mathlib.RingTheory.TensorProduct

set_option autoImplicit true
set_option relaxedAutoImplicit true

open scoped TensorProduct

def Coalgebra.id' (R : Type) (A : Type)
  [CommRing R] [AddCommGroup A] [Module R A] : A →ₗ[R] A := LinearMap.id

class Coalgebra (R : Type) (A : Type) [CommRing R] [AddCommGroup A] [Module R A] where
  Δ : A →ₗ[R] A ⊗[R] A
  ε : A →ₗ[R] R
  coassoc : ∀ a : A, (TensorProduct.assoc R A A A) ((TensorProduct.map Δ id') (Δ a)) = ((TensorProduct.map id' Δ) (Δ a))
  ε_id : ∀ a : A, (TensorProduct.lid R A) ((TensorProduct.map ε id') (Δ a)) = id' a
  id_ε : ∀ a : A, (TensorProduct.lid R A) ((TensorProduct.comm R A R) ((TensorProduct.map id' ε) (Δ a))) = id' a

[Adam Topaz]

well rather it's both. If one of the two options is set to false, then you get the error.

[Adam Topaz]

both options are false by default in mathlib.

[Kevin Buzzard]

I am quite confused about why this fixes the problem, to be honest. (oh, I get it now). But thanks!

[Eric Wieser]

Note that Adam's version is nonsense

[Eric Wieser]

It parameterizies coassoc with an id' variabl

[Eric Wieser]

Coalgebra.coassoc {R A : Type} [inst✝ : CommRing R] [inst✝¹ : AddCommGroup A] [inst✝² : Module R A]
  [self : Coalgebra R A] {id' : A →ₗ[R] A} (a : A) :
  ↑(TensorProduct.assoc R A A A) (↑(TensorProduct.map Coalgebra.Δ id') (↑Coalgebra.Δ a)) =
    ↑(TensorProduct.map id' Coalgebra.Δ) (↑Coalgebra.Δ a)

[Adam Topaz]

Is that not what happens in the web editor with Kevin's original code?

[Eric Wieser]

Oh sure, but my point is that this doesn't "fix" the problem, this hides it

[Adam Topaz]

Oh ok, yeah I agree. By "fix" I really mean "we should now understand what's going on."

[Eric Wieser]

I think the key observation is that the Foo namespace is not open within class Foo

[Adam Topaz]

The real problem is that id' has two explicit variables.

[Eric Wieser]

That's not enough to fix it, you also need open Coalgebra in

[Adam Topaz]

import Mathlib.RingTheory.TensorProduct

set_option autoImplicit false
set_option relaxedAutoImplicit false

open scoped TensorProduct

def Coalgebra.id' (R : Type) (A : Type)
  [CommRing R] [AddCommGroup A] [Module R A] : A →ₗ[R] A := LinearMap.id

open Coalgebra in
class Coalgebra (R : Type) (A : Type) [CommRing R] [AddCommGroup A] [Module R A] where
  Δ : A →ₗ[R] A ⊗[R] A
  ε : A →ₗ[R] R
  coassoc : ∀ a : A, (TensorProduct.assoc R A A A) ((TensorProduct.map Δ (id' _ _)) (Δ a)) = ((TensorProduct.map (id' _ _) Δ) (Δ a))
  ε_id : ∀ a : A, (TensorProduct.lid R A) ((TensorProduct.map ε (id' _ _)) (Δ a)) = id' R _ a
  id_ε : ∀ a : A, (TensorProduct.lid R A) ((TensorProduct.comm R A R) ((TensorProduct.map (id' _ _) ε) (Δ a))) = id' R _ a

[Adam Topaz]

Eric Wieser said:

I think the key observation is that the Foo namespace is not open within class Foo

That's right. If we rename Coalgebra to Coalgebra.Foo then I suppose everything will become clear (even with the original code)

[Eric Wieser]

Of course, you should really write:

class Coalgebra (R : Type) (A : Type) [CommRing R] [AddCommGroup A] [Module R A] where
  Δ : A →ₗ[R] A ⊗[R] A
  ε : A →ₗ[R] R
  coassoc : TensorProduct.assoc R A A A ∘ₗ TensorProduct.map Δ .id ∘ₗ Δ = TensorProduct.map .id Δ ∘ₗ Δ
  ε_id : TensorProduct.lid R A ∘ₗ TensorProduct.map ε .id ∘ₗ Δ = .id
  id_ε : TensorProduct.rid R A ∘ₗ TensorProduct.map .id ε ∘ₗ Δ = .id

[Eric Wieser]

Where .id is just LinearMap.id, which doesn't need a second name

[Eric Wieser]

And stating the proof fields as equalities of morphisms makes ext super powerful for proving them

[Kevin Buzzard]

You both think that it's better to be composing those linear maps rather than evaluating them at x, for all x?

[Eric Wieser]

I am currently writing a thesis section about that very principle!

[Eric Wieser]

It means that if A is a tensor product or a direct sum, you can start the proof with ext; dsimp and you're already only dealing with pure tensors or single elements of the direct sum

[Adam Topaz]

Kevin Buzzard said:

You both think that it's better to be composing those linear maps rather than evaluating them at x, for all x?

I defer to the experts:

Eric Wieser said:

I am currently writing a thesis section about that very principle!

[Kevin Buzzard]

yup, I can confirm that my proofs for the first example of a coalgebra in Wikipedia just completely broke with this refactor, but when fixed they were shorter with this new definition.

[Eric Wieser]

I'm surprised, I would have thought a lot of things would be easier to prove while id' was a free variable and not just the identity function! nevermind, you're proving instances not lemmas

[Eric Wieser]

Kevin Buzzard said:

You both think that it's better to be composing those linear maps rather than evaluating them at x, for all x?

The compromise would be to write the applied version because that's what mathematicians expect to read, but then write an abbrev that takes the equalities of morphisms, and always use that

[Kevin Buzzard]

oh sorry, I independently fixed the id' problem :-) But I fixed it in a different way to you: I did open LinearMap and then used id. What is this .id thing? I've never understood that. It means "look in every namespace until you find the right one"??

[Ruben Van de Velde]

"Look at the namespace for the type you're expecting to fill this hole" was my understanding, but might be wrong

[Adam Topaz]

No, it means that if the type expected is LinearMap then .id will mean LinearMap.id, etc.

[Eric Wieser]

if you have a hole (_ : Foo X), then (.bar : Foo X) means (Foo.bar : Foo X)

[Adam Topaz]

:racecar:

[Kevin Buzzard]

Oh I've learnt so much in this thread :-) Thanks all!