Properties of Maps |
Require
misc___.
Implicit Arguments On.
Module
Map___.
Export
Misc___.
Bijective maps |
Section
Bijection.
Variable
A,B:Type.
Record
Bijection_Theory [f:A->B; g:B->A] : Prop := {
ax_bijection_eq1 : (x:A)(g (f x))==x;
ax_bijection_eq2 : (x:B)(f (g x))==x
}.
Record
Bijection_Data : Type := {
bijection_map :> A->B;
bijection_inv_map : B->A
}.
Record
Bijection : Type := {
bijection_data :> Bijection_Data;
bijection_theory :>
(Bijection_Theory (!bijection_map bijection_data)
(!bijection_inv_map bijection_data))
}.
End
Bijection.
Inverse of a bijection |
Definition
bijection_inverse [A,B:Type; f:(Bijection A B)] :
(Bijection B A).
Proof
.
Intros.
Split with (Build_Bijection_Data (bijection_inv_map f) f).
Abstract Split; Simpl; Intros;
Apply (ax_bijection_eq2 f) Orelse Apply (ax_bijection_eq1 f).
Defined
.
Section
Bijection_Facts.
Variable
A,B:Type; f:(Bijection A B).
Lemma
bijection_eq1 : (x:A)(bijection_inverse f (f x))==x.
Proof
.
Apply (ax_bijection_eq1 f).
Qed
.
Lemma
bijection_eq2 : (x:B)(f (bijection_inverse f x))==x.
Proof
.
Apply (ax_bijection_eq2 f).
Qed
.
End
Bijection_Facts.
Hints
Resolve bijection_eq1 bijection_eq2.
Section
Injective_Surjective.
Variable
A,B:Type; f:A->B.
Definition
is_surjective : Prop :=
(y:B)(EXT x:A | (f x)==y).
Record
section : Type := {
section_map :> B->A;
section_eq : (x:B) (f (section_map x))==x
}.
Record
cosection : Type := {
cosection_map :> B->A;
cosection_eq : (x:A) (cosection_map (f x))==x
}.
Hints
Resolve section_eq cosection_eq.
Lemma
section_surj : (g:section) is_surjective.
Proof
.
Unfold is_surjective; Intros.
Split with (g y).
Apply section_eq.
Qed
.
Definition
is_injective : Prop :=
(x,y:A) (f x)==(f y) -> x==y.
Lemma
cosection_inj : (g:cosection) is_injective.
Proof
.
Unfold is_injective; Intros.
Rewrite <- (cosection_eq g) with x.
Rewrite H.
Auto.
Qed
.
Hints
Resolve section_surj cosection_inj.
Record
Inverse_Theory [inv:B->A] : Prop := {
ax_inverse_sx_eq : (x:A) (inv (f x))==x;
ax_inverse_dx_eq : (x:B) (f (inv x))==x
}.
Record
inverse : Type := {
inverse_map :> B->A;
inverse_theory :> (Inverse_Theory inverse_map)
}.
Lemma
inverse_sx_eq : (g:inverse)
(x:A) (g (f x))==x.
Proof
.
Intros; NewDestruct (inverse_theory g); Trivial.
Qed
.
Lemma
inverse_dx_eq : (g:inverse)
(x:B) (f (g x))==x.
Proof
.
Intros; NewDestruct (inverse_theory g); Trivial.
Qed
.
Hints
Resolve inverse_sx_eq inverse_dx_eq.
Definition
section_of_inverse : inverse->section.
Proof
.
Intro g; Split with g; Abstract Auto.
Defined
.
Definition
cosection_of_inverse : inverse->cosection.
Proof
.
Intro g; Split with g; Abstract Auto.
Defined
.
Lemma
section_eq_cosection : (g1:section; g2:cosection)
(x:B)(g1 x)==(g2 x).
Proof
.
Intros.
Rewrite <- (section_eq g1) with x.
Rewrite (cosection_eq g2) with (g1 x).
Rewrite section_eq.
Auto.
Qed
.
Remark
make_inverse_theory : (g1:section; g2:cosection)
(Inverse_Theory g1).
Proof
.
Split; Simpl; Intros.
Rewrite (section_eq_cosection g1 g2 (f x)).
Auto.
Auto.
Qed
.
Definition
make_inverse : section->cosection->inverse.
Proof
.
Intros g1 g2; Split with g1.
Exact (make_inverse_theory g1 g2).
Defined
.
Lemma
inverse_unique : (g1,g2:inverse) g1==g2.
Proof
.
Intros.
Cut (x:B)(g1 x)==(g2 x).
NewDestruct g1; NewDestruct g2; Simpl; Intros.
Assert E: inverse_map0==inverse_map1.
Apply nondep_extensionality; Trivial.
NewDestruct E.
Assert E: inverse_theory0==inverse_theory1.
Apply proof_irrelevance.
NewDestruct E.
Reflexivity.
Intros.
Rewrite <- (inverse_dx_eq g1) with x.
Rewrite (inverse_sx_eq g2) with (g1 x).
Auto.
Qed
.
End
Injective_Surjective.
Hints
Resolve section_eq cosection_eq section_surj cosection_inj
section_eq_cosection inverse_sx_eq inverse_dx_eq inverse_unique.
Section
Inverse_Lemmas.
Variable
A,B:Type.
Subtility of this version of inverse transport: eqT_rect do not appear in the informative part of the definition.
|
Definition
inverse_transport [f1,f2:A->B; H:f1==f2; g1:(inverse f1)] :
(inverse f2).
Proof
.
Intros.
Split with [x:B](g1 x).
Abstract NewDestruct H; Split; Auto.
Defined
.
Lemma
inverse_eq : (f1,f2:A->B; g1:(inverse f1); g2:(inverse f2))
f1==f2 -> (x:B)(g1 x)==(g2 x).
Proof
.
NewDestruct 1.
Replace g2 with g1.
Reflexivity.
Apply inverse_unique.
Qed
.
Lemma
eq_from_inverse_eq : (f1,f2:A->B; g1:(inverse f1); g2:(inverse f2))
((x:B)(g1 x)==(g2 x)) -> f1==f2.
Proof
.
Intros.
Apply nondep_extensionality.
Intros.
Rewrite <- (inverse_dx_eq g1) with (f2 x).
Rewrite H.
Rewrite inverse_sx_eq.
Reflexivity.
Qed
.
Hints
Resolve inverse_eq eq_from_inverse_eq.
Definition
inverse_inverse [f:A->B; g:(inverse f)] :
(inverse g).
Proof
.
Intros; Split with f.
Abstract Split; Auto.
Defined
.
Lemma
inverse_inverse_eq : (f:A->B; g:(inverse f); h:(inverse g))
f==h.
Proof
.
Intros.
Apply nondep_extensionality; Intros.
Rewrite <- (inverse_dx_eq g) with (h x).
Rewrite (inverse_dx_eq h).
Reflexivity.
Qed
.
Hints
Resolve inverse_inverse_eq.
End
Inverse_Lemmas.
Hints
Resolve inverse_eq eq_from_inverse_eq.
Hints
Resolve inverse_inverse_eq.
Compositions of sections, cosections and inverses |
Section
Injective_Surjective_Comp.
Variable
A,B,C:Type; g:B->C; f:A->B.
Definition
section_comp : (g1:(section g); f1:(section f))
(section [x:A](g (f x))).
Proof
.
Intros; Split with [x:C](f1 (g1 x)).
Abstract Intro; Rewrite section_eq; Auto.
Defined
.
Definition
cosection_comp : (g1:(cosection g); f1:(cosection f))
(cosection [x:A](g (f x))).
Proof
.
Intros; Split with [x:C](f1 (g1 x)).
Abstract Intro; Rewrite cosection_eq; Auto.
Defined
.
Remark
inverse_comp_theory : (g1:(inverse g); f1:(inverse f))
(Inverse_Theory [x:A](g (f x)) [x:C](f1 (g1 x))).
Proof
.
Split; Simpl; Intros.
Rewrite inverse_sx_eq; Auto.
Rewrite inverse_dx_eq; Auto.
Qed
.
Definition
inverse_comp : (g1:(inverse g); f1:(inverse f))
(inverse [x:A](g (f x))).
Proof
.
Intros; Split with [x:C](f1 (g1 x)).
Exact (inverse_comp_theory g1 f1).
Defined
.
End
Injective_Surjective_Comp.
End
Map___.