unfolding "1"

Stream: new members

[Winston Yin]

When I'm faced with a goal such as ⇑1 x = x, where the 1 here is the .one of M ≃ₗ[R] M, how can I efficiently rewrite it into linear_equiv.refl ... according to the definition of linear_map.automorphism_group? I find myself doing some tedious stuff like unfold has_one.one mul_one_class.one monoid.one div_inv_monoid.one group.one before I get to that point.

[Adam Topaz]

in this case, I think you can close the goal with refl. In general, we have the tactic#change tactic which lets you change something to anything that's defeq (with some limitations if your term involves applications of functions)

[Adam Topaz]

Generally you should try to avoid unfolding, and instead use the lemmas that exist in the library.

[Winston Yin]

Indeed refl works. It is however a bit of a black box to me, so I'm never quite sure when to use it

[Adam Topaz]

In this particular case, I suspect mathlib is missing a simp lemma...

[Adam Topaz]

E.g.

import linear_algebra

variables {R M : Type*} [add_comm_group M] [ring R] [module R M]

@[simp]
lemma coe_one : ((1 : M ≃ₗ[R] M) : M → M) = id := rfl

example {m : M} : (1 : M ≃ₗ[R] M) m = m :=
by simp

[Kevin Buzzard]

Winston Yin said:

Indeed refl works. It is however a bit of a black box to me, so I'm never quite sure when to use it

To understand when refl works one has to have a good understanding of (a) what the definition of everything is (which you can get by right clicking on definitions) and (b) what Lean means by definitional equality (the formal definition is here). The first thing to know is that definitional equality is in some sense "not mathematical". For example if x is a natural thenx + 0 = x is true by refl but 0 + x = x is not; to see why this is true you need to know the actual way that addition is implemented on the naturals (i.e. something computer scientists know about addition), as opposed to just the list of properties which it has (i.e. the things mathematicians know about it). The reason refl works here is that you will not be surprised to know that the definition of the isomorphism $1:M\to M$ is that it is the map sending $x$ to $x$.

[Winston Yin]

To me the tricky might be the first part—knowing how exactly something is defined. This has been leading me down this tree of definitions on mathlib. Is it right to say that the graph of defeq terms in Lean contains no cycles (diamonds)? So if something is defined equivalently in two ways, e.g. reals as Dedekind cuts vs Cauchy sequences, the two are not defeq?

[Kevin Buzzard]

Everything is defined in one way in Lean. You might think that the real numbers has two definitions, but in Lean the real numbers are defined to be equivalence classes of Cauchy sequences, and the isomorphism with Dedekind cuts would not be refl, it would be maps in both directions between different types (in particular it would not even be an equality, it would be something else, namely an equiv : docs#equiv

[Winston Yin]

Got it

[Kevin Buzzard]

I realise that it's actually quite an involved procedure to find the definition of 1 for a beginner. Here is how I do it. Step 1 is to make the thing I want to inspect in Lean:

import linear_algebra

variables {R M : Type*} [add_comm_group M] [ring R] [module R M] (x : M)

example : (1 : M ≃ₗ[R] M) x = x := sorry

And then I put my cursor just before the sorry and in the infoview I see

⊢ ⇑1 x = x

I then click on the 1 and I understand enough about the system to know that the output means "the 1 here has come from mul_one_class.to_has_one (M ≃ₗ[R] M) so I click on that and discover that it's come from the fact that the isomorphisms are a monoid, a so-called div_inv_monoid (an implementation detail defining a mathematical object that mathematicians are not particularly interested in) and ultimately from a group, and the definition is linear_map.automorphism_group. I then click on the little arrow and it takes me to linear_algebra.basic where I see on line 2521 the definition of linear_map.automorphism_group, and one is defined to be linear_equiv.refl R M. I right click on this and see that the map is defined to be linear_map.id, and a final jump to definition, this time in algebra.module.linear_map line 88 shows me that the map is indeed defined to be id, whose definition in core Lean is defined to be id a = a. So now I know that rfl will work.

You can inspect anything like this -- you can pretty much always figure out what's going on, at least at this kind of level.

[Adam Topaz]

Kevin's method is, of course, the correct way to find the definition of something in vscode, but perhaps I should mention how I approach this.

1. I assume that mathlib has the "reasonable" definitions for things.
2. In this case, there is only one reasonable definition, namely the identity function.
3. Hence this should be true by refl.

Of course these steps fail fairly often, and when that happens (after getting frustrated that what I expect to be the "reasonable" definition is not the actual definition) I go digging approximately like Kevin suggests.