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