Library Algebra.Finite_dim.Finite_dim_MS_def

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

Definitions for finite-dimensional module spaces.

Description

When there is a finite generator family, linear algebra is simplified. With the notions of basis and dimension (the cardinal of bases), many results are simplified.
Let K : Ring and E : ModuleSpace K. Let PE : E Prop. Let B : 'E^n. Let u v w : E.
  • lin_span B is the linear span of B, i.e. the subset of the linear combinations of vectors of B.
    lin_span_EX provides a strong existential for linear spans.
    lin_span_ex provides some smoothness to build the coefficients of the linear combination.
  • line u is the subset of E generated by u. It is a vector line iff u 0.
  • plane u v is the subset of E generated by u and v. It is a vector plane iff u 0 v scal lu u.
  • space_3 u v w is the subset of E generated by u, v and w. It is a vector 3d-space iff u 0 v scal lu u w scal lu u + scal lv v .
  • lc_surjL PE B means that each element of PE is a linear combination of B.
  • lc_injL B means that linear combinations of B are unique.
  • lc_bijL PE B means that each element of PE is a unique linear combination of B.
  • lin_gen PE B means that the vectors of B span PE (i.e. PE = lin_span B), i.e. B is a linear generator of PE.
  • fin_dim PE means that PE admits a finite generator.
  • lin_indep B means that the vectors of B are linearly independent, i.e. that the trivial linear combination of B is the only decomposition of 0. free is an alias for lin_indep.
  • lin_dep B means that the vectors of B are linearly dependent, i.e. that there exists a nontrivial decomposition of 0 over B.
  • basis PE B means that B is both generator of PE and free, i.e. it is a basis of PE.
  • has_dim PE n means that PE admits a basis of length n.

Used logic axioms

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

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.

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

Section FD_MS_Def.

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


Inductive lin_span {n} (B : 'E^n) : E Prop :=
  Lin_span : L, lin_span B (lin_comb L B).

Lemma lin_span_EX :
   {n} (B : 'E^n) x, lin_span B x { L | x = lin_comb L B }.
Proof. move=>> Hx; apply ex_EX; induction Hx as [L]; L; easy. Qed.

Lemma lin_span_ex :
   {n} (B : 'E^n) x, ( L, x = lin_comb L B) lin_span B x.
Proof. move=>> [L HL]; rewrite HL; easy. Qed.

Definition line (x0 : E) := lin_span (singleF x0).
Definition plane (x0 x1 : E) := lin_span (coupleF x0 x1).
Definition space_3 (x0 x1 x2 : E) := lin_span (tripleF x0 x1 x2).

Definition lc_surjL (PE : E Prop) {n} (B : 'E^n) :=
   x, PE x L, x = lin_comb L B.
Definition lc_injL {n} (B : 'E^n) := injective (lin_comb^~ B).
Definition lc_bijL (PE : E Prop) {n} (B : 'E^n) :=
   x, PE x ! L, x = lin_comb L B.

Definition lin_gen (PE : E Prop) {n} (B : 'E^n) : Prop := PE = lin_span B.

Lemma lin_gen_ext :
   {PE} {n} (B1 : 'E^n) {B2}, B1 = B2 lin_gen PE B1 lin_gen PE B2.
Proof. intros; subst; easy. Qed.

Lemma lin_gen_ext2 :
   PE1 {PE2} {n} (B1 : 'E^n) {B2},
    PE1 = PE2 B1 = B2 lin_gen PE1 B1 lin_gen PE2 B2.
Proof. intros; subst; easy. Qed.

Definition fin_dim (PE : E Prop) : Prop :=
   n (B : 'E^n), lin_gen PE B.

Lemma fin_dim_ext : PE1 {PE2}, PE1 = PE2 fin_dim PE1 fin_dim PE2.
Proof. intros; subst; easy. Qed.

Definition lin_indep {n} (B : 'E^n) :=
   (L : 'K^n), lin_comb L B = 0 L = 0.
Definition free {n} (B : 'E^n) := lin_indep B.

Lemma lin_indep_ext :
   {n} (B1 : 'E^n) {B2}, B1 = B2 lin_indep B1 lin_indep B2.
Proof. intros; subst; easy. Qed.

Definition lin_dep {n} (B : 'E^n) := ¬ lin_indep B.

Lemma lin_dep_ext :
   {n} (B1 : 'E^n) {B2}, B1 = B2 lin_dep B1 lin_dep B2.
Proof. intros; subst; easy. Qed.

Definition basis (PE : E Prop) {n} (B : 'E^n) :=
  lin_gen PE B lin_indep B.

Lemma basis_ext :
   {PE} {n} (B1 : 'E^n) {B2}, B1 = B2 basis PE B1 basis PE B2.
Proof. intros; subst; easy. Qed.

Lemma basis_ext2 :
   PE1 {PE2} {n} (B1 : 'E^n) {B2},
    PE1 = PE2 B1 = B2 basis PE1 B1 basis PE2 B2.
Proof. intros; subst; easy. Qed.

Inductive has_dim (PE : E Prop) n : Prop :=
  Dim : (B : 'E^n), basis PE B has_dim PE n.

Lemma has_dim_EX : PE n, has_dim PE n { B : 'E^n | basis PE B }.
Proof. move=>> H; apply ex_EX; induction H as [B]; B; easy. Qed.

Lemma has_dim_ex: PE n, ( B : 'E^n, basis PE B) has_dim PE n.
Proof. move=>> [B HB]. apply (Dim _ _ B HB). Qed.

Lemma has_dim_ext :
   {PE} n1 {n2}, n1 = n2 has_dim PE n1 has_dim PE n2.
Proof. intros; subst; easy. Qed.

Lemma has_dim_ext2 :
   PE1 {PE2} n1 {n2},
    PE1 = PE2 n1 = n2 has_dim PE1 n1 has_dim PE2 n2.
Proof. intros; subst; easy. Qed.

End FD_MS_Def.