# Zulip Chat Archive

## 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_2 : add_comm_group M, _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_2 : add_comm_group M, _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`

.

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

Yury's advice is better

#### 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 `instance`

s, and every time you apply your theorem Lean will find an instance automatically. It is used, e.g., for various information about `Type`

s (`[group α]`

etc)

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

If you're not going to have many `instance`

s, 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)`

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

of course !!!!

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

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