Library Algebra.Finite_dim.Finite_dim_MS_lin_map

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
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.

Brief description

Support for linear maps in finite-dimensional module spaces.

Description

For results that are only valid when the ring of scalars is commutative, or being ordered, see Algebra.Finite_dim.Finite_dim_MS_lin_map_R where they are only stated in the case of the ring of real numbers R_Ring.

Usage

This module may be used through the import of Algebra.Finite_dim.Finite_dim_MS, Algebra.Finite_dim.Finite_dim, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

From Requisite Require Import ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring ModuleSpace.
From Algebra Require Import Finite_dim_MS_def Finite_dim_MS_lin_gen.
From Algebra Require Import Finite_dim_MS_basis.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.

Section Linear_mapping_Facts1.

Context {K : Ring}.
Context {E F : ModuleSpace K}.

Variable f : E F.
Hypothesis Hf : lin_map f.

Variable PE : E Prop.
Hypothesis HPE : compatible_ms PE.

Lemma lm_lin_indep_compat :
   {n} (B : 'E^n),
    injS PE f ( i, PE (B i)) lin_indep B lin_indep (mapF f B).
Proof.
intros n B H1 H2 H3 L HL; rewrite <- f_lc_compat_lm in HL; try easy.
apply H3, H1.
apply cms_lc; easy.
apply cms_zero; easy.
rewrite lm_zero; easy.
Qed.

Lemma lm_lin_gen_compat :
   {n} (B : 'E^n),
    ( i, PE (B i))
    lin_gen PE B lin_gen (image f PE) (mapF f B).
Proof.
intros n B H1 H2.
apply subset_ext_equiv; split; intros x Hx.
induction Hx as [y Hy].
rewrite H2 in Hy.
destruct Hy as [L].
rewrite f_lc_compat_lm; easy.
destruct Hx as [L].
rewrite <- f_lc_compat_lm; try easy.
apply Im.
apply cms_lc; try easy.
Qed.

Lemma lm_basis_compat :
   n (B : 'E^n),
    injS PE f ( i, PE (B i))
    basis PE B basis (image f PE) (mapF f B).
Proof.
move=>> Hf1 HB1 [HB2 HB3]; split.
apply lm_lin_gen_compat; easy.
apply lm_lin_indep_compat; easy.
Qed.

Lemma lm_preimageF :
   {n} (B : 'F^n), inclF B (image f PE)
     (A : 'E^n), inclF A PE B = mapF f A.
Proof.
intros n B HB; rewrite image_eq in HB.
destruct (choiceF _ HB) as [A HA]; A; split;
    [| apply extF]; intro; apply HA.
Qed.

End Linear_mapping_Facts1.

Section Linear_mapping_Facts2.

Context {K : Ring}.
Context {E F : ModuleSpace K}.

Variable f : E F.
Hypothesis Hf : lin_map f.

Variable PE : E Prop.
Hypothesis HPE : compatible_ms PE.

Lemma lm_basis_compat_equiv :
   n (B : 'E^n),
    injS PE f ( i, PE (B i))
    basis PE B basis (image f PE) (fun if (B i)).
Proof.
intros n B Hf1 HB1; split; [apply lm_basis_compat; easy |].
assert (Hf2 : bijS PE (image f PE) f).
  apply bijS_RgS_equiv; [apply inhabited_ms | easy].
intros HB2.
apply (basis_sub_equiv HPE HB1).
pose (PEs := sub_ModuleSpace HPE).
assert (HPI: compatible_ms (image f PE)).
apply cms_image; easy.
pose (PIs := sub_ModuleSpace HPI).
pose (Bs := fun i : 'I_nmk_sub (HB1 i): PEs); fold Bs.
assert (V: t:PEs, (image f PE) (f (val t))).
intros t; apply Im; try easy.
destruct t; easy.
pose (fs := fun t:PEsmk_sub (V t): PIs).
pose (fBs := fun ifs (Bs i)).
assert (Hfs: bijective fs).
apply sub_bij with f; try easy; apply inhabited_ms.
pose (gs:= f_inv Hfs).
apply basis_ext with (mapF gs fBs).
apply extF; intros i.
rewrite mapF_correct; unfold fBs, gs.
now rewrite f_inv_can_l.
assert (W: (@fullset (@sub_ModuleSpace K E PE HPE) = image gs (image fs fullset))).
apply subset_ext_equiv; split; intros x Hx; try easy.
rewrite -(f_inv_can_l Hfs x); easy.
assert (Hfs2 : lin_map fs).
apply: sub_ms_lm; easy.
rewrite W; apply lm_basis_compat; try easy.
apply lm_bij_compat; easy.
apply cms_image; easy.
apply (bijS_injS fullset).
replace (image fs fullset) with (@fullset PIs).
apply bij_S_equiv; try apply inhabited_ms.
apply f_inv_bij.
apply subset_ext_equiv; split; intros (x,Hx1) Hx2; try easy.
rewrite image_eq; inversion Hx1 as (y,Hy).
(mk_sub Hy); split; try easy.
apply val_inj; simpl; easy.
assert (T: inclF (fun i : 'I_nf (B i)) (image f PE)).
intros i; easy.
generalize (basis_sub_equiv HPI T); intros (_,TT1).
specialize (TT1 HB2).
apply basis_ext2 with (3:=TT1).
apply subset_ext_equiv; split; intros (x,Hx1) Hx2; try easy.
rewrite image_eq; inversion Hx1 as (y,Hy).
(mk_sub Hy); split; try easy.
apply val_inj; simpl; easy.
apply extF; intros i.
apply val_inj; now simpl.
Qed.

End Linear_mapping_Facts2.

Section Linear_mapping_Facts3a.

Context {K : Ring}.
Context {E F : ModuleSpace K}.

Context {PE : E Prop}.
Context {nPE : nat}.
Hypothesis HPE : has_dim PE nPE.

Context {f : E F}.
Hypothesis Hf : lin_map f.

Lemma RgS_generator :
   {n} {B : 'E^n}, basis PE B lin_gen (RgS PE f) (mapF f B).
Proof.
intros n B [HB _]; apply lm_lin_gen_compat; try easy;
    [apply (has_dim_cms _ HPE) | apply (lin_gen_inclF HB)].
Qed.

Lemma RgS_fin_dim : fin_dim (RgS PE f).
Proof.
destruct HPE as [B HB]; rewrite (RgS_generator HB); apply fin_dim_lin_span.
Qed.

Lemma RgS_preimageF :
   {nr} {Br : 'F^nr}, inclF Br (RgS PE f)
     (Ar : 'E^nr), inclF Ar PE Br = mapF f Ar.
Proof. apply lm_preimageF. Qed.

Lemma lmS_injS_has_dim_equiv : injS PE f has_dim (KerS PE f) 0.
Proof.
rewrite (lmS_injS_equiv (has_dim_cms _ HPE) Hf).
apply iff_sym, has_dim_0_equiv.
Qed.

Lemma lmS_bijS_has_dim_equiv : bijS PE (RgS PE f) f has_dim (KerS PE f) 0.
Proof.
rewrite bijS_RgS_equiv; [| apply inhabited_ms]; apply lmS_injS_has_dim_equiv.
Qed.

End Linear_mapping_Facts3a.

Section Linear_mapping_Facts3b.

Context {K : Ring}.
Context {E F : ModuleSpace K}.

Context {PE : E Prop}.
Variable nPE : nat.
Hypothesis HPE : has_dim PE nPE.
Let HPE' := has_dim_cms _ HPE.

Context {PF : F Prop}.

Context {f : E F}.
Hypothesis Hf : lin_map f.

Lemma RgS_gen_fin_dim : funS PE PF f fin_dim (RgS_gen PE PF f).
Proof. intros; rewrite RgS_gen_eq//; apply (RgS_fin_dim HPE Hf). Qed.

Lemma lmS_injS_val_equiv_alt :
  injS PE f (x : sub_ModuleSpace HPE'), f (val x) = 0 x = 0.
Proof.
pose (f_sub := fun x : sub_ModuleSpace HPE'mk_sub (in_fullset (f (val x)))).
assert (Hf2 : x : sub_ModuleSpace HPE', val (f_sub x) = f (val x)) by easy.
apply: (lmS_injS_val_equiv Hf2 Hf); apply cms_fullset.
Qed.

End Linear_mapping_Facts3b.