## Stream: maths

### Topic: linear equiv constructor

#### orlando (Apr 17 2020 at 17:55):

Hello, in the file  basic / module
There is the definition of linear equivalence :

structure linear_equiv (R : Type u) (M : Type v) (M₂ : Type w)
[ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂]
extends M →ₗ[R] M₂, M ≃ M₂
end


I never work with a structure extend structure, how is the form of the constructor ?

#### Kevin Buzzard (Apr 17 2020 at 17:59):

One way which always works is this: def foo (R : Type u) (M : Type v) (M₂ : Type w) [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂] : M ≃ₗ[R] M₂ := {! !} and then click on the ! and then click on the little yellow lightbulb and select the last-but-one option: "generate a skeleton for the structure under construction".

#### Kevin Buzzard (Apr 17 2020 at 18:00):

(I assume you're talking about linear_algebra.basic; M ≃ₗ[R] M₂ is notation for linear_equiv R M M₂)

#### orlando (Apr 17 2020 at 18:02):

Thx Kevin, I think you already gave me this trick ! sorry !

Yes linear_algebra.basic

#### Kevin Buzzard (Apr 17 2020 at 18:03):

But if you already have e : M ≃ M₂ then you do not have to fill in to_fun or inv_fun or left_inv or right_inv, you can just write ..e after you have defined the other fields.

#### Kevin Buzzard (Apr 17 2020 at 18:04):

import linear_algebra.basic

universes u v w

def foo (R : Type u) (M : Type v) (M₂ : Type w)
[ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂]
(e : M ≃ M₂) : M ≃ₗ[R] M₂  :=
{
smul := sorry,
..e}


#### Kevin Buzzard (Apr 17 2020 at 18:05):

and similarly if you already have a linear mapf : M →ₗ[R] M₂ then you only have to fill in the inverse map and the proofs that it is an inverse, and then add ..f

#### orlando (Apr 17 2020 at 18:05):

@Kevin Buzzard my bad, i use your trick two hour ago ! with this structure

lemma rest_is_lin_equiv (h : stable_sub_module ρ p) (g : G) : p ≃ₗ[R] p :=  begin
{! ! }end


And i have i message :

too many constructors
state:
G : Type u,
R : Type v,
M : Type w,
_inst_1 : group G,
_inst_2 : ring R,
_inst_4 : module R M,
ρ : group_representation G R M,
p : submodule R M,
h : stable_sub_module ρ p,
g : G
⊢ tactic {! !}


But without begin end  it's ok !

#### Kevin Buzzard (Apr 17 2020 at 18:06):

Yes, {! !} is term mode.

rohhhhh

#### Kevin Buzzard (Apr 17 2020 at 18:06):

Make definitions in term mode, and prove theorems in tactic mode.

#### Kevin Buzzard (Apr 17 2020 at 18:07):

If you are defining X : Type* or P : Prop or x : X with X : Type*, it's best to use term mode. If you are defining h : P with P : Prop then tactic mode is fine. If you see ⊢ P in tactic mode then it is best if P : Prop.

#### Kevin Buzzard (Apr 17 2020 at 18:09):

import linear_algebra.basic

def foo (R : Type*) (M : Type*) (M₂ : Type*)
[ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂]
: M ≃ₗ[R] M₂  :=
begin
constructor,
sorry, sorry, sorry, sorry, sorry, sorry
end


is not a good idea.

#### orlando (Apr 17 2020 at 18:10):

I do that :sweat_smile: and it's not a good idea ! Complicated to understand the field !

Thx !!!!

#### Kevin Buzzard (Apr 17 2020 at 18:12):

But this is OK:

import linear_algebra.basic data.rat.basic

def foo : ℚ ≃ₗ[ℤ] ℚ :=
begin
refine_struct
{ to_fun := id,
inv_fun := id
},
{ sorry},
{ sorry},
{ sorry},
{ sorry}
end


Here I define the data using term mode, and then I have four goals to solve in tactic mode.

#### Kevin Buzzard (Apr 17 2020 at 18:13):

refine_struct is a tactic which takes some structure field definitions (in term mode), and then leaves the rest of them as goals (in tactic mode). So now you can work on the goals which are theorems, in tactic mode.

#### orlando (Apr 17 2020 at 19:41):

@Kevin Buzzard : all good ... thx :+1:

#### orlando (Apr 17 2020 at 23:45):

@Kevin Buzzard i have show that a linear map is an linear equiv. Can i have access to $f^{-1}$ notation ? I don't understand how ? (there is no example in the file) .

#### Kevin Buzzard (Apr 17 2020 at 23:53):

No, \-1 is notation for has_inv.inv and has_inv.inv : X -> X. But here the type of $f$ and $f^{-1}$ differ in general.

#### Kevin Buzzard (Apr 17 2020 at 23:54):

\-1 notation is really bad anyway. For example $\sin^{-1}(x^{-1})$ is two different uses of it, and $\sin^{-1}$ isn't a two-sided inverse for $\sin$ anyway.

#### Kevin Buzzard (Apr 17 2020 at 23:55):

If e : M ≃ₗ[R] M₂ then...I can't remember if there's a coercion to function or not for equivalences.

#### Kevin Buzzard (Apr 17 2020 at 23:55):

If there is, then e.symm is probably the inverse function (or \u= e.symm) and if there isn't then it's e.inv_fun.

#### orlando (Apr 18 2020 at 00:00):

Ok Kevin, i check e.symm another thing tomorow :slight_smile:

#### Scott Morrison (Apr 18 2020 at 00:03):

Avoid using inv_fun. The preference is definitely to use e.symm, and the coercion to a function. So hopefully you can just write something like e.symm x. If the coercion to a function fails (this is fairly flaky in Lean 3; it's a hard problem for the elaborator), adding types usually works: (e.symm : X \to Y) x.

Last updated: May 12 2021 at 07:17 UTC