Library Algebra.ModuleSpace.ModuleSpace_sub
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 module subspaces.
For results that are only valid when the ring of scalars is commutative, or
being ordered, see Algebra.ModuleSpace.ModuleSpace_R_compl where they are
only stated in the case of the ring of real numbers R_Ring.
Let K : Ring and E : ModuleSpace K.
Let PE : E → Prop.
Lemmas about predicate compatible_ms have "cms" in their names, usually as
prefix "cms_", sometimes as suffix "_cms".
Let gen : E → Prop.
Let K : Ring and E1 E2 : ModuleSpace K.
Let PE1 : E1 → Prop.
Let f : E1 → E2.
Let K : Ring and E : ModuleSpace K.
Let PE : E → Prop.
Let HPE : compatible_ms PE.
Let K : Ring and E1 E2 : ModuleSpace K.
Let PE1 : E1 → Prop and PE2 : E2 → Prop.
Let HPE1 : compatible_ms PE1 and HPE2 : compatible_ms PE2.
Let f : E1 → E2.
Let Hf : funS PE1 PE2 f.
[GostiauxT1]
Bernard Gostiaux,
Cours de mathématiques spéciales - 1. Algèbre,
Mathématiques, Presses Universitaires de France, Paris, 1993,
https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre.
This module may be used through the import of Algebra.ModuleSpace.ModuleSpace,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Support for module subspace
- scal_closed PE states that PE is closed under the external law scal;
- scal_rev_closed PE states that for invertible a, PE (scal a u) implies PE u;
- lc_closed PE states that PE is closed under linear combination lin_comb.
- span_ms gen is the specialization span compatible_ms gen (see Algebra.Sub_struct), ie it is the intersection of all subsets (= the smallest) compatible with the ModuleSpace structure that also contain gen.
Additional support for linear map
- f_scal_compat_sub PE1 f states that f preserves the external law scal on PE1;
- lm_sub PE1 f states that f transports the ModuleSpace structure from PE1.
Additional support for module subspace
- sub_ModuleSpace HPE is the type sub PE endowed with the ModuleSpace structure (see Subsets.Sub_type).
- fct_sub_ms HPE1 HPE2 Hf is the function fct_sub Hf with type sub_ModuleSpace HPE1 → sub_ModuleSpace HPE2 (see Subsets.Sub_type).
Bibliography
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 Sub_struct Monoid Group Ring.
From Algebra Require Import ModuleSpace_compl ModuleSpace_lin_comb.
From Algebra Require Import ModuleSpace_lin_map.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Compatible_ModuleSpace_Def.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Definition scal_closed (PE : E → Prop) : Prop :=
∀ a u, PE u → PE (scal a u).
Definition scal_rev_closed (PE : E → Prop) : Prop :=
∀ a u, invertible a → PE (scal a u) → PE u.
Definition lc_closed (PE : E → Prop) : Prop :=
∀ n L (B : 'E^n), inclF B PE → PE (lin_comb L B).
Definition compatible_ms (PE : E → Prop) : Prop:=
compatible_g PE ∧ scal_closed PE.
End Compatible_ModuleSpace_Def.
Section Compatible_ModuleSpace_Facts.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Lemma scal_scal_rev_closed :
∀ {PE : E → Prop}, scal_closed PE → scal_rev_closed PE.
Proof.
intros PE HPE a u [b [Hb _]]; rewrite -{2}(scal_one u) -Hb -scal_assoc; auto.
Qed.
Lemma scal_rev_scal_closed :
∀ {PE : E → Prop},
has_inv K → zero_closed PE → scal_rev_closed PE → scal_closed PE.
Proof.
move=>> HK HPE0 HPE a u Hu; destruct (classic (a = 0)) as [Ha | Ha].
rewrite Ha scal_zero_l; easy. specialize (HK a Ha).
generalize HK; intros [b Hb]; generalize Hb; intros [Hb1 _].
rewrite -(scal_one u) -Hb1 -scal_assoc in Hu; apply (HPE b); try easy.
apply (is_inverse_invertible_r a _ Hb).
Qed.
Lemma scal_closed_equiv :
∀ {PE : E → Prop},
has_inv K → zero_closed PE → scal_closed PE ↔ scal_rev_closed PE.
Proof.
move=>> HK HPE; split.
apply scal_scal_rev_closed.
apply scal_rev_scal_closed; easy.
Qed.
Lemma scal_zero_closed :
∀ {PE : E → Prop}, nonempty PE → scal_closed PE → zero_closed PE.
Proof.
intros PE [x Hx]; unfold zero_closed; rewrite -(scal_zero_l x); auto.
Qed.
Lemma scal_opp_closed :
∀ {PE : E → Prop}, scal_closed PE → opp_closed PE.
Proof. intros PE H u; rewrite <- scal_opp_one; apply H. Qed.
Lemma lc_zero_closed :
∀ {PE : E → Prop}, lc_closed PE → zero_closed PE.
Proof.
move=>> HPE.
destruct (hat0F_is_nonempty K) as [L], (hat0F_is_nonempty E) as [B].
specialize (HPE 0%nat L B); rewrite lc_nil in HPE.
apply HPE, inclF_nil.
Qed.
Lemma plus_scal_lc_closed :
∀ {PE : E → Prop},
nonempty PE → plus_closed PE → scal_closed PE → lc_closed PE.
Proof.
intros PE HPE0 HPE1 HPE2 n L B HB; induction n as [| n Hn].
rewrite lc_nil; apply scal_zero_closed; easy.
rewrite lc_ind_l; apply HPE1. apply HPE2, HB. apply Hn; intro; apply HB.
Qed.
Lemma lc_plus_scal_closed :
∀ {PE : E → Prop},
lc_closed PE → plus_closed PE ∧ scal_closed PE.
Proof.
intros PE HPE; split.
intros u v Hu Hv; rewrite -sum_coupleF -lc_ones_l.
apply HPE; intros i; destruct (ord2_dec i);
[rewrite coupleF_l | rewrite coupleF_r]; easy.
intros a u Hu; replace (scal a u) with (lin_comb (singleF a) (singleF u)).
apply HPE; intro; rewrite singleF_0; easy.
rewrite lc_1 2!singleF_0; easy.
Qed.
Lemma lc_plus_scal_closed_equiv :
∀ {PE : E → Prop},
nonempty PE → lc_closed PE ↔ plus_closed PE ∧ scal_closed PE.
Proof.
intros; split.
apply lc_plus_scal_closed.
intros; apply plus_scal_lc_closed; easy.
Qed.
Lemma plus_scal_closed_cms :
∀ {PE : E → Prop},
nonempty PE → plus_closed PE → scal_closed PE → compatible_ms PE.
Proof.
intros; split; auto.
apply plus_opp_closed_cg; try apply scal_opp_closed; easy.
Qed.
Lemma lc_closed_cms :
∀ {PE : E → Prop}, lc_closed PE → compatible_ms PE.
Proof.
move=>> HPE; apply plus_scal_closed_cms.
∃ 0; apply lc_zero_closed; easy.
1,2: apply lc_plus_scal_closed; easy.
Qed.
Lemma cms_cg : ∀ {PE : E → Prop}, compatible_ms PE → compatible_g PE.
Proof. move=>> H; apply H. Qed.
Lemma cg_cms :
∀ {PE : E → Prop},
scal_closed PE → compatible_g PE → compatible_ms PE.
Proof.
intros; apply plus_scal_closed_cms;
[apply cg_nonempty | apply: cg_plus |]; easy.
Qed.
Lemma cms_cg_equiv :
∀ {PE : E → Prop},
scal_closed PE → compatible_ms PE ↔ compatible_g PE.
Proof. intros; split; [apply cms_cg | apply cg_cms; easy]. Qed.
Lemma cms_cm : ∀ {PE : E → Prop}, compatible_ms PE → compatible_m PE.
Proof. move=>> /cms_cg; apply: cg_cm. Qed.
Lemma cm_cms :
∀ {PE : E → Prop},
scal_closed PE → compatible_m PE → compatible_ms PE.
Proof.
intros; apply cg_cms; [| apply cm_cg; [apply scal_opp_closed |]]; easy.
Qed.
Lemma cms_cm_equiv :
∀ {PE : E → Prop},
scal_closed PE → compatible_ms PE ↔ compatible_m PE.
Proof. intros; split; [apply cms_cm | apply cm_cms; easy]. Qed.
Lemma cms_nonempty : ∀ {PE : E → Prop}, compatible_ms PE → nonempty PE.
Proof. move=>> /cms_cg; apply cg_nonempty. Qed.
Lemma cms_zero : ∀ {PE : E → Prop}, compatible_ms PE → zero_closed PE.
Proof. move=>> /cms_cg; apply: cg_zero. Qed.
Lemma cms_plus : ∀ {PE : E → Prop}, compatible_ms PE → plus_closed PE.
Proof. move=>> /cms_cg; apply: cg_plus. Qed.
Lemma cms_opp : ∀ {PE : E → Prop}, compatible_ms PE → opp_closed PE.
Proof. move=>> /cms_cg; apply cg_opp. Qed.
Lemma cms_minus : ∀ {PE : E → Prop}, compatible_ms PE → minus_closed PE.
Proof. move=>> /cms_cg; apply cg_minus. Qed.
Lemma cms_scal : ∀ {PE : E → Prop}, compatible_ms PE → scal_closed PE.
Proof. move=>> [_ H]; move=>>; apply H. Qed.
Lemma cms_scal_rev :
∀ {PE : E → Prop}, compatible_ms PE → scal_rev_closed PE.
Proof. move=>> /cms_scal; apply scal_scal_rev_closed. Qed.
Lemma cms_lc : ∀ {PE : E → Prop}, compatible_ms PE → lc_closed PE.
Proof.
intros PE HPE n L B HB; induction n as [| n Hn].
rewrite lc_nil.
apply cms_zero; easy.
rewrite lc_ind_l.
apply cms_plus; try easy.
apply HPE, HB.
apply Hn.
intros i; apply HB.
Qed.
Lemma cms_lc_equiv :
∀ {PE : E → Prop}, compatible_ms PE ↔ lc_closed PE.
Proof. intros; split; [apply cms_lc | apply lc_closed_cms]. Qed.
Lemma cms_plus_equiv :
∀ {PE : E → Prop},
compatible_ms PE → ∀ u v, PE u → PE (u + v) ↔ PE v.
Proof.
intros PE HPE u v Hu; split; [rewrite -{2}(minus_plus_l u v) minus_sym | ].
1,2: apply cms_plus; try easy.
apply cms_opp; easy.
Qed.
Lemma cms_zero_sub_struct : compatible_ms (@zero_sub_struct E).
Proof.
split; try apply: cg_zero_sub_struct.
intros u a Hu; rewrite Hu scal_zero_r; easy.
Qed.
Lemma cms_full : ∀ {PE : E → Prop}, full PE → compatible_ms PE.
Proof. intros; split; try apply cg_full; easy. Qed.
Lemma cms_fullset : compatible_ms (@fullset E).
Proof. apply cms_full; easy. Qed.
Lemma scal_closed_inter :
∀ {PE QE : E → Prop},
scal_closed PE → scal_closed QE → scal_closed (inter PE QE).
Proof. move=>> HPE HQE u a [HuPE HuQE]; split; auto. Qed.
Lemma cms_inter :
∀ {PE QE : E → Prop},
compatible_ms PE → compatible_ms QE → compatible_ms (inter PE QE).
Proof.
move=>> [HPE1 HPE2] [HQE1 HQE2]; split;
[apply cg_inter | apply scal_closed_inter]; easy.
Qed.
[GostiauxT1]
Th 6.15, p. 167.
Lemma scal_closed_inter_any :
∀ {Idx : Type} {PE : Idx → E → Prop},
(∀ i, scal_closed (PE i)) → scal_closed (inter_any PE).
Proof. move=>> HPE x l Hx i; apply HPE; easy. Qed.
∀ {Idx : Type} {PE : Idx → E → Prop},
(∀ i, scal_closed (PE i)) → scal_closed (inter_any PE).
Proof. move=>> HPE x l Hx i; apply HPE; easy. Qed.
[GostiauxT1]
Th 6.15, p. 167.
Lemma cms_inter_any :
∀ {Idx : Type} {PE : Idx → E → Prop},
(∀ i, compatible_ms (PE i)) → compatible_ms (inter_any PE).
Proof.
move=>> HPE; split.
apply cg_inter_any; intro; apply cms_cg; easy.
apply scal_closed_inter_any; intro; apply HPE.
Qed.
∀ {Idx : Type} {PE : Idx → E → Prop},
(∀ i, compatible_ms (PE i)) → compatible_ms (inter_any PE).
Proof.
move=>> HPE; split.
apply cg_inter_any; intro; apply cms_cg; easy.
apply scal_closed_inter_any; intro; apply HPE.
Qed.
[GostiauxT1]
Th 6.17, p. 168.
Definition span_ms (gen : E → Prop) := span compatible_ms gen.
Lemma span_ms_cms : ∀ gen, compatible_ms (span_ms gen).
Proof. apply span_compatible; move=>>; apply cms_inter_any. Qed.
Lemma span_ms_nonempty : ∀ (gen : E → Prop), nonempty (span_ms gen).
Proof. intros; apply cms_nonempty, span_ms_cms. Qed.
Lemma span_ms_zero : ∀ (gen : E → Prop), zero_closed (span_ms gen).
Proof. intros; apply cms_zero; apply span_ms_cms. Qed.
Lemma span_ms_plus : ∀ (gen : E → Prop), plus_closed (span_ms gen).
Proof. intros; apply cms_plus, span_ms_cms. Qed.
Lemma span_ms_opp : ∀ (gen : E → Prop), opp_closed (span_ms gen).
Proof. intros; apply cms_opp, span_ms_cms. Qed.
Lemma span_ms_minus : ∀ (gen : E → Prop), minus_closed (span_ms gen).
Proof. intros; apply cms_minus, span_ms_cms. Qed.
Lemma span_ms_scal : ∀ (gen : E → Prop), scal_closed (span_ms gen).
Proof. intros; apply cms_scal, span_ms_cms. Qed.
Lemma span_ms_lc : ∀ (gen : E → Prop), lc_closed (span_ms gen).
Proof. intros; apply cms_lc, span_ms_cms. Qed.
Lemma span_ms_incl : ∀ gen, incl gen (span_ms gen).
Proof. apply span_incl. Qed.
Lemma span_ms_cms : ∀ gen, compatible_ms (span_ms gen).
Proof. apply span_compatible; move=>>; apply cms_inter_any. Qed.
Lemma span_ms_nonempty : ∀ (gen : E → Prop), nonempty (span_ms gen).
Proof. intros; apply cms_nonempty, span_ms_cms. Qed.
Lemma span_ms_zero : ∀ (gen : E → Prop), zero_closed (span_ms gen).
Proof. intros; apply cms_zero; apply span_ms_cms. Qed.
Lemma span_ms_plus : ∀ (gen : E → Prop), plus_closed (span_ms gen).
Proof. intros; apply cms_plus, span_ms_cms. Qed.
Lemma span_ms_opp : ∀ (gen : E → Prop), opp_closed (span_ms gen).
Proof. intros; apply cms_opp, span_ms_cms. Qed.
Lemma span_ms_minus : ∀ (gen : E → Prop), minus_closed (span_ms gen).
Proof. intros; apply cms_minus, span_ms_cms. Qed.
Lemma span_ms_scal : ∀ (gen : E → Prop), scal_closed (span_ms gen).
Proof. intros; apply cms_scal, span_ms_cms. Qed.
Lemma span_ms_lc : ∀ (gen : E → Prop), lc_closed (span_ms gen).
Proof. intros; apply cms_lc, span_ms_cms. Qed.
Lemma span_ms_incl : ∀ gen, incl gen (span_ms gen).
Proof. apply span_incl. Qed.
[GostiauxT1]
Def 6.16, p. 167.
Lemma span_ms_lub :
∀ {gen PE}, compatible_ms PE → incl gen PE → incl (span_ms gen) PE.
Proof. apply span_lub. Qed.
Lemma span_ms_full : ∀ {PE}, compatible_ms PE → span_ms PE = PE.
Proof. apply span_full. Qed.
End Compatible_ModuleSpace_Facts.
Section Compatible_ModuleSpace_Lin_map_Facts0.
Context {K : Ring}.
Context {E1 E2 E3 : ModuleSpace K}.
Lemma cg_lm : compatible_g (@lin_map _ E1 E2).
Proof.
split; [split |]; [move=>>; apply lm_fct_plus | apply lm_fct_zero |
move=>>; apply lm_fct_opp].
Qed.
Lemma cg_blm : compatible_g (@bilin_map _ E1 E2 E3).
Proof.
split; [split |]; [move=>>; apply blm_fct_plus | apply blm_fct_zero |
move=>>; apply blm_fct_opp].
Qed.
End Compatible_ModuleSpace_Lin_map_Facts0.
Section Compatible_ModuleSpace_Lin_map_Facts1.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Context {f : E1 → E2}.
Hypothesis Hf : lin_map f.
Lemma cms_image : compatible_ms PE1 → compatible_ms (image f PE1).
Proof.
destruct Hf as [_ Hf1]; intros [HPE1a HPE1b]; split.
apply cg_image; [apply lm_mg |]; easy.
intros a _ [u1 Hu1]; rewrite -Hf1; apply Im; auto.
Qed.
Lemma cms_preimage : compatible_ms PE2 → compatible_ms (preimage f PE2).
Proof.
destruct Hf as [_ Hf1]; intros [HPE2a HPE2b]; split.
apply cg_preimage; [apply lm_mg |]; easy.
intros u a Hu; unfold preimage; rewrite Hf1; auto.
Qed.
End Compatible_ModuleSpace_Lin_map_Facts1.
Section Compatible_ModuleSpace_Lin_map_Def.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Variable PE1 : E1 → Prop.
Variable f : E1 → E2.
Definition f_scal_compat_sub : Prop :=
∀ a x1 , PE1 x1 → f (scal a x1) = scal a (f x1).
Definition lm_sub : Prop := f_plus_compat_sub PE1 f ∧ f_scal_compat_sub.
End Compatible_ModuleSpace_Lin_map_Def.
Section Compatible_ModuleSpace_Lin_map_Facts2a.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Hypothesis HPE1 : compatible_ms PE1.
Context {PE2 : E2 → Prop}.
Hypothesis HPE2 : compatible_ms PE2.
Context {f : E1 → E2}.
Hypothesis Hf : lin_map f.
Lemma KerS_cms : compatible_ms (KerS PE1 f).
Proof. apply cms_inter, cms_preimage, cms_zero_sub_struct; easy. Qed.
Lemma RgS_gen_cms : compatible_ms (RgS_gen PE1 PE2 f).
Proof. apply cms_inter, cms_image; easy. Qed.
Lemma RgS_cms : compatible_ms (RgS PE1 f).
Proof. apply cms_image; easy. Qed.
Lemma KerS_zero_equiv :
KerS PE1 f = zero_sub_struct ↔ incl (KerS PE1 f) zero_sub_struct.
Proof. apply: KerS_g_zero_equiv; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_injS : incl (KerS PE1 f) zero_sub_struct → injS PE1 f.
Proof. apply: gmS_injS; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_injS_rev : injS PE1 f → KerS PE1 f = zero_sub_struct.
Proof. apply: gmS_injS_rev; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_injS_equiv : injS PE1 f ↔ KerS PE1 f = zero_sub_struct.
Proof. apply: gmS_injS_equiv; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_gen :
funS PE1 PE2 f → incl (KerS PE1 f) zero_sub_struct → incl PE2 (RgS PE1 f) →
bijS PE1 PE2 f.
Proof. apply: gmS_bijS_gen; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_gen_rev :
bijS PE1 PE2 f →
funS PE1 PE2 f ∧ KerS PE1 f = zero_sub_struct ∧ RgS_gen PE1 PE2 f = PE2.
Proof. apply: gmS_bijS_gen_rev; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_gen_equiv :
bijS PE1 PE2 f ↔
funS PE1 PE2 f ∧ KerS PE1 f = zero_sub_struct ∧ RgS_gen PE1 PE2 f = PE2.
Proof. apply: gmS_bijS_gen_equiv; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS : incl (KerS PE1 f) zero_sub_struct → bijS PE1 (RgS PE1 f) f.
Proof. apply: gmS_bijS; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_rev : bijS PE1 (RgS PE1 f) f → KerS PE1 f = zero_sub_struct.
Proof. apply: gmS_bijS_rev; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_equiv : bijS PE1 (RgS PE1 f) f ↔ KerS PE1 f = zero_sub_struct.
Proof. apply: gmS_bijS_equiv; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_injS_equiv : bijS PE1 (RgS PE1 f) f ↔ injS PE1 f.
Proof. apply gmS_bijS_injS_equiv. Qed.
End Compatible_ModuleSpace_Lin_map_Facts2a.
Section Compatible_ModuleSpace_Lin_map_Facts2b.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {f : E1 → E2}.
Hypothesis Hf : lin_map f.
Lemma Ker_cms : compatible_ms (Ker f).
Proof. rewrite -KerS_full; apply (KerS_cms cms_fullset Hf). Qed.
Lemma Rg_cms : compatible_ms (Rg f).
Proof. rewrite -RgS_full; apply (RgS_cms cms_fullset Hf). Qed.
Lemma Ker_zero_equiv :
Ker f = zero_sub_struct ↔ incl (Ker f) zero_sub_struct.
Proof. apply: Ker_g_zero_equiv; apply lm_mg; easy. Qed.
Lemma lm_inj : incl (Ker f) zero_sub_struct → injective f.
Proof. apply: gm_inj; apply lm_mg; easy. Qed.
Lemma lm_inj_rev : injective f → Ker f = zero_sub_struct.
Proof. apply: gm_inj_rev; apply lm_mg; easy. Qed.
Lemma lm_inj_equiv : injective f ↔ Ker f = zero_sub_struct.
Proof. apply: gm_inj_equiv; apply lm_mg; easy. Qed.
Lemma lm_bij :
incl (Ker f) zero_sub_struct → incl fullset (Rg f) → bijective f.
Proof. apply: gm_bij; apply lm_mg; easy. Qed.
Lemma lm_bij_rev : bijective f → Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof. apply: gm_bij_rev; apply lm_mg; easy. Qed.
Lemma lm_bij_equiv : bijective f ↔ Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof. apply: gm_bij_equiv; apply lm_mg; easy. Qed.
End Compatible_ModuleSpace_Lin_map_Facts2b.
Section Compatible_ModuleSpace_Lin_map_Facts3.
Context {K : Ring}.
Context {E1 E2 E3 : ModuleSpace K}.
Context {f : E1 → E2}.
Hypothesis Hf : lin_map f.
Context {g : E2 → E3}.
Hypothesis Hg : lin_map g.
Lemma Ker_comp_r : injective g → RgS (Ker (g \o f)) f = Ker g.
Proof. apply: Ker_g_comp_r; apply lm_mg; easy. Qed.
Lemma Ker_comp_r_alt :
∀ h x2, injective g → h = g \o f →
(∃ x1, h x1 = 0 ∧ f x1 = x2) ↔ g x2 = 0.
Proof. apply: Ker_g_comp_r_alt; apply lm_mg; easy. Qed.
End Compatible_ModuleSpace_Lin_map_Facts3.
Section Compatible_ModuleSpace_Lin_map_Facts4a.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Variable PE1 : E1 → Prop.
Lemma f_scal_compat_sub_id : f_scal_compat_sub PE1 ssrfun.id.
Proof. easy. Qed.
Lemma lm_sub_id : lm_sub PE1 ssrfun.id.
Proof. easy. Qed.
Context {f : E1 → E2}.
Lemma f_scal_compat_is_sub : f_scal_compat f → f_scal_compat_sub PE1 f.
Proof. easy. Qed.
Lemma lm_is_sub : lin_map f → lm_sub PE1 f.
Proof. intros [Hfa Hfb]; easy. Qed.
End Compatible_ModuleSpace_Lin_map_Facts4a.
Section Compatible_ModuleSpace_Lin_map_Facts4b.
Context {K : Ring}.
Context {E1 E2 E3 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Variable PE2 : E2 → Prop.
Context {f : E1 → E2}.
Hypothesis Hf : funS PE1 PE2 f.
Variable g : E2 → E3.
Lemma f_scal_compat_comp_sub :
f_scal_compat_sub PE1 f → f_scal_compat_sub PE2 g →
f_scal_compat_sub PE1 (g \o f).
Proof.
intros Hf1 Hg1 a x1 Hx1; rewrite comp_correct Hf1// Hg1//; apply Hf; easy.
Qed.
Lemma lm_comp_sub : lm_sub PE1 f → lm_sub PE2 g → lm_sub PE1 (g \o f).
Proof.
intros [Hfa Hfb] [Hga Hgb]; split;
[apply (f_plus_compat_comp_sub PE2) | apply f_scal_compat_comp_sub]; easy.
Qed.
End Compatible_ModuleSpace_Lin_map_Facts4b.
Section Sub_ModuleSpace_Def.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_g := sub_AbelianGroup (cms_cg HPE).
Definition sub_scal a (x : PE_g) : PE_g :=
mk_sub (cms_scal HPE a (val x) (in_sub x)).
Lemma sub_scal_assoc :
∀ a b x, sub_scal a (sub_scal b x) = sub_scal (a × b) x.
Proof. intros; apply val_inj, scal_assoc. Qed.
Lemma sub_scal_one_l : ∀ x, sub_scal 1 x = x.
Proof. intros; apply val_inj, scal_one. Qed.
Lemma sub_scal_distr_l :
∀ a x y, sub_scal a (x + y) = sub_scal a x + sub_scal a y.
Proof. intros; apply val_inj, scal_distr_l. Qed.
Lemma sub_scal_distr_r :
∀ a b x, sub_scal (a + b) x = sub_scal a x + sub_scal b x.
Proof. intros; apply val_inj, scal_distr_r. Qed.
Definition sub_ModuleSpace_mixin :=
ModuleSpace.Mixin _ _ _
sub_scal_assoc sub_scal_one_l sub_scal_distr_l sub_scal_distr_r.
Canonical Structure sub_ModuleSpace :=
ModuleSpace.Pack _ _
(ModuleSpace.Class _ _ _ sub_ModuleSpace_mixin) PE_g.
Lemma val_scal : f_scal_compat val.
Proof. easy. Qed.
Lemma val_lc : f_lc_compat val.
Proof.
intros n; induction n as [| n Hn].
intros; rewrite 2!lc_nil; easy.
intros; rewrite 2!lc_ind_l; simpl; f_equal; apply Hn.
Qed.
Lemma val_lm : lin_map val.
Proof. easy. Qed.
Lemma mk_sub_ms_zero : mk_sub (cms_zero HPE : PE 0) = 0 :> sub_ModuleSpace.
Proof. apply val_inj; easy. Qed.
Lemma mk_sub_ms_zero_equiv :
∀ {x} (Hx : PE x), mk_sub Hx = 0 :> sub_ModuleSpace ↔ x = 0.
Proof. apply mk_sub_zero_equiv. Qed.
Lemma mk_sub_scal :
∀ a (x : E) (Hx : PE x),
scal a (mk_sub Hx) = mk_sub (cms_scal HPE a _ Hx).
Proof. easy. Qed.
Lemma mk_sub_lc :
∀ {n} L (B : 'E^n) (HB : inclF B PE),
lin_comb L (fun i ⇒ mk_sub (HB i)) = mk_sub (cms_lc HPE _ L _ HB).
Proof. intros; apply val_inj, val_lc. Qed.
Lemma sub_scal_eq :
∀ a (x : sub_ModuleSpace),
scal a x = mk_sub (cms_scal HPE a _ (in_sub x)).
Proof. easy. Qed.
Lemma sub_lc_eq :
∀ {n} L (B : '(sub_ModuleSpace)^n),
lin_comb L B = mk_sub (cms_lc HPE _ L _ (fun i ⇒ in_sub (B i))).
Proof. intros; apply mk_sub_lc. Qed.
Lemma val_ms_inv_r :
∀ {x} (Hx : PE x), val (mk_sub Hx : sub_ModuleSpace) = x.
Proof. apply val_g_inv_r, cms_cg; easy. Qed.
Lemma mk_sub_ms_inv_r : ∀ {x}, mk_sub (in_sub x) = x :> sub_ModuleSpace.
Proof. intros; apply mk_sub_inv_r. Qed.
Lemma mk_sub_ms_inj :
∀ {x y} (Hx : PE x) (Hy : PE y),
mk_sub Hx = mk_sub Hy :> sub_ModuleSpace → x = y.
Proof. intros x y; apply mk_sub_inj. Qed.
End Sub_ModuleSpace_Def.
Section Sub_ModuleSpace_Facts1.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PEa PE : E → Prop}.
Hypothesis HPEa : incl PEa PE.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Let PEa' : PE_ms → Prop := preimage val PEa.
Lemma RgS_val_ms_eq : RgS PEa' val = PEa.
Proof. apply RgS_val_eq; easy. Qed.
Lemma preimage_val_cms : compatible_ms PEa → compatible_ms PEa'.
Proof. intros; apply cms_preimage; easy. Qed.
Lemma preimage_val_cms_rev : compatible_ms PEa' → compatible_ms PEa.
Proof. intros; rewrite -RgS_val_ms_eq; apply RgS_cms; easy. Qed.
Lemma preimage_val_cms_equiv : compatible_ms PEa' ↔ compatible_ms PEa.
Proof. split; [apply preimage_val_cms_rev | apply preimage_val_cms]. Qed.
End Sub_ModuleSpace_Facts1.
Section Sub_ModuleSpace_Facts2.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Variable PEa : PE_ms → Prop.
Let PEa' := RgS PEa val.
Lemma preimage_val_ms_eq : preimage val PEa' = PEa.
Proof. apply preimage_val_eq. Qed.
Lemma RgS_val_cms : compatible_ms PEa → compatible_ms PEa'.
Proof. intros; apply RgS_cms; easy. Qed.
Lemma RgS_val_cms_rev : compatible_ms PEa' → compatible_ms PEa.
Proof. intros; rewrite -preimage_val_ms_eq; apply cms_preimage; easy. Qed.
Lemma RgS_val_cms_equiv : compatible_ms PEa' ↔ compatible_ms PEa.
Proof. split; [apply RgS_val_cms_rev | apply RgS_val_cms]. Qed.
End Sub_ModuleSpace_Facts2.
Section Sub_ModuleSpace_Lin_map_Facts1.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Context {HPE1 : compatible_ms PE1}.
Context {HPE2 : compatible_ms PE2}.
Let PE1_ms := sub_ModuleSpace HPE1.
Let PE2_ms := sub_ModuleSpace HPE2.
Context {f : E1 → E2}.
Context {fS : PE1_ms → PE2_ms}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_ms_f_scal_compat : f_scal_compat f → f_scal_compat fS.
Proof. intros Hf a x1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
Lemma sub_ms_f_lc_compat : f_lc_compat f → f_lc_compat fS.
Proof.
intros Hf n L B; apply val_inj; rewrite HfS !val_lc Hf; f_equal.
apply extF; intros i; rewrite !mapF_correct; easy.
Qed.
Lemma sub_ms_lm : lin_map f → lin_map fS.
Proof.
intros [Hf1 Hf2]; split; [apply (sub_g_morphism HfS Hf1) |
move=>>; apply sub_ms_f_scal_compat; move=>>; easy].
Qed.
Lemma Ker_sub_ms_KerS_zero_equiv :
lin_map f →
Ker fS = zero_sub_struct ↔ KerS PE1 f = zero_sub_struct.
Proof. intros Hf; apply (Ker_sub_g_KerS_zero_equiv HfS), lm_mg, Hf. Qed.
Lemma KerS_ms_zero_equiv_alt :
lin_map f →
KerS PE1 f = zero_sub_struct ↔
∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. intros H; apply: KerS_g_zero_equiv_alt; apply lm_mg, H. Qed.
Lemma Ker_sub_ms_zero_equiv :
lin_map f →
Ker fS = zero_sub_struct ↔
∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. intros Hf; apply (Ker_sub_g_zero_equiv HfS), lm_mg, Hf. Qed.
Lemma lmS_injS_sub_equiv :
lin_map f → injS PE1 f ↔ Ker fS = zero_sub_struct.
Proof. intros Hf; apply (gmS_injS_sub_equiv HfS), lm_mg, Hf. Qed.
Lemma lmS_injS_val_equiv :
lin_map f →
injS PE1 f ↔ ∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. intros Hf; apply: (gmS_injS_val_equiv HfS); apply lm_mg, Hf. Qed.
Lemma lmS_bijS_sub_equiv :
lin_map f → bijS PE1 (RgS PE1 f) f ↔ Ker fS = zero_sub_struct.
Proof. intros Hf; apply (gmS_bijS_sub_equiv HfS), lm_mg, Hf. Qed.
Lemma lmS_bijS_val_equiv :
lin_map f →
bijS PE1 (RgS PE1 f) f ↔
∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. intros Hf; apply: (gmS_bijS_val_equiv HfS); apply lm_mg, Hf. Qed.
End Sub_ModuleSpace_Lin_map_Facts1.
Section Sub_ModuleSpace_Lin_map_Facts2.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Hypothesis HPE1 : compatible_ms PE1.
Hypothesis HPE2 : compatible_ms PE2.
Let PE1_ms := sub_ModuleSpace HPE1.
Let PE2_ms := sub_ModuleSpace HPE2.
Context {f : E1 → E2}.
Hypothesis Hf : funS PE1 PE2 f.
Definition fct_sub_ms : PE1_ms → PE2_ms := fct_sub Hf.
Lemma fct_sub_ms_inj : injS PE1 f → injective fct_sub_ms.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_ms_inj_rev : injective fct_sub_ms → injS PE1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_ms_inj_equiv : injective fct_sub_ms ↔ injS PE1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_ms_surj : surjS PE1 PE2 f → surjective fct_sub_ms.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_ms_surj_rev : surjective fct_sub_ms → surjS PE1 PE2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_ms_surj_equiv : surjective fct_sub_ms ↔ surjS PE1 PE2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_ms_bij : bijS PE1 PE2 f → bijective fct_sub_ms.
Proof. apply fct_sub_bij, inhabited_ms. Qed.
Lemma fct_sub_ms_bij_rev : bijective fct_sub_ms → bijS PE1 PE2 f.
Proof. apply fct_sub_bij_rev, inhabited_ms. Qed.
Lemma fct_sub_ms_bij_equiv : bijective fct_sub_ms ↔ bijS PE1 PE2 f.
Proof. apply fct_sub_bij_equiv, inhabited_ms. Qed.
Lemma fct_sub_ms_f_scal_compat : f_scal_compat f → f_scal_compat fct_sub_ms.
Proof. apply sub_ms_f_scal_compat, fct_sub_correct. Qed.
Lemma fct_sub_ms_f_lc_compat : f_lc_compat f → f_lc_compat fct_sub_ms.
Proof. apply sub_ms_f_lc_compat, fct_sub_correct. Qed.
Lemma fct_sub_ms_lm : lin_map f → lin_map fct_sub_ms.
Proof. apply sub_ms_lm, fct_sub_correct. Qed.
Lemma fct_sub_ms_f_inv_lm :
∀ (Hfb : bijS PE1 PE2 f),
lin_map f → lin_map (f_inv (fct_sub_ms_bij Hfb)).
Proof. intros; apply lm_bij_compat, fct_sub_ms_lm; easy. Qed.
Lemma Ker_fct_sub_ms_KerS_zero_equiv :
lin_map f →
Ker fct_sub_ms = zero_sub_struct ↔ KerS PE1 f = zero_sub_struct.
Proof. apply Ker_sub_ms_KerS_zero_equiv, fct_sub_correct. Qed.
Lemma Ker_fct_sub_ms_zero_equiv :
lin_map f →
Ker fct_sub_ms = zero_sub_struct ↔
∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. apply Ker_sub_ms_zero_equiv, fct_sub_correct. Qed.
Lemma lmS_injS_fct_sub_equiv :
lin_map f → injS PE1 f ↔ Ker fct_sub_ms = zero_sub_struct.
Proof. apply lmS_injS_sub_equiv, fct_sub_correct. Qed.
Lemma lmS_bijS_fct_sub_equiv :
lin_map f →
bijS PE1 (RgS PE1 f) f ↔ Ker fct_sub_ms = zero_sub_struct.
Proof. apply lmS_bijS_sub_equiv, fct_sub_correct. Qed.
End Sub_ModuleSpace_Lin_map_Facts2.
Section Compose_n_ModuleSpace_Facts.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Context {n : nat}.
Variable f : '(E → E)^n.
Hypothesis Hf : ∀ i, funS PE PE (f i).
Lemma comp_n_f_scal_compat_sub :
(∀ i, f_scal_compat_sub PE (f i)) → f_scal_compat_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
[rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (f_scal_compat_comp_sub PE);
[apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.
Lemma comp_n_lm_sub :
(∀ i, lm_sub PE (f i)) →
lm_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
[rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (lm_comp_sub PE);
[apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.
End Compose_n_ModuleSpace_Facts.
Section Compose_n_part_ModuleSpace_Facts.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Context {n : nat}.
Variable f : '(E → E)^n.
Variable j : 'I_n.+1.
Hypothesis Hf : ∀ i, funS PE PE (widenF (leq_ord j) f i).
Lemma comp_n_part_f_scal_compat_sub :
(∀ i, f_scal_compat_sub PE (widenF (leq_ord j) f i)) →
f_scal_compat_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
[rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (f_scal_compat_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.
Lemma comp_n_part_lm_sub :
(∀ i, lm_sub PE (widenF (leq_ord j) f i)) →
lm_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
[rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (lm_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.
End Compose_n_part_ModuleSpace_Facts.
∀ {gen PE}, compatible_ms PE → incl gen PE → incl (span_ms gen) PE.
Proof. apply span_lub. Qed.
Lemma span_ms_full : ∀ {PE}, compatible_ms PE → span_ms PE = PE.
Proof. apply span_full. Qed.
End Compatible_ModuleSpace_Facts.
Section Compatible_ModuleSpace_Lin_map_Facts0.
Context {K : Ring}.
Context {E1 E2 E3 : ModuleSpace K}.
Lemma cg_lm : compatible_g (@lin_map _ E1 E2).
Proof.
split; [split |]; [move=>>; apply lm_fct_plus | apply lm_fct_zero |
move=>>; apply lm_fct_opp].
Qed.
Lemma cg_blm : compatible_g (@bilin_map _ E1 E2 E3).
Proof.
split; [split |]; [move=>>; apply blm_fct_plus | apply blm_fct_zero |
move=>>; apply blm_fct_opp].
Qed.
End Compatible_ModuleSpace_Lin_map_Facts0.
Section Compatible_ModuleSpace_Lin_map_Facts1.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Context {f : E1 → E2}.
Hypothesis Hf : lin_map f.
Lemma cms_image : compatible_ms PE1 → compatible_ms (image f PE1).
Proof.
destruct Hf as [_ Hf1]; intros [HPE1a HPE1b]; split.
apply cg_image; [apply lm_mg |]; easy.
intros a _ [u1 Hu1]; rewrite -Hf1; apply Im; auto.
Qed.
Lemma cms_preimage : compatible_ms PE2 → compatible_ms (preimage f PE2).
Proof.
destruct Hf as [_ Hf1]; intros [HPE2a HPE2b]; split.
apply cg_preimage; [apply lm_mg |]; easy.
intros u a Hu; unfold preimage; rewrite Hf1; auto.
Qed.
End Compatible_ModuleSpace_Lin_map_Facts1.
Section Compatible_ModuleSpace_Lin_map_Def.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Variable PE1 : E1 → Prop.
Variable f : E1 → E2.
Definition f_scal_compat_sub : Prop :=
∀ a x1 , PE1 x1 → f (scal a x1) = scal a (f x1).
Definition lm_sub : Prop := f_plus_compat_sub PE1 f ∧ f_scal_compat_sub.
End Compatible_ModuleSpace_Lin_map_Def.
Section Compatible_ModuleSpace_Lin_map_Facts2a.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Hypothesis HPE1 : compatible_ms PE1.
Context {PE2 : E2 → Prop}.
Hypothesis HPE2 : compatible_ms PE2.
Context {f : E1 → E2}.
Hypothesis Hf : lin_map f.
Lemma KerS_cms : compatible_ms (KerS PE1 f).
Proof. apply cms_inter, cms_preimage, cms_zero_sub_struct; easy. Qed.
Lemma RgS_gen_cms : compatible_ms (RgS_gen PE1 PE2 f).
Proof. apply cms_inter, cms_image; easy. Qed.
Lemma RgS_cms : compatible_ms (RgS PE1 f).
Proof. apply cms_image; easy. Qed.
Lemma KerS_zero_equiv :
KerS PE1 f = zero_sub_struct ↔ incl (KerS PE1 f) zero_sub_struct.
Proof. apply: KerS_g_zero_equiv; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_injS : incl (KerS PE1 f) zero_sub_struct → injS PE1 f.
Proof. apply: gmS_injS; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_injS_rev : injS PE1 f → KerS PE1 f = zero_sub_struct.
Proof. apply: gmS_injS_rev; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_injS_equiv : injS PE1 f ↔ KerS PE1 f = zero_sub_struct.
Proof. apply: gmS_injS_equiv; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_gen :
funS PE1 PE2 f → incl (KerS PE1 f) zero_sub_struct → incl PE2 (RgS PE1 f) →
bijS PE1 PE2 f.
Proof. apply: gmS_bijS_gen; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_gen_rev :
bijS PE1 PE2 f →
funS PE1 PE2 f ∧ KerS PE1 f = zero_sub_struct ∧ RgS_gen PE1 PE2 f = PE2.
Proof. apply: gmS_bijS_gen_rev; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_gen_equiv :
bijS PE1 PE2 f ↔
funS PE1 PE2 f ∧ KerS PE1 f = zero_sub_struct ∧ RgS_gen PE1 PE2 f = PE2.
Proof. apply: gmS_bijS_gen_equiv; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS : incl (KerS PE1 f) zero_sub_struct → bijS PE1 (RgS PE1 f) f.
Proof. apply: gmS_bijS; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_rev : bijS PE1 (RgS PE1 f) f → KerS PE1 f = zero_sub_struct.
Proof. apply: gmS_bijS_rev; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_equiv : bijS PE1 (RgS PE1 f) f ↔ KerS PE1 f = zero_sub_struct.
Proof. apply: gmS_bijS_equiv; [apply cms_cg | apply lm_mg]; easy. Qed.
Lemma lmS_bijS_injS_equiv : bijS PE1 (RgS PE1 f) f ↔ injS PE1 f.
Proof. apply gmS_bijS_injS_equiv. Qed.
End Compatible_ModuleSpace_Lin_map_Facts2a.
Section Compatible_ModuleSpace_Lin_map_Facts2b.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {f : E1 → E2}.
Hypothesis Hf : lin_map f.
Lemma Ker_cms : compatible_ms (Ker f).
Proof. rewrite -KerS_full; apply (KerS_cms cms_fullset Hf). Qed.
Lemma Rg_cms : compatible_ms (Rg f).
Proof. rewrite -RgS_full; apply (RgS_cms cms_fullset Hf). Qed.
Lemma Ker_zero_equiv :
Ker f = zero_sub_struct ↔ incl (Ker f) zero_sub_struct.
Proof. apply: Ker_g_zero_equiv; apply lm_mg; easy. Qed.
Lemma lm_inj : incl (Ker f) zero_sub_struct → injective f.
Proof. apply: gm_inj; apply lm_mg; easy. Qed.
Lemma lm_inj_rev : injective f → Ker f = zero_sub_struct.
Proof. apply: gm_inj_rev; apply lm_mg; easy. Qed.
Lemma lm_inj_equiv : injective f ↔ Ker f = zero_sub_struct.
Proof. apply: gm_inj_equiv; apply lm_mg; easy. Qed.
Lemma lm_bij :
incl (Ker f) zero_sub_struct → incl fullset (Rg f) → bijective f.
Proof. apply: gm_bij; apply lm_mg; easy. Qed.
Lemma lm_bij_rev : bijective f → Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof. apply: gm_bij_rev; apply lm_mg; easy. Qed.
Lemma lm_bij_equiv : bijective f ↔ Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof. apply: gm_bij_equiv; apply lm_mg; easy. Qed.
End Compatible_ModuleSpace_Lin_map_Facts2b.
Section Compatible_ModuleSpace_Lin_map_Facts3.
Context {K : Ring}.
Context {E1 E2 E3 : ModuleSpace K}.
Context {f : E1 → E2}.
Hypothesis Hf : lin_map f.
Context {g : E2 → E3}.
Hypothesis Hg : lin_map g.
Lemma Ker_comp_r : injective g → RgS (Ker (g \o f)) f = Ker g.
Proof. apply: Ker_g_comp_r; apply lm_mg; easy. Qed.
Lemma Ker_comp_r_alt :
∀ h x2, injective g → h = g \o f →
(∃ x1, h x1 = 0 ∧ f x1 = x2) ↔ g x2 = 0.
Proof. apply: Ker_g_comp_r_alt; apply lm_mg; easy. Qed.
End Compatible_ModuleSpace_Lin_map_Facts3.
Section Compatible_ModuleSpace_Lin_map_Facts4a.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Variable PE1 : E1 → Prop.
Lemma f_scal_compat_sub_id : f_scal_compat_sub PE1 ssrfun.id.
Proof. easy. Qed.
Lemma lm_sub_id : lm_sub PE1 ssrfun.id.
Proof. easy. Qed.
Context {f : E1 → E2}.
Lemma f_scal_compat_is_sub : f_scal_compat f → f_scal_compat_sub PE1 f.
Proof. easy. Qed.
Lemma lm_is_sub : lin_map f → lm_sub PE1 f.
Proof. intros [Hfa Hfb]; easy. Qed.
End Compatible_ModuleSpace_Lin_map_Facts4a.
Section Compatible_ModuleSpace_Lin_map_Facts4b.
Context {K : Ring}.
Context {E1 E2 E3 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Variable PE2 : E2 → Prop.
Context {f : E1 → E2}.
Hypothesis Hf : funS PE1 PE2 f.
Variable g : E2 → E3.
Lemma f_scal_compat_comp_sub :
f_scal_compat_sub PE1 f → f_scal_compat_sub PE2 g →
f_scal_compat_sub PE1 (g \o f).
Proof.
intros Hf1 Hg1 a x1 Hx1; rewrite comp_correct Hf1// Hg1//; apply Hf; easy.
Qed.
Lemma lm_comp_sub : lm_sub PE1 f → lm_sub PE2 g → lm_sub PE1 (g \o f).
Proof.
intros [Hfa Hfb] [Hga Hgb]; split;
[apply (f_plus_compat_comp_sub PE2) | apply f_scal_compat_comp_sub]; easy.
Qed.
End Compatible_ModuleSpace_Lin_map_Facts4b.
Section Sub_ModuleSpace_Def.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_g := sub_AbelianGroup (cms_cg HPE).
Definition sub_scal a (x : PE_g) : PE_g :=
mk_sub (cms_scal HPE a (val x) (in_sub x)).
Lemma sub_scal_assoc :
∀ a b x, sub_scal a (sub_scal b x) = sub_scal (a × b) x.
Proof. intros; apply val_inj, scal_assoc. Qed.
Lemma sub_scal_one_l : ∀ x, sub_scal 1 x = x.
Proof. intros; apply val_inj, scal_one. Qed.
Lemma sub_scal_distr_l :
∀ a x y, sub_scal a (x + y) = sub_scal a x + sub_scal a y.
Proof. intros; apply val_inj, scal_distr_l. Qed.
Lemma sub_scal_distr_r :
∀ a b x, sub_scal (a + b) x = sub_scal a x + sub_scal b x.
Proof. intros; apply val_inj, scal_distr_r. Qed.
Definition sub_ModuleSpace_mixin :=
ModuleSpace.Mixin _ _ _
sub_scal_assoc sub_scal_one_l sub_scal_distr_l sub_scal_distr_r.
Canonical Structure sub_ModuleSpace :=
ModuleSpace.Pack _ _
(ModuleSpace.Class _ _ _ sub_ModuleSpace_mixin) PE_g.
Lemma val_scal : f_scal_compat val.
Proof. easy. Qed.
Lemma val_lc : f_lc_compat val.
Proof.
intros n; induction n as [| n Hn].
intros; rewrite 2!lc_nil; easy.
intros; rewrite 2!lc_ind_l; simpl; f_equal; apply Hn.
Qed.
Lemma val_lm : lin_map val.
Proof. easy. Qed.
Lemma mk_sub_ms_zero : mk_sub (cms_zero HPE : PE 0) = 0 :> sub_ModuleSpace.
Proof. apply val_inj; easy. Qed.
Lemma mk_sub_ms_zero_equiv :
∀ {x} (Hx : PE x), mk_sub Hx = 0 :> sub_ModuleSpace ↔ x = 0.
Proof. apply mk_sub_zero_equiv. Qed.
Lemma mk_sub_scal :
∀ a (x : E) (Hx : PE x),
scal a (mk_sub Hx) = mk_sub (cms_scal HPE a _ Hx).
Proof. easy. Qed.
Lemma mk_sub_lc :
∀ {n} L (B : 'E^n) (HB : inclF B PE),
lin_comb L (fun i ⇒ mk_sub (HB i)) = mk_sub (cms_lc HPE _ L _ HB).
Proof. intros; apply val_inj, val_lc. Qed.
Lemma sub_scal_eq :
∀ a (x : sub_ModuleSpace),
scal a x = mk_sub (cms_scal HPE a _ (in_sub x)).
Proof. easy. Qed.
Lemma sub_lc_eq :
∀ {n} L (B : '(sub_ModuleSpace)^n),
lin_comb L B = mk_sub (cms_lc HPE _ L _ (fun i ⇒ in_sub (B i))).
Proof. intros; apply mk_sub_lc. Qed.
Lemma val_ms_inv_r :
∀ {x} (Hx : PE x), val (mk_sub Hx : sub_ModuleSpace) = x.
Proof. apply val_g_inv_r, cms_cg; easy. Qed.
Lemma mk_sub_ms_inv_r : ∀ {x}, mk_sub (in_sub x) = x :> sub_ModuleSpace.
Proof. intros; apply mk_sub_inv_r. Qed.
Lemma mk_sub_ms_inj :
∀ {x y} (Hx : PE x) (Hy : PE y),
mk_sub Hx = mk_sub Hy :> sub_ModuleSpace → x = y.
Proof. intros x y; apply mk_sub_inj. Qed.
End Sub_ModuleSpace_Def.
Section Sub_ModuleSpace_Facts1.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PEa PE : E → Prop}.
Hypothesis HPEa : incl PEa PE.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Let PEa' : PE_ms → Prop := preimage val PEa.
Lemma RgS_val_ms_eq : RgS PEa' val = PEa.
Proof. apply RgS_val_eq; easy. Qed.
Lemma preimage_val_cms : compatible_ms PEa → compatible_ms PEa'.
Proof. intros; apply cms_preimage; easy. Qed.
Lemma preimage_val_cms_rev : compatible_ms PEa' → compatible_ms PEa.
Proof. intros; rewrite -RgS_val_ms_eq; apply RgS_cms; easy. Qed.
Lemma preimage_val_cms_equiv : compatible_ms PEa' ↔ compatible_ms PEa.
Proof. split; [apply preimage_val_cms_rev | apply preimage_val_cms]. Qed.
End Sub_ModuleSpace_Facts1.
Section Sub_ModuleSpace_Facts2.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Variable PEa : PE_ms → Prop.
Let PEa' := RgS PEa val.
Lemma preimage_val_ms_eq : preimage val PEa' = PEa.
Proof. apply preimage_val_eq. Qed.
Lemma RgS_val_cms : compatible_ms PEa → compatible_ms PEa'.
Proof. intros; apply RgS_cms; easy. Qed.
Lemma RgS_val_cms_rev : compatible_ms PEa' → compatible_ms PEa.
Proof. intros; rewrite -preimage_val_ms_eq; apply cms_preimage; easy. Qed.
Lemma RgS_val_cms_equiv : compatible_ms PEa' ↔ compatible_ms PEa.
Proof. split; [apply RgS_val_cms_rev | apply RgS_val_cms]. Qed.
End Sub_ModuleSpace_Facts2.
Section Sub_ModuleSpace_Lin_map_Facts1.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Context {HPE1 : compatible_ms PE1}.
Context {HPE2 : compatible_ms PE2}.
Let PE1_ms := sub_ModuleSpace HPE1.
Let PE2_ms := sub_ModuleSpace HPE2.
Context {f : E1 → E2}.
Context {fS : PE1_ms → PE2_ms}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_ms_f_scal_compat : f_scal_compat f → f_scal_compat fS.
Proof. intros Hf a x1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
Lemma sub_ms_f_lc_compat : f_lc_compat f → f_lc_compat fS.
Proof.
intros Hf n L B; apply val_inj; rewrite HfS !val_lc Hf; f_equal.
apply extF; intros i; rewrite !mapF_correct; easy.
Qed.
Lemma sub_ms_lm : lin_map f → lin_map fS.
Proof.
intros [Hf1 Hf2]; split; [apply (sub_g_morphism HfS Hf1) |
move=>>; apply sub_ms_f_scal_compat; move=>>; easy].
Qed.
Lemma Ker_sub_ms_KerS_zero_equiv :
lin_map f →
Ker fS = zero_sub_struct ↔ KerS PE1 f = zero_sub_struct.
Proof. intros Hf; apply (Ker_sub_g_KerS_zero_equiv HfS), lm_mg, Hf. Qed.
Lemma KerS_ms_zero_equiv_alt :
lin_map f →
KerS PE1 f = zero_sub_struct ↔
∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. intros H; apply: KerS_g_zero_equiv_alt; apply lm_mg, H. Qed.
Lemma Ker_sub_ms_zero_equiv :
lin_map f →
Ker fS = zero_sub_struct ↔
∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. intros Hf; apply (Ker_sub_g_zero_equiv HfS), lm_mg, Hf. Qed.
Lemma lmS_injS_sub_equiv :
lin_map f → injS PE1 f ↔ Ker fS = zero_sub_struct.
Proof. intros Hf; apply (gmS_injS_sub_equiv HfS), lm_mg, Hf. Qed.
Lemma lmS_injS_val_equiv :
lin_map f →
injS PE1 f ↔ ∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. intros Hf; apply: (gmS_injS_val_equiv HfS); apply lm_mg, Hf. Qed.
Lemma lmS_bijS_sub_equiv :
lin_map f → bijS PE1 (RgS PE1 f) f ↔ Ker fS = zero_sub_struct.
Proof. intros Hf; apply (gmS_bijS_sub_equiv HfS), lm_mg, Hf. Qed.
Lemma lmS_bijS_val_equiv :
lin_map f →
bijS PE1 (RgS PE1 f) f ↔
∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. intros Hf; apply: (gmS_bijS_val_equiv HfS); apply lm_mg, Hf. Qed.
End Sub_ModuleSpace_Lin_map_Facts1.
Section Sub_ModuleSpace_Lin_map_Facts2.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Hypothesis HPE1 : compatible_ms PE1.
Hypothesis HPE2 : compatible_ms PE2.
Let PE1_ms := sub_ModuleSpace HPE1.
Let PE2_ms := sub_ModuleSpace HPE2.
Context {f : E1 → E2}.
Hypothesis Hf : funS PE1 PE2 f.
Definition fct_sub_ms : PE1_ms → PE2_ms := fct_sub Hf.
Lemma fct_sub_ms_inj : injS PE1 f → injective fct_sub_ms.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_ms_inj_rev : injective fct_sub_ms → injS PE1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_ms_inj_equiv : injective fct_sub_ms ↔ injS PE1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_ms_surj : surjS PE1 PE2 f → surjective fct_sub_ms.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_ms_surj_rev : surjective fct_sub_ms → surjS PE1 PE2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_ms_surj_equiv : surjective fct_sub_ms ↔ surjS PE1 PE2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_ms_bij : bijS PE1 PE2 f → bijective fct_sub_ms.
Proof. apply fct_sub_bij, inhabited_ms. Qed.
Lemma fct_sub_ms_bij_rev : bijective fct_sub_ms → bijS PE1 PE2 f.
Proof. apply fct_sub_bij_rev, inhabited_ms. Qed.
Lemma fct_sub_ms_bij_equiv : bijective fct_sub_ms ↔ bijS PE1 PE2 f.
Proof. apply fct_sub_bij_equiv, inhabited_ms. Qed.
Lemma fct_sub_ms_f_scal_compat : f_scal_compat f → f_scal_compat fct_sub_ms.
Proof. apply sub_ms_f_scal_compat, fct_sub_correct. Qed.
Lemma fct_sub_ms_f_lc_compat : f_lc_compat f → f_lc_compat fct_sub_ms.
Proof. apply sub_ms_f_lc_compat, fct_sub_correct. Qed.
Lemma fct_sub_ms_lm : lin_map f → lin_map fct_sub_ms.
Proof. apply sub_ms_lm, fct_sub_correct. Qed.
Lemma fct_sub_ms_f_inv_lm :
∀ (Hfb : bijS PE1 PE2 f),
lin_map f → lin_map (f_inv (fct_sub_ms_bij Hfb)).
Proof. intros; apply lm_bij_compat, fct_sub_ms_lm; easy. Qed.
Lemma Ker_fct_sub_ms_KerS_zero_equiv :
lin_map f →
Ker fct_sub_ms = zero_sub_struct ↔ KerS PE1 f = zero_sub_struct.
Proof. apply Ker_sub_ms_KerS_zero_equiv, fct_sub_correct. Qed.
Lemma Ker_fct_sub_ms_zero_equiv :
lin_map f →
Ker fct_sub_ms = zero_sub_struct ↔
∀ (x1 : sub_ModuleSpace HPE1), f (val x1) = 0 → x1 = 0.
Proof. apply Ker_sub_ms_zero_equiv, fct_sub_correct. Qed.
Lemma lmS_injS_fct_sub_equiv :
lin_map f → injS PE1 f ↔ Ker fct_sub_ms = zero_sub_struct.
Proof. apply lmS_injS_sub_equiv, fct_sub_correct. Qed.
Lemma lmS_bijS_fct_sub_equiv :
lin_map f →
bijS PE1 (RgS PE1 f) f ↔ Ker fct_sub_ms = zero_sub_struct.
Proof. apply lmS_bijS_sub_equiv, fct_sub_correct. Qed.
End Sub_ModuleSpace_Lin_map_Facts2.
Section Compose_n_ModuleSpace_Facts.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Context {n : nat}.
Variable f : '(E → E)^n.
Hypothesis Hf : ∀ i, funS PE PE (f i).
Lemma comp_n_f_scal_compat_sub :
(∀ i, f_scal_compat_sub PE (f i)) → f_scal_compat_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
[rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (f_scal_compat_comp_sub PE);
[apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.
Lemma comp_n_lm_sub :
(∀ i, lm_sub PE (f i)) →
lm_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
[rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (lm_comp_sub PE);
[apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.
End Compose_n_ModuleSpace_Facts.
Section Compose_n_part_ModuleSpace_Facts.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Context {n : nat}.
Variable f : '(E → E)^n.
Variable j : 'I_n.+1.
Hypothesis Hf : ∀ i, funS PE PE (widenF (leq_ord j) f i).
Lemma comp_n_part_f_scal_compat_sub :
(∀ i, f_scal_compat_sub PE (widenF (leq_ord j) f i)) →
f_scal_compat_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
[rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (f_scal_compat_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.
Lemma comp_n_part_lm_sub :
(∀ i, lm_sub PE (widenF (leq_ord j) f i)) →
lm_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
[rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (lm_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.
End Compose_n_part_ModuleSpace_Facts.