# Zulip Chat Archive

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

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

and similarly if you already have a linear map`f : 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_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 (Apr 17 2020 at 18:06):

Yes, `{! !}`

is term mode.

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

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 !

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

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