Zulip Chat Archive

Stream: maths

Topic: Coersion and composition


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

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

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

view this post on Zulip Johan Commelin (Apr 25 2020 at 05:15):

You can try to change your goal:

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

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

view this post on Zulip Johan Commelin (Apr 25 2020 at 05:15):

Yury's advice is better

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

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

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

I thinck there is a stuff with using * !

view this post on Zulip Yury G. Kudryashov (Apr 25 2020 at 05:19):

It's called linear_map.mul_app

view this post on Zulip Yury G. Kudryashov (Apr 25 2020 at 05:20):

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

view this post on Zulip orlando (Apr 25 2020 at 05:22):

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

view this post on Zulip orlando (Apr 25 2020 at 05:23):

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

view this post on Zulip orlando (Apr 25 2020 at 05:26):

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

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

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

view this post on Zulip orlando (Apr 25 2020 at 05:30):

ok, is_projector is really a better name !

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

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

view this post on Zulip Reid Barton (Apr 25 2020 at 16:08):

1: specialize is a tactic, not a function

view this post on Zulip Reid Barton (Apr 25 2020 at 16:10):

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

view this post on Zulip orlando (Apr 25 2020 at 16:10):

of course !!!!

view this post on Zulip orlando (Apr 25 2020 at 16:10):

thx

view this post on Zulip Reid Barton (Apr 25 2020 at 16:11):

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

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

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

view this post on Zulip orlando (Apr 25 2020 at 16:12):

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

view this post on Zulip Reid Barton (Apr 25 2020 at 16:14):

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

view this post on Zulip orlando (Apr 25 2020 at 16:17):

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

view this post on Zulip orlando (Apr 25 2020 at 16:19):

@Reid Barton : exact H without intro is ok !


Last updated: May 11 2021 at 17:39 UTC