Require
Export
cat__.
Implicit Arguments On.
Presheafs |
We use the name "presheaf" for contravariant functors. |
Module
Presheaf__.
Export
Misc__.
Export
Cat__.
Section
Presheaf_Theory.
Variable
A,B:Cat.
Variable
F0:A->B; F1:(x,y:A) (mor x y) -> (mor (F0 y) (F0 x)).
Record
Presheaf_Theory : Prop := {
ax_presh_oo : (x,y,z:A; g:(mor y z); f:(mor x y))
(F1 (oo g f))==(oo (F1 f) (F1 g));
ax_presh_ii : (x:A) (F1 (ii x))==(ii (F0 x))
}.
End
Presheaf_Theory.
Record
Presheaf_Data [A,B:Cat] : Type := {
presh_obj :> A->B;
presh : (x,y:A; f:(mor x y)) (mor (presh_obj y) (presh_obj x))
}.
Record
Presheaf [A,B:Cat] : Type := {
presheaf_data :> (Presheaf_Data A B);
presheaf_theory :> (Presheaf_Theory (presh presheaf_data))
}.
Section
Presheaf_Facts.
Variable
A,B:Cat; F:(Presheaf A B).
Lemma
presh_oo : (x,y,z:A; g:(mor y z); f:(mor x y))
(presh F (oo g f))==(oo (presh F f) (presh F g)).
Proof
.
Intros; Apply (ax_presh_oo F).
Qed
.
Lemma
presh_ii : (x:A) (presh F (ii x))==(ii (F x)).
Proof
.
Intros; Apply (ax_presh_ii F).
Qed
.
End
Presheaf_Facts.
Hints
Resolve presh_oo presh_ii.
Definition
Morph [A,B:Cat] : Type := (Presheaf A B).
Section
Eq_Presh.
Variable
A,B:Cat.
Definition
eq_presh [F,G:(Presheaf A B)] : Prop :=
(x,y:A; f:(mor x y)) (eq_mor (presh F f) (presh G f)).
Variable
F,G:(Presheaf A B); F_eq_G:(eq_presh F G).
Lemma
eq_presh_src : (x,y:A; f:(mor x y))
(src (presh F f))==(src (presh G f)).
Proof
.
Intros; NewDestruct (F_eq_G f); Reflexivity.
Qed
.
Lemma
eq_presh_trg : (x,y:A; f:(mor x y))
(trg (presh F f))==(trg (presh G f)).
Proof
.
Intros; NewDestruct (F_eq_G f); Reflexivity.
Qed
.
Lemma
eq_presh_obj : (x:A)(F x)==(G x).
Proof
.
Intros.
Change (src (ii (F x)))==(src (ii (G x))).
Do 2 Rewrite <- presh_ii.
Apply eq_presh_src.
Qed
.
Extensionality for presheafs |
We prove that eq_presh implies eqT .
|
Lemma
presheaf_extens : F==G.
Proof
.
Assert U := eq_presh_obj.
NewDestruct F; NewDestruct G.
NewDestruct presheaf_data0.
NewDestruct presheaf_data1.
Simpl in U.
Assert E : presh_obj0==presh_obj1.
Apply nondep_extensionality.
Apply U.
NewDestruct E.
Clear F G U.
Rename presh_obj0 into FF.
Assert E : presh0==presh1.
Apply extensionality
with T := [x:A](y:A)(mor x y)->(mor (FF y) (FF x)).
Intros.
Apply extensionality
with T := [y:A](mor x y)->(mor (FF y) (FF x)).
Intros.
Apply nondep_extensionality.
Intros.
Unfold eq_presh in F_eq_G.
Simpl in F_eq_G.
Apply eq_mor_eqT.
Apply (F_eq_G x1).
NewDestruct E.
Assert E : presheaf_theory0 == presheaf_theory1.
Apply proof_irrelevance.
NewDestruct E.
Reflexivity.
Qed
.
End
Eq_Presh.
Morphisms of presheafs. |
Morphisms of presheafs are natural tranformations between contravariant functors. |
Section
NT'.
Variable
A,B:Cat; F,G:(Presheaf A B).
Definition
NT'_Comm [n:(x:A)(mor (F x) (G x))] : Prop :=
(x,y:A; f:(mor x y))
(oo (n x) (presh F f))==(oo (presh G f) (n y)).
Record
NT' : Type := {
nt'_data :> (x:A) (mor (F x) (G x));
ax_nt'_comm :> (NT'_Comm nt'_data)
}.
Lemma
nt'_comm : (n:NT'; x,y:A; f:(mor x y))
(oo (n x) (presh F f))==(oo (presh G f) (n y)).
Proof
.
Intros; Apply ax_nt'_comm.
Qed
.
Lemma
nt'_extens : (n,m:NT')
((x:A) (n x)==(m x)) -> n==m.
Proof
.
NewDestruct n; NewDestruct m; Simpl; Intros.
Assert nt'_data0==nt'_data1.
Apply extensionality with T := [x:A](mor (F x) (G x)).
Assumption.
NewDestruct H0.
Assert ax_nt'_comm0==ax_nt'_comm1.
Apply proof_irrelevance.
NewDestruct H0.
Reflexivity.
Qed
.
End
NT'.
Hints
Resolve nt'_comm nt'_extens.
Category of functors |
Presheafs with natural transformations form a category. |
Section
Presheaf_Cat.
Variable
A,B:Cat.
Definition
nt'_id [F:(Presheaf A B)] : (NT' F F).
Proof
.
Intros; Split with [x:A](ii (F x)).
Abstract Unfold NT'_Comm; Intros;
Rewrite ii_sx; Rewrite ii_dx; Reflexivity.
Defined
.
Implicits
nt'_id [1].
Section
NT'_Comp.
Variable
F,G,H:(Presheaf A B).
Variable
m:(NT' G H); n:(NT' F G).
Local
p [x:A] : (mor (F x) (H x)) := (oo (m x) (n x)).
Remark
p_theory : (NT'_Comm p).
Proof
.
Unfold p NT'_Comm; Intros.
Rewrite <- oo_assoc.
Rewrite (nt'_comm n).
Rewrite oo_assoc.
Rewrite (nt'_comm m).
Rewrite oo_assoc.
Reflexivity.
Qed
.
Definition
nt'_comp : (NT' F H).
Proof
.
Split with p; Exact p_theory.
Defined
.
End
NT'_Comp.
Lemma
nt'_comp_assoc : (F,G,H,I:(Presheaf A B))
(n:(NT' F G); m:(NT' G H); p:(NT' H I))
(nt'_comp p (nt'_comp m n))==(nt'_comp (nt'_comp p m) n).
Proof
.
Intros; Apply nt'_extens; Simpl; Auto.
Qed
.
Lemma
nt'_sx_id : (F,G:(Presheaf A B); n:(NT' F G))
(nt'_comp nt'_id n)==n.
Proof
.
Intros; Apply nt'_extens; Simpl; Auto.
Qed
.
Lemma
nt'_dx_id : (F,G:(Presheaf A B); n:(NT' F G))
(nt'_comp n nt'_id)==n.
Proof
.
Intros; Apply nt'_extens; Simpl; Auto.
Qed
.
Hints
Resolve nt'_comp_assoc nt'_sx_id nt'_dx_id.
Definition
Presheaf_Cat : Cat.
Proof
.
Split with (Build_Cat_Data nt'_comp !nt'_id).
Abstract Split; Simpl; Intros; Auto.
Defined
.
End
Presheaf_Cat.
Hints
Resolve nt'_comp_assoc nt'_sx_id nt'_dx_id.
End
Presheaf__.