Library Algebra.Finite_dim.Finite_dim_AS_basis

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 affine basis finite families in affine spaces.

Description

Some results are only valid when the ring of scalars is commutative, or being ordered, 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_AS, 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.
From Algebra Require Import Monoid Group Ring ModuleSpace AffineSpace.
From Algebra Require Import Finite_dim_MS.
From Algebra Require Import Finite_dim_AS_def Finite_dim_AS_aff_span.
From Algebra Require Import Finite_dim_AS_aff_gen Finite_dim_AS_aff_indep.

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

Section Affine_span_Subset_Facts.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Lemma aff_basis_aff_gen :
   (PE : E Prop) {n} (A : 'E^n.+1), aff_basis PE A aff_gen PE A.
Proof. move=>> [HA _]; easy. Qed.

Lemma aff_basis_aff_indep :
   (PE : E Prop) {n} (A : 'E^n.+1), aff_basis PE A aff_indep A.
Proof. move=>> [_ HA]; easy. Qed.

Lemma aff_basis_nonempty :
   {PE : E Prop} {n} {A : 'E^n.+1}, aff_basis PE A O, PE O.
Proof. move=>> [HA _]; apply (aff_gen_nonempty HA). Qed.

Lemma has_aff_dim_is_nonempty :
   {PE : E Prop} {n}, has_aff_dim PE n O, PE O.
Proof. move=>> [A HA]; apply (aff_basis_nonempty HA). Qed.

End Affine_span_Subset_Facts.

Section AffineSpace_FD_R_Facts.

Context {V : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.

Lemma aff_basis_lin_basis :
   {PE : E Prop} {n} {A : 'E^n.+1} O i0,
    aff_span A O basis (vectP PE O) (frameF A i0) aff_basis PE A.
Proof.
intros PE n A O i0 HO [HA1 HA2]; split.
apply (aff_gen_lin_gen _ _ HO HA1).
apply (aff_indep_alt i0); easy.
Qed.

Lemma aff_basis_lin_basis_rev :
   {PE : E Prop} {n} {A : 'E^n.+1} {O} i0,
    PE O aff_basis PE A basis (vectP PE O) (frameF A i0).
Proof.
move=>> HO [HA1 HA2]; split; try easy; apply aff_gen_lin_gen_rev; easy.
Qed.

Lemma aff_basis_lin_basis_equiv :
   {PE : E Prop} {n} {A : 'E^n.+1} {O} i0,
    PE O aff_basis PE A
    aff_span A O basis (vectP PE O) (frameF A i0).
Proof.
intros PE n A O i0; unfold aff_basis, basis.
rewrite -and_assoc (aff_gen_lin_gen_equiv _ i0) and_assoc.
split; intros [HA1 [HA2 HA3]]; repeat split; try easy.
apply (aff_indep_alt i0); easy.
Qed.

Lemma lin_basis_aff_basis :
   {PV : V Prop} {n} {B : 'V^n} (O : E) i0,
    zero_closed PV
    aff_basis (translP PV O) (inv_frameF O B i0) basis PV B.
Proof.
movePV n B O i0
    /(translP_zero_closed_equiv O) HO /(aff_basis_lin_basis_rev i0 HO).
rewrite vectP_translP frameF_inv_frameF; easy.
Qed.

Lemma lin_basis_aff_basis_rev :
   {PV : V Prop} {n} {B : 'V^n} (O : E) i0,
    basis PV B aff_basis (translP PV O) (inv_frameF O B i0).
Proof.
intros PV n B O i0 HB.
apply (aff_basis_lin_basis _ i0 (aff_span_inv_frameF_orig _ _ _)).
rewrite vectP_translP frameF_inv_frameF; easy.
Qed.

Lemma lin_basis_aff_basis_equiv :
   {PV : V Prop} {n} {B : 'V^n} (O : E) i0,
    basis PV B
    zero_closed PV aff_basis (translP PV O) (inv_frameF O B i0).
Proof.
intros; split.
intros HB; split.
apply cms_zero, (basis_cms _ HB).
apply (lin_basis_aff_basis_rev _ _ HB).
intros [HPV HB]; apply (lin_basis_aff_basis _ _ HPV HB).
Qed.

Lemma has_aff_dim_has_dim :
   {PE : E Prop} {n} O, has_dim (vectP PE O) n has_aff_dim PE n.
Proof.
movePE n O [B /(lin_basis_aff_basis_rev O ord0) HB];
    rewrite translP_vectP in HB; apply (Aff_dim _ _ _ HB).
Qed.

Lemma has_aff_dim_has_dim_rev :
   {PE : E Prop} {n} {O},
    PE O has_aff_dim PE n has_dim (vectP PE O) n.
Proof.
move=>> HO [A /(aff_basis_lin_basis_rev ord0 HO) HA]; apply (Dim _ _ _ HA).
Qed.

Lemma has_aff_dim_has_dim_equiv :
   {PE : E Prop} {n} {O},
    PE O has_aff_dim PE n has_dim (vectP PE O) n.
Proof.
intros; split; [intros [HO HPE] | intros HPE; split].
apply (has_aff_dim_has_dim_rev HO HPE).
apply vectP_zero_closed_equiv, (has_dim_zero_closed _ HPE).
apply (has_aff_dim_has_dim _ HPE).
Qed.

Lemma has_dim_has_aff_dim :
   {PV : V Prop} {n} (O : E),
    zero_closed PV has_aff_dim (translP PV O) n has_dim PV n.
Proof.
movePV n O /(translP_zero_closed_equiv O) HO
    [A /(aff_basis_lin_basis_rev ord0 HO) HA];
    rewrite vectP_translP in HA; apply (Dim _ _ _ HA).
Qed.

Lemma has_dim_has_aff_dim_rev :
   {PV : V Prop} {n} (O : E),
    has_dim PV n has_aff_dim (translP PV O) n.
Proof.
movePV n O [B /(lin_basis_aff_basis_rev O ord0) HB];
    apply (Aff_dim _ _ _ HB).
Qed.

Lemma has_dim_has_aff_dim_equiv :
   {PV : V Prop} {n} (O : E),
    has_dim PV n zero_closed PV has_aff_dim (translP PV O) n.
Proof.
intros; split; [intros HPV; split | intros [HO HPV]].
apply (has_dim_zero_closed _ HPV).
apply (has_dim_has_aff_dim_rev _ HPV).
apply (has_dim_has_aff_dim _ HO HPV).
Qed.

Lemma has_aff_dim_has_dim_eq :
   {PE : E Prop} na nms {O},
    PE O has_aff_dim PE na has_dim (vectP PE O) nms na = nms.
Proof.
move=>> HO Ha Hms; apply: (dim_is_unique _ Hms); apply has_aff_dim_has_dim_rev; easy.
Qed.

Lemma aff_gen_aff_basis :
   {PE : E Prop} {n} {A : 'E^n.+1},
    has_aff_dim PE n aff_gen PE A aff_basis PE A.
Proof.
intros PE n A HPE HA; destruct (has_aff_dim_is_nonempty HPE) as [O HO].
assert (HO' : aff_span A O) by now rewrite -HA.
move: (has_aff_dim_has_dim_rev HO HPE) ⇒ HPE'.
move: (aff_gen_lin_gen_rev ord0 HO HA) ⇒ HA'.
apply (aff_basis_lin_basis _ ord0 HO').
apply (lin_gen_basis HPE' HA').
Qed.

Lemma aff_gen_aff_indep :
   {PE : E Prop} {n} {A : 'E^n.+1},
    has_aff_dim PE n aff_gen PE A aff_indep A.
Proof.
intros PE n A HPE HA; apply (aff_basis_aff_indep PE).
apply aff_gen_aff_basis; easy.
Qed.

Lemma aff_indep_aff_gen :
   {PE : E Prop} {n} {A : 'E^n.+1},
    has_aff_dim PE n inclF A PE aff_indep A aff_gen PE A.
Proof.
intros PE n A HPE HA1 HA2.
move: (has_aff_dim_has_dim_rev (HA1 ord0) HPE) ⇒ HPE'.
apply (aff_gen_lin_gen (A ord0) ord0).
apply aff_span_inclF_diag.
apply (lin_indep_lin_gen HPE'); try easy.
apply frameF_inclF; easy.
Qed.

Lemma aff_indep_aff_basis :
   {PE : E Prop} {n} {A : 'E^n.+1},
    has_aff_dim PE n inclF A PE aff_indep A aff_basis PE A.
Proof. intros; split; [apply aff_indep_aff_gen |]; easy. Qed.

Lemma aff_indep_aff_basis_equiv :
   {PE : E Prop} {n} {A : 'E^n.+1},
    has_aff_dim PE n inclF A PE aff_indep A aff_gen PE A.
Proof.
intros; split; [apply aff_indep_aff_gen | apply aff_gen_aff_indep]; easy.
Qed.

End AffineSpace_FD_R_Facts.

Section ModuleSpace_AffineSpace_R_Facts.

Context {E : ModuleSpace R_Ring}.

Lemma affine_independent_generator :
   {n} (A : 'E^n.+1),
    has_dim (@fullset E) n affine_independent A affine_generator A.
Proof.
moven A /(has_dim_has_aff_dim_rev (A ord0)) HE /affine_independent_equiv HA.
apply affine_generator_equiv.
apply aff_indep_aff_gen; easy.
Qed.

End ModuleSpace_AffineSpace_R_Facts.