Library Algebra.Finite_dim.Finite_dim_AS_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 affine spaces.

Description

When there is a finite generator family, affine algebra is simplified. With the notions of basis and dimension (the cardinal of bases), many results are simplified.
Let K : Ring, V : ModuleSpace K and E : AffineSpace V. Let PE : E Prop. Let A : 'E^n and A' : 'E^n.+1. Let A0 A1 A2 : E.

Used logic axioms

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

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

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


Inductive aff_span {n} (A : 'E^n) : E Prop :=
  Aff_span : L, invertible (sum L) aff_span A (barycenter L A).

Lemma aff_span_EX :
   {n} (A : 'E^n) G,
    aff_span A G { L | sum L = 1 G = barycenter L A }.
Proof.
move=>> Hx; apply ex_EX; induction Hx as [L HL];
    eexists; apply (baryc_normalized _ _ _ HL); easy.
Qed.

Lemma aff_span_ex :
   {n} (A : 'E^n) G,
    ( L, invertible (sum L) G = barycenter L A) aff_span A G.
Proof. move=>> [L [HL1 HL2]]; rewrite HL2; easy. Qed.

Definition aff_point (A0 : E) := aff_span (singleF A0).
Definition aff_line (A0 A1 : E) := aff_span (coupleF A0 A1).
Definition aff_plane (A0 A1 A2 : E) := aff_span (tripleF A0 A1 A2).

Definition baryc_surjL (PE : E Prop) {n} (A : 'E^n) :=
   G, PE G L, invertible (sum L) G = barycenter L A.
Definition baryc_injL {n} (A : 'E^n) :=
   L L', invertible (sum L) sum L = sum L'
    barycenter L A = barycenter L' A L = L'.
Definition baryc_bijL (PE : E Prop) {n} (A : 'E^n) :=
   G, PE G ! L, sum L = 1 G = barycenter L A.

Definition aff_gen (PE : E Prop) {n} (A : 'E^n) := PE = aff_span A.

Lemma aff_gen_ext :
   {PE} {n} (A1 : 'E^n) {A2}, A1 = A2 aff_gen PE A1 aff_gen PE A2.
Proof. intros; subst; easy. Qed.

Lemma aff_gen_ext2 :
   PE1 {PE2} {n} (A1 : 'E^n) {A2},
    PE1 = PE2 A1 = A2 aff_gen PE1 A1 aff_gen PE2 A2.
Proof. intros; subst; easy. Qed.

Definition aff_indep {n} (A : 'E^n.+1) :=
   i0, lin_indep (frameF A i0).

Lemma aff_indep_ext :
   {n} (A1 : 'E^n.+1) {A2}, A1 = A2 aff_indep A1 aff_indep A2.
Proof. intros; subst; easy. Qed.

Definition aff_dep {n} (A : 'E^n.+1) := ¬ aff_indep A.

Lemma aff_dep_ext :
   {n} (A1 : 'E^n.+1) {A2}, A1 = A2 aff_dep A1 aff_dep A2.
Proof. intros; subst; easy. Qed.

Definition aff_basis (PE : E Prop) {n} (A : 'E^n.+1) :=
  aff_gen PE A aff_indep A.

Lemma aff_basis_ext :
   {PE} {n} (A1 : 'E^n.+1) {A2},
    A1 = A2 aff_basis PE A1 aff_basis PE A2.
Proof. intros; subst; easy. Qed.

Lemma aff_basis_ext2 :
   PE1 {PE2} {n} (A1 : 'E^n.+1) {A2},
    PE1 = PE2 A1 = A2 aff_basis PE1 A1 aff_basis PE2 A2.
Proof. intros; subst; easy. Qed.

Inductive has_aff_dim (PE : E Prop) n : Prop :=
  Aff_dim : (A : 'E^n.+1), aff_basis PE A has_aff_dim PE n.

Lemma has_aff_dim_EX :
   PE n, has_aff_dim PE n { A : 'E^n.+1 | aff_basis PE A }.
Proof. move=>> H; apply ex_EX; induction H as [A]; A; easy. Qed.

Lemma has_aff_dim_ex:
   PE n, ( A : 'E^n.+1, aff_basis PE A) has_aff_dim PE n.
Proof. move=>> [A HA]. apply (Aff_dim _ _ A HA). Qed.

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

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

End FD_AS_Def.