## Stream: maths

### Topic: Coersion and composition

#### orlando (Apr 25 2020 at 03:21):

Hello, I have problem with coersion :innocent:

import algebra.module
import linear_algebra.basic
--infix   *      := linear_map.comp
universes u v
variables {R : Type u}[comm_ring R]{M : Type v}[add_comm_group M] [module R M ]
open linear_map
def  Projector (p : M →ₗ[R] M) := p * p = p

/--
if p² = p then (1-p)² = 1 - p - p +p² = ... = 1-p
-/
lemma Complementary (p : M →ₗ[R]M) [Projector p] : Projector (1 - p) := begin
unfold Projector,
rw mul_sub_left_distrib,
iterate 2 { rw mul_sub_right_distrib,rw mul_one},
unfold Projector at *,
rw _inst_4,
rw one_mul,
simp,
end
variables (p : M→ₗ[R]M)
lemma ker_eq_im_complementary (hyp : Projector p ) : range p = ker (1-p) := begin
apply submodule.ext,
intros x,
split,
intros x_in_range,
rw mem_range at x_in_range,
rcases x_in_range with ⟨y,hyp_y⟩,
rw mem_ker,
rw ← hyp_y,
simp,
rw ← function.comp_apply ⇑p,
unfold Projector at hyp,
erw hyp,       --- here  do you have an idea to make the coersion of the  composition easy ?
end


#### Yury G. Kudryashov (Apr 25 2020 at 05:10):

Could you please copy+paste proof state? BTW, why do you use Projector as a typeclass in Complementary and as an explicit argument in the next lemma?

#### orlando (Apr 25 2020 at 05:14):

Hello, it's a problem  ⇑p ∘ ⇑p = ⇑(p * p)  coersion !

rewrite tactic failed, did not find instance of the pattern in the target expression
p * p
state:
2 goals
R : Type u,
_inst_1 : comm_ring R,
M : Type v,
_inst_3 : module R M,
p : M →ₗ[R] M,
x y : M,
hyp_y : ⇑p y = x,
hyp : p * p = p
⊢ ⇑p y - (⇑p ∘ ⇑p) y = 0

R : Type u,
_inst_1 : comm_ring R,
M : Type v,
_inst_3 : module R M,
p : M →ₗ[R] M,
hyp : Projector p,
x : M
⊢ x ∈ ker (1 - p) → x ∈ range p


#### Johan Commelin (Apr 25 2020 at 05:15):

You can try to change your goal:

change p y - (p * p) y = 0


#### Yury G. Kudryashov (Apr 25 2020 at 05:15):

There should be a linear_map.mul_apply lemma. Use it instead of function.comp_apply.

#### Yury G. Kudryashov (Apr 25 2020 at 05:17):

If there is no such lemma, please add it right after the instance that gives you *

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

But it's work Johan !

@Yury G. Kudryashov the tatic state change to  ⊢ ⇑p y - ⇑(comp p p) y = 0  lean transform  *  to composition and i can't rw after :frown:

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

I thinck there is a stuff with using  *  !

#### Yury G. Kudryashov (Apr 25 2020 at 05:19):

It's called linear_map.mul_app

#### Yury G. Kudryashov (Apr 25 2020 at 05:20):

If you rw ← p.mul_app instead of function.comp_apply, then you should get *

#### orlando (Apr 25 2020 at 05:22):

oh Sorry, i read linear_map.comp_apply  so ok nice !

#### orlando (Apr 25 2020 at 05:23):

For your question : i don't understand when a have to use  class or def or structure

#### orlando (Apr 25 2020 at 05:26):

if i understand, i have to use  (hyp : Projector p)

#### Yury G. Kudryashov (Apr 25 2020 at 05:26):

You should use class and [Projector p] if you will have quite a few instances, and every time you apply your theorem Lean will find an instance automatically. It is used, e.g., for various information about Types ([group α] etc)

#### Yury G. Kudryashov (Apr 25 2020 at 05:28):

If you're not going to have many instances, then you should use (hyp : Projector p). BTW, if you're going to PR this to mathlib, then I'd recommend to call it is_projector p.

#### orlando (Apr 25 2020 at 05:30):

ok, is_projector is really a better name !

#### orlando (Apr 25 2020 at 05:41):

change : if i have an equality to show  left = right  and  left = left'  by rfl , i can change my goal for  left' = right  with change  ... waaaaahou ... my new favorite  tactic :grinning_face_with_smiling_eyes:

#### orlando (Apr 25 2020 at 16:07):

Hello two questions about specialize  and  change

1/ Why  let H := specialize (proj_ker (id - p)) (Complementary p hyp)  doesn't work but let H := proj_ker (id-p), specialize H (Complementary p hyp),  work ?

2/ At the end, can i change without intro m  ?

import tactic.ring
import algebra.module
import linear_algebra.basic
--infix   *      := linear_map.comp
universes u v
variables {R : Type u}[comm_ring R]{M : Type v}[add_comm_group M] [module R M]
open linear_map

def  is_projector (p : M →ₗ[R] M) := p * p = p

lemma is_projector_ext {p : M →ₗ[R]M} (hyp : is_projector p) : p * p = p :=
begin unfold is_projector at hyp,exact hyp, end
/--
if p² = p then (1-p)² = 1 - p - p +p² = ... = 1-p
-/
lemma Complementary (p : M →ₗ[R]M) (hyp : is_projector p) : is_projector (id - p) := begin
change linear_map.id - p with 1 -p,
unfold is_projector,
rw mul_sub_left_distrib,
iterate 2 { rw mul_sub_right_distrib,rw mul_one},
unfold is_projector at *,
rw hyp,
rw one_mul,
simp,
end
variables (p : M →ₗ[R]M )
lemma ker_eq_im_comp (hyp : is_projector p) : range p = ker (id-p) := begin
apply submodule.ext,intros x,split,rintros ⟨y,hyp  ⟩, rw mem_ker, change x- p x = 0, rw ← hyp.2,
change (p - p * p) y = 0, rw is_projector_ext, rw sub_self, exact rfl,assumption,
intros hyp, rw mem_ker at hyp, change x-p x = 0 at hyp, rw mem_range, use x,
sorry,
end
lemma image_in_range (x : M) : p x ∈ range p := begin
rw mem_range,use x,
end
lemma proj_ker (p : M →ₗ[R]M) (hyp : is_projector p) : ∀ m : M, p m ∈ ker (id - p) :=
begin
rw ← ker_eq_im_comp, exact image_in_range p,assumption,
end
lemma  calcul : linear_map.id - (id - p) = p := begin sorry, end

lemma proj_im(p : M →ₗ[R]M) (hyp : is_projector p) : ∀ m : M, m - p m ∈ ker (p) :=
begin
let H := proj_ker (id-p),
-- let H := specialize (proj_ker (id - p)) (Complementary p hyp)                  -- unknown identifier 'specialize'
specialize  H  (Complementary p hyp),
rw calcul at H,
intros m,                                                    -- change without intro doesn't work ?
change m- p m with (linear_map.id -p) m,
exact H m,
end


#### Reid Barton (Apr 25 2020 at 16:08):

1: specialize is a tactic, not a function

#### Reid Barton (Apr 25 2020 at 16:10):

The term mode equivalent is simply let H := proj_ker (id-p) (Complementary p hyp)

of course !!!!

thx

#### Reid Barton (Apr 25 2020 at 16:11):

For 2, you can't change m - p m with ... when m is not in scope

#### Reid Barton (Apr 25 2020 at 16:11):

here, the simplest thing is to notice that you just used exact after change anyways, and almost always that means you can simply delete change

#### Reid Barton (Apr 25 2020 at 16:12):

and then intros m, exact H m can (in this case at least) be simplified to exact H

#### orlando (Apr 25 2020 at 16:12):

I thinck i try but i mistake a  ( )  :grinning_face_with_smiling_eyes:

#### Reid Barton (Apr 25 2020 at 16:14):

without intro m, you can also write for example change ∀ m, (linear_map.id - p) m ∈ _,

#### orlando (Apr 25 2020 at 16:17):

OK @Reid Barton : i understand why  intros m, exact H m,  work !

#### orlando (Apr 25 2020 at 16:19):

@Reid Barton :  exact H  without intro  is ok !

Last updated: May 11 2021 at 17:39 UTC