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.
Support for the affine space algebraic structure.
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:
Let K : Ring, V : ModuleSpace K and E : AffineSpace V.
Let K : Ring, V : ModuleSpace K and E : AffineSpace V.
Let T : Type and fA fB : T → E.
Let K : Ring and V1 V2 : ModuleSpace K.
Let E1 : AffineSpace V1 E2 : AffineSpace V2.
Let A B : E1 × E2.
Let K : Ring and V : ModuleSpace K.
Let A B : V.
[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.
This module may be used through the import of Algebra.AffineSpace.AffineSpace,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- 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
- point_of_as E is the nonemptyness witness.
- transl A : V → E is the inverse of the bijection vect A : E → V.
- Notation A --> B is for vect A B;
- A +++ u is for transl A u;
- A ++- u is for transl A (- u).
Support for functions to an affine space
- fct_point_of_as is equal to fun _ ⇒ point_of_as E;
- fct_vect fA fB is equal to fun x ⇒ fA x --> fB x;
- fct_AffineSpace is the type T → E endowed with an AffineSpace structure over the fct_ModuleSpace module space.
Support for the cartesian product of two affine spaces
- prod_point_of_as is equal to (point_of_as E1, point_of_as E2);
- prod_vect A B is equal to (A.1 --> B.1, A.2 --> B.2);
- prod_AffineSpace is the type E1 × E2 endowed with an AffineSpace structure over the prod_ModuleSpace module space.
Support for module spaces seen as affine spaces
- ms_point_of_as is equal to 0;
- ms_vect A B is equal to B - A;
- ModuleSpace_AffineSpace is the type V endowed with an AffineSpace structure over the itself.
Bibliography
Used logic axioms
- unique_choice;
- 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 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.
move⇒ A' /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 x ⇒ fA 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 B ⇒ fA 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.
move⇒ fB' /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.