Require Export cat_.
Require Export sieve_.
Implicit Arguments On.
Grothendieck Topologies. |
Module Topology_.
Export Sieve_.
Section Topology.
Variable A:Cat.
Section Topology_Theory.
| Datum of a topology. |
Variable J : (u:A)(Sieve u)->Type.
| Axioms for a topology. |
Record Topology_Theory : Type := {
ax_top_maximal : (u:A; s:(Sieve u))
(is_maximal_target s) -> (J s);
ax_top_larger : (u:A; s,t:(Sieve u))
(J s) -> (target_sub s t) -> (J t);
ax_top_transport : (u,v:A; f:(mor u v); s:(Sieve v))
(J s) -> (J (sieve_transport f s));
ax_top_comp :
(u:A; s:(Sieve u); Hs:(J s))
(t:(x:A; f:(mor x u); Hf:(sieve s f))(Sieve x))
(Ht:(x:A; f:(mor x u); Hf:(sieve s f))(J (t x f Hf)))
(J (sieve_comp t))
}.
End Topology_Theory.
| Type of a topology. |
Record Topology : Type := {
cov_obj : (u:A)(Sieve u)->Type;
topology_theory : (Topology_Theory cov_obj)
}.
Section Topology_Facts.
Variable J:Topology.
| The maximal sieve is a covering sieve. |
Lemma top_maximal : (u:A; s:(Sieve u))
(is_maximal_target s) -> (cov_obj J s).
Proof.
Elim J; Simpl.
NewDestruct 1; Auto.
Qed.
| Any larger sieve of a covering sieve is also a covering sieve. |
Lemma top_larger : (u:A; s,t:(Sieve u))
(cov_obj J s) -> (target_sub s t) -> (cov_obj J t).
Proof.
Elim J; Simpl.
NewDestruct 1; Auto.
Qed.
| Transport property. |
Lemma top_transport : (u,v:A; f:(mor u v); s:(Sieve v))
(cov_obj J s) -> (cov_obj J (sieve_transport f s)).
Proof.
Elim J; Simpl.
NewDestruct 1; Auto.
Qed.
| Composition property. |
Lemma top_comp :
(u:A; s:(Sieve u); Hs:(cov_obj J s))
(t:(x:A; f:(mor x u); Hf:(sieve s f))(Sieve (src f)))
(Ht:(x:A; f:(mor x u); Hf:(sieve s f))(cov_obj J (t x f Hf)))
(cov_obj J (sieve_comp t)).
Proof.
Elim J; Simpl.
NewDestruct 1; Auto.
Qed.
| Transitivity property. |
Lemma top_transitivity : (u:A; s,t:(Sieve u))
(cov_obj J s) ->
((x:A; f:(mor x u); Hf:(sieve s f))(cov_obj J (sieve_transport f t)))
-> (cov_obj J t).
Proof.
Intros.
Apply top_larger
with (sieve_comp [x:A; f:(mor x u); Hf:(sieve s f)](sieve_transport f t)).
Apply top_comp.
Assumption.
Auto.
Unfold target_sub.
NewDestruct 1; Auto.
Qed.
Hints Resolve top_transitivity.
Lemma cov_obj_transport: (u:A; s:(Sieve u))
(x:A; f:(mor x u); Hf:(sieve s f))
(cov_obj J (sieve_transport f s)).
Proof.
Intros.
Apply top_maximal.
Apply is_maximal_sieve_ii; Simpl.
Unfold target_transport.
Rewrite ii_dx.
Auto.
Qed.
End Topology_Facts.
Hints Resolve top_maximal top_larger top_transport top_comp.
Hints Resolve top_transitivity cov_obj_transport.
Section Cov_Sieve.
Variable J:Topology; u:A; s:(Sieve u).
Local cov_sieve_data [x:A; f:(mor x u)] : Prop :=
(prop_of_type (cov_obj J (sieve_transport f s))).
Remark cov_sieve_theory : (Sieve_Theory cov_sieve_data).
Proof.
Unfold cov_sieve_data Sieve_Theory; Intros.
Rewrite sieve_transport_trans.
NewDestruct H.
Auto.
Qed.
Definition Cov : (Sieve u).
Proof.
Split with cov_sieve_data.
Exact cov_sieve_theory.
Defined.
Lemma cov_sieve_geq : (target_sub s Cov).
Proof.
Unfold target_sub; Simpl.
Unfold cov_sieve_data; Auto.
Qed.
Hints Resolve cov_sieve_geq.
Definition cov [x:A; f:(mor x u)] : Prop := (sieve Cov f).
End Cov_Sieve.
Lemma top_trans_arrow : (J:Topology; u:A; s,t:(Sieve u); f:s)
((g:s)(cov J t g)) -> (cov J t f).
Proof.
Unfold cov; Auto.
Qed.
Hints Resolve top_trans_arrow.
Lemma top_coerence : (J:Topology; u:A; s:(Sieve u); x:A; f:s)
(cov J s f).
Proof.
Intros; NewDestruct f; Unfold cov; Simpl; Auto.
Qed.
Hints Resolve top_coerence.
End Topology.
Hints Resolve top_maximal top_transport top_comp top_transitivity.
Hints Resolve sieve_prop.
Sites |
| A site is a category with a Grothendieck topology. |
Record Site : Type := {
site_cat :> Cat;
site_top : (Topology site_cat)
}.
End Topology_.