Library Algebra.Finite_dim.Finite_dim_MS_basis_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.

Brief description

Support for basis finite families in module spaces on the ring of real numbers.

Description

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_basis.

Bibliography

[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.

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 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_lin_indep.
From Algebra Require Import Finite_dim_MS_basis Finite_dim_MS_lin_indep_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 Basis_R_Facts1.

Properties of basis on R module spaces (from those of lin_gen and lin_indep).

Context {E : ModuleSpace R_Ring}.
Variable PE : E Prop.

Context {n1 n2 : nat}.
Variable B1 : 'E^n1.
Variable B2 : 'E^n2.

Lemma lin_indep_le_basis :
  inclF B1 PE lin_indep B1 basis PE B2 (n1 n2)%coq_nat.
Proof.
intros HB1a HB1b [HB2 _]; apply (lin_indep_le_lin_gen PE B1 B2); easy.
Qed.

Lemma lin_gen_ge_basis : basis PE B1 lin_gen PE B2 (n1 n2)%coq_nat.
Proof.
intros [HB1a HB1b] HB2.
apply (lin_indep_le_lin_gen PE B1 B2); try easy.
apply lin_gen_inclF; easy.
Qed.

End Basis_R_Facts1.

Section Basis_R_Facts2.

More properties of basis on R module spaces (from those of lin_gen and lin_indep).

Context {E : ModuleSpace R_Ring}.
Context {PE : E Prop}.

Lemma basis_monot :
   {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
    n1 = n2 invalF B1 B2 basis PE B1 basis PE B2.
Proof.
intros n1 n2 B1 B2 Hn HB [HB1a HB1b].
move: (lin_indep_injF nonzero_struct_R HB1b) ⇒ HB1c.
move: (injF_monot _ _ Hn HB HB1c) ⇒ HB2.
move: (invalF_sym _ _ Hn HB1c HB) ⇒ HBa.
subst n2; split.
apply (lin_gen_monot B1); try easy.
apply (inclF_monot_l _ B1); try easy.
apply lin_gen_inclF; easy.
apply (lin_indep_monot B1); easy.
Qed.

Lemma basis_1_equiv : {B : 'E^1}, basis (lin_span B) B B ord0 0.
Proof. intros; rewrite basis_lin_span_equiv; apply lin_indep_1_equiv. Qed.

Lemma basis_singleF_equiv :
   {x0 : E}, basis (line x0) (singleF x0) x0 0.
Proof. intros; apply: basis_1_equiv. Qed.

Lemma basis_2_equiv :
   {B : 'E^2},
    basis (lin_span B) B B ord0 0 ¬ line (B ord0) (B ord_max).
Proof. intros; rewrite basis_lin_span_equiv; apply lin_indep_2_equiv. Qed.

Lemma basis_coupleF_equiv :
   {x0 x1 : E},
    basis (plane x0 x1) (coupleF x0 x1) x0 0 ¬ line x0 x1.
Proof. intros; rewrite basis_lin_span_equiv; apply lin_indep_coupleF_equiv. Qed.

Lemma basis_3_equiv :
   {B : 'E^3}, basis (lin_span B) B
    B ord0 0 ¬ line (B ord0) (B ord1)
    ¬ plane (B ord0) (B ord1) (B ord_max).
Proof. intros; rewrite basis_lin_span_equiv; apply lin_indep_3_equiv. Qed.

Lemma basis_tripleF_equiv :
   {x0 x1 x2 : E},
    basis (space_3 x0 x1 x2) (tripleF x0 x1 x2)
    x0 0 ¬ line x0 x1 ¬ plane x0 x1 x2.
Proof. intros; rewrite basis_lin_span_equiv; apply lin_indep_tripleF_equiv. Qed.

End Basis_R_Facts2.


Section Has_dimension_R_Facts0.

Properties of has_dim on R module spaces (from those of basis).

Context {E : ModuleSpace R_Ring}.
Context {PE : E Prop}.

Lemma has_dim_1 : {x0 : E}, x0 0 has_dim (line x0) 1.
Proof. intros x0 H0; apply (Dim _ _ (singleF x0)), basis_1_equiv; easy. Qed.

Lemma has_dim_1_rev : has_dim PE 1 x0, x0 0 PE = line x0.
Proof.
intros [B [HB1 HB2]]; rewrite HB1; (B ord0); split;
    [apply lin_indep_1_equiv; easy | apply lin_span_singleF].
Qed.

Lemma has_dim_1_equiv : has_dim PE 1 x0, x0 0 PE = line x0.
Proof.
split; [apply has_dim_1_rev |]. intros [x0 [H0 H]]; rewrite H; apply has_dim_1; easy.
Qed.

Lemma has_dim_2 :
   {x0 x1 : E}, x0 0 ¬ line x0 x1 has_dim (plane x0 x1) 2.
Proof.
intros x0 x1 H0 H1; apply (Dim _ _ (coupleF x0 x1)), basis_2_equiv;
    rewrite coupleF_0 coupleF_1; easy.
Qed.

Lemma has_dim_2_rev :
  has_dim PE 2 x0 x1, (x0 0 ¬ line x0 x1) PE = plane x0 x1.
Proof.
intros [B [HB1 HB2]]; rewrite HB1; (B ord0), (B ord_max); split;
    [apply lin_indep_2_equiv; easy | apply lin_span_coupleF].
Qed.

Lemma has_dim_2_equiv :
  has_dim PE 2 x0 x1, (x0 0 ¬ line x0 x1) PE = plane x0 x1.
Proof.
split; [apply has_dim_2_rev |].
intros [x0 [x1 [H01 H]]]; rewrite H; apply has_dim_2; easy.
Qed.

Lemma has_dim_3 :
   {x0 x1 x2 : E},
    x0 0 ¬ line x0 x1 ¬ plane x0 x1 x2
    has_dim (space_3 x0 x1 x2) 3.
Proof.
intros x0 x1 x2 H0 H1 H2;
    apply (Dim _ _ (tripleF x0 x1 x2)), basis_3_equiv;
    rewrite tripleF_0 tripleF_1 tripleF_2; easy.
Qed.

Lemma has_dim_3_rev :
  has_dim PE 3 x0 x1 x2,
    (x0 0 ¬ line x0 x1 ¬ plane x0 x1 x2)
    PE = space_3 x0 x1 x2.
Proof.
intros [B [HB1 HB2]]; rewrite HB1;
     (B ord0), (B ord1), (B ord_max); split;
    [apply lin_indep_3_equiv; easy | apply lin_span_tripleF].
Qed.

Lemma has_dim_3_equiv :
  has_dim PE 3 x0 x1 x2,
    (x0 0 ¬ line x0 x1 ¬ plane x0 x1 x2)
    PE = space_3 x0 x1 x2.
Proof.
split; [apply has_dim_3_rev |].
intros [x0 [x1 [x2 [H012 H]]]]; rewrite H; apply has_dim_3; easy.
Qed.

Lemma has_dim_Rn : {n}, has_dim (@fullset 'R^n) n.
Proof.
intros; apply (Dim _ _ (fun i j : 'I_nkronR i j)); split.
apply subset_ext_equiv; split; try easy; intros x _.
rewrite -(lc_kron_r x); easy.
intros L HL; rewrite lc_kron_r in HL; easy.
Qed.

End Has_dimension_R_Facts0.

Section Has_dimension_R_Facts1.

More properties of has_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.

[GostiauxT1] Th 6.64, pp. 192-193.
Lemma lin_gen_has_dim :
   {PE : E Prop} {n} {B : 'E^n},
    lin_gen PE B m, has_dim PE m.
Proof.
intros PE n B HB.
destruct (nat_has_greatest_element
    (fun m (C : 'E^m), invalF C B lin_indep C) 0 n)
    as [m [Hm1 [[C [HC1 HC2]] Hm2]]].
(fun 0); split. intros [i Hi]; easy. apply lin_indep_nil.
intros m Hm [C [HC1 HC2]].
assert (Hm' : ¬ (m n)%coq_nat) by now apply Nat.lt_nge.
contradict Hm'.
apply (lin_indep_le_lin_gen PE C B); try easy.
apply (inclF_monot_l _ B), lin_gen_inclF; easy.
m; apply (Dim _ _ C); split; try easy.
rewrite HB (lin_gen_equiv _ B).
apply lin_gen_lin_span.
apply lin_span_inclF; easy.
intros i; destruct (classic ( j, B i = C j)) as [[j Hj] | Hi'].
rewrite Hj; apply lin_span_inclF_diag.
specialize (not_ex_all_not _ _ Hi'); simpl; intros Hi; clear Hi'.
assert (H : lin_dep (insertF C (B i) ord_max)).
  move: (Nat.lt_irrefl m) ⇒ H Hi'; contradict H.
  apply Hm2; (insertF C (B i) ord_max); split; try easy.
  apply insertF_monot_invalF_l; try easy; i; easy.
destruct (lin_dep_insertF_rev _ HC2 H) as [L]; easy.
Qed.

Lemma fin_dim_has_dim : {PE : E Prop}, fin_dim PE n, has_dim PE n.
Proof. intros PE [n [B HB]]; apply (lin_gen_has_dim HB). Qed.

Lemma lin_span_has_dim :
   {n} (B : 'E^n), m, has_dim (lin_span B) m.
Proof. intros n B; apply (lin_gen_has_dim (lin_gen_lin_span B)). Qed.

Context {PE : E Prop}.

[GostiauxT1] Th 6.65, p. 193.
Also known as the dimension theorem.
Lemma dim_is_unique :
   {n1 n2}, has_dim PE n1 has_dim PE n2 n1 = n2.
Proof.
intros n1 n2 [B1 H1] [B2 H2]; apply Nat.le_antisymm.
destruct H1; apply (lin_indep_le_basis PE B1 B2); try easy.
apply lin_gen_inclF; easy.
destruct H2; apply (lin_indep_le_basis PE B2 B1); try easy.
apply lin_gen_inclF; easy.
Qed.

[GostiauxT1] Th 6.66, pp. 193-194.
Close to Steinitz exchange lemma.
Lemma incomplete_basis_theorem :
   {n nf ng} {Bf : 'E^nf} {Bg : 'E^ng},
    has_dim PE n inclF Bf PE lin_indep Bf lin_gen PE Bg
     m (C : 'E^m), n = (nf + m)%coq_nat
      ( j, ¬ lin_span Bf (C j)) invalF C Bg
      basis PE (concatF Bf C).
Proof.
intros n nf ng Bf Bg [B HB] Hf1 Hf2 Hg.
destruct (nat_has_greatest_element
    (fun m (C : 'E^m), ( j, ¬ lin_span Bf (C j))
      invalF C Bg lin_indep (concatF Bf C)) 0 (n - nf)%coq_nat)
      as [m [Hm1 [[C [HC1 [HC2 HC3]]] Hm2]]].
0; repeat split; [intros [j Hj]; easy.. |].
rewrite concatF_nil_r lin_indep_castF_equiv; easy.
intros m Hm; apply all_not_not_ex; intros C [HC1 [HC2 HC3]].
contradict HC3; apply (lin_dep_gt_lin_span B).
apply Nat.lt_sub_lt_add_l; easy.
destruct HB as [HB _]; rewrite -HB; apply concatF_lub_inclF; try easy.
rewrite Hg; apply lin_span_inclF; easy.
m, C.
specialize (Hm2 m.+1); apply (proj1 contra_equiv) in Hm2; auto with arith.
rewrite not_ex_all_not_equiv in Hm2.
assert (H0 : ¬ (@ord_max (nf + m) < nf)%coq_nat).
  rewrite ord_max_correct; auto with arith.
assert (H1 : basis PE (concatF Bf C)).
  split; [rewrite (lin_gen_equiv _ Bg)// | easy].
  apply concatF_lub_inclF, lin_span_inclF; try rewrite -Hg; easy.
  intros ig; apply lin_dep_insertF_rev with ord_max; try easy.
  specialize (Hm2 (insertF C (Bg ig) ord_max)).
  unfold lin_dep; contradict Hm2; repeat split.
  1,2: intros j; destruct (ord_eq_dec j ord_max) as [Hj | Hj];
    [rewrite insertF_correct_l// | rewrite insertF_correct_r//].
  contradict Hm2; apply (lin_dep_insertF nonzero_struct_R),
      (lin_span_monot _ _ (concatF_ub_l _ _) _ Hm2).
   ig; easy.
  rewrite insertF_concatF_r lin_indep_castF_equiv in Hm2.
  replace (concat_r_ord _) with (@ord_max m) in Hm2;
      try apply ord_inj; simpl; auto with arith.
split; try easy.
apply dim_is_unique; [apply (Dim _ _ _ HB) | apply (Dim _ _ _ H1)].
Qed.

[GostiauxT1] Cor. 6.67, p. 194.
Lemma lin_indep_le_dim :
   PE {n nf} (Bf : 'E^nf),
    has_dim PE n inclF Bf PE lin_indep Bf (nf n)%coq_nat.
Proof.
move=>> [B HB] Hf1 Hf2; apply (lin_indep_le_basis _ _ _ Hf1 Hf2 HB).
Qed.

Lemma lin_dep_dim_gt :
   PE {n nf} {Bf : 'E^nf},
    has_dim PE n inclF Bf PE (n < nf)%coq_nat lin_dep Bf.
Proof.
move=>> HPE HBf; rewrite contra_not_r_equiv Nat.nlt_ge.
apply (lin_indep_le_dim _ _ HPE); easy.
Qed.

[GostiauxT1] Cor. 6.67, p. 194.
Lemma lin_indep_basis :
   {n} {Bf : 'E^n},
    has_dim PE n inclF Bf PE lin_indep Bf basis PE Bf.
Proof.
move=>> HPE Hf1 Hf2; generalize HPE; intros [B [HB _]].
destruct (incomplete_basis_theorem HPE Hf1 Hf2 HB) as [m [C [Hm [_ [_ HC]]]]].
apply eq_sym, nat_plus_zero_reg_l in Hm; subst m.
rewrite concatF_nil_r basis_castF_equiv in HC; easy.
Qed.

[GostiauxT1] Cor. 6.67, p. 194.
Lemma lin_indep_overbasis_ex :
   {n nf} {Bf : 'E^nf},
    has_dim PE n inclF Bf PE lin_indep Bf
     m (C : 'E^m), n = (nf + m)%coq_nat
      ( j, ¬ lin_span Bf (C j)) basis PE (concatF Bf C).
Proof.
move=>> HPE Hf1 Hf2; generalize HPE; intros [B [HB _]].
destruct (incomplete_basis_theorem HPE Hf1 Hf2 HB)
    as [m [C [Hm [HC1 [_ HC2]]]]].
subst; m, C; easy.
Qed.

Lemma lin_indep_overbasis_ex_alt :
   {n nf} {Bf : 'E^nf},
    has_dim PE n inclF Bf PE lin_indep Bf
     (B : 'E^n), invalF Bf B basis PE B.
Proof.
intros n nf Bf HPE Hf1 Hf2.
destruct (lin_indep_overbasis_ex HPE Hf1 Hf2) as [m [C [Hm [_ HC]]]].
(castF (eq_sym Hm) (concatF Bf C)); split.
apply invalF_castF_r_equiv, concatF_ub_l.
apply basis_castF_compat; easy.
Qed.

Lemma lin_indep_fin_dim_overbasis_ex :
   {nf} {Bf : 'E^nf},
    fin_dim PE inclF Bf PE lin_indep Bf
     n (B : 'E^n), invalF Bf B basis PE B.
Proof.
move=>> /fin_dim_has_dim [n HPE] HBf1 HBf2.
n; apply (lin_indep_overbasis_ex_alt HPE HBf1 HBf2).
Qed.

Lemma lin_indep_lin_gen :
   {n} {Bf : 'E^n},
    has_dim PE n inclF Bf PE lin_indep Bf lin_gen PE Bf.
Proof. intros; apply basis_lin_gen, lin_indep_basis; easy. Qed.

[GostiauxT1] Cor. 6.68, p. 194.
Lemma lin_gen_ge_dim :
   {n ng} (Bg : 'E^ng),
    has_dim PE n lin_gen PE Bg (n ng)%coq_nat.
Proof. move=>> [B HB] Hg; apply (lin_gen_ge_basis _ _ _ HB Hg). Qed.

Lemma not_lin_gen_dim_lt :
   {n ng} (Bg : 'E^ng),
    has_dim PE n (ng < n)%coq_nat ¬ lin_gen PE Bg.
Proof.
move=>> HPE; rewrite contra_not_r_equiv Nat.nlt_ge.
apply lin_gen_ge_dim; easy.
Qed.

[GostiauxT1] Cor. 6.68, p. 194.
Lemma lin_gen_basis :
   {n} {Bg : 'E^n}, has_dim PE n lin_gen PE Bg basis PE Bg.
Proof.
intros n Bg HPE Hg; generalize HPE; intros [B HB]; destruct n.
rewrite (hat0F_unit B Bg); easy.
move: (lin_gen_nonzero _ Hg
    (has_dim_nonzero_sub_struct nonzero_struct_R _ HPE)).
move⇒ /nextF_rev [i Hi].
assert (Hf1 : inclF (singleF (Bg i)) PE).
  apply lin_gen_inclF in Hg; intro; apply Hg.
assert (Hf2 : lin_indep (singleF (Bg i))) by now apply lin_indep_singleF_equiv.
destruct (incomplete_basis_theorem HPE Hf1 Hf2 Hg)
    as [m [C [Hm [HC1 HC2]]]].
apply (basis_monot (concatF (singleF (Bg i)) C)); try easy.
apply concatF_lub_invalF; try easy.
apply invalF_singleF_refl.
Qed.

[GostiauxT1] Cor. 6.68, p. 194.
Lemma lin_gen_subbasis_ex :
   {n ng} {Bg : 'E^ng},
    has_dim PE n lin_gen PE Bg (B : 'E^n), invalF B Bg basis PE B.
Proof.
intros n ng Bg HPE Hg; generalize HPE; intros [B HB]; destruct n.
B; split; try easy; intros [i Hi]; easy.
move: (lin_gen_nonzero _ Hg
    (has_dim_nonzero_sub_struct nonzero_struct_R _ HPE)).
move⇒ /nextF_rev [i Hi].
assert (Hf1 : inclF (singleF (Bg i)) PE).
  apply lin_gen_inclF in Hg; intro; apply Hg.
assert (Hf2 : lin_indep (singleF (Bg i))) by now apply lin_indep_singleF_equiv.
destruct (incomplete_basis_theorem HPE Hf1 Hf2 Hg)
    as [m [C [Hm [_ [HC1 HC2]]]]].
(castF (eq_sym Hm) (concatF (singleF (Bg i)) C)); split.
apply invalF_castF_l_equiv, concatF_lub_invalF; try easy.
apply invalF_singleF_refl.
apply basis_castF_equiv; easy.
Qed.

Lemma lin_gen_fin_dim_subbasis_ex :
   {ng} {Bg : 'E^ng}, fin_dim PE lin_gen PE Bg
     n (B : 'E^n), invalF B Bg basis PE B.
Proof.
move=>> /fin_dim_has_dim [n HPE] HBg.
n; apply (lin_gen_subbasis_ex HPE HBg).
Qed.

Lemma lin_gen_lin_indep :
   {n} {Bg : 'E^n}, has_dim PE n lin_gen PE Bg lin_indep Bg.
Proof.
intros; apply (basis_lin_indep PE), lin_gen_basis; easy.
Qed.

Lemma lin_indep_lin_gen_equiv :
   {n} {B : 'E^n},
    has_dim PE n inclF B PE lin_indep B lin_gen PE B.
Proof.
intros; split; [apply lin_indep_lin_gen | apply lin_gen_lin_indep]; easy.
Qed.

End Has_dimension_R_Facts1.

Section Has_dimension_R_Facts2.

More properties of has_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.
Context {PE : E Prop}.

Context {n : nat}.
Hypothesis HPE : has_dim PE n.
Let PE_ms := sub_ModuleSpace (has_dim_cms _ HPE).
Context {PE1 : PE_ms Prop}.
Hypothesis HPE1 : compatible_ms PE1.

[GostiauxT1] Th. 6.69, pp. 194-195.
Lemma dim_le_eq_alt :
   n1, has_dim PE1 n1 (n1 n)%coq_nat (n1 = n PE1 = fullset).
Proof.
destruct (nat_has_greatest_element
    (fun m (C : 'PE_ms^m), inclF C PE1 lin_indep C)
      0 n) as [n1 [Hn1a [[C [HC1 HC2]] Hn1b]]].
   0; split. intros [i Hi]; easy. apply lin_indep_nil.
  intros p Hp; apply not_ex_all_not_equiv; intros C.
  rewrite -(NNPP_equiv (lin_indep _)) -imp_and_equiv; intros _.
  apply (lin_dep_dim_gt _ (has_dim_sub_alt HPE) (inclF_fullset _) Hp).
assert (HC3 : basis PE1 C).
  split; try easy; apply subset_ext_equiv; split.
  intros x Hx.
  apply (lin_dep_insertF_rev ord0); try easy.
  specialize (Hn1b n1.+1); apply (proj1 contra_equiv) in Hn1b; auto with arith.
  rewrite not_ex_all_not_equiv in Hn1b; specialize (Hn1b (insertF C x ord0)).
  rewrite not_and_equiv -imp_or_equiv in Hn1b; apply Hn1b.
  apply insertF_monot_inclF; easy.
  apply lin_span_lb; easy.
n1; repeat split; [apply (Dim _ _ C HC3) | easy |].
intros; subst; clear Hn1a.
assert (HC3' : basis PE (mapF val C)).
  apply lin_indep_basis; try easy.
  apply in_subF.
  apply lin_indep_val_equiv; easy.
apply subset_ext_equiv; split; try easy.
intros x _; destruct (basis_ex_decomp HC3' (val x) (in_sub x)) as [L HL].
rewrite -val_lc in HL; apply val_inj in HL; rewrite HL.
apply cms_lc; easy.
Qed.

[GostiauxT1] Th. 6.69, pp. 194-195.
Lemma dim_le_alt : n1, has_dim PE1 n1 (n1 n)%coq_nat.
Proof. destruct dim_le_eq_alt as [n1 Hn1]; n1; easy. Qed.

[GostiauxT1] Th. 6.69, pp. 194-195.
Lemma dim_eq_alt : {n1}, has_dim PE1 n1 n1 = n PE1 = fullset.
Proof.
destruct dim_le_eq_alt as [n1 [Hn1a [_ Hn1b]]].
intros p Hp; rewrite -(dim_is_unique Hn1a Hp); easy.
Qed.

[GostiauxT1] Th. 6.69, pp. 194-195. Supplementary...
More properties of has_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.
Context {PE1 PE : E Prop}.
Hypothesis HPE1 : incl PE1 PE.
Hypothesis HPE1' : compatible_ms PE1.

Context {n : nat}.
Hypothesis HPE : has_dim PE n.

[GostiauxT1] Th. 6.69, pp. 194-195.
Lemma dim_le_eq :
   n1, has_dim PE1 n1 (n1 n)%coq_nat (n1 = n PE1 = PE).
Proof.
pose (HPE' := has_dim_cms _ HPE).
pose (PE_ms := sub_ModuleSpace HPE').
pose (PE1' := preimage val PE1 : PE_ms Prop).
destruct (dim_le_eq_alt HPE (preimage_val_cms _ HPE1'))
    as [n1 [H1 [H2 H3]]]; n1; repeat split; [| easy |].
apply (has_dim_preimage_val_rev HPE1 HPE' H1).
intros Hn1; specialize (H3 Hn1); apply incl_antisym; [easy |].
rewrite -(proj1 (inter_left _ _) HPE1) -image_preimage_val H3.
intros x Hx; rewrite -(val_ms_inv_r _ Hx); easy.
Qed.

End Has_dimension_R_Facts3a.

Section Has_dimension_R_Facts3b.

More properties of has_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.
Context {PE1 : E Prop}.
Variable PE : E Prop.
Hypothesis HPE1 : incl PE1 PE.

[GostiauxT1] Th. 6.69, pp. 194-195.
Lemma dim_le :
   {n}, compatible_ms PE1 has_dim PE n
     n1, has_dim PE1 n1 (n1 n)%coq_nat.
Proof.
move=>> HPE1' HPE;
    destruct (dim_le_eq HPE1 HPE1' HPE) as [n1 Hn1]; n1; easy.
Qed.

Lemma fin_dim_monot : compatible_ms PE1 fin_dim PE fin_dim PE1.
Proof.
moveHPE1' /fin_dim_has_dim [n HPE].
destruct (dim_le HPE1' HPE) as [n1 [Hn1 _]]; apply (has_dim_fin_dim _ Hn1).
Qed.

Lemma dim_monot : {n1 n}, has_dim PE1 n1 has_dim PE n (n1 n)%coq_nat.
Proof.
move=>> HPE1a HPE; move: (has_dim_cms _ HPE1a) ⇒ HPE1'.
destruct (dim_le HPE1' HPE) as [p [Hp1 Hp2]].
rewrite -(dim_is_unique Hp1 HPE1a); easy.
Qed.

End Has_dimension_R_Facts3b.

Section Has_dimension_R_Facts3c.

More properties of has_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.
Context {PE1 PE : E Prop}.
Hypothesis HPE1 : incl PE1 PE.

Context {n1 n : nat}.
Hypothesis HPE1a : has_dim PE1 n1.
Hypothesis HPE : has_dim PE n.

[GostiauxT1] Th. 6.69, pp. 194-195.
Lemma dim_eq : n1 = n PE1 = PE.
Proof.
move: (has_dim_cms _ HPE1a) ⇒ HPE1'.
destruct (dim_le_eq HPE1 HPE1' HPE) as [p [Hp1 [_ Hp2]]].
rewrite -(dim_is_unique Hp1 HPE1a); easy.
Qed.

End Has_dimension_R_Facts3c.

Section Has_dimension_R_Facts4.

More properties of has_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.

Lemma has_dim_lin_span_rev :
   {n} {B : 'E^n}, has_dim (lin_span B) n lin_indep B.
Proof.
intros n B HB; apply (basis_lin_indep (lin_span B)),
    (lin_gen_basis HB), lin_gen_lin_span.
Qed.

Lemma has_dim_lin_span_equiv :
   {n} {B : 'E^n}, has_dim (lin_span B) n lin_indep B.
Proof. intros; split; [apply has_dim_lin_span_rev | apply has_dim_lin_span]. Qed.

End Has_dimension_R_Facts4.

Section Has_dimension_R_Facts5.

More properties of has_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.
Context {PE1 PE2 : E Prop}.

Context {n1 n2 : nat}.
Hypothesis HPE1 : has_dim PE1 n1.
Hypothesis HPE2 : has_dim PE2 n2.

Lemma has_dim_inter : n, has_dim (inter PE1 PE2) n.
Proof.
move: (inter_lb_l PE1 PE2) ⇒ HPE.
move: (has_dim_cms _ HPE1) ⇒ HPE1'.
move: (has_dim_cms _ HPE2) ⇒ HPE2'.
move: (cms_inter HPE1' HPE2') ⇒ HPE'.
destruct (dim_le _ HPE HPE' HPE1) as [n [Hn _]]; n; easy.
Qed.

Lemma dim_inter_lb_l :
   {n}, has_dim (inter PE1 PE2) n (n n1)%coq_nat.
Proof. move=>> HPE; apply (dim_monot _ (inter_lb_l _ _) HPE HPE1). Qed.

Lemma has_dim_inter_l : has_dim (inter PE1 PE2) n1 incl PE1 PE2.
Proof.
split; [intros HPE | move⇒ /inter_left ->; easy].
assert (HPEa : compatible_ms (inter PE1 PE2)).
  apply cms_inter; [apply (has_dim_cms _ HPE1) | apply (has_dim_cms _ HPE2)].
assert (HPEb : incl (inter PE1 PE2) PE1) by apply inter_lb_l.
apply inter_left, (dim_eq HPEb HPE HPE1); easy.
Qed.

End Has_dimension_R_Facts5.

Section Has_dimension_R_Facts6.

More properties of fin_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.
Context {PE1 PE2 : E Prop}.

Lemma fin_dim_inter : fin_dim PE1 fin_dim PE2 fin_dim (inter PE1 PE2).
Proof.
move⇒ /fin_dim_has_dim [n1 Hn1] /fin_dim_has_dim [n2 Hn2].
destruct (has_dim_inter Hn1 Hn2) as [n Hn]; apply (has_dim_fin_dim _ Hn).
Qed.

End Has_dimension_R_Facts6.

Section Has_dimension_R_Facts7.

Properties of has_dim on R module spaces.

Context {E : ModuleSpace R_Ring}.
Variable PE1 PE2 : E Prop.

Context {n1 n2 : nat}.
Hypothesis HPE1 : has_dim PE1 n1.
Hypothesis HPE2 : has_dim PE2 n2.

Lemma dim_inter_lb_r :
   {n}, has_dim (inter PE1 PE2) n (n n2)%coq_nat.
Proof. intro; rewrite inter_comm; apply (dim_inter_lb_l HPE2). Qed.

Lemma has_dim_inter_r : has_dim (inter PE1 PE2) n2 incl PE2 PE1.
Proof. rewrite inter_comm; apply (has_dim_inter_l HPE2 HPE1). Qed.

End Has_dimension_R_Facts7.