Require Export cat.
Require Export target.
Implicit Arguments On.
Sieves |
| A sieve is a kind of left ideal in a category. Sieves are useful to define a Grothendieck topology. |
Module Sieve.
Export Cat.
Export Target.
Section Sieves.
Variable A:Cat.
Section Sieve_Theory.
Variable u:A; s:(Target u).
Definition Sieve_Theory : Prop := (x,y:A; f:(mor x u); g:(mor y x))
(s f) -> (s (oo f g)).
End Sieve_Theory.
Section Sieve.
Variable u:A.
Record Sieve : Type := {
sieve :> (Target u);
sieve_theory : (Sieve_Theory sieve)
}.
Lemma sieve_prop : (s:Sieve; x,y:A; f:(mor x u); g:(mor y x))
(sieve s f) -> (sieve s (oo f g)).
Proof.
NewDestruct s; Simpl; Auto.
Qed.
Hints Resolve sieve_prop.
Lemma sieve_set_prop : (s:Sieve; f:s) (sieve s f).
Proof.
NewDestruct f.
Tauto.
Qed.
End Sieve.
Hints Resolve sieve_prop sieve_set_prop.
Section Sieve_Transport.
Variable u,v:A; f:(mor u v); s:(Sieve v).
Remark t_theory : (Sieve_Theory (target_transport f s)).
Proof.
Unfold Sieve_Theory target_transport; Intros.
Rewrite oo_assoc; Auto.
Qed.
Definition sieve_transport : (Sieve u).
Proof.
Split with (target_transport f s); Exact t_theory.
Defined.
End Sieve_Transport.
Lemma is_maximal_sieve_ii : (u:A; s:(Sieve u))
(sieve s (ii u)) -> (is_maximal_target s).
Proof.
Unfold is_maximal_target; Intros.
Rewrite <- ii_sx; Auto.
Qed.
Hints Resolve is_maximal_sieve_ii.
Definition maximal_sieve [u:A] : (Sieve u).
Proof.
Intros; Split with [x:A; f:(mor x u)] True.
Abstract Unfold Sieve_Theory; Auto.
Defined.
Lemma maximal_sieve_is_maximal : (u:A)
(is_maximal_target (maximal_sieve u)).
Proof.
Unfold is_maximal_target; Simpl; Auto.
Qed.
Hints Resolve maximal_sieve_is_maximal.
Lemma sieve_extens : (u:A; s,t:(Sieve u))
(target_sub s t) -> (target_sub t s) -> s==t.
Proof.
Unfold target_sub; NewDestruct s; NewDestruct t; Intros.
Simpl in H; Simpl in H0.
Assert U : sieve0==sieve1.
Apply extensionality with T:=[x:A](mor x u)->Prop.
Intros.
Apply nondep_extensionality.
Intros.
Apply prop_uni; Auto.
NewDestruct U.
Assert E: sieve_theory0 == sieve_theory1.
Apply proof_irrelevance.
NewDestruct E; Reflexivity.
Qed.
Lemma sieve_transport_trans :
(u,v,w:A; g:(mor v w); f:(mor u v); s:(Sieve w))
(sieve_transport (oo g f) s)==(sieve_transport f (sieve_transport g s)).
Proof.
Intros; Apply sieve_extens; Unfold target_sub;
Simpl; Unfold target_transport; Intros.
Rewrite oo_assoc; Auto.
Rewrite <- oo_assoc; Auto.
Qed.
Hints Resolve sieve_transport_trans.
Section Sieve_Composition.
Variable u:A; s:(Sieve u).
Variable t:(x:A; f:(mor x u); Hf:(sieve s f))(Sieve x).
Local r [x:A; f:(mor x u); Hf:(sieve s f)] : (Target x) :=
(sieve (t Hf)).
Remark sieve_comp_sieve : (Sieve_Theory (target_comp r)).
Proof.
Unfold r Sieve_Theory; Intros.
NewDestruct H.
Rewrite <- oo_assoc.
Split with Hf; Auto.
Qed.
Definition sieve_comp : (Sieve u).
Proof.
Split with (target_comp r); Exact sieve_comp_sieve.
Defined.
Lemma sieve_comp_prop : (x:A; f:(mor x u); Hf:(sieve s f))
(y:A; g:(mor y x); Hg:(sieve (t Hf) g))
(sieve sieve_comp (oo f g)).
Proof.
Intros; Split with Hf; Auto.
Qed.
End Sieve_Composition.
End Sieves.
End Sieve.