QuotTop.v

(* Compatible with Coq >= 8.17.0 *)

Reserved Infix "∈" (no associativity, at level 70).
Reserved Infix "⊆" (no associativity, at level 70).
Reserved Infix "==" (no associativity, at level 70).

#[universes(polymorphic=yes)]
Definition ensemble@{u} (A : Type@{u}) : Type@{u} :=
  A -> Prop.

#[universes(polymorphic=yes)]
Definition In@{u} {A : Type@{u}} x (X : ensemble@{u} A) : Prop :=
  X x.

Infix "∈" := In : type_scope.

#[universes(polymorphic=yes)]
Definition subseteq@{u} {A : Type@{u}} X1 X2 : Prop :=
  forall x : A, @In@{u} A x X1 -> @In@{u} A x X2.

Infix "⊆" := subseteq : type_scope.

#[universes(polymorphic=yes)]
Definition ext_eq@{u} {A : Type@{u}} X1 X2 : Prop :=
  forall x : A, @In@{u} A x X1 <-> @In@{u} A x X2.

Infix "==" := ext_eq : type_scope.

Inductive full {A : Type} (x : A) : Prop :=
  | In_full
    : x ∈ full.

Inductive intersection {A : Type} X1 X2 (x : A) : Prop :=
  | In_intersection
    (IN1 : x ∈ X1)
    (IN2 : x ∈ X2)
    : x ∈ intersection X1 X2.

Inductive empty {A : Type} (x : A) : Prop :=.

Inductive unions {A : Type} Xs (x : A) : Prop :=
  | In_unions X
    (IN : x ∈ X)
    (X_IN : X ∈ Xs)
    : x ∈ unions Xs.

Class AxiomsForOpenSets (X : Type) (T : ensemble (ensemble X)) : Prop :=
  { full_Open
    : full ∈ T
  ; unions_Open Os
    (OPENs : Os ⊆ T)
    : unions Os ∈ T
  ; intersection_Open O1 O2
    (OPEN1 : O1 ∈ T)
    (OPEN2 : O2 ∈ T)
    : intersection O1 O2 ∈ T
  }.

Class topology (X : Type) : Type :=
  { OpenSets : ensemble (ensemble X)
  ; satisfiesAxiomsForOpenSets :: AxiomsForOpenSets X OpenSets
  ; OpenSets_ext_eq O1 O2
    (OPEN : O1 ∈ OpenSets)
    (EXT_EQ : O1 == O2)
    : O2 ∈ OpenSets 
  }.

Lemma empty_Open {X : Type} {TOPOLOGY : topology X}
  : empty ∈ OpenSets.
Proof.
  eapply OpenSets_ext_eq with (O1 := unions empty).
  - eapply unions_Open. firstorder.
  - firstorder.
Qed.

Require Import Coq.Classes.RelationClasses.
Require Import Coq.Setoids.Setoid.

Inductive preimage {A : Type} {B : Type} (f : A -> B) Y (x : A) : Prop :=
  | In_preimage
    (IN : f x ∈ Y)
    : x ∈ preimage f Y.

Class isSetoid (A : Type) : Type :=
  { eqProp (lhs : A) (rhs : A) : Prop
  ; eqProp_Equivalence :: Equivalence eqProp
  }.

Infix "≡" := eqProp (no associativity, at level 70) : type_scope.

#[global, program]
Instance ensemble_isSetoid {A : Type} : isSetoid (ensemble A) :=
  { eqProp := ext_eq }.
Next Obligation.
  split; firstorder.
Qed.

Section QuotientTopology.

Context {X : Type} {SETOID : isSetoid X}.

(* The equivalence class of an element x *)
Definition cls (x : X) : ensemble X :=
  fun z => z ≡ x.

(* The quotient set of X by ≡ *)
Definition Q : Type :=
  { U : ensemble X | exists x, cls x ≡ U }.

(* The canonical surjection *)
Definition q : X -> Q :=
  fun x => @exist (ensemble X) (fun U => exists x, cls x ≡ U) (cls x) (@ex_intro X (fun y => cls y ≡ cls x) x (Equivalence_Reflexive (cls x))).

Context {TOPOLOGY : topology X}.

(* The set of open sets in Q *)
Definition OpenSets_in_Q : ensemble (ensemble Q) :=
  fun U => preimage q U ∈ OpenSets.

#[global]
Instance OpenSets_in_Q_satisfiesAxiomsForOpenSets
  : AxiomsForOpenSets Q OpenSets_in_Q.
Proof with reflexivity || eauto.
  unfold OpenSets_in_Q. destruct TOPOLOGY.(satisfiesAxiomsForOpenSets) as [H1 H2 H3]. split.
  - red. eapply OpenSets_ext_eq with (O1 := full)... intros x. split; intros IN... econstructor...
  - intros. red. do 2 red in OPENs. eapply OpenSets_ext_eq with (O1 := unions (fun U => exists O, O ∈ Os /\ U ∈ OpenSets /\ preimage q O ≡ U)).
    + eapply H2. intros U H_U. red in H_U. destruct H_U as (O & O_in & U_in & EQ). eapply OpenSets_ext_eq with (O1 := preimage q O)...
    + intros x. split; intros H_IN.
      * destruct H_IN as [U H_IN U_IN]. red in U_IN. destruct U_IN as (O & O_IN & U_IN & H_EQ).
        do 3 red in H_EQ. rewrite <- H_EQ in H_IN. split... econstructor... inversion H_IN...
      * inversion H_IN. destruct IN as [O IN O_IN]. exists (preimage q O).
        { econstructor... }
        { exists O. split... split... }
  - intros. red in OPEN1, OPEN2 |- *. eapply OpenSets_ext_eq with (O1 := intersection (preimage q O1) (preimage q O2)).
    + eapply intersection_Open...
    + intros x; split; intros H_IN.
      * destruct H_IN as [[H_IN1] [H_IN2]]. split... econstructor...
      * inversion H_IN. destruct IN as [IN1 IN2]. split... econstructor... econstructor...
Qed.

#[global, program]
Instance QuotientTopology : topology Q :=
  { OpenSets := OpenSets_in_Q
  ; satisfiesAxiomsForOpenSets := OpenSets_in_Q_satisfiesAxiomsForOpenSets
  }.
Next Obligation.
  do 2 red in OPEN |- *. eapply OpenSets_ext_eq with (O1 := preimage q O1); firstorder.
Qed.

End QuotientTopology.