Library Algebra.AffineSpace.AffineSpace_sub
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 affine subspaces.
Let K : Ring, V : ModuleSpace K and E : AffineSpace V.
Let PE : E → Prop, O : E and PV : V → Prop.
Let O : E.
Lemmas about predicate compatible_as have "cas" in their names, usually as
prefix "cas_", sometimes as suffix "_cas".
Let gen : E → Prop.
Let K : Ring, V1 V2 : ModuleSpace K.
Let E1 : AffineSpace V1 and E2 : AffineSpace V2.
Let f : E1 → E2 and PE1 : E1 → Prop.
Let K : Ring and HK : invertible (2 : K).
Let V : ModuleSpace K and E : AffineSpace V.
Let PE : E → Prop and HPE : compatible_as PE.
Let O : E and HO : PE O.
Let K : Ring and HK : invertible (2 : K).
Let V1 V2 : ModuleSpace K.
Let E1 : AffineSpace V1 and E2 : AffineSpace V2.
Let PE1 : E1 → Prop and PE2 : E2 → Prop.
Let HPE1 : compatible_as PE1 and HPE2 : compatible_as PE2.
Let O1 : E1, HO1 : PE1 O1, O2 : E2 and HO2 : PE2 O2.
Let f : E1 → E2 and Hf : funS PE1 PE2 f.
This is only stated for the ring of real numbers R_Ring.
Let V1 V2 : ModuleSpace R_Ring.
Let E1 : AffineSpace V1 and E2 : AffineSpace V2.
[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
Support for affine subspace
- vectP PE O is the preimage of PE by transl O, ie fun u ⇒ PE (O +++ u);
- translP PV O is the preimage of PV by vect O, ie fun A ⇒ PV (O --> A);
- vect_closed_gen PE PV states that if PE O, then PE is the preimage of PV by vect O;
- transl_closed_gen PE PV states that if PE O, then PV is the preimage of PE by transl O;
- vect_closed PE O is the specialization vect_closed_gen PE (vectP PE O);
- transl_closed PE O is the specialization
transl_closed_gen PE (translP PE O);
- compatible_as PE states that PE is closed under regular barycenters, this could have been called baryc_closed.
- span_as gen is the specialization span compatible_as gen (see Algebra.Sub_struct), ie it is the intersection of all subsets (= the smallest) compatible with the AffineSpace structure that also contain gen;
- baryc_closure gen is the subset of all regular barycenters of points of gen.
Additional support for affine map
Additional support for affine subspace
- sub_AffineSpace HK HPE HO is the type sub PE endowed with the AffineSpace structure (see Subsets..Sub_type).
- fct_sub_as HPE1 HPE2 Hf is the function fct_sub Hf with type sub_AffineSpace HK HPE1 HO1 → sub_ModuleSpace HK HPE2 O2 HO2 (see Subsets.Sub_type).
Additional definition for commutative rings of scalars
Bibliography
Used logic axioms
- classic_dec, an alias for excluded_middle_informative, the strong form of excluded middle;
- ex_EX, an alias for constructive_indefinite_description.
Usage
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 Sub_struct.
From Algebra Require Import Monoid Group Ring ModuleSpace.
From Algebra Require Import AffineSpace_def AffineSpace_FF.
From Algebra Require Import AffineSpace_baryc AffineSpace_aff_map.
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 Compatible_AffineSpace_Def.
Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Definition vectP (PE : E → Prop) (O : E) : V → Prop :=
preimage (transl O) PE.
Definition translP (PV : V → Prop) (O : E) : E → Prop :=
preimage (vect O) PV.
Definition vect_closed_gen (PE : E → Prop) (PV : V → Prop) : Prop :=
∀ O A, PE O → PE A ↔ translP PV O A.
Definition transl_closed_gen (PE : E → Prop) (PV : V → Prop) : Prop :=
∀ O u, PE O → PV u ↔ vectP PE O u.
Definition vect_closed PE O := vect_closed_gen PE (vectP PE O).
Definition transl_closed PE O := transl_closed_gen PE (vectP PE O).
[GostiauxT4]
Def. 1.23, p. 9.
compatible_as is actually baryc_closed.
Definition compatible_as (PE : E → Prop) : Prop :=
∀ n L (A : 'E^n),
invertible (sum L) → inclF A PE → PE (barycenter L A).
Definition span_as (gen : E → Prop) : E → Prop :=
span compatible_as gen.
Inductive baryc_closure (gen : E → Prop) : E → Prop :=
| Barycenter_closure :
∀ n L (B : 'E^n),
invertible (sum L) → inclF B gen →
baryc_closure gen (barycenter L B).
End Compatible_AffineSpace_Def.
Section Compatible_AffineSpace_Facts.
Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Lemma vectP_correct :
∀ {PE : E → Prop} {O}, PE O → PE = image (transl O) (vectP PE O).
Proof. intros; rewrite image_of_preimage transl_l_fullset inter_full_r //. Qed.
Lemma vectP_eq : ∀ {PE : E → Prop} {O}, vectP PE O = image (vect O) PE.
Proof.
intros; apply preimage_eq; [apply transl_correct_r | apply transl_correct_l].
Qed.
Lemma vectP_inj :
∀ {PE QE : E → Prop} O, vectP PE O = vectP QE O → PE = QE.
Proof. move=>>; eapply preimage_inj, transl_correct_l. Qed.
Lemma vectP_full :
∀ {PE : E → Prop} O, full PE → full (vectP PE O).
Proof. intros; apply preimage_full_equiv; easy. Qed.
Lemma vectP_fullset : ∀ (O : E), vectP fullset O = fullset.
Proof. easy. Qed.
Lemma vectP_inter :
∀ {PE1 PE2 : E → Prop} {O},
vectP (inter PE1 PE2) O = inter (vectP PE1 O) (vectP PE2 O).
Proof. easy. Qed.
Lemma vectP_inter_any :
∀ {Idx : Type} {PE : Idx → E → Prop} {O},
vectP (inter_any PE) O = inter_any (fun idx ⇒ vectP (PE idx) O).
Proof. easy. Qed.
Lemma vectP_zero_closed_equiv :
∀ {PE : E → Prop} {O}, zero_closed (vectP PE O) ↔ PE O.
Proof. intros PE O; rewrite -{2}(transl_zero O); easy. Qed.
Lemma translP_correct :
∀ {PV : V → Prop} (O : E), PV = image (vect O) (translP PV O).
Proof. intros; rewrite image_of_preimage vect_l_fullset inter_full_r //. Qed.
Lemma translP_eq :
∀ {PV : V → Prop} {O : E}, translP PV O = image (transl O) PV.
Proof.
intros; apply preimage_eq; [apply transl_correct_l | apply transl_correct_r].
Qed.
Lemma translP_inj :
∀ {PV QV : V → Prop} (O : E), translP PV O = translP QV O → PV = QV.
Proof. move=>>; eapply preimage_inj, transl_correct_r. Qed.
Lemma translP_full :
∀ {PV : V → Prop} (O : E), full PV → full (translP PV O).
Proof. intros; apply preimage_full_equiv; easy. Qed.
Lemma translP_fullset : ∀ (O : E), translP fullset O = fullset.
Proof. easy. Qed.
Lemma translP_inter :
∀ {PV1 PV2 : V → Prop} {O : E},
translP (inter PV1 PV2) O = inter (translP PV1 O) (translP PV2 O).
Proof. easy. Qed.
Lemma translP_inter_any :
∀ {Idx : Type} {PV : Idx → V → Prop} {O : E},
translP (inter_any PV) O = inter_any (fun idx ⇒ translP (PV idx) O).
Proof. easy. Qed.
Lemma translP_zero_closed_equiv :
∀ {PV : V → Prop} (O : E), zero_closed PV ↔ translP PV O O.
Proof. intros; unfold translP, preimage; rewrite vect_zero; easy. Qed.
Lemma vectP_translP :
∀ (PV : V → Prop) (O : E), vectP (translP PV O) O = PV.
Proof. intros; apply preimage_can, transl_correct_r. Qed.
Lemma translP_vectP :
∀ {PE : E → Prop} O, translP (vectP PE O) O = PE.
Proof. intros; apply preimage_can, transl_correct_l. Qed.
Lemma vect_transl_closed_gen_equiv :
∀ {PE : E → Prop} {PV},
vect_closed_gen PE PV ↔ transl_closed_gen PE PV.
Proof.
intros; split; intros HPE A; unfold vectP, translP, preimage.
intros u HA; rewrite -{1}(transl_correct_r A u) (HPE A); easy.
intros B HA; rewrite -{1}(transl_correct_l A B) (HPE A); easy.
Qed.
Lemma vect_transl_closed_equiv :
∀ {PE : E → Prop} {O}, vect_closed PE O ↔ transl_closed PE O.
Proof. intros; apply vect_transl_closed_gen_equiv. Qed.
Lemma transl_plus_closed :
∀ {PE : E → Prop} {O}, transl_closed PE O → plus_closed (vectP PE O).
Proof.
move=>> HPE u v; unfold vectP, preimage; rewrite -transl_assoc; apply HPE; easy.
Qed.
Lemma vect_plus_closed :
∀ {PE : E → Prop} {O}, vect_closed PE O → plus_closed (vectP PE O).
Proof. move=>> /vect_transl_closed_equiv; apply transl_plus_closed. Qed.
Lemma cms_transl :
∀ {PE : E → Prop} {O}, PE O →
compatible_ms (vectP PE O) → transl_closed PE O.
Proof.
unfold vectP; intros PE O HO HPE A u; unfold vectP, preimage.
rewrite -(transl_correct_l O A) transl_assoc iff_sym_equiv.
apply (cms_plus_equiv HPE).
Qed.
Lemma cms_vect :
∀ {PE : E → Prop} {O}, PE O →
compatible_ms (vectP PE O) → vect_closed PE O.
Proof.
unfold vect_closed.
move=>>; rewrite vect_transl_closed_gen_equiv; apply cms_transl.
Qed.
Lemma vectP_orig_indep :
∀ {PE : E → Prop} {O} (O' : E), PE O →
compatible_ms (vectP PE O') → vectP PE O = vectP PE O'.
Proof.
intros; apply subset_ext; intros u.
apply iff_sym, cms_transl; try easy.
apply vectP_zero_closed_equiv, cms_zero; easy.
Qed.
Lemma translP_orig_indep :
∀ {PV : V → Prop} {O} (O' : E), translP PV O O' →
compatible_ms PV → translP PV O = translP PV O'.
Proof.
intros PV O O' HO' HPV; apply subset_ext; intros A.
rewrite -{2}(vectP_translP PV O); apply cms_vect; try easy.
apply translP_zero_closed_equiv, cms_zero; easy.
rewrite vectP_translP; easy.
Qed.
Lemma vect_closed_orig_indep :
∀ {PE : E → Prop} O O',
PE O → compatible_ms (vectP PE O') →
vect_closed PE O → vect_closed PE O'.
Proof.
move=>> HO HPV HPE; move=>>; rewrite -(vectP_orig_indep _ HO); auto.
Qed.
Lemma transl_closed_orig_indep :
∀ {PE : E → Prop} O O',
PE O → compatible_ms (vectP PE O') →
transl_closed PE O → transl_closed PE O'.
Proof.
move=>> HO HPV HPE; move=>>; rewrite -(vectP_orig_indep _ HO); auto.
Qed.
Lemma transl_closed_gen_sms_uniq :
∀ {PE : E → Prop} {PV} {O : E},
PE O → compatible_ms PV → transl_closed_gen PE PV → PV = vectP PE O.
Proof.
move=>> HO HPV HPE; apply subset_ext_equiv; split; intro;
[apply HPE | apply (HPE _ _ HO)]; easy.
Qed.
Lemma vect_closed_gen_sms_uniq :
∀ {PE : E → Prop} {PV} {O : E},
PE O → compatible_ms PV → vect_closed_gen PE PV → PV = vectP PE O.
Proof.
move=>>; rewrite vect_transl_closed_gen_equiv; apply transl_closed_gen_sms_uniq.
Qed.
Lemma cas_empty :
∀ {PE : E → Prop}, nonzero_struct K → empty PE → compatible_as PE.
Proof.
intros PE HK HPE n L A HL HA; destruct n.
contradict HL; apply sum_nil_noninvertible; easy.
contradict HA; rewrite not_all_ex_not_equiv; ∃ ord0.
intros HA0; apply (HPE _ HA0).
Qed.
Lemma cas_emptyset :
∀ {PE : E → Prop}, nonzero_struct K → compatible_as (@emptyset E).
Proof. intros; apply cas_empty; easy. Qed.
Lemma cas_singleton : ∀ (O : E), compatible_as (singleton O).
Proof. move=>> HL /extF ->; apply baryc_constF; easy. Qed.
Lemma cas_unit :
∀ {PE : E → Prop},
nonzero_struct K → is_unit_type E → compatible_as PE.
Proof.
intros PE HK [O HE].
destruct (empty_dec PE) as [HPE | HPE].
apply cas_empty; easy.
rewrite (unit_subset_is_singleton PE HE HPE).
apply cas_singleton.
Qed.
Lemma cas_full : ∀ {PE : E → Prop}, full PE → compatible_as PE.
Proof. easy. Qed.
Lemma cas_fullset : compatible_as (@fullset E).
Proof. easy. Qed.
Lemma cms_cas :
∀ {PE : E → Prop} {O},
PE O → nonzero_struct K → invertible (2 : K) →
compatible_ms (vectP PE O) → compatible_as PE.
Proof.
move=>> HO HK1 HK2 HPE n L A HL HA.
destruct n. contradict HL; apply sum_nil_noninvertible; easy.
generalize (cms_vect HO HPE (A ord0)); intros HPE'.
unfold translP, vectP, preimage in HPE'.
apply HPE', (cms_scal_rev HPE (sum L) _ HL); try easy.
rewrite baryc_correct_orig; try easy.
apply cms_lc; try easy.
unfold vectP, preimage; intro; rewrite vectF_correct -HPE'; easy.
Qed.
Lemma cas_scal :
∀ {PE : E → Prop} {O},
PE O → compatible_as PE → scal_closed (vectP PE O).
Proof.
intros PE O HO HPE a u Hu; unfold vectP, preimage in ×.
assert (H0 : invertible (sum (coupleF (1 - a) a))).
rewrite sum_coupleF -plus_assoc plus_opp_l plus_zero_r.
apply invertible_one.
assert (H : O +++ scal a u =
barycenter (coupleF (1 - a) a) (coupleF O (O +++ u))).
apply baryc_coupleF_equiv; try easy.
rewrite -{2}(transl_zero O) 2!vect_transl.
rewrite 2!scal_minus_distr_l scal_zero_r scal_minus_distr_r scal_one.
rewrite minus_zero_l plus_opp_l; easy.
unfold vectP; rewrite H; apply HPE; try easy.
intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi;
[rewrite coupleF_0 | rewrite coupleF_1]; easy.
Qed.
Lemma cas_scal_rev :
∀ {PE : E → Prop} {O},
PE O → compatible_as PE → scal_rev_closed (vectP PE O).
Proof. intros; apply scal_scal_rev_closed, cas_scal; easy. Qed.
Lemma cas_plus :
∀ {PE : E → Prop} {O},
PE O → invertible (2 : K) →
compatible_as PE → plus_closed (vectP PE O).
Proof.
intros PE O HO HK HPE; unfold vectP, preimage.
unfold two in HK; rewrite -(sum_2 ones) in HK.
intros u v Hu Hv; pose (A := coupleF (O +++ u) (O +++ v)).
rewrite (transl_l_eq _ _ (sum (vectF O A))).
rewrite -lc_ones_l -baryc_correct_orig; try easy.
apply (cas_scal_rev HO HPE (inv (@sum _ 2 ones)));
try now apply inv_invertible. unfold vectP, preimage.
rewrite → scal_assoc, mult_inv_l, scal_one, transl_correct_l; try easy.
apply HPE; try easy; unfold A;
intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi;
[rewrite coupleF_0 | rewrite coupleF_1]; easy.
unfold A; rewrite vectF_coupleF sum_2 coupleF_0 coupleF_1 !transl_correct_r //.
Qed.
Lemma cas_cms :
∀ {PE : E → Prop} {O},
PE O → invertible (2 : K) →
compatible_as PE → compatible_ms (vectP PE O).
Proof.
intros; apply plus_scal_closed_cms.
unfold vectP, preimage; ∃ 0; rewrite transl_zero; easy.
apply cas_plus; easy.
apply cas_scal; easy.
Qed.
Lemma cas_cms_equiv :
∀ {PE : E → Prop} {O},
PE O → nonzero_struct K → invertible (2 : K) →
compatible_as PE ↔ compatible_ms (vectP PE O).
Proof. intros; split; [apply cas_cms | apply cms_cas]; easy. Qed.
Lemma cas_sms_orig_indep :
∀ {PE : E → Prop} {O O'},
PE O → PE O' → invertible (2 : K) →
compatible_as PE → vectP PE O = vectP PE O'.
Proof. intros; apply vectP_orig_indep; try apply cas_cms; easy. Qed.
Lemma cas_vect :
∀ {PE : E → Prop} {O},
PE O → invertible (2 : K) →
compatible_as PE → vect_closed PE O.
Proof. intros; apply cms_vect, cas_cms; easy. Qed.
Lemma cas_transl :
∀ {PE : E → Prop} {O},
PE O → invertible (2 : K) →
compatible_as PE → transl_closed PE O.
Proof.
intros; apply vect_transl_closed_gen_equiv, cas_vect; easy.
Qed.
Lemma cas_inter :
∀ {PE1 PE2 : E → Prop},
compatible_as PE1 → compatible_as PE2 → compatible_as (inter PE1 PE2).
Proof.
move=>> HPE1 HPE2; move=>> HL HA; split; [apply HPE1 | apply HPE2];
try easy; intro; apply HA.
Qed.
Lemma cas_inter_any :
∀ {Idx : Type} {PE : Idx → E → Prop},
(∀ idx, compatible_as (PE idx)) →
compatible_as (inter_any PE).
Proof.
move=>> HPE; move=>> HL HA idx; apply HPE; try easy; intro; apply HA.
Qed.
Lemma span_as_cas : ∀ (gen : E → Prop), compatible_as (span_as gen).
Proof. apply span_compatible; move=>>; apply cas_inter_any. Qed.
Lemma span_as_incl : ∀ (gen : E → Prop), incl gen (span_as gen).
Proof. apply span_incl. Qed.
Lemma span_as_lub :
∀ gen {PE : E → Prop},
compatible_as PE → incl gen PE → incl (span_as gen) PE.
Proof. apply span_lub. Qed.
Lemma span_as_full :
∀ {PE : E → Prop}, compatible_as PE → span_as PE = PE.
Proof. apply span_full. Qed.
Lemma baryc_closure_ex :
∀ (gen : E → Prop) A,
(∃ n L (B : 'E^n),
invertible (sum L) ∧ inclF B gen ∧ A = barycenter L B) →
baryc_closure gen A.
Proof.
move=>> [n [L [B [HL [HB HA]]]]]; rewrite HA; apply Barycenter_closure; easy.
Qed.
Lemma baryc_closure_ex_rev :
∀ (gen : E → Prop) A,
baryc_closure gen A →
∃ n L (B : 'E^n),
sum L = 1 ∧ (∀ i, L i ≠ 0) ∧ inclF B gen ∧ A = barycenter L B.
Proof.
intros gen A HA; induction HA as [n L B HL HB].
destruct (baryc_normalized_n0_ex L B HL)
as [n1 [L1 [A1 [HL1a [HL1b [HA1a HA1b]]]]]].
∃ n1, L1, A1; repeat split; try easy.
apply (inclF_monot_l _ B); easy.
Qed.
Lemma bc_len_EX :
∀ (gen : E → Prop) A,
{ n | baryc_closure gen A →
∃ L (B : 'E^n),
sum L = 1 ∧ (∀ i, L i ≠ 0) ∧
inclF B gen ∧ A = barycenter L B }.
Proof.
intros gen A; apply ex_EX.
destruct (classic_dec (baryc_closure gen A)) as [HA | HA].
destruct (baryc_closure_ex_rev _ _ HA) as [n [L [B HLB]]].
∃ n; intros _; ∃ L, B; easy.
∃ 0; intros HA'; easy.
Qed.
Definition bc_len (gen : E → Prop) A := proj1_sig (bc_len_EX gen A).
Lemma bc_EX :
∀ (gen : E → Prop) A,
{ LB : 'K^(bc_len gen A) × 'E^(bc_len gen A) |
baryc_closure gen A →
sum LB.1 = 1 ∧ (∀ i, LB.1 i ≠ 0) ∧
inclF LB.2 gen ∧ A = barycenter LB.1 LB.2 }.
Proof.
intros gen A; apply ex_EX.
destruct (classic_dec (baryc_closure gen A)) as [HA | HA].
destruct (proj2_sig (bc_len_EX gen A)) as [L [B HLB]]; try easy.
∃ (L, B); intros _; easy.
destruct (inhabited_as E) as [O].
∃ ((fun _ ⇒ 0), (fun _ ⇒ O)); intros HA'; easy.
Qed.
Definition bc_coef (gen : E → Prop) A := fst (proj1_sig (bc_EX gen A)).
Definition bc_point (gen : E → Prop) A := snd (proj1_sig (bc_EX gen A)).
Lemma bc_nLB_correct :
∀ (gen : E → Prop) A,
baryc_closure gen A →
sum (bc_coef gen A) = 1 ∧
(∀ i, bc_coef gen A i ≠ 0) ∧
inclF (bc_point gen A) gen ∧
A = barycenter (bc_coef gen A) (bc_point gen A).
Proof. intros gen A HA; destruct (proj2_sig (bc_EX gen A)); easy. Qed.
Lemma baryc_closure_exs :
∀ {gen : E → Prop} {n} (A : 'E^n),
inclF A (baryc_closure gen) →
∃ (b : 'nat^n) L (B : ∀ i, 'E^(b i)),
(∀ i, sum (L i) = 1) ∧ (∀ i j, L i j ≠ 0) ∧
(∀ i, inclF (B i) gen) ∧ A = fun i ⇒ barycenter (L i) (B i).
Proof.
intros gen n A HA; destruct n.
destruct (inhabited_as E) as [O]; ∃ 0, (fun _ ⇒ 0), (fun _ _ ⇒ O).
repeat split; try apply extF; intros [i Hi]; easy.
∃ (fun i ⇒ bc_len gen (A i)), (fun i ⇒ bc_coef gen (A i)),
(fun i ⇒ bc_point gen (A i)).
repeat split; try apply extF; intro; apply bc_nLB_correct; easy.
Qed.
Lemma cas_equiv :
∀ (PE : E → Prop), compatible_as PE ↔ PE = baryc_closure PE.
Proof.
intros PE; split; intros HPE.
apply subset_ext_equiv; split; intros A HA; try induction HA; auto.
rewrite -(baryc_singleF 1 A (singleF 1) (singleF A)); try easy.
apply Barycenter_closure; try easy.
apply sum_singleF_invertible.
1,2: apply invertible_one.
move=>> HL HB; rewrite HPE; apply Barycenter_closure; easy.
Qed.
Lemma baryc_closure_incl :
∀ (gen : E → Prop), incl gen (baryc_closure gen).
Proof.
intros gen A HA.
rewrite -(baryc_singleF 1 A (singleF 1) (singleF A));
try apply invertible_one; try easy.
apply Barycenter_closure; try easy.
rewrite sum_1 singleF_0; apply invertible_one.
Qed.
End Compatible_AffineSpace_Facts.
Section Compatible_AffineSpace_Affine_Mapping_Facts1.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Context {f : E1 → E2}.
Hypothesis Hf : aff_map f.
Lemma cas_image : compatible_as PE1 → compatible_as (image f PE1).
Proof.
intro; move=>> HL /inclF_image_equiv [A [HA1 HA2]].
rewrite HA2 -Hf; try easy; apply Im; auto.
Qed.
Lemma cas_preimage : compatible_as PE2 → compatible_as (preimage f PE2).
Proof. intro; move=>> Hl HA; unfold preimage; rewrite Hf; auto. Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts1.
Section Compatible_AffineSpace_Affine_Mapping_Def.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Variable PE1 : E1 → Prop.
Variable f : E1 → E2.
Definition am_sub : Prop :=
∀ n L (A1 : 'E1^n),
inclF A1 PE1 →
invertible (sum L) → f (barycenter L A1) = barycenter L (mapF f A1).
End Compatible_AffineSpace_Affine_Mapping_Def.
Section Compatible_AffineSpace_Affine_Mapping_Facts2a.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 → Prop}.
Hypothesis HPE1 : compatible_as PE1.
Context {PE2 : E2 → Prop}.
Hypothesis HPE2 : compatible_as PE2.
Context {f : E1 → E2}.
Hypothesis Hf : aff_map f.
Lemma RgS_gen_cas : compatible_as (RgS_gen PE1 PE2 f).
Proof. apply cas_inter, cas_image; easy. Qed.
Lemma RgS_cas : compatible_as (RgS PE1 f).
Proof. apply cas_image; easy. Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts2a.
Section Compatible_AffineSpace_Affine_Mapping_Facts2b.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {f : E1 → E2}.
Hypothesis Hf : aff_map f.
Lemma Rg_cas : compatible_as (Rg f).
Proof. rewrite -RgS_full; apply (RgS_cas cas_fullset Hf). Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts2b.
Section Compatible_AffineSpace_Affine_Mapping_Facts4a.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Variable PE1 : E1 → Prop.
Lemma am_sub_id : am_sub PE1 ssrfun.id.
Proof. easy. Qed.
Context {f : E1 → E2}.
Lemma am_is_sub : aff_map f → am_sub PE1 f.
Proof. intros Hf n L A1 _; apply Hf. Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts4a.
Section Compatible_AffineSpace_Affine_Mapping_Facts4b.
Context {K : Ring}.
Context {V1 V2 V3 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {E3 : AffineSpace V3}.
Context {PE1 : E1 → Prop}.
Variable PE2 : E2 → Prop.
Context {f : E1 → E2}.
Hypothesis Hf : funS PE1 PE2 f.
Variable g : E2 → E3.
Lemma am_comp_sub : am_sub PE1 f → am_sub PE2 g → am_sub PE1 (g \o f).
Proof.
intros Hfa Hga n L A1 HA1 HL; unfold ssrfun.comp; rewrite Hfa// Hga//.
apply (inclF_monot_r (RgS PE1 f)); [easy |].
apply mapF_inclF; easy.
Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts4b.
Section Sub_AffineSpace_Def.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_as PE.
Context {O : E}.
Hypothesis HO : PE O.
Definition sub_point_of_as : sub PE := mk_sub HO.
Let PV := vectP PE O.
Let HPV : compatible_ms PV := cas_cms HO HK HPE.
Lemma sub_vect_aux : ∀ {A B}, PE A → PE B → PV (A --> B).
Proof. move=>>; apply cas_vect; easy. Qed.
Lemma sub_vectF_aux :
∀ {n} {A} {B : 'E^n}, PE A → inclF B PE → inclF (vectF A B) PV.
Proof. intros; intro; apply sub_vect_aux; easy. Qed.
Definition sub_vect (A B : sub PE) : sub_ModuleSpace HPV :=
mk_sub (sub_vect_aux (in_sub A) (in_sub B)).
Lemma sub_vect_chasles :
∀ A B C, sub_vect B A + sub_vect A C = sub_vect B C.
Proof. intros; apply val_inj, vect_chasles. Qed.
Lemma sub_vect_l_bij_ex : ∀ A u, ∃! B, sub_vect A B = u.
Proof.
intros [A HA] [u Hu]; unfold PV in Hu.
assert (Hu' : vectP PE A u) by now rewrite -(cas_transl HO).
∃ (mk_sub_ PE (A +++ u) Hu'); split.
apply val_inj, transl_correct_r.
move⇒ [B HB1] /(f_equal val) /= HB2.
apply val_inj; simpl; rewrite -HB2; apply transl_correct_l.
Qed.
Definition sub_AffineSpace_mixin :=
AffineSpace.Mixin _ _ _ sub_point_of_as _ sub_vect_chasles sub_vect_l_bij_ex.
Canonical Structure sub_AffineSpace :=
AffineSpace.Pack _ _ sub_AffineSpace_mixin (sub PE).
Lemma sub_transl_aux : ∀ {A u}, PE A → PV u → PE (A +++ u).
Proof. move=>>; apply cas_transl; easy. Qed.
Lemma sub_translF_aux :
∀ {n} {A} {u : 'V^n}, PE A → inclF u PV → inclF (translF A u) PE.
Proof. intros; intro; apply sub_transl_aux; easy. Qed.
Definition sub_transl
(A : sub_AffineSpace) (u : sub_ModuleSpace HPV) : sub_AffineSpace :=
mk_sub (sub_transl_aux (in_sub A) (in_sub u)).
Lemma val_vect : f_vect_compat_gen val val.
Proof. easy. Qed.
Lemma val_vectF : f_vectF_compat_gen val val.
Proof. easy. Qed.
Lemma val_transl : f_transl_compat_gen val val.
Proof.
intros A u; pose (B := A +++ u).
assert (HB : u = A --> B) by now unfold B; rewrite transl_correct_r.
rewrite HB val_vect 2!transl_correct_l; easy.
Qed.
Lemma val_translF : f_translF_compat_gen val val.
Proof. move=>>; apply extF; intro; apply val_transl. Qed.
Lemma val_baryc :
∀ {n} L (A : 'sub_AffineSpace^n),
invertible (sum L) → val (barycenter L A) = barycenter L (mapF val A).
Proof.
intros n L A HL; apply baryc_correct_equiv; [easy |].
unfold aff_comb; rewrite -val_vectF -val_lc baryc_correct; easy.
Qed.
Lemma val_am : aff_map val.
Proof. intro; apply val_baryc. Qed.
Lemma mk_sub_vect :
∀ {A B : E} (HA : PE A) (HB : PE B),
mk_sub HA --> mk_sub HB = mk_sub (sub_vect_aux HA HB).
Proof. easy. Qed.
Lemma mk_sub_vectF :
∀ {n} {O} {A : 'E^n} (HO : PE O) (HA : inclF A PE),
vectF (mk_sub HO) (fun i ⇒ mk_sub (HA i)) =
fun i ⇒ mk_sub (sub_vect_aux HO (HA i)).
Proof. easy. Qed.
Lemma mk_sub_transl :
∀ {A u} (HA : PE A) (Hu : PV u),
mk_sub HA +++ mk_sub Hu = mk_sub (sub_transl_aux HA Hu).
Proof. intros; apply val_inj, val_transl. Qed.
Lemma mk_sub_translF :
∀ {n} {A} {u : 'V^n} (HA : PE A) (Hu : inclF u PV),
translF (mk_sub HA) (fun i ⇒ mk_sub (Hu i)) =
fun i ⇒ mk_sub (sub_transl_aux HA (Hu i)).
Proof. intros; apply extF; intro; apply mk_sub_transl. Qed.
Lemma mk_sub_baryc :
∀ {n} {L} {A : 'E^n} (HL : invertible (sum L)) (HA : inclF A PE),
barycenter L (fun i ⇒ mk_sub (HA i)) = mk_sub (HPE _ _ _ HL HA).
Proof. intros; apply val_inj, val_baryc; easy. Qed.
Lemma sub_vect_eq :
∀ (A B : sub_AffineSpace),
A --> B = mk_sub (sub_vect_aux (in_sub A) (in_sub B)).
Proof. easy. Qed.
Lemma sub_vectF_eq :
∀ {n} O (A : 'sub_AffineSpace^n),
vectF O A = fun i ⇒ mk_sub (sub_vect_aux (in_sub O) (in_sub (A i))).
Proof. easy. Qed.
Lemma sub_transl_eq :
∀ (A : sub_AffineSpace) (u : sub_ModuleSpace HPV),
A +++ u = mk_sub (sub_transl_aux (in_sub A) (in_sub u)).
Proof. intros; apply val_inj, val_transl. Qed.
Lemma sub_translF_eq :
∀ {n} (A : sub_AffineSpace) (u : '(sub_ModuleSpace HPV)^n),
translF A u = fun i ⇒ mk_sub (sub_transl_aux (in_sub A) (in_sub (u i))).
Proof. intros; apply extF; intro; apply sub_transl_eq. Qed.
Lemma sub_baryc_eq :
∀ {n} {L} {A : 'sub_AffineSpace^n} (HL : invertible (sum L)),
barycenter L A = mk_sub (HPE _ _ _ HL (fun i ⇒ in_sub (A i))).
Proof. intros; apply val_inj, val_baryc; easy. Qed.
End Sub_AffineSpace_Def.
Section Sub_AffineSpace_Facts1.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PEa PEb : E → Prop}.
Hypothesis HPE : incl PEa PEb.
Hypothesis HPEb : compatible_as PEb.
Context {O : E}.
Hypothesis HO : PEb O.
Let PEb_as := sub_AffineSpace HK HPEb HO.
Let PEa' : PEb_as → Prop := preimage val PEa.
Lemma RgS_val_as_eq : RgS PEa' val = PEa.
Proof. apply RgS_val_eq; easy. Qed.
Lemma preimage_val_cas : compatible_as PEa → compatible_as PEa'.
Proof. intros; apply cas_preimage; [apply val_am | easy]. Qed.
Lemma preimage_val_cas_rev : compatible_as PEa' → compatible_as PEa.
Proof.
intros; rewrite -RgS_val_as_eq; apply RgS_cas; [easy | apply val_am].
Qed.
Lemma preimage_val_cas_equiv : compatible_as PEa' ↔ compatible_as PEa.
Proof. split; [apply preimage_val_cas_rev | apply preimage_val_cas]. Qed.
End Sub_AffineSpace_Facts1.
Section Sub_AffineSpace_Facts2.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PEb : E → Prop}.
Hypothesis HPEb : compatible_as PEb.
Context {O : E}.
Hypothesis HO : PEb O.
Let PEb_as := sub_AffineSpace HK HPEb HO.
Context {PEa : PEb_as → Prop}.
Let PEa' := RgS PEa val.
Lemma preimage_val_as_eq : preimage val PEa' = PEa.
Proof. apply preimage_val_eq. Qed.
Lemma RgS_val_cas : compatible_as PEa → compatible_as PEa'.
Proof. intros; apply RgS_cas; [easy | apply val_am]. Qed.
Lemma RgS_val_cas_rev : compatible_as PEa' → compatible_as PEa.
Proof.
intros; rewrite -preimage_val_as_eq; apply cas_preimage; [apply val_am | easy].
Qed.
Lemma RgS_val_cas_equiv : compatible_as PEa' ↔ compatible_as PEa.
Proof. split; [apply RgS_val_cas_rev | apply RgS_val_cas]. Qed.
End Sub_AffineSpace_Facts2.
Section Sub_AffineSpace_Affine_Mapping_Facts1.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Context {HPE1 : compatible_as PE1}.
Context {HPE2 : compatible_as PE2}.
Context {O1 : E1}.
Context {O2 : E2}.
Context {HO1 : PE1 O1}.
Context {HO2 : PE2 O2}.
Let PE1_as := sub_AffineSpace HK HPE1 HO1.
Let PE2_as := sub_AffineSpace HK HPE2 HO2.
Context {f : E1 → E2}.
Context {fS : PE1_as → PE2_as}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_as_am : aff_map f → aff_map fS.
Proof.
intros Hf n; intros; apply val_inj; rewrite HfS !val_baryc// Hf//.
f_equal; apply extF; intro; rewrite !mapF_correct; easy.
Qed.
End Sub_AffineSpace_Affine_Mapping_Facts1.
Section Sub_AffineSpace_Affine_Mapping_Facts2.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Hypothesis HPE1 : compatible_as PE1.
Hypothesis HPE2 : compatible_as PE2.
Context {O1 : E1}.
Context {O2 : E2}.
Hypothesis HO1 : PE1 O1.
Hypothesis HO2 : PE2 O2.
Let PE1_as := sub_AffineSpace HK HPE1 HO1.
Let PE2_as := sub_AffineSpace HK HPE2 HO2.
Context {f : E1 → E2}.
Hypothesis Hf : funS PE1 PE2 f.
Definition fct_sub_as : PE1_as → PE2_as := fct_sub Hf.
Lemma fct_sub_as_inj : injS PE1 f → injective fct_sub_as.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_as_inj_rev : injective fct_sub_as → injS PE1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_as_inj_equiv : injective fct_sub_as ↔ injS PE1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_as_surj : surjS PE1 PE2 f → surjective fct_sub_as.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_as_surj_rev : surjective fct_sub_as → surjS PE1 PE2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_as_surj_equiv : surjective fct_sub_as ↔ surjS PE1 PE2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_as_bij : bijS PE1 PE2 f → bijective fct_sub_as.
Proof. apply fct_sub_bij, inhabited_as. Qed.
Lemma fct_sub_as_bij_rev : bijective fct_sub_as → bijS PE1 PE2 f.
Proof. apply fct_sub_bij_rev, inhabited_as. Qed.
Lemma fct_sub_as_bij_equiv : bijective fct_sub_as ↔ bijS PE1 PE2 f.
Proof. apply fct_sub_bij_equiv, inhabited_as. Qed.
Lemma fct_sub_as_am : aff_map f → aff_map fct_sub_as.
Proof. apply sub_as_am, fct_sub_correct. Qed.
Lemma fct_sub_as_f_inv_am :
∀ (Hfb : bijS PE1 PE2 f),
aff_map f → aff_map (f_inv (fct_sub_as_bij Hfb)).
Proof. intros; apply am_bij_compat, fct_sub_as_am; easy. Qed.
End Sub_AffineSpace_Affine_Mapping_Facts2.
Section Sub_AffineSpace_Affine_Mapping_Facts3.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V W : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.
Context {PE : E → Prop}.
Context {PF : F → Prop}.
Hypothesis HPE : compatible_as PE.
Hypothesis HPF : compatible_as PF.
Context {f : E → F}.
Hypothesis Hf : aff_map f.
Variable O : E.
Hypothesis HO : PE O.
Let lf := fct_lm f O.
Let PV := vectP PE O.
Let PW := vectP PF (f O).
Lemma funS_aff_lin_equiv : funS PE PF f ↔ funS PV PW lf.
Proof.
rewrite !funS_equiv; split.
intros Hf1 v Hv; unfold PW, vectP, preimage, lf;
rewrite transl_correct_l; auto.
intros Hlf A HA;
rewrite -(transl_correct_l (f O) (f A)) -(transl_correct_l O A).
apply Hlf; unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
Qed.
Lemma injS_aff_lin_equiv : injS PE f ↔ injS PV lf.
Proof.
split.
intros Hf1 u1 u2 Hu1 Hu2 Hu; apply (transl_l_inj O), Hf1; auto.
apply (vect_l_inj (f O)); auto.
intros Hlf1 A1 A2 HA1 HA2 HA; apply (vect_l_inj O), Hlf1.
1,2: unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
unfold lf, fct_lm; rewrite !transl_correct_l HA; easy.
Qed.
Lemma injS_aff_lin_equiv_alt : injS PE f ↔ incl (KerS PV lf) zero_sub_struct.
Proof.
rewrite injS_aff_lin_equiv -KerS_zero_equiv.
rewrite -lmS_injS_equiv; [easy |..].
1,3: apply cas_cms; easy.
1,2: apply am_lm_equiv; easy.
Qed.
Lemma surjS_gen_aff_lin_equiv : surjS PE PF f ↔ surjS PV PW lf.
Proof.
split.
intros Hf1 w Hw; destruct (Hf1 (f O +++ w)) as [A [HA1 HA2]]; try easy.
∃ (O --> A); split.
unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
unfold lf, fct_lm; rewrite transl_correct_l HA2 transl_correct_r; easy.
intros Hlf B HB; destruct (Hlf (f O --> B)) as [v [Hv1 Hv2]].
unfold PW, vectP, preimage; rewrite transl_correct_l; easy.
∃ (O +++ v); split; try apply (vect_l_inj (f O)); easy.
Qed.
Lemma surjS_gen_aff_lin_equiv_alt : surjS PE PF f ↔ incl PW (RgS PV lf).
Proof.
rewrite surjS_gen_aff_lin_equiv -RgS_gen_full_equiv; apply surjS_RgS_gen_equiv.
Qed.
Lemma bijS_gen_aff_lin_equiv : bijS PE PF f ↔ bijS PV PW lf.
Proof.
rewrite !bijS_equiv; [| apply inhabited_ms | easy].
rewrite funS_aff_lin_equiv injS_aff_lin_equiv surjS_gen_aff_lin_equiv; easy.
Qed.
Lemma bijS_gen_aff_lin_equiv_alt :
bijS PE PF f ↔
funS PV PW lf ∧ incl (KerS PV lf) zero_sub_struct ∧ incl PW (RgS PV lf).
Proof.
rewrite bijS_equiv; [| apply inhabited_as].
rewrite funS_aff_lin_equiv injS_aff_lin_equiv_alt surjS_gen_aff_lin_equiv_alt//.
Qed.
End Sub_AffineSpace_Affine_Mapping_Facts3.
Section Sub_AffineSpace_Affine_Mapping_Facts4.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V W : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_as PE.
Context {f : E → F}.
Hypothesis Hf : aff_map f.
Variable O : E.
Hypothesis HO : PE O.
Let lf := fct_lm f O.
Let PV := vectP PE O.
Lemma surjS_aff_lin_equiv : surjS PE fullset f ↔ surjS PV fullset lf.
Proof. rewrite (surjS_gen_aff_lin_equiv O) vectP_fullset; easy. Qed.
Lemma surjS_aff_lin_equiv_alt :
surjS PE fullset f ↔ incl fullset (RgS PV lf).
Proof. rewrite (surjS_gen_aff_lin_equiv_alt O) vectP_fullset; easy. Qed.
Lemma bijS_aff_lin_equiv : bijS PE fullset f ↔ bijS PV fullset lf.
Proof. rewrite (bijS_gen_aff_lin_equiv O) vectP_fullset; easy. Qed.
Lemma bijS_aff_lin_equiv_alt :
bijS PE fullset f ↔
incl (KerS PV lf) zero_sub_struct ∧ incl fullset (RgS PV lf).
Proof.
rewrite (bijS_gen_aff_lin_equiv_alt HK HPE Hf O)// vectP_fullset; easy.
Qed.
End Sub_AffineSpace_Affine_Mapping_Facts4.
Section Compatible_AffineSpace_R_Facts.
Context {V : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.
Context {PE : E → Prop}.
Context {O : E}.
Hypothesis HO : PE O.
Lemma cas_cms_equiv_R : compatible_as PE ↔ compatible_ms (vectP PE O).
Proof.
apply cas_cms_equiv; [easy | apply nonzero_struct_R | apply invertible_2].
Qed.
Variable gen : E → Prop.
Lemma cas_baryc_closure_R : compatible_as (baryc_closure gen).
Proof.
intros n L A HL HA; destruct (baryc_normalized_n0_ex _ A HL)
as [n1 [L1 [A1 [HL1a [HL1b [HA1a HA1b]]]]]]; rewrite HA1b.
destruct (baryc_closure_exs _ (inclF_monot_l _ _ _ HA1a HA))
as [b [M [B [HM1 [HM2 [HB HA']]]]]].
assert (HL1' : L1 = fun i1 ⇒ sum (scal (L1 i1) (M i1))).
apply extF; intro; rewrite -scal_sum_distr_l HM1 scal_one_r; easy.
rewrite (baryc_eq_r (fun i1 ⇒ barycenter (scal (L1 i1) (M i1)) (B i1))).
2: { rewrite HA'; apply extF; intro; apply baryc_homogeneous.
apply invertible_equiv_R; easy.
rewrite HM1; apply invertible_one. }
rewrite {1}HL1' -baryc_assoc.
apply Barycenter_closure.
1,4: rewrite sum_assoc -HL1' HL1a; apply invertible_one.
apply concatnF_inclF_equiv; easy.
intros i; rewrite -(extF_rev _ _ HL1' i).
apply invertible_equiv_R; easy.
Qed.
Lemma baryc_closure_idem_R :
baryc_closure (baryc_closure gen) = baryc_closure gen.
Proof. apply eq_sym, cas_equiv, cas_baryc_closure_R. Qed.
∀ n L (A : 'E^n),
invertible (sum L) → inclF A PE → PE (barycenter L A).
Definition span_as (gen : E → Prop) : E → Prop :=
span compatible_as gen.
Inductive baryc_closure (gen : E → Prop) : E → Prop :=
| Barycenter_closure :
∀ n L (B : 'E^n),
invertible (sum L) → inclF B gen →
baryc_closure gen (barycenter L B).
End Compatible_AffineSpace_Def.
Section Compatible_AffineSpace_Facts.
Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Lemma vectP_correct :
∀ {PE : E → Prop} {O}, PE O → PE = image (transl O) (vectP PE O).
Proof. intros; rewrite image_of_preimage transl_l_fullset inter_full_r //. Qed.
Lemma vectP_eq : ∀ {PE : E → Prop} {O}, vectP PE O = image (vect O) PE.
Proof.
intros; apply preimage_eq; [apply transl_correct_r | apply transl_correct_l].
Qed.
Lemma vectP_inj :
∀ {PE QE : E → Prop} O, vectP PE O = vectP QE O → PE = QE.
Proof. move=>>; eapply preimage_inj, transl_correct_l. Qed.
Lemma vectP_full :
∀ {PE : E → Prop} O, full PE → full (vectP PE O).
Proof. intros; apply preimage_full_equiv; easy. Qed.
Lemma vectP_fullset : ∀ (O : E), vectP fullset O = fullset.
Proof. easy. Qed.
Lemma vectP_inter :
∀ {PE1 PE2 : E → Prop} {O},
vectP (inter PE1 PE2) O = inter (vectP PE1 O) (vectP PE2 O).
Proof. easy. Qed.
Lemma vectP_inter_any :
∀ {Idx : Type} {PE : Idx → E → Prop} {O},
vectP (inter_any PE) O = inter_any (fun idx ⇒ vectP (PE idx) O).
Proof. easy. Qed.
Lemma vectP_zero_closed_equiv :
∀ {PE : E → Prop} {O}, zero_closed (vectP PE O) ↔ PE O.
Proof. intros PE O; rewrite -{2}(transl_zero O); easy. Qed.
Lemma translP_correct :
∀ {PV : V → Prop} (O : E), PV = image (vect O) (translP PV O).
Proof. intros; rewrite image_of_preimage vect_l_fullset inter_full_r //. Qed.
Lemma translP_eq :
∀ {PV : V → Prop} {O : E}, translP PV O = image (transl O) PV.
Proof.
intros; apply preimage_eq; [apply transl_correct_l | apply transl_correct_r].
Qed.
Lemma translP_inj :
∀ {PV QV : V → Prop} (O : E), translP PV O = translP QV O → PV = QV.
Proof. move=>>; eapply preimage_inj, transl_correct_r. Qed.
Lemma translP_full :
∀ {PV : V → Prop} (O : E), full PV → full (translP PV O).
Proof. intros; apply preimage_full_equiv; easy. Qed.
Lemma translP_fullset : ∀ (O : E), translP fullset O = fullset.
Proof. easy. Qed.
Lemma translP_inter :
∀ {PV1 PV2 : V → Prop} {O : E},
translP (inter PV1 PV2) O = inter (translP PV1 O) (translP PV2 O).
Proof. easy. Qed.
Lemma translP_inter_any :
∀ {Idx : Type} {PV : Idx → V → Prop} {O : E},
translP (inter_any PV) O = inter_any (fun idx ⇒ translP (PV idx) O).
Proof. easy. Qed.
Lemma translP_zero_closed_equiv :
∀ {PV : V → Prop} (O : E), zero_closed PV ↔ translP PV O O.
Proof. intros; unfold translP, preimage; rewrite vect_zero; easy. Qed.
Lemma vectP_translP :
∀ (PV : V → Prop) (O : E), vectP (translP PV O) O = PV.
Proof. intros; apply preimage_can, transl_correct_r. Qed.
Lemma translP_vectP :
∀ {PE : E → Prop} O, translP (vectP PE O) O = PE.
Proof. intros; apply preimage_can, transl_correct_l. Qed.
Lemma vect_transl_closed_gen_equiv :
∀ {PE : E → Prop} {PV},
vect_closed_gen PE PV ↔ transl_closed_gen PE PV.
Proof.
intros; split; intros HPE A; unfold vectP, translP, preimage.
intros u HA; rewrite -{1}(transl_correct_r A u) (HPE A); easy.
intros B HA; rewrite -{1}(transl_correct_l A B) (HPE A); easy.
Qed.
Lemma vect_transl_closed_equiv :
∀ {PE : E → Prop} {O}, vect_closed PE O ↔ transl_closed PE O.
Proof. intros; apply vect_transl_closed_gen_equiv. Qed.
Lemma transl_plus_closed :
∀ {PE : E → Prop} {O}, transl_closed PE O → plus_closed (vectP PE O).
Proof.
move=>> HPE u v; unfold vectP, preimage; rewrite -transl_assoc; apply HPE; easy.
Qed.
Lemma vect_plus_closed :
∀ {PE : E → Prop} {O}, vect_closed PE O → plus_closed (vectP PE O).
Proof. move=>> /vect_transl_closed_equiv; apply transl_plus_closed. Qed.
Lemma cms_transl :
∀ {PE : E → Prop} {O}, PE O →
compatible_ms (vectP PE O) → transl_closed PE O.
Proof.
unfold vectP; intros PE O HO HPE A u; unfold vectP, preimage.
rewrite -(transl_correct_l O A) transl_assoc iff_sym_equiv.
apply (cms_plus_equiv HPE).
Qed.
Lemma cms_vect :
∀ {PE : E → Prop} {O}, PE O →
compatible_ms (vectP PE O) → vect_closed PE O.
Proof.
unfold vect_closed.
move=>>; rewrite vect_transl_closed_gen_equiv; apply cms_transl.
Qed.
Lemma vectP_orig_indep :
∀ {PE : E → Prop} {O} (O' : E), PE O →
compatible_ms (vectP PE O') → vectP PE O = vectP PE O'.
Proof.
intros; apply subset_ext; intros u.
apply iff_sym, cms_transl; try easy.
apply vectP_zero_closed_equiv, cms_zero; easy.
Qed.
Lemma translP_orig_indep :
∀ {PV : V → Prop} {O} (O' : E), translP PV O O' →
compatible_ms PV → translP PV O = translP PV O'.
Proof.
intros PV O O' HO' HPV; apply subset_ext; intros A.
rewrite -{2}(vectP_translP PV O); apply cms_vect; try easy.
apply translP_zero_closed_equiv, cms_zero; easy.
rewrite vectP_translP; easy.
Qed.
Lemma vect_closed_orig_indep :
∀ {PE : E → Prop} O O',
PE O → compatible_ms (vectP PE O') →
vect_closed PE O → vect_closed PE O'.
Proof.
move=>> HO HPV HPE; move=>>; rewrite -(vectP_orig_indep _ HO); auto.
Qed.
Lemma transl_closed_orig_indep :
∀ {PE : E → Prop} O O',
PE O → compatible_ms (vectP PE O') →
transl_closed PE O → transl_closed PE O'.
Proof.
move=>> HO HPV HPE; move=>>; rewrite -(vectP_orig_indep _ HO); auto.
Qed.
Lemma transl_closed_gen_sms_uniq :
∀ {PE : E → Prop} {PV} {O : E},
PE O → compatible_ms PV → transl_closed_gen PE PV → PV = vectP PE O.
Proof.
move=>> HO HPV HPE; apply subset_ext_equiv; split; intro;
[apply HPE | apply (HPE _ _ HO)]; easy.
Qed.
Lemma vect_closed_gen_sms_uniq :
∀ {PE : E → Prop} {PV} {O : E},
PE O → compatible_ms PV → vect_closed_gen PE PV → PV = vectP PE O.
Proof.
move=>>; rewrite vect_transl_closed_gen_equiv; apply transl_closed_gen_sms_uniq.
Qed.
Lemma cas_empty :
∀ {PE : E → Prop}, nonzero_struct K → empty PE → compatible_as PE.
Proof.
intros PE HK HPE n L A HL HA; destruct n.
contradict HL; apply sum_nil_noninvertible; easy.
contradict HA; rewrite not_all_ex_not_equiv; ∃ ord0.
intros HA0; apply (HPE _ HA0).
Qed.
Lemma cas_emptyset :
∀ {PE : E → Prop}, nonzero_struct K → compatible_as (@emptyset E).
Proof. intros; apply cas_empty; easy. Qed.
Lemma cas_singleton : ∀ (O : E), compatible_as (singleton O).
Proof. move=>> HL /extF ->; apply baryc_constF; easy. Qed.
Lemma cas_unit :
∀ {PE : E → Prop},
nonzero_struct K → is_unit_type E → compatible_as PE.
Proof.
intros PE HK [O HE].
destruct (empty_dec PE) as [HPE | HPE].
apply cas_empty; easy.
rewrite (unit_subset_is_singleton PE HE HPE).
apply cas_singleton.
Qed.
Lemma cas_full : ∀ {PE : E → Prop}, full PE → compatible_as PE.
Proof. easy. Qed.
Lemma cas_fullset : compatible_as (@fullset E).
Proof. easy. Qed.
Lemma cms_cas :
∀ {PE : E → Prop} {O},
PE O → nonzero_struct K → invertible (2 : K) →
compatible_ms (vectP PE O) → compatible_as PE.
Proof.
move=>> HO HK1 HK2 HPE n L A HL HA.
destruct n. contradict HL; apply sum_nil_noninvertible; easy.
generalize (cms_vect HO HPE (A ord0)); intros HPE'.
unfold translP, vectP, preimage in HPE'.
apply HPE', (cms_scal_rev HPE (sum L) _ HL); try easy.
rewrite baryc_correct_orig; try easy.
apply cms_lc; try easy.
unfold vectP, preimage; intro; rewrite vectF_correct -HPE'; easy.
Qed.
Lemma cas_scal :
∀ {PE : E → Prop} {O},
PE O → compatible_as PE → scal_closed (vectP PE O).
Proof.
intros PE O HO HPE a u Hu; unfold vectP, preimage in ×.
assert (H0 : invertible (sum (coupleF (1 - a) a))).
rewrite sum_coupleF -plus_assoc plus_opp_l plus_zero_r.
apply invertible_one.
assert (H : O +++ scal a u =
barycenter (coupleF (1 - a) a) (coupleF O (O +++ u))).
apply baryc_coupleF_equiv; try easy.
rewrite -{2}(transl_zero O) 2!vect_transl.
rewrite 2!scal_minus_distr_l scal_zero_r scal_minus_distr_r scal_one.
rewrite minus_zero_l plus_opp_l; easy.
unfold vectP; rewrite H; apply HPE; try easy.
intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi;
[rewrite coupleF_0 | rewrite coupleF_1]; easy.
Qed.
Lemma cas_scal_rev :
∀ {PE : E → Prop} {O},
PE O → compatible_as PE → scal_rev_closed (vectP PE O).
Proof. intros; apply scal_scal_rev_closed, cas_scal; easy. Qed.
Lemma cas_plus :
∀ {PE : E → Prop} {O},
PE O → invertible (2 : K) →
compatible_as PE → plus_closed (vectP PE O).
Proof.
intros PE O HO HK HPE; unfold vectP, preimage.
unfold two in HK; rewrite -(sum_2 ones) in HK.
intros u v Hu Hv; pose (A := coupleF (O +++ u) (O +++ v)).
rewrite (transl_l_eq _ _ (sum (vectF O A))).
rewrite -lc_ones_l -baryc_correct_orig; try easy.
apply (cas_scal_rev HO HPE (inv (@sum _ 2 ones)));
try now apply inv_invertible. unfold vectP, preimage.
rewrite → scal_assoc, mult_inv_l, scal_one, transl_correct_l; try easy.
apply HPE; try easy; unfold A;
intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi;
[rewrite coupleF_0 | rewrite coupleF_1]; easy.
unfold A; rewrite vectF_coupleF sum_2 coupleF_0 coupleF_1 !transl_correct_r //.
Qed.
Lemma cas_cms :
∀ {PE : E → Prop} {O},
PE O → invertible (2 : K) →
compatible_as PE → compatible_ms (vectP PE O).
Proof.
intros; apply plus_scal_closed_cms.
unfold vectP, preimage; ∃ 0; rewrite transl_zero; easy.
apply cas_plus; easy.
apply cas_scal; easy.
Qed.
Lemma cas_cms_equiv :
∀ {PE : E → Prop} {O},
PE O → nonzero_struct K → invertible (2 : K) →
compatible_as PE ↔ compatible_ms (vectP PE O).
Proof. intros; split; [apply cas_cms | apply cms_cas]; easy. Qed.
Lemma cas_sms_orig_indep :
∀ {PE : E → Prop} {O O'},
PE O → PE O' → invertible (2 : K) →
compatible_as PE → vectP PE O = vectP PE O'.
Proof. intros; apply vectP_orig_indep; try apply cas_cms; easy. Qed.
Lemma cas_vect :
∀ {PE : E → Prop} {O},
PE O → invertible (2 : K) →
compatible_as PE → vect_closed PE O.
Proof. intros; apply cms_vect, cas_cms; easy. Qed.
Lemma cas_transl :
∀ {PE : E → Prop} {O},
PE O → invertible (2 : K) →
compatible_as PE → transl_closed PE O.
Proof.
intros; apply vect_transl_closed_gen_equiv, cas_vect; easy.
Qed.
Lemma cas_inter :
∀ {PE1 PE2 : E → Prop},
compatible_as PE1 → compatible_as PE2 → compatible_as (inter PE1 PE2).
Proof.
move=>> HPE1 HPE2; move=>> HL HA; split; [apply HPE1 | apply HPE2];
try easy; intro; apply HA.
Qed.
Lemma cas_inter_any :
∀ {Idx : Type} {PE : Idx → E → Prop},
(∀ idx, compatible_as (PE idx)) →
compatible_as (inter_any PE).
Proof.
move=>> HPE; move=>> HL HA idx; apply HPE; try easy; intro; apply HA.
Qed.
Lemma span_as_cas : ∀ (gen : E → Prop), compatible_as (span_as gen).
Proof. apply span_compatible; move=>>; apply cas_inter_any. Qed.
Lemma span_as_incl : ∀ (gen : E → Prop), incl gen (span_as gen).
Proof. apply span_incl. Qed.
Lemma span_as_lub :
∀ gen {PE : E → Prop},
compatible_as PE → incl gen PE → incl (span_as gen) PE.
Proof. apply span_lub. Qed.
Lemma span_as_full :
∀ {PE : E → Prop}, compatible_as PE → span_as PE = PE.
Proof. apply span_full. Qed.
Lemma baryc_closure_ex :
∀ (gen : E → Prop) A,
(∃ n L (B : 'E^n),
invertible (sum L) ∧ inclF B gen ∧ A = barycenter L B) →
baryc_closure gen A.
Proof.
move=>> [n [L [B [HL [HB HA]]]]]; rewrite HA; apply Barycenter_closure; easy.
Qed.
Lemma baryc_closure_ex_rev :
∀ (gen : E → Prop) A,
baryc_closure gen A →
∃ n L (B : 'E^n),
sum L = 1 ∧ (∀ i, L i ≠ 0) ∧ inclF B gen ∧ A = barycenter L B.
Proof.
intros gen A HA; induction HA as [n L B HL HB].
destruct (baryc_normalized_n0_ex L B HL)
as [n1 [L1 [A1 [HL1a [HL1b [HA1a HA1b]]]]]].
∃ n1, L1, A1; repeat split; try easy.
apply (inclF_monot_l _ B); easy.
Qed.
Lemma bc_len_EX :
∀ (gen : E → Prop) A,
{ n | baryc_closure gen A →
∃ L (B : 'E^n),
sum L = 1 ∧ (∀ i, L i ≠ 0) ∧
inclF B gen ∧ A = barycenter L B }.
Proof.
intros gen A; apply ex_EX.
destruct (classic_dec (baryc_closure gen A)) as [HA | HA].
destruct (baryc_closure_ex_rev _ _ HA) as [n [L [B HLB]]].
∃ n; intros _; ∃ L, B; easy.
∃ 0; intros HA'; easy.
Qed.
Definition bc_len (gen : E → Prop) A := proj1_sig (bc_len_EX gen A).
Lemma bc_EX :
∀ (gen : E → Prop) A,
{ LB : 'K^(bc_len gen A) × 'E^(bc_len gen A) |
baryc_closure gen A →
sum LB.1 = 1 ∧ (∀ i, LB.1 i ≠ 0) ∧
inclF LB.2 gen ∧ A = barycenter LB.1 LB.2 }.
Proof.
intros gen A; apply ex_EX.
destruct (classic_dec (baryc_closure gen A)) as [HA | HA].
destruct (proj2_sig (bc_len_EX gen A)) as [L [B HLB]]; try easy.
∃ (L, B); intros _; easy.
destruct (inhabited_as E) as [O].
∃ ((fun _ ⇒ 0), (fun _ ⇒ O)); intros HA'; easy.
Qed.
Definition bc_coef (gen : E → Prop) A := fst (proj1_sig (bc_EX gen A)).
Definition bc_point (gen : E → Prop) A := snd (proj1_sig (bc_EX gen A)).
Lemma bc_nLB_correct :
∀ (gen : E → Prop) A,
baryc_closure gen A →
sum (bc_coef gen A) = 1 ∧
(∀ i, bc_coef gen A i ≠ 0) ∧
inclF (bc_point gen A) gen ∧
A = barycenter (bc_coef gen A) (bc_point gen A).
Proof. intros gen A HA; destruct (proj2_sig (bc_EX gen A)); easy. Qed.
Lemma baryc_closure_exs :
∀ {gen : E → Prop} {n} (A : 'E^n),
inclF A (baryc_closure gen) →
∃ (b : 'nat^n) L (B : ∀ i, 'E^(b i)),
(∀ i, sum (L i) = 1) ∧ (∀ i j, L i j ≠ 0) ∧
(∀ i, inclF (B i) gen) ∧ A = fun i ⇒ barycenter (L i) (B i).
Proof.
intros gen n A HA; destruct n.
destruct (inhabited_as E) as [O]; ∃ 0, (fun _ ⇒ 0), (fun _ _ ⇒ O).
repeat split; try apply extF; intros [i Hi]; easy.
∃ (fun i ⇒ bc_len gen (A i)), (fun i ⇒ bc_coef gen (A i)),
(fun i ⇒ bc_point gen (A i)).
repeat split; try apply extF; intro; apply bc_nLB_correct; easy.
Qed.
Lemma cas_equiv :
∀ (PE : E → Prop), compatible_as PE ↔ PE = baryc_closure PE.
Proof.
intros PE; split; intros HPE.
apply subset_ext_equiv; split; intros A HA; try induction HA; auto.
rewrite -(baryc_singleF 1 A (singleF 1) (singleF A)); try easy.
apply Barycenter_closure; try easy.
apply sum_singleF_invertible.
1,2: apply invertible_one.
move=>> HL HB; rewrite HPE; apply Barycenter_closure; easy.
Qed.
Lemma baryc_closure_incl :
∀ (gen : E → Prop), incl gen (baryc_closure gen).
Proof.
intros gen A HA.
rewrite -(baryc_singleF 1 A (singleF 1) (singleF A));
try apply invertible_one; try easy.
apply Barycenter_closure; try easy.
rewrite sum_1 singleF_0; apply invertible_one.
Qed.
End Compatible_AffineSpace_Facts.
Section Compatible_AffineSpace_Affine_Mapping_Facts1.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Context {f : E1 → E2}.
Hypothesis Hf : aff_map f.
Lemma cas_image : compatible_as PE1 → compatible_as (image f PE1).
Proof.
intro; move=>> HL /inclF_image_equiv [A [HA1 HA2]].
rewrite HA2 -Hf; try easy; apply Im; auto.
Qed.
Lemma cas_preimage : compatible_as PE2 → compatible_as (preimage f PE2).
Proof. intro; move=>> Hl HA; unfold preimage; rewrite Hf; auto. Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts1.
Section Compatible_AffineSpace_Affine_Mapping_Def.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Variable PE1 : E1 → Prop.
Variable f : E1 → E2.
Definition am_sub : Prop :=
∀ n L (A1 : 'E1^n),
inclF A1 PE1 →
invertible (sum L) → f (barycenter L A1) = barycenter L (mapF f A1).
End Compatible_AffineSpace_Affine_Mapping_Def.
Section Compatible_AffineSpace_Affine_Mapping_Facts2a.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 → Prop}.
Hypothesis HPE1 : compatible_as PE1.
Context {PE2 : E2 → Prop}.
Hypothesis HPE2 : compatible_as PE2.
Context {f : E1 → E2}.
Hypothesis Hf : aff_map f.
Lemma RgS_gen_cas : compatible_as (RgS_gen PE1 PE2 f).
Proof. apply cas_inter, cas_image; easy. Qed.
Lemma RgS_cas : compatible_as (RgS PE1 f).
Proof. apply cas_image; easy. Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts2a.
Section Compatible_AffineSpace_Affine_Mapping_Facts2b.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {f : E1 → E2}.
Hypothesis Hf : aff_map f.
Lemma Rg_cas : compatible_as (Rg f).
Proof. rewrite -RgS_full; apply (RgS_cas cas_fullset Hf). Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts2b.
Section Compatible_AffineSpace_Affine_Mapping_Facts4a.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Variable PE1 : E1 → Prop.
Lemma am_sub_id : am_sub PE1 ssrfun.id.
Proof. easy. Qed.
Context {f : E1 → E2}.
Lemma am_is_sub : aff_map f → am_sub PE1 f.
Proof. intros Hf n L A1 _; apply Hf. Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts4a.
Section Compatible_AffineSpace_Affine_Mapping_Facts4b.
Context {K : Ring}.
Context {V1 V2 V3 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {E3 : AffineSpace V3}.
Context {PE1 : E1 → Prop}.
Variable PE2 : E2 → Prop.
Context {f : E1 → E2}.
Hypothesis Hf : funS PE1 PE2 f.
Variable g : E2 → E3.
Lemma am_comp_sub : am_sub PE1 f → am_sub PE2 g → am_sub PE1 (g \o f).
Proof.
intros Hfa Hga n L A1 HA1 HL; unfold ssrfun.comp; rewrite Hfa// Hga//.
apply (inclF_monot_r (RgS PE1 f)); [easy |].
apply mapF_inclF; easy.
Qed.
End Compatible_AffineSpace_Affine_Mapping_Facts4b.
Section Sub_AffineSpace_Def.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_as PE.
Context {O : E}.
Hypothesis HO : PE O.
Definition sub_point_of_as : sub PE := mk_sub HO.
Let PV := vectP PE O.
Let HPV : compatible_ms PV := cas_cms HO HK HPE.
Lemma sub_vect_aux : ∀ {A B}, PE A → PE B → PV (A --> B).
Proof. move=>>; apply cas_vect; easy. Qed.
Lemma sub_vectF_aux :
∀ {n} {A} {B : 'E^n}, PE A → inclF B PE → inclF (vectF A B) PV.
Proof. intros; intro; apply sub_vect_aux; easy. Qed.
Definition sub_vect (A B : sub PE) : sub_ModuleSpace HPV :=
mk_sub (sub_vect_aux (in_sub A) (in_sub B)).
Lemma sub_vect_chasles :
∀ A B C, sub_vect B A + sub_vect A C = sub_vect B C.
Proof. intros; apply val_inj, vect_chasles. Qed.
Lemma sub_vect_l_bij_ex : ∀ A u, ∃! B, sub_vect A B = u.
Proof.
intros [A HA] [u Hu]; unfold PV in Hu.
assert (Hu' : vectP PE A u) by now rewrite -(cas_transl HO).
∃ (mk_sub_ PE (A +++ u) Hu'); split.
apply val_inj, transl_correct_r.
move⇒ [B HB1] /(f_equal val) /= HB2.
apply val_inj; simpl; rewrite -HB2; apply transl_correct_l.
Qed.
Definition sub_AffineSpace_mixin :=
AffineSpace.Mixin _ _ _ sub_point_of_as _ sub_vect_chasles sub_vect_l_bij_ex.
Canonical Structure sub_AffineSpace :=
AffineSpace.Pack _ _ sub_AffineSpace_mixin (sub PE).
Lemma sub_transl_aux : ∀ {A u}, PE A → PV u → PE (A +++ u).
Proof. move=>>; apply cas_transl; easy. Qed.
Lemma sub_translF_aux :
∀ {n} {A} {u : 'V^n}, PE A → inclF u PV → inclF (translF A u) PE.
Proof. intros; intro; apply sub_transl_aux; easy. Qed.
Definition sub_transl
(A : sub_AffineSpace) (u : sub_ModuleSpace HPV) : sub_AffineSpace :=
mk_sub (sub_transl_aux (in_sub A) (in_sub u)).
Lemma val_vect : f_vect_compat_gen val val.
Proof. easy. Qed.
Lemma val_vectF : f_vectF_compat_gen val val.
Proof. easy. Qed.
Lemma val_transl : f_transl_compat_gen val val.
Proof.
intros A u; pose (B := A +++ u).
assert (HB : u = A --> B) by now unfold B; rewrite transl_correct_r.
rewrite HB val_vect 2!transl_correct_l; easy.
Qed.
Lemma val_translF : f_translF_compat_gen val val.
Proof. move=>>; apply extF; intro; apply val_transl. Qed.
Lemma val_baryc :
∀ {n} L (A : 'sub_AffineSpace^n),
invertible (sum L) → val (barycenter L A) = barycenter L (mapF val A).
Proof.
intros n L A HL; apply baryc_correct_equiv; [easy |].
unfold aff_comb; rewrite -val_vectF -val_lc baryc_correct; easy.
Qed.
Lemma val_am : aff_map val.
Proof. intro; apply val_baryc. Qed.
Lemma mk_sub_vect :
∀ {A B : E} (HA : PE A) (HB : PE B),
mk_sub HA --> mk_sub HB = mk_sub (sub_vect_aux HA HB).
Proof. easy. Qed.
Lemma mk_sub_vectF :
∀ {n} {O} {A : 'E^n} (HO : PE O) (HA : inclF A PE),
vectF (mk_sub HO) (fun i ⇒ mk_sub (HA i)) =
fun i ⇒ mk_sub (sub_vect_aux HO (HA i)).
Proof. easy. Qed.
Lemma mk_sub_transl :
∀ {A u} (HA : PE A) (Hu : PV u),
mk_sub HA +++ mk_sub Hu = mk_sub (sub_transl_aux HA Hu).
Proof. intros; apply val_inj, val_transl. Qed.
Lemma mk_sub_translF :
∀ {n} {A} {u : 'V^n} (HA : PE A) (Hu : inclF u PV),
translF (mk_sub HA) (fun i ⇒ mk_sub (Hu i)) =
fun i ⇒ mk_sub (sub_transl_aux HA (Hu i)).
Proof. intros; apply extF; intro; apply mk_sub_transl. Qed.
Lemma mk_sub_baryc :
∀ {n} {L} {A : 'E^n} (HL : invertible (sum L)) (HA : inclF A PE),
barycenter L (fun i ⇒ mk_sub (HA i)) = mk_sub (HPE _ _ _ HL HA).
Proof. intros; apply val_inj, val_baryc; easy. Qed.
Lemma sub_vect_eq :
∀ (A B : sub_AffineSpace),
A --> B = mk_sub (sub_vect_aux (in_sub A) (in_sub B)).
Proof. easy. Qed.
Lemma sub_vectF_eq :
∀ {n} O (A : 'sub_AffineSpace^n),
vectF O A = fun i ⇒ mk_sub (sub_vect_aux (in_sub O) (in_sub (A i))).
Proof. easy. Qed.
Lemma sub_transl_eq :
∀ (A : sub_AffineSpace) (u : sub_ModuleSpace HPV),
A +++ u = mk_sub (sub_transl_aux (in_sub A) (in_sub u)).
Proof. intros; apply val_inj, val_transl. Qed.
Lemma sub_translF_eq :
∀ {n} (A : sub_AffineSpace) (u : '(sub_ModuleSpace HPV)^n),
translF A u = fun i ⇒ mk_sub (sub_transl_aux (in_sub A) (in_sub (u i))).
Proof. intros; apply extF; intro; apply sub_transl_eq. Qed.
Lemma sub_baryc_eq :
∀ {n} {L} {A : 'sub_AffineSpace^n} (HL : invertible (sum L)),
barycenter L A = mk_sub (HPE _ _ _ HL (fun i ⇒ in_sub (A i))).
Proof. intros; apply val_inj, val_baryc; easy. Qed.
End Sub_AffineSpace_Def.
Section Sub_AffineSpace_Facts1.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PEa PEb : E → Prop}.
Hypothesis HPE : incl PEa PEb.
Hypothesis HPEb : compatible_as PEb.
Context {O : E}.
Hypothesis HO : PEb O.
Let PEb_as := sub_AffineSpace HK HPEb HO.
Let PEa' : PEb_as → Prop := preimage val PEa.
Lemma RgS_val_as_eq : RgS PEa' val = PEa.
Proof. apply RgS_val_eq; easy. Qed.
Lemma preimage_val_cas : compatible_as PEa → compatible_as PEa'.
Proof. intros; apply cas_preimage; [apply val_am | easy]. Qed.
Lemma preimage_val_cas_rev : compatible_as PEa' → compatible_as PEa.
Proof.
intros; rewrite -RgS_val_as_eq; apply RgS_cas; [easy | apply val_am].
Qed.
Lemma preimage_val_cas_equiv : compatible_as PEa' ↔ compatible_as PEa.
Proof. split; [apply preimage_val_cas_rev | apply preimage_val_cas]. Qed.
End Sub_AffineSpace_Facts1.
Section Sub_AffineSpace_Facts2.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PEb : E → Prop}.
Hypothesis HPEb : compatible_as PEb.
Context {O : E}.
Hypothesis HO : PEb O.
Let PEb_as := sub_AffineSpace HK HPEb HO.
Context {PEa : PEb_as → Prop}.
Let PEa' := RgS PEa val.
Lemma preimage_val_as_eq : preimage val PEa' = PEa.
Proof. apply preimage_val_eq. Qed.
Lemma RgS_val_cas : compatible_as PEa → compatible_as PEa'.
Proof. intros; apply RgS_cas; [easy | apply val_am]. Qed.
Lemma RgS_val_cas_rev : compatible_as PEa' → compatible_as PEa.
Proof.
intros; rewrite -preimage_val_as_eq; apply cas_preimage; [apply val_am | easy].
Qed.
Lemma RgS_val_cas_equiv : compatible_as PEa' ↔ compatible_as PEa.
Proof. split; [apply RgS_val_cas_rev | apply RgS_val_cas]. Qed.
End Sub_AffineSpace_Facts2.
Section Sub_AffineSpace_Affine_Mapping_Facts1.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Context {HPE1 : compatible_as PE1}.
Context {HPE2 : compatible_as PE2}.
Context {O1 : E1}.
Context {O2 : E2}.
Context {HO1 : PE1 O1}.
Context {HO2 : PE2 O2}.
Let PE1_as := sub_AffineSpace HK HPE1 HO1.
Let PE2_as := sub_AffineSpace HK HPE2 HO2.
Context {f : E1 → E2}.
Context {fS : PE1_as → PE2_as}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_as_am : aff_map f → aff_map fS.
Proof.
intros Hf n; intros; apply val_inj; rewrite HfS !val_baryc// Hf//.
f_equal; apply extF; intro; rewrite !mapF_correct; easy.
Qed.
End Sub_AffineSpace_Affine_Mapping_Facts1.
Section Sub_AffineSpace_Affine_Mapping_Facts2.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 → Prop}.
Context {PE2 : E2 → Prop}.
Hypothesis HPE1 : compatible_as PE1.
Hypothesis HPE2 : compatible_as PE2.
Context {O1 : E1}.
Context {O2 : E2}.
Hypothesis HO1 : PE1 O1.
Hypothesis HO2 : PE2 O2.
Let PE1_as := sub_AffineSpace HK HPE1 HO1.
Let PE2_as := sub_AffineSpace HK HPE2 HO2.
Context {f : E1 → E2}.
Hypothesis Hf : funS PE1 PE2 f.
Definition fct_sub_as : PE1_as → PE2_as := fct_sub Hf.
Lemma fct_sub_as_inj : injS PE1 f → injective fct_sub_as.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_as_inj_rev : injective fct_sub_as → injS PE1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_as_inj_equiv : injective fct_sub_as ↔ injS PE1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_as_surj : surjS PE1 PE2 f → surjective fct_sub_as.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_as_surj_rev : surjective fct_sub_as → surjS PE1 PE2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_as_surj_equiv : surjective fct_sub_as ↔ surjS PE1 PE2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_as_bij : bijS PE1 PE2 f → bijective fct_sub_as.
Proof. apply fct_sub_bij, inhabited_as. Qed.
Lemma fct_sub_as_bij_rev : bijective fct_sub_as → bijS PE1 PE2 f.
Proof. apply fct_sub_bij_rev, inhabited_as. Qed.
Lemma fct_sub_as_bij_equiv : bijective fct_sub_as ↔ bijS PE1 PE2 f.
Proof. apply fct_sub_bij_equiv, inhabited_as. Qed.
Lemma fct_sub_as_am : aff_map f → aff_map fct_sub_as.
Proof. apply sub_as_am, fct_sub_correct. Qed.
Lemma fct_sub_as_f_inv_am :
∀ (Hfb : bijS PE1 PE2 f),
aff_map f → aff_map (f_inv (fct_sub_as_bij Hfb)).
Proof. intros; apply am_bij_compat, fct_sub_as_am; easy. Qed.
End Sub_AffineSpace_Affine_Mapping_Facts2.
Section Sub_AffineSpace_Affine_Mapping_Facts3.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V W : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.
Context {PE : E → Prop}.
Context {PF : F → Prop}.
Hypothesis HPE : compatible_as PE.
Hypothesis HPF : compatible_as PF.
Context {f : E → F}.
Hypothesis Hf : aff_map f.
Variable O : E.
Hypothesis HO : PE O.
Let lf := fct_lm f O.
Let PV := vectP PE O.
Let PW := vectP PF (f O).
Lemma funS_aff_lin_equiv : funS PE PF f ↔ funS PV PW lf.
Proof.
rewrite !funS_equiv; split.
intros Hf1 v Hv; unfold PW, vectP, preimage, lf;
rewrite transl_correct_l; auto.
intros Hlf A HA;
rewrite -(transl_correct_l (f O) (f A)) -(transl_correct_l O A).
apply Hlf; unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
Qed.
Lemma injS_aff_lin_equiv : injS PE f ↔ injS PV lf.
Proof.
split.
intros Hf1 u1 u2 Hu1 Hu2 Hu; apply (transl_l_inj O), Hf1; auto.
apply (vect_l_inj (f O)); auto.
intros Hlf1 A1 A2 HA1 HA2 HA; apply (vect_l_inj O), Hlf1.
1,2: unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
unfold lf, fct_lm; rewrite !transl_correct_l HA; easy.
Qed.
Lemma injS_aff_lin_equiv_alt : injS PE f ↔ incl (KerS PV lf) zero_sub_struct.
Proof.
rewrite injS_aff_lin_equiv -KerS_zero_equiv.
rewrite -lmS_injS_equiv; [easy |..].
1,3: apply cas_cms; easy.
1,2: apply am_lm_equiv; easy.
Qed.
Lemma surjS_gen_aff_lin_equiv : surjS PE PF f ↔ surjS PV PW lf.
Proof.
split.
intros Hf1 w Hw; destruct (Hf1 (f O +++ w)) as [A [HA1 HA2]]; try easy.
∃ (O --> A); split.
unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
unfold lf, fct_lm; rewrite transl_correct_l HA2 transl_correct_r; easy.
intros Hlf B HB; destruct (Hlf (f O --> B)) as [v [Hv1 Hv2]].
unfold PW, vectP, preimage; rewrite transl_correct_l; easy.
∃ (O +++ v); split; try apply (vect_l_inj (f O)); easy.
Qed.
Lemma surjS_gen_aff_lin_equiv_alt : surjS PE PF f ↔ incl PW (RgS PV lf).
Proof.
rewrite surjS_gen_aff_lin_equiv -RgS_gen_full_equiv; apply surjS_RgS_gen_equiv.
Qed.
Lemma bijS_gen_aff_lin_equiv : bijS PE PF f ↔ bijS PV PW lf.
Proof.
rewrite !bijS_equiv; [| apply inhabited_ms | easy].
rewrite funS_aff_lin_equiv injS_aff_lin_equiv surjS_gen_aff_lin_equiv; easy.
Qed.
Lemma bijS_gen_aff_lin_equiv_alt :
bijS PE PF f ↔
funS PV PW lf ∧ incl (KerS PV lf) zero_sub_struct ∧ incl PW (RgS PV lf).
Proof.
rewrite bijS_equiv; [| apply inhabited_as].
rewrite funS_aff_lin_equiv injS_aff_lin_equiv_alt surjS_gen_aff_lin_equiv_alt//.
Qed.
End Sub_AffineSpace_Affine_Mapping_Facts3.
Section Sub_AffineSpace_Affine_Mapping_Facts4.
Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V W : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_as PE.
Context {f : E → F}.
Hypothesis Hf : aff_map f.
Variable O : E.
Hypothesis HO : PE O.
Let lf := fct_lm f O.
Let PV := vectP PE O.
Lemma surjS_aff_lin_equiv : surjS PE fullset f ↔ surjS PV fullset lf.
Proof. rewrite (surjS_gen_aff_lin_equiv O) vectP_fullset; easy. Qed.
Lemma surjS_aff_lin_equiv_alt :
surjS PE fullset f ↔ incl fullset (RgS PV lf).
Proof. rewrite (surjS_gen_aff_lin_equiv_alt O) vectP_fullset; easy. Qed.
Lemma bijS_aff_lin_equiv : bijS PE fullset f ↔ bijS PV fullset lf.
Proof. rewrite (bijS_gen_aff_lin_equiv O) vectP_fullset; easy. Qed.
Lemma bijS_aff_lin_equiv_alt :
bijS PE fullset f ↔
incl (KerS PV lf) zero_sub_struct ∧ incl fullset (RgS PV lf).
Proof.
rewrite (bijS_gen_aff_lin_equiv_alt HK HPE Hf O)// vectP_fullset; easy.
Qed.
End Sub_AffineSpace_Affine_Mapping_Facts4.
Section Compatible_AffineSpace_R_Facts.
Context {V : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.
Context {PE : E → Prop}.
Context {O : E}.
Hypothesis HO : PE O.
Lemma cas_cms_equiv_R : compatible_as PE ↔ compatible_ms (vectP PE O).
Proof.
apply cas_cms_equiv; [easy | apply nonzero_struct_R | apply invertible_2].
Qed.
Variable gen : E → Prop.
Lemma cas_baryc_closure_R : compatible_as (baryc_closure gen).
Proof.
intros n L A HL HA; destruct (baryc_normalized_n0_ex _ A HL)
as [n1 [L1 [A1 [HL1a [HL1b [HA1a HA1b]]]]]]; rewrite HA1b.
destruct (baryc_closure_exs _ (inclF_monot_l _ _ _ HA1a HA))
as [b [M [B [HM1 [HM2 [HB HA']]]]]].
assert (HL1' : L1 = fun i1 ⇒ sum (scal (L1 i1) (M i1))).
apply extF; intro; rewrite -scal_sum_distr_l HM1 scal_one_r; easy.
rewrite (baryc_eq_r (fun i1 ⇒ barycenter (scal (L1 i1) (M i1)) (B i1))).
2: { rewrite HA'; apply extF; intro; apply baryc_homogeneous.
apply invertible_equiv_R; easy.
rewrite HM1; apply invertible_one. }
rewrite {1}HL1' -baryc_assoc.
apply Barycenter_closure.
1,4: rewrite sum_assoc -HL1' HL1a; apply invertible_one.
apply concatnF_inclF_equiv; easy.
intros i; rewrite -(extF_rev _ _ HL1' i).
apply invertible_equiv_R; easy.
Qed.
Lemma baryc_closure_idem_R :
baryc_closure (baryc_closure gen) = baryc_closure gen.
Proof. apply eq_sym, cas_equiv, cas_baryc_closure_R. Qed.
[GostiauxT4]
Th 1.26, p. 10.
Lemma span_as_eq_R : span_as gen = baryc_closure gen.
Proof.
apply subset_ext_equiv; split.
apply (span_as_lub gen).
apply cas_baryc_closure_R.
apply baryc_closure_incl.
intros A HA; induction HA; apply span_as_cas; try easy.
apply inclF_monot_r with gen; try easy.
apply span_as_incl.
Qed.
End Compatible_AffineSpace_R_Facts.
Section Sub_AffineSpace_Affine_Mapping_R_Facts.
Context {V W : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.
Lemma cas_am : compatible_as (@aff_map _ _ _ E F).
Proof.
intros n2 L2 f2 HL2 Hf2 n1 L1 A1 HL1; generalize HL1 HL2.
move⇒ /invertible_equiv_R HL1' /invertible_equiv_R HL2'.
rewrite fct_baryc_eq; try easy.
assert (Hf2a :
f2^~ (barycenter L1 A1) = fun i2 ⇒ barycenter L1 (mapF (f2 i2) A1))
by now apply extF; intros i2; apply (Hf2 i2).
rewrite Hf2a.
pose (f := barycenter L2 f2).
generalize (baryc_correct f2 HL2); fold f; intros Hf.
pose (B1 := mapF f A1); fold B1.
pose (B2 := fun i2 ⇒ barycenter L1 (mapF (f2 i2) A1)); fold B2.
assert (HB2 : ∀ i2, aff_comb L1 (mapF (f2 i2) A1) (B2 i2))
by now intros; apply baryc_correct_equiv.
pose (B := barycenter L2 B2).
generalize (baryc_correct B2 HL2); fold B; intros HB.
apply baryc_correct_equiv; try easy; unfold aff_comb in ×.
pose (M i1 i2 := f2 i2 (A1 i1) --> B2 i2).
assert (HM : lin_comb L1 (mapF (lin_comb L2 (vectF f f2)) A1) +
lin_comb L1 (mapF (lin_comb L2) M) = 0).
rewrite Hf mapF_zero_f lc_zero_r plus_zero_l.
rewrite -lc_flipT_r lc2_r_sym flipT_invol; unfold M.
apply lc_zero_compat_r, extF; intros i2.
rewrite fct_lc_r_eq fct_zero_eq opp_zero_equiv -lc_opp_r -(HB2 i2).
apply lc_eq_r, extF; intro; rewrite vectF_correct vect_sym; easy.
apply (scal_zero_reg_r_R (sum L2)); try easy.
rewrite -(plus_zero_r (scal _ _)) -{1}HM -lc_plus_r; unfold M.
rewrite (lc_eq_r _ (_ + _) (lin_comb L2 (fun i2 i1 ⇒ B1 i1 --> B2 i2))).
2: { apply extF; intro.
rewrite fct_plus_eq !mapF_correct !fct_lc_r_eq -lc_plus_r; f_equal.
rewrite vectF_chasles; easy. }
rewrite -lc_scal_r -lc_constF_r -!lc_plus_r.
apply lc_zero_compat_r, extF; intros i1.
rewrite fct_lc_r_eq fct_zero_eq -HB; f_equal; apply extF; intros i2.
rewrite !fct_plus_eq constF_correct !vectF_correct; apply vect_chasles.
Qed.
Definition Am := sub_AffineSpace invertible_2 cas_am fct_point_of_as_am.
End Sub_AffineSpace_Affine_Mapping_R_Facts.
Proof.
apply subset_ext_equiv; split.
apply (span_as_lub gen).
apply cas_baryc_closure_R.
apply baryc_closure_incl.
intros A HA; induction HA; apply span_as_cas; try easy.
apply inclF_monot_r with gen; try easy.
apply span_as_incl.
Qed.
End Compatible_AffineSpace_R_Facts.
Section Sub_AffineSpace_Affine_Mapping_R_Facts.
Context {V W : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.
Lemma cas_am : compatible_as (@aff_map _ _ _ E F).
Proof.
intros n2 L2 f2 HL2 Hf2 n1 L1 A1 HL1; generalize HL1 HL2.
move⇒ /invertible_equiv_R HL1' /invertible_equiv_R HL2'.
rewrite fct_baryc_eq; try easy.
assert (Hf2a :
f2^~ (barycenter L1 A1) = fun i2 ⇒ barycenter L1 (mapF (f2 i2) A1))
by now apply extF; intros i2; apply (Hf2 i2).
rewrite Hf2a.
pose (f := barycenter L2 f2).
generalize (baryc_correct f2 HL2); fold f; intros Hf.
pose (B1 := mapF f A1); fold B1.
pose (B2 := fun i2 ⇒ barycenter L1 (mapF (f2 i2) A1)); fold B2.
assert (HB2 : ∀ i2, aff_comb L1 (mapF (f2 i2) A1) (B2 i2))
by now intros; apply baryc_correct_equiv.
pose (B := barycenter L2 B2).
generalize (baryc_correct B2 HL2); fold B; intros HB.
apply baryc_correct_equiv; try easy; unfold aff_comb in ×.
pose (M i1 i2 := f2 i2 (A1 i1) --> B2 i2).
assert (HM : lin_comb L1 (mapF (lin_comb L2 (vectF f f2)) A1) +
lin_comb L1 (mapF (lin_comb L2) M) = 0).
rewrite Hf mapF_zero_f lc_zero_r plus_zero_l.
rewrite -lc_flipT_r lc2_r_sym flipT_invol; unfold M.
apply lc_zero_compat_r, extF; intros i2.
rewrite fct_lc_r_eq fct_zero_eq opp_zero_equiv -lc_opp_r -(HB2 i2).
apply lc_eq_r, extF; intro; rewrite vectF_correct vect_sym; easy.
apply (scal_zero_reg_r_R (sum L2)); try easy.
rewrite -(plus_zero_r (scal _ _)) -{1}HM -lc_plus_r; unfold M.
rewrite (lc_eq_r _ (_ + _) (lin_comb L2 (fun i2 i1 ⇒ B1 i1 --> B2 i2))).
2: { apply extF; intro.
rewrite fct_plus_eq !mapF_correct !fct_lc_r_eq -lc_plus_r; f_equal.
rewrite vectF_chasles; easy. }
rewrite -lc_scal_r -lc_constF_r -!lc_plus_r.
apply lc_zero_compat_r, extF; intros i1.
rewrite fct_lc_r_eq fct_zero_eq -HB; f_equal; apply extF; intros i2.
rewrite !fct_plus_eq constF_correct !vectF_correct; apply vect_chasles.
Qed.
Definition Am := sub_AffineSpace invertible_2 cas_am fct_point_of_as_am.
End Sub_AffineSpace_Affine_Mapping_R_Facts.