Library Algebra.Finite_dim.Finite_dim_MS_lin_map_R
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 on the ring of
real numbers.
Some results need that the ring of scalars is commutative, or being ordered.
Such results are stated here in the case of the ring of real numbers R_Ring.
For generic results that do not need additional assumption on the ring of
scalars, see Algebra.Finite_dim.Finite_dim_MS_lin_map.
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 stdlib_wR 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_span.
From Algebra Require Import Finite_dim_MS_lin_gen Finite_dim_MS_basis.
From Algebra Require Import Finite_dim_MS_lin_map Finite_dim_MS_basis_R.
Local Open Scope R_scope.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Section Linear_mapping_R_Facts1.
Context {E F : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Context {nPE : nat}.
Hypothesis HPE : has_dim PE nPE.
Context {f : E → F}.
Hypothesis Hf : lin_map f.
Lemma KerS_fin_dim : fin_dim (KerS PE f).
Proof.
apply (fin_dim_monot PE (KerS_incl _ _)).
apply (KerS_cms (has_dim_cms _ HPE) Hf).
apply (has_dim_fin_dim _ HPE).
Qed.
Lemma rank_nullity_thm :
∀ {nr nk},
has_dim (RgS PE f) nr → has_dim (KerS PE f) nk → (nr + nk)%coq_nat = nPE.
Proof.
move: (has_dim_cms _ HPE) ⇒ HPE'.
intros nr nk Hnr Hnk; apply: (dim_is_unique _ HPE).
destruct Hnk as [Bk [HBk1 HBk2]], Hnr as [Br [HBr1 HBr2]].
destruct (RgS_preimageF (lin_gen_inclF HBr1)) as [Ar [HAr1 HAr2]].
apply (Dim _ _ (concatF Ar Bk)); split.
apply lin_gen_ex_decomp_rev; [easy | | intros x Hx].
apply concatF_lub_inclF; [easy |].
apply (inclF_monot_r (KerS PE f));
[apply KerS_incl | apply (lin_gen_inclF HBk1)].
destruct (lin_gen_ex_decomp HBr1 (f x)) as [Lr HLr]; [easy |].
destruct (lin_gen_ex_decomp HBk1 (x - lin_comb Lr Ar)) as [Lk HLk].
apply KerS_correct.
apply cms_minus; [| | apply cms_lc]; easy.
rewrite (lm_minus Hf) HLr HAr2
-f_lc_compat_lm// minus_eq_zero//.
∃ (concatF Lr Lk); rewrite lc_concatF plus_minus_r_equiv; easy.
intros L; rewrite lc_splitF_l; intros HL.
assert (HLr : firstF L = 0).
apply HBr2; rewrite HAr2 -(lm_zero Hf) -HL.
rewrite lm_plus// !(f_lc_compat_lm Hf).
rewrite → (lc_zero_compat_r _ (mapF f Bk)), plus_zero_r; [easy |].
apply extF; intro; apply (lin_gen_inclF HBk1).
rewrite (concatF_splitF L); apply concatF_zero_compat; [easy |].
rewrite HLr lc_zero_l plus_zero_l in HL.
apply (HBk2 _ HL).
Qed.
Lemma rank_nullity_thm_alt_proof :
∀ {nr nk},
has_dim (RgS PE f) nr → has_dim (KerS PE f) nk → (nr + nk)%coq_nat = nPE.
Proof.
move: (has_dim_cms _ HPE) ⇒ HPE'.
intros nr nk Hnr Hnk.
assert (Hn : (nk ≤ nPE)%coq_nat)
by apply (dim_monot _ (KerS_incl _ _) Hnk HPE).
apply eq_sym, (nat_add_sub_equiv_l Hn), (dim_is_unique Hnr).
destruct Hnk as [Bk [HBk1 HBk2]].
move: (lin_gen_inclF HBk1) ⇒ /(inclF_monot_r _ _ _ (KerS_incl PE f)) HBk3.
assert (HBk4 : mapF f Bk = 0)
by (apply extF; intro; apply (lin_gen_inclF HBk1)).
destruct (lin_indep_overbasis_ex HPE HBk3 HBk2) as [m [C [Hm [HC1 HC2]]]].
rewrite Hm Nat.add_comm Nat.add_sub; apply (Dim _ _ (mapF f C)).
rewrite (RgS_generator HPE Hf HC2) mapF_concatF HBk4 lin_span_concatF_r;
[| intro; apply lin_span_zero_closed].
apply basis_lin_span_equiv; intros L; rewrite -f_lc_compat_lm//.
assert (HL : PE (lin_comb L C)).
apply cms_lc; [easy |].
apply (concatF_inclF_reg_r Bk), (basis_inclF HC2).
move⇒ /(KerS_correct HL) /(lin_gen_ex_decomp HBk1) [Lk HLk]; move: HLk.
rewrite -(plus_zero_l (lin_comb _ C)) -(plus_zero_r (lin_comb _ Bk)).
rewrite -{1}(lc_zero_l Bk) -(lc_zero_l C) -!lc_concatF.
move⇒ /(basis_uniq_decomp _ HC2); apply concatF_inj_r.
Qed.
End Linear_mapping_R_Facts1.
Section Linear_mapping_R_Facts2.
Context {E F : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Variable nPE : nat.
Hypothesis HPE : has_dim PE nPE.
Let HPE' := has_dim_cms _ HPE.
Context {PF : F → Prop}.
Variable nPF : nat.
Hypothesis HPF : has_dim PF nPF.
Let HPF' := has_dim_cms _ HPF.
Context {f : E → F}.
Hypothesis Hf : lin_map f.
Hypothesis Hf1 : funS PE PF f.
Lemma lmS_surjS_gen_has_dim_equiv :
surjS PE PF f ↔ has_dim (RgS_gen PE PF f) nPF.
Proof.
rewrite surjS_RgS_gen_equiv RgS_gen_eq//; split. intros; subst; easy.
intros Hf2; apply (dim_eq Hf1 Hf2 HPF); easy.
Qed.
Lemma lmS_bijS_gen_has_dim_equiv :
bijS PE PF f ↔ has_dim (KerS PE f) 0 ∧ has_dim (RgS_gen PE PF f) nPF.
Proof.
rewrite bijS_equiv; [| apply inhabited_ms].
rewrite (lmS_injS_has_dim_equiv HPE Hf) (lmS_surjS_gen_has_dim_equiv); easy.
Qed.
Lemma rank_nullity_thm_gen :
∀ {nr nk},
has_dim (RgS_gen PE PF f) nr → has_dim (KerS PE f) nk →
(nr + nk)%coq_nat = nPE.
Proof. rewrite RgS_gen_eq//; apply rank_nullity_thm; easy. Qed.
Lemma lmS_injS_surjS_gen_equiv : nPF = nPE → injS PE f ↔ surjS PE PF f.
Proof.
intros HnP; rewrite (lmS_injS_has_dim_equiv HPE)// lmS_surjS_gen_has_dim_equiv.
destruct (fin_dim_has_dim (KerS_fin_dim HPE Hf)) as [nk Hnk].
destruct (fin_dim_has_dim (RgS_gen_fin_dim _ HPE Hf Hf1)) as [nr Hnr].
move: (rank_nullity_thm_gen Hnr Hnk) ⇒ Hn; subst; split; intros H.
rewrite (dim_is_unique Hnk H) Nat.add_0_r; easy.
assert (Hnk' : nk = 0).
apply (nat_plus_reg_l nr); rewrite Nat.add_0_r.
apply (dim_is_unique H Hnr).
rewrite Hnk' in Hnk; easy.
Qed.
Lemma lmS_bijS_injS_gen_equiv : nPF = nPE → bijS PE PF f ↔ injS PE f.
Proof.
rewrite bijS_equiv; [| apply inhabited_ms]; split;
[| rewrite lmS_injS_surjS_gen_equiv]; easy.
Qed.
Lemma lmS_bijS_KerS0 : nPF = nPE → KerS0 PE f ↔ bijS PE PF f.
Proof.
intros HnP; rewrite lmS_bijS_injS_gen_equiv// lmS_injS_equiv//.
apply KerS0_correct; [apply cms_zero | apply lm_zero]; easy.
Qed.
Lemma lmS_bijS_surjS_gen_equiv : nPF = nPE → bijS PE PF f ↔ surjS PE PF f.
Proof.
rewrite bijS_equiv; [| apply inhabited_ms]; split;
[| rewrite lmS_injS_surjS_gen_equiv]; easy.
Qed.
Lemma lmS_bijS_val_equiv_alt :
nPF = nPE →
bijS PE PF f ↔ ∀ (x : sub_ModuleSpace HPE'), f (val x) = 0 → x = 0.
Proof.
intros Hn; rewrite (lmS_bijS_injS_gen_equiv Hn);
apply lmS_injS_val_equiv_alt; easy.
Qed.
End Linear_mapping_R_Facts2.
Section Linear_mapping_R_Facts3.
Context {E F : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Variable nPE : nat.
Hypothesis HPE : has_dim PE nPE.
Let HPE' := has_dim_cms _ HPE.
Variable nF : nat.
Hypothesis HF : has_dim (@fullset F) nF.
Context {f : E → F}.
Hypothesis Hf : lin_map f.
Lemma lmS_bijS_val_full_equiv :
nF = nPE →
bijS PE fullset f ↔ ∀ (x : sub_ModuleSpace HPE'), f (val x) = 0 → x = 0.
Proof. apply lmS_bijS_val_equiv_alt; easy. Qed.
End Linear_mapping_R_Facts3.
Section Linear_mapping_R_Facts4.
Context {E : ModuleSpace R_Ring}.
Context {PE' : (E → R) → Prop}.
Context {nPE' : nat}.
Hypothesis HPE' : has_dim PE' nPE'.
Let HPE'' := has_dim_cms _ HPE'.
Context {n : nat}.
Variable A : 'E^n.
Let f : '((E → R) → R)^n := fun i u ⇒ u (A i).
Let Hf : ∀ i, lin_map (f i) := fun i ⇒ lm_pt_eval (A i).
Lemma lmS_bijS_val_gather_equiv :
n = nPE' →
bijS PE' fullset (gather f) ↔
∀ (u : sub_ModuleSpace HPE''), (∀ i, val u (A i) = 0) → u = 0.
Proof.
intros Hn; rewrite (lmS_bijS_val_full_equiv _ HPE' _ has_dim_Rn _ Hn);
[| apply gather_lm_compat, Hf].
split; intros Hf1 [u Hu] Hu1; apply Hf1.
apply extF; intros i; apply Hu1.
intros i; apply (extF_rev _ _ Hu1).
Qed.
End Linear_mapping_R_Facts4.