linear equiv constructor

Stream: maths

[orlando]

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]

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]

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

[orlando]

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

Yes linear_algebra.basic

[Kevin Buzzard]

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]

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₂  :=
{
  add := sorry,
  smul := sorry,
  ..e}

[Kevin Buzzard]

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]

@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_3 : add_comm_group M,
_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]

Yes, {! !} is term mode.

[orlando]

rohhhhh

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[orlando]

Thx !!!!

[Kevin Buzzard]

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]

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]

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

[orlando]

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

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]

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

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

[Kevin Buzzard]

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]

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

[Scott Morrison]

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.