Library Top.linear_map

This file is part of the Elfic library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Import FunctionalExtensionality.
Require Export compatible.

About functions from E to F
Note that Coquelicot has: U UniformSpace, then T->U UniformSpace, and similar for CompleteSpace
Functions to a ModuleSpace are a ModuleSpace

Section Fcts.

Context {E : Type}.
Context {F : ModuleSpace R_Ring}.

Definition fct_plus (f:EF) (g:EF) : (EF) :=
  fun xplus (f x) (g x).

Definition fct_scal (l:R) (f:EF) : (EF) :=
  fun xscal l (f x).

Definition fct_opp (f:EF) : (E F) :=
  fun xopp (f x).

Definition fct_zero:EF := fun _zero.

Lemma fct_plus_comm: (f g:EF), fct_plus f g = fct_plus g f.

Lemma fct_plus_assoc:
   (f g h:EF), fct_plus f (fct_plus g h) = fct_plus (fct_plus f g) h.

Lemma fct_plus_zero_r: f:EF, fct_plus f fct_zero = f.

Lemma fct_plus_opp_r: f:EF, fct_plus f (fct_opp f) = fct_zero.

Definition fct_AbelianGroup_mixin :=
  AbelianGroup.Mixin (EF) fct_plus fct_opp fct_zero fct_plus_comm
   fct_plus_assoc fct_plus_zero_r fct_plus_opp_r.

Canonical fct_AbelianGroup :=
  AbelianGroup.Pack (EF) (fct_AbelianGroup_mixin) (EF).

Lemma fct_scal_assoc: x y (u:EF),
   fct_scal x (fct_scal y u) = fct_scal (mult x y) u.

Lemma fct_scal_one: (u:EF), fct_scal one u = u.

Lemma fct_scal_distr_l: x (u v:EF), fct_scal x (plus u v) = fct_plus (fct_scal x u) (fct_scal x v).

Lemma fct_scal_distr_r: (x y:R) (u:EF), fct_scal (Rplus x y) u = fct_plus (fct_scal x u) (fct_scal y u).

Definition fct_ModuleSpace_mixin :=
  ModuleSpace.Mixin R_Ring fct_AbelianGroup fct_scal fct_scal_assoc
     fct_scal_one fct_scal_distr_l fct_scal_distr_r.

Canonical fct_ModuleSpace :=
  ModuleSpace.Pack R_Ring (EF)
   (ModuleSpace.Class R_Ring (EF) _ fct_ModuleSpace_mixin) (EF).

End Fcts.

Linear Mapping

Section SSG_linear_mapping.

Context {E : ModuleSpace R_Ring}.
Context {F : ModuleSpace R_Ring}.

Definition is_linear_mapping (phi: E F) :=
  ( (x y : E), phi (plus x y) = plus (phi x) (phi y))
      ( (x : E) (l:R), phi (scal l x) = scal l (phi x)).

Theorem compatible_g_is_linear_mapping:
    compatible_g is_linear_mapping.

Lemma is_linear_mapping_zero: f,
   is_linear_mapping f f zero = zero.

Lemma is_linear_mapping_opp: f x,
   is_linear_mapping f f (opp x) = opp (f x).

Lemma is_linear_mapping_f_zero:
   is_linear_mapping (fun (x:E) ⇒ @zero F).

Lemma is_linear_mapping_f_opp: (f:EF),
    is_linear_mapping f
      is_linear_mapping (opp f).

Lemma is_linear_mapping_f_plus: (f g:EF),
    is_linear_mapping f is_linear_mapping g
      is_linear_mapping (plus f g).

Lemma is_linear_mapping_f_scal: l, (f:EF),
    is_linear_mapping f
      is_linear_mapping (scal l f).

End SSG_linear_mapping.

Section SSG_bilinear_mapping.

Context {E : ModuleSpace R_Ring}.
Context {F : ModuleSpace R_Ring}.
Context {G : ModuleSpace R_Ring}.

Definition is_bilinear_mapping (phi: E F G) :=
  ( (x:E) (y:F) (l:R), phi (scal l x) y = scal l (phi x y))
  ( (x:E) (y:F) (l:R), phi x (scal l y) = scal l (phi x y))
  ( (x y: E) (z:F), phi (plus x y) z = plus (phi x z) (phi y z))
  ( (x:E) (y z : F), phi x (plus y z) = plus (phi x y) (phi x z)).

Theorem compatible_g_is_bilinear_mapping:
    compatible_g is_bilinear_mapping.

End SSG_bilinear_mapping.

Injections, surjections, bijections

Section Inj_Surj_Bij.

Context {E : ModuleSpace R_Ring}.
Context {F : ModuleSpace R_Ring}.

Definition is_injective (f: E F) :=
   (x y : E), f x = f y x = y.

Definition is_surjective (f: E F) :=
   (y : F), (x : E), f x = y.

Definition is_bijective (f: E F) :=
           (is_injective f) (is_surjective f).

End Inj_Surj_Bij.