Coersion and composition

Stream: maths

[orlando]

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]

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]

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]

You can try to change your goal:

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

[Yury G. Kudryashov]

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

[Johan Commelin]

Yury's advice is better

[Yury G. Kudryashov]

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

[orlando]

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]

I thinck there is a stuff with using * !

[Yury G. Kudryashov]

It's called linear_map.mul_app

[Yury G. Kudryashov]

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

[orlando]

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

[orlando]

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

[orlando]

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

[Yury G. Kudryashov]

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]

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]

ok, is_projector is really a better name !

[orlando]

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]

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]

1: specialize is a tactic, not a function

[Reid Barton]

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

[orlando]

of course !!!!

[orlando]

thx

[Reid Barton]

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

[Reid Barton]

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]

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

[orlando]

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

[Reid Barton]

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

[orlando]

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

[orlando]

@Reid Barton : exact H without intro is ok !