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.
Definitions for finite-dimensional module spaces.
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.
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
- lin_span B is the linear span of B,
i.e. the subset of the linear combinations of vectors of B.
- 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
- ex_EX, an alias for constructive_indefinite_description.
Usage
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.