Library Algebra.AffineSpace.AffineSpace_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

Support for the affine space algebraic structure.

Description

The abstract definition of affine space goes as follows. An affine space over a module space V (type of vectors) is any nonempty type E (type of points) equipped with an external law vect : E E V satisfying the Chasles relation vect A B + vect B C = vect A C for all points A B C, and such that vect A is bijective for all point A.
Many definitions and properties of module spaces may be transposed to affine spaces.
Results that are only valid when the ring of scalars is commutative are only stated in the case of the ring of real numbers R_Ring.
Provides:
  • definitions and notations;
  • support for functions to an affine space;
  • support for the cartesian product of two affine spaces;
  • support for module spaces seen as affine spaces.

Definitions and notations

Let K : Ring, V : ModuleSpace K and E : AffineSpace V. Let A : E.

Support for functions to an affine space

Let K : Ring, V : ModuleSpace K and E : AffineSpace V. Let T : Type and fA fB : T E.

Support for the cartesian product of two affine spaces

Let K : Ring and V1 V2 : ModuleSpace K. Let E1 : AffineSpace V1 E2 : AffineSpace V2. Let A B : E1 × E2.

Support for module spaces seen as affine spaces

Let K : Ring and V : ModuleSpace K. Let A B : V.

Bibliography

[GostiauxT4] Bernard Gostiaux, Cours de mathématiques spéciales - 4. Géométrie affine et métrique Mathématiques, Presses Universitaires de France, Paris, 1995, https://www.puf.com/cours-de-mathematiques-speciales-tome-4-geometrie-affine-et-metrique.

Used logic axioms

Usage

This module may be used through the import of Algebra.AffineSpace.AffineSpace, 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 ModuleSpace.

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

Module AffineSpace.

Record mixin_of {K : Ring} (V : ModuleSpace K) (E : Type) := Mixin {
  ax0 : E;
  vect : E E V;
  ax1 : A B C, vect B A + vect A C = vect B C;
  ax2 : A u, ! B, vect A B = u;
}.

Notation class_of := mixin_of (only parsing).

Section ClassDef.

Context {K : Ring}.
Variable V : ModuleSpace K.

Structure type := Pack { sort; _ : class_of V sort; _ : Type; }.
Local Coercion sort : type >-> Sortclass.
Definition class (cT : type) := let: Pack _ c _ := cT return class_of V cT in c.

End ClassDef.

Module Exports.

Coercion sort : type >-> Sortclass.
Notation AffineSpace := type.

End Exports.

End AffineSpace.

Export AffineSpace.Exports.

Section AffineSpace_Def1.

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

Definition vect := AffineSpace.vect _ _ (AffineSpace.class V E).

End AffineSpace_Def1.

Declare Scope AffineSpace_scope.
Delimit Scope AffineSpace_scope with AS.
Notation "A --> B" := (vect A B) (at level 55) : AffineSpace_scope.

Local Open Scope AffineSpace_scope.

Section AffineSpace_Facts0.

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

Definition point_of_as : E := AffineSpace.ax0 _ _ (AffineSpace.class V _).

Lemma inhabited_as : inhabited E.
Proof. apply (inhabits point_of_as). Qed.

Lemma inhabited_fct_as : {T : Type}, inhabited (T E).
Proof. intros; apply fun_to_nonempty_compat, inhabited_as. Qed.

End AffineSpace_Facts0.

Section AffineSpace_Facts1.

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

Lemma vect_chasles : (A B C : E), (B --> A) + (A --> C) = B --> C.
Proof. intros; apply AffineSpace.ax1. Qed.

Lemma vect_l_bij_ex : (A : E) u, ! B, A --> B = u.
Proof. apply AffineSpace.ax2. Qed.

Lemma vect_l_bij : (A : E), bijective (vect A).
Proof. intros; apply bij_ex_uniq_rev, vect_l_bij_ex. Qed.

Lemma vect_zero : (A : E), A --> A = 0.
Proof.
intros A; apply (plus_reg_l (A --> A)); rewrite vect_chasles plus_zero_r; easy.
Qed.

Lemma vect_zero_equiv : (A B : E), A --> B = 0 B = A.
Proof.
intros A B; split; intros H.
apply eq_sym; destruct (vect_l_bij_ex A 0) as [C [_ HC]].
rewrite -(HC A (vect_zero _)); apply HC; easy.
rewrite H; apply vect_zero.
Qed.

Lemma vect_sym : (A B : E), A --> B = - (B --> A).
Proof.
intros; apply plus_is_zero_l_equiv; rewrite vect_chasles; apply vect_zero.
Qed.

Lemma vect_r_bij_ex : (B : E) u, ! A, A --> B = u.
Proof.
intros B u; destruct (vect_l_bij_ex B (- u)) as [A [HA1 HA2]].
A; split. rewrite vect_sym HA1 opp_opp; easy.
moveA' /opp_eq; rewrite -vect_sym; apply HA2.
Qed.

Lemma vect_r_bij : (B : E), bijective (vect^~ B).
Proof. intros; apply bij_ex_uniq_rev, vect_r_bij_ex. Qed.

Lemma vect_l_eq : (A B1 B2 : E), B1 = B2 A --> B1 = A --> B2.
Proof. intros; subst; easy. Qed.

Lemma vect_r_eq : (B A1 A2 : E), A1 = A2 A1 --> B = A2 --> B.
Proof. intros; subst; easy. Qed.

Lemma vect_l_inj : (A B1 B2 : E), A --> B1 = A --> B2 B1 = B2.
Proof. move=>>; eapply (bij_inj (vect_l_bij _)). Qed.

Lemma vect_r_inj : (B A1 A2 : E), A1 --> B = A2 --> B A1 = A2.
Proof. move=>>; eapply (bij_inj (vect_r_bij _)). Qed.

Lemma vect_l_inj_equiv : (A B1 B2 : E), A --> B1 = A --> B2 B1 = B2.
Proof. intros; split. apply vect_l_inj. apply vect_l_eq. Qed.

Lemma vect_r_inj_equiv : (B A1 A2 : E), A1 --> B = A2 --> B A1 = A2.
Proof. intros; split. apply vect_r_inj. apply vect_r_eq. Qed.

End AffineSpace_Facts1.

Section AffineSpace_Facts2.

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

Lemma as_w_zero_struct_ms : zero_struct V is_unit_type E.
Proof.
destruct (inhabited_as E) as [A]; intros HV; A; intros B.
apply (vect_l_inj A); rewrite !(HV (_ --> _)); easy.
Qed.

Lemma as_w_zero_struct_r : zero_struct K is_unit_type E.
Proof. intros; apply as_w_zero_struct_ms, ms_w_zero_struct_r; easy. Qed.

End AffineSpace_Facts2.

Section AffineSpace_Def2.

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

Lemma transl_EX :
  { f | (A : E), cancel (vect A) (f A) cancel (f A) (vect A) }.
Proof.
assert (H : A : E, ! f, cancel (vect A) f cancel f (vect A)).
  intros A; destruct (vect_l_bij A) as [f Hf1 Hf2]; f; split; [easy |].
  intros f' [Hf'1 Hf'2]; apply fun_ext; intros u.
  apply (vect_l_inj A); rewrite Hf2 Hf'2; easy.
apply ex_EX; destruct (unique_choice _ H) as [f Hf]; f; easy.
Qed.

Definition transl : E V E := proj1_sig transl_EX.

Lemma transl_correct_l : (A : E), cancel (vect A) (transl A).
Proof. apply (proj2_sig transl_EX). Qed.

Lemma transl_correct_r : (A : E), cancel (transl A) (vect A).
Proof. apply (proj2_sig transl_EX). Qed.

End AffineSpace_Def2.

Notation "A +++ u" := (transl A u) (at level 50) : AffineSpace_scope.
Notation "A ++- u" := (transl A (- u)) (at level 50) : AffineSpace_scope.

Local Open Scope AffineSpace_scope.

Section AffineSpace_Facts3.

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

Lemma vect_l_full :
   (PE : E Prop) (O : E), full PE full (image (vect O) PE).
Proof. intros PE O HPE u; rewrite -(transl_correct_r O u); easy. Qed.

Lemma vect_l_fullset : (O : E), image (vect O) fullset = fullset.
Proof. intros; rewrite -full_fullset; apply vect_l_full; easy. Qed.

Lemma transl_l_full : PV (O : E), full PV full (image (transl O) PV).
Proof. intros PV O HPV A; rewrite -(transl_correct_l O A); easy. Qed.

Lemma transl_l_fullset : (O : E), image (transl O) fullset = fullset.
Proof. intros; rewrite -full_fullset; apply transl_l_full; easy. Qed.

Lemma transl_assoc : (A : E) u v, (A +++ u) +++ v = A +++ (u + v).
Proof.
intros A u v; rewrite -(transl_correct_l A ((A +++ u) +++ v))
    -(vect_chasles (A +++ u)) 2!transl_correct_r; easy.
Qed.

Lemma transl_zero : (A : E), A +++ 0 = A.
Proof. intros; erewrite <- vect_zero; apply transl_correct_l. Qed.

Lemma transl_zero_equiv : (A : E) u, A +++ u = A u = 0.
Proof. intros; rewrite -vect_zero_equiv transl_correct_r; easy. Qed.

Lemma transl_l_eq : (A : E) u1 u2, u1 = u2 A +++ u1 = A +++ u2.
Proof. intros; subst; easy. Qed.

Lemma transl_r_eq : u (A1 A2 : E), A1 = A2 A1 +++ u = A2 +++ u.
Proof. intros; subst; easy. Qed.

Lemma transl_l_inj : (A : E) u1 u2, A +++ u1 = A +++ u2 u1 = u2.
Proof.
intros A u1 u2 H; rewrite -(transl_correct_r A u1) -(transl_correct_r A u2).
apply vect_l_eq; easy.
Qed.

Lemma transl_r_inj : u (A1 A2 : E), A1 +++ u = A2 +++ u A1 = A2.
Proof.
intros u A1 A2 H.
rewrite -(transl_zero A1) -(transl_zero A2) -(plus_opp_r u) -2!transl_assoc.
apply transl_r_eq; easy.
Qed.

Lemma transl_l_inj_equiv : (A : E) u1 u2, A +++ u1 = A +++ u2 u1 = u2.
Proof. intros; split. apply transl_l_inj. apply transl_l_eq. Qed.

Lemma transl_r_inj_equiv : u (A1 A2 : E), A1 +++ u = A2 +++ u A1 = A2.
Proof. intros; split. apply transl_r_inj. apply transl_r_eq. Qed.

Lemma transl_opp_equiv : (A B : E) u, A +++ u = B A = B ++- u.
Proof.
intros A B u.
rewrite -(transl_r_inj_equiv (- u)) transl_assoc plus_opp_r transl_zero; easy.
Qed.

Lemma transl_vect_equiv : (A B : E) u, B = A +++ u u = A --> B.
Proof. intros; erewrite <- vect_l_inj_equiv, transl_correct_r; easy. Qed.

Lemma transl_l_bij : (A : E), bijective (transl A).
Proof.
intros A; apply (bij_can_bij (vect_l_bij A)); apply transl_correct_l.
Qed.

Lemma transl_l_bij_ex : (A B : E), ! u, A +++ u = B.
Proof. intros; apply bij_ex_uniq, transl_l_bij. Qed.

Lemma transl_r_bij_ex : u (B : E), ! A, A +++ u = B.
Proof.
intros u B; (B ++- u); split.
apply transl_opp_equiv; easy.
intros A; rewrite transl_opp_equiv; easy.
Qed.

Lemma transl_r_bij : u, bijective (transl^~ u : E E).
Proof. intros; apply bij_ex_uniq_rev, transl_r_bij_ex. Qed.

Lemma vect_transl : (O : E) u v, (O +++ u) --> (O +++ v) = v - u.
Proof.
intros O u v; rewrite -{1}(plus_minus_l v u) plus_comm -transl_assoc.
apply transl_correct_r.
Qed.

Lemma vect_transl_assoc : (O A : E) u, O --> (A +++ u) = (O --> A) + u.
Proof. intros; rewrite -(vect_chasles A) transl_correct_r; easy. Qed.

Lemma vect_transl_plus :
   (O : E) u v,
    O --> (O +++ (u + v)) = (O --> (O +++ u)) + (O --> (O +++ v)).
Proof. intros; rewrite !transl_correct_r; easy. Qed.

Lemma vect_transl_scal :
   (O : E) a u, O --> (O +++ (scal a u)) = scal a (O --> (O +++ u)).
Proof. intros; rewrite !transl_correct_r; easy. Qed.

End AffineSpace_Facts3.

Section Fct_AffineSpace.

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

Definition fct_point_of_as : T E := fun _point_of_as E.

Definition fct_vect (fA fB : T E) : T V := fun xfA x --> fB x.

Lemma fct_vect_chasles :
   (fA fB fC : T E), fct_vect fB fA + fct_vect fA fC = fct_vect fB fC.
Proof. intros; apply fun_ext; intro; apply vect_chasles. Qed.

Lemma fct_vect_l_bij_ex :
   (fA : T E) (fu : T V), ! fB, fct_vect fA fB = fu.
Proof.
intros fA fu.
destruct (unique_choice (fun x BfA x --> B = fu x)) as [fB HfB].
intros x; apply (vect_l_bij_ex (fA x) (fu x)).
fB; split. apply fun_ext_equiv; easy.
movefB' /fun_ext_equiv HfB'; apply fun_ext; intros x.
apply (vect_l_inj (fA x)); rewrite HfB -HfB'; easy.
Qed.

Definition fct_AffineSpace_mixin :=
  AffineSpace.Mixin _ _ _ fct_point_of_as _ fct_vect_chasles fct_vect_l_bij_ex.

Canonical Structure fct_AffineSpace :=
  AffineSpace.Pack _ _ fct_AffineSpace_mixin (T E).

Lemma fct_vect_eq : (fA fB : T E) t, (fA --> fB) t = fA t --> fB t.
Proof. easy. Qed.

Lemma fct_transl_eq :
   (fA : T E) (fu : T V) t, (fA +++ fu) t = fA t +++ fu t.
Proof.
intros fA fu t; apply (vect_l_inj (fA t)).
rewrite -fct_vect_eq 2!transl_correct_r; easy.
Qed.

End Fct_AffineSpace.

Section prod_AffineSpace.

Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.

Definition prod_point_of_as : E1 × E2 := (point_of_as E1, point_of_as E2).

Definition prod_vect (A B : E1 × E2) : V1 × V2 := (A.1 --> B.1, A.2 --> B.2).

Lemma prod_vect_chasles :
   A B C, prod_vect B A + prod_vect A C = prod_vect B C.
Proof. intros; apply (f_equal2 Datatypes.pair); apply vect_chasles. Qed.

Lemma prod_vect_l_bij_ex : A u, ! B, prod_vect A B = u.
Proof.
intros [A1 A2] [u1 u2]; destruct (vect_l_bij_ex A1 u1) as [B1 [HB1a HB1b]],
    (vect_l_bij_ex A2 u2) as [B2 [HB2a HB2b]].
(B1, B2); split. rewrite -HB1a -HB2a; easy.
move⇒ [C1 C2] /pair_equal_spec /= [HC1 HC2]; apply (f_equal2 Datatypes.pair);
    [apply HB1b | apply HB2b]; easy.
Qed.

Definition prod_AffineSpace_mixin :=
  AffineSpace.Mixin _ _ _ prod_point_of_as _
    prod_vect_chasles prod_vect_l_bij_ex.

Canonical Structure prod_AffineSpace :=
  AffineSpace.Pack _ _ prod_AffineSpace_mixin (E1 × E2).

Lemma prod_vect_eq : (A B : E1 × E2), A --> B = (A.1 --> B.1, A.2 --> B.2).
Proof. easy. Qed.

Lemma prod_transl_eq :
   (A : E1 × E2) (u : V1 × V2), A +++ u = (A.1 +++ u.1, A.2 +++ u.2).
Proof.
intros A [u1 u2]; apply (vect_l_inj A).
rewrite (prod_vect_eq _ (A.1 +++ u1, A.2 +++ u2)) 3!transl_correct_r; easy.
Qed.

End prod_AffineSpace.

Section ModuleSpace_Is_AffineSpace.

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

Definition ms_point_of_as : V := 0.

Definition ms_vect (A B : V) : V := B - A.

Lemma ms_vect_chasles : A B C, ms_vect B A + ms_vect A C = ms_vect B C.
Proof. intros; rewrite plus_comm -minus_trans; easy. Qed.

Lemma ms_vect_l_bij_ex : A u, ! B, ms_vect A B = u.
Proof.
intros A u; (A + u); split; [apply: minus_plus_l |].
intros v Hv; rewrite -Hv plus_comm; apply: plus_minus_l.
Qed.

Definition ModuleSpace_AffineSpace_mixin :=
  AffineSpace.Mixin _ _ _ ms_point_of_as _ ms_vect_chasles ms_vect_l_bij_ex.

Canonical Structure ModuleSpace_AffineSpace :=
  AffineSpace.Pack _ _ ModuleSpace_AffineSpace_mixin V.

Lemma ms_vect_eq : (A B : V), A --> B = B - A.
Proof. easy. Qed.

Lemma ms_transl_eq : (A u : V), A +++ u = A + u.
Proof.
intros A u; apply (vect_l_inj A); unfold vect at 2; simpl; unfold ms_vect.
rewrite transl_correct_r minus_plus_l; easy.
Qed.

End ModuleSpace_Is_AffineSpace.

Coercion ModuleSpace_AffineSpace : ModuleSpace >-> AffineSpace.