Zulip Chat Archive

Stream: maths

Topic: linear equiv constructor


view this post on Zulip 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 ?

view this post on Zulip 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".

view this post on Zulip 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₂)

view this post on Zulip orlando (Apr 17 2020 at 18:02):

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

Yes linear_algebra.basic

view this post on Zulip 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.

view this post on Zulip 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₂  :=
{
  add := sorry,
  smul := sorry,
  ..e}

view this post on Zulip 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

view this post on Zulip 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_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 !

view this post on Zulip Kevin Buzzard (Apr 17 2020 at 18:06):

Yes, {! !} is term mode.

view this post on Zulip orlando (Apr 17 2020 at 18:06):

rohhhhh

view this post on Zulip Kevin Buzzard (Apr 17 2020 at 18:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip orlando (Apr 17 2020 at 18:10):

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

view this post on Zulip orlando (Apr 17 2020 at 18:10):

Thx !!!!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip orlando (Apr 17 2020 at 19:41):

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

view this post on Zulip 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 f1 f^{-1} notation ? I don't understand how ? (there is no example in the file) .

view this post on Zulip 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 ff and f1f^{-1} differ in general.

view this post on Zulip Kevin Buzzard (Apr 17 2020 at 23:54):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip orlando (Apr 18 2020 at 00:00):

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

view this post on Zulip 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