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.
Support for linear maps in finite-dimensional module spaces.
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.
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.
Brief description
Description
Usage
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 i ⇒ f (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_n ⇒ mk_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:PEs ⇒ mk_sub (V t): PIs).
pose (fBs := fun i ⇒ fs (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_n ⇒ f (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.