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